A Polynomial Translation of Mobile Ambients into Safe Petri Nets: Understanding a Calculus of Hierarchical Protection Domains

پایان نامه کارشناسی ارشد سوزان گوبل درک عمیقی از محاسبات محیط موبایل (MA) ایجاد می کند که برای استفاده از آن به عنوان یک زبان مدل سازی ضروری است. به جای اصطلاحات حساب دیفرانسیل و انتگرال، یک نمایش بسیار راحت‌تر از طریق درختان MA به طور طبیعی به منطقه کاربردی شبکه‌ها که در آن فرآیندها از حوزه‌های حفاظت سلسله مراتبی مانند فایروال‌ها عبور می‌کنند، نگاشت می‌شود. این کار اصول عملکرد MA را تحلیل می‌کند و ترجمه‌ای را به شبکه‌های پتری ایمن استخراج می‌کند. این به فرآیندهای MA دلخواه گسترش می‌یابد، اما محدود بودن شبکه و بنابراین تصمیم‌پذیری قابلیت دسترسی فقط برای فرآیندهای محدود تضمین شده است. ساختار در اندازه و کران فرآیند چند جمله ای است به طوری که تجزیه و تحلیل دسترس پذیری فقط PSPACE کامل است.

The master thesis of Susanne Göbel generates the deep understanding of the Mobile Ambient (MA) calculus that is necessary to use it as a modeling language. Instead of calculus terms a much more convenient representation via MA trees naturally maps to the application area of networks where processes pass hierarchical protection domains like firewalls. The work analyses MA’s function principles and derives a translation into Safe Petri nets. It extends to arbitrary MA processes but finiteness of the net and therefore decidability of reachability is only guaranteed for bounded processes. The construction is polynomial in process size and bounds so that reachability analysis is only PSPACE-complete.