Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Charatonik, Witold
Dal Zilio, Silvano
Gordon, Andrew Donald
Mukhopadhyay, Supratik
Talbot, Jean-Marc		dblp
dblp
dblp
dblp
dblp
Not MPG Author(s):
Dal Zilio, Silvano
Gordon, Andrew Donald
Mukhopadhyay, Supratik
Talbot, Jean-Marc

BibTeX cite key*:

CharatonikDGMT2003

Title

Title*:

Model checking mobile ambients

Journal

Journal Title*:

Theoretical Computer Science
Journal's URL:

http://www.elsevier.nl/locate/tcs

Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Elsevier
Publisher's URL:

http://www.elsevier.nl/

Publisher's
Address:

Amsterdam, The Netherlands
ISSN:

0304-3975

Vol, No, pp, Date

Volume*:

308
Number:

1-3

Publishing Date:

November 2003

Pages*:

277-331
Number of
VG Pages:


Page Start:

277
Page End:

331

Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) 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.


URL for the Abstract:


Categories,
Keywords:

ambient calculus, model checking, ambient logic, mobile computation, verification.

HyperLinks / References / URLs:

http://www.sciencedirect.com/science/article/B6V1G-47C49JM-1/2/518046be248a9992c4f1b9f060357768

Copyright Message:


Personal Comments:


Download
Access Level:

Intranet

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
popular
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:
@ARTICLE{CharatonikDGMT2003,
AUTHOR = {Charatonik, Witold and Dal Zilio, Silvano and Gordon, Andrew Donald and Mukhopadhyay, Supratik and Talbot, Jean-Marc},
 TITLE = {Model checking mobile ambients},
 JOURNAL = {Theoretical Computer Science},
 PUBLISHER = {Elsevier},
 YEAR = {2003},
 NUMBER = {1-3},
 VOLUME = {308},
 PAGES = {277--331},
 ADDRESS = {Amsterdam, The Netherlands},
 MONTH = {November},
 ISBN = {0304-3975},
}

Entry last modified by Uwe Waldmann, 01/28/2008
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Witold Charatonik		Created
05/08/2003 05:25:59 PM
Revisions
8.
7.
6.
5.
4.		Editor(s)
Uwe Waldmann
Christine Kiesel
Uwe Brahm
Uwe Brahm
Uwe Brahm		Edit Dates
04/14/2005 03:55:06 AM
17.06.2004 14:35:13
05/11/2004 06:34:33 PM
05/11/2004 05:46:08 PM
07.07.2003 16:35:51