We propose a new logic for expressing properties of concurrent and distributed systems, Dynamic Epistemic Spatial Logic, as an extension of Hennessy-Milner logic with spatial and epistemic operators. Aiming to provide a completely axiomatized and decidable logic for concurrency, we devise epistemic operators, indexed by processes, to replace the guarantee operator in the classical spatial logics. The knowledge of a process, considered as epistemic agent, is understood as the information, locally available to our process, about the overallglobal system/process in which it is an agent/subprocess. Dynamic Epistemic Spatial Logic supports a semantics based on a fragment of CCS against which the classical spatial logics have been proved to be undecidable. Underpinning on a new congruence relation on processes - the structural bisimulation - we prove the finite model property for our logic, thus concluding on its decidability against the same semantics. A sound complete Hilbert-style axiomatic system is developed, comprehending the behavior of spatial operators in relation with dynamic/temporal and epistemic ones. Eventually we emphasize on the similarities with the classical axioms and rules of knowledge, that present our logic as an authentic dynamic-epistemic logic.

Dynamic-Epistemic Spatial Logic / Mardare, Radu; Priami, Corrado. - ELETTRONICO. - (2006), pp. 1-59.

Dynamic-Epistemic Spatial Logic

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

Abstract

We propose a new logic for expressing properties of concurrent and distributed systems, Dynamic Epistemic Spatial Logic, as an extension of Hennessy-Milner logic with spatial and epistemic operators. Aiming to provide a completely axiomatized and decidable logic for concurrency, we devise epistemic operators, indexed by processes, to replace the guarantee operator in the classical spatial logics. The knowledge of a process, considered as epistemic agent, is understood as the information, locally available to our process, about the overallglobal system/process in which it is an agent/subprocess. Dynamic Epistemic Spatial Logic supports a semantics based on a fragment of CCS against which the classical spatial logics have been proved to be undecidable. Underpinning on a new congruence relation on processes - the structural bisimulation - we prove the finite model property for our logic, thus concluding on its decidability against the same semantics. A sound complete Hilbert-style axiomatic system is developed, comprehending the behavior of spatial operators in relation with dynamic/temporal and epistemic ones. Eventually we emphasize on the similarities with the classical axioms and rules of knowledge, that present our logic as an authentic dynamic-epistemic logic.
2006
Trento
Università degli Studi di Trento - Dipartimento di Informatica e Telecomunicazioni
Dynamic-Epistemic Spatial Logic / Mardare, Radu; Priami, Corrado. - ELETTRONICO. - (2006), pp. 1-59.
Mardare, Radu; Priami, Corrado
File in questo prodotto:
File Dimensione Formato  
DIT-06-010.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 490.66 kB
Formato Adobe PDF
490.66 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/358131
 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
  • OpenAlex ND
social impact