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.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