We advocate the use of a CTL* logic, built upon the Ambient Calculus in dealing with mobile computing phenomena. Our logic is a more expressive alternative to Ambient Logic, based on a single modality, but still powerful enough to handle mobility and dynamic hierarchies of locations. In applications, the possibility of expressing path properties of computation together with state properties opens new perspectives. Moreover, having a temporal logic to express properties of computation, we can reuse the algorithms for model checking temporal logics in analyzing the phenomena described using Ambient Calculus. We resort to syntax trees of Ambient Calculus and enrich them with labelling functions that generates the state processes. These constitute a sound model for Ambient Calculus and are used as possible worlds in a Kripke structure developed for a propositional branching temporal logic. The accessibility relation is generated by the reduction of Ambient Calculus considered as reduction between syntax trees. We provide the algorithms able to compute, giving the initial state of a system, any possible next state. These algorithms could be used together with the algorithms for model checking temporal logic in order to develop model checking analysis for Ambient Calculus.

A Propositional Branching Temporal Logic for the Ambient Calculus / Priami, Corrado; Mardare, Radu. - ELETTRONICO. - (2003).

A Propositional Branching Temporal Logic for the Ambient Calculus

Priami, Corrado;Mardare, Radu
2003-01-01

Abstract

We advocate the use of a CTL* logic, built upon the Ambient Calculus in dealing with mobile computing phenomena. Our logic is a more expressive alternative to Ambient Logic, based on a single modality, but still powerful enough to handle mobility and dynamic hierarchies of locations. In applications, the possibility of expressing path properties of computation together with state properties opens new perspectives. Moreover, having a temporal logic to express properties of computation, we can reuse the algorithms for model checking temporal logics in analyzing the phenomena described using Ambient Calculus. We resort to syntax trees of Ambient Calculus and enrich them with labelling functions that generates the state processes. These constitute a sound model for Ambient Calculus and are used as possible worlds in a Kripke structure developed for a propositional branching temporal logic. The accessibility relation is generated by the reduction of Ambient Calculus considered as reduction between syntax trees. We provide the algorithms able to compute, giving the initial state of a system, any possible next state. These algorithms could be used together with the algorithms for model checking temporal logic in order to develop model checking analysis for Ambient Calculus.
2003
Trento, Italia
Università degli Studi di Trento. DEPARTMENT OF INFORMATION AND COMMUNICATION TECHNOLOGY
A Propositional Branching Temporal Logic for the Ambient Calculus / Priami, Corrado; Mardare, Radu. - ELETTRONICO. - (2003).
Priami, Corrado; Mardare, Radu
File in questo prodotto:
File Dimensione Formato  
053.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 589.04 kB
Formato Adobe PDF
589.04 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/358889
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact