English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Model checking mobile ambients

Charatonik, W., Dal Zilio, S., Gordon, A. D., Mukhopadhyay, S., & Talbot, J.-M. (2003). Model checking mobile ambients. Theoretical Computer Science, 308, 277-331.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2D77-D Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2D78-B
Genre: Journal Article

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Charatonik, Witold1, Author           
Dal Zilio, Silvano, Author
Gordon, Andrew Donald, Author
Mukhopadhyay, Supratik1, Author           
Talbot, Jean-Marc1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: We settle the complexity bounds of the model checking problem for the ambient calculus with public names against the ambient logic. We show that if either the calculus contains replication or the logic contains the guarantee operator, the problem is undecidable. In the case of the replication-free calculus and guarantee-free logic we prove 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.

Details

show
hide
Language(s): eng - English
 Dates: 2004-06-172003
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: Peer
 Identifiers: eDoc: 202031
Other: Local-ID: C1256104005ECAFC-30C5005D9C1C805CC1256D200054C703-CharatonikDGMT2003
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Theoretical Computer Science
Source Genre: Journal
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 308 Sequence Number: - Start / End Page: 277 - 331 Identifier: ISSN: 0304-3975