de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

The Complexity of Model Checking Mobile Ambients

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44232

Charatonik,  Witold
Programming Logics, MPI for Informatics, Max Planck Society;

Dal Zilio,  Silvano
Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45084

Mukhopadhyay,  Supratik
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45585

Talbot,  Jean-Marc
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Charatonik, W., Dal Zilio, S., Gordon, A. D., Mukhopadhyay, S., & Talbot, J.-M. (2001). The Complexity of Model Checking Mobile Ambients. In F. Honsell, & M. Miculan (Eds.), Foundations of Software Science and Computation Structures. Proceedings of the 4th International Conference (FOSSACS-01). Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS-01) (pp. 152-167). Berlin, Germany: Springer.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-324C-B
Zusammenfassung
We settle the complexity bounds of the model checking problem for the replication-free ambient calculus with public names against the ambient logic without parallel adjunct. We show that the problem is PSPACE-complete. For the complexity upper-bound, we devise a new representation of processes that remains of polynomial size during process execution; this allows us to keep the model checking procedure in polynomial space. Moreover, we prove PSPACE-hardness of the problem for several quite simple fragments of the calculus and the logic; this suggests that there are no interesting fragments with polynomial-time model checking algorithms.