Model checking mobile ambients

DOI10.1016/S0304-3975(02)00832-0MaRDI QIDQ1884885zbMATH OpenOpenAlexFDO

Authors Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Jean-Marc Talbot, Supratik Mukhopadhyay

Publication date 27 October 2004

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(02)00832-0, https://zenodo.org/record/32927

zbMATH Keywords

Ambient calculusAmbient logicMobile computationModel checkingVerification

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The complexity of model checking mobile ambients
• The decidability of model checking mobile ambients
• A fully abstract model for mobile ambients
• Finite-control mobile ambients
• Model checking mobile processes

Cites work

• A query language based on the ambient logic
• A spatial logic for concurrency. II
• A spatial logic for querying graphs
• Anytime, anywhere: modal logics for mobile ambients
• BI as an assertion language for mutable data structures
• Extensionality and intensionality of the ambient logics
• Finite-control mobile ambients
• scientific article; zbMATH DE number 4055576 (Why is no real title available?)
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 1406807 (Why is no real title available?)
• scientific article; zbMATH DE number 2242579 (Why is no real title available?)
• scientific article; zbMATH DE number 3057871 (Why is no real title available?)
• Local reasoning about programs that alter data structures
• Logical properties of name restriction
• Mobile ambients
• Recursively enumerable sets of positive integers and their decision problems
• Relationships between nondeterministic and deterministic tape complexities
• Semantics for relevant logics
• Separability in the Ambient Logic
• Spatial congruence for ambients is decidable
• The complexity of model checking mobile ambients
• The decidability of model checking mobile ambients
• The Logic of Bunched Implications
• The polynomial-time hierarchy

Cited in

(20)

• Validating firewalls using flow logics
• Checking modal contracts for virtually timed ambients
• Model checking mobile processes
• Model checking mobile ad hoc networks
• Spatial congruence for ambients is decidable
• The complexity of model checking mobile ambients
• Undecidability of model checking in brane logic
• Formal Modeling of Mobile Computing Systems Based on Ambient Abstract State Machines
• On Model Checking Boolean BI
• Deciding safety properties in infinite-state pi-calculus via behavioural types
• Finite-control mobile ambients
• The decidability of model checking mobile ambients
• Deciding reachability in mobile ambients with name restriction
• Programming Languages and Systems
• Foundations of Software Science and Computational Structures
• Computational Methods in Systems Biology
• On higher-order communication in ambient calculi
• Axiomatisation and decidability of multi-dimensional Duration Calculus
• Expressiveness and complexity of graph logic
• Abstract interpretation based verification of temporal properties for BioAmbients

Describes a project that uses

Uses Software

• SLMC

This page was built for publication: Model checking mobile ambients

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1884885)