Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Decidable extensions of Hennessy-Milner logic
Radu Mardare, Corrado Priami
abstract:
We propose a new class of logics for specifying and model-checking properties of distributed systems - Dynamic Epistemic Spatial Logics. They have been designed as extensions of Hennessy-Milner logic with spatial operators (inspired by Cardelli-Caires spatial logic) and epistemic operators (inspired by dynamic-epistemic logics). Our logics focus on observers, agents placed in different locations of the system having access to some subsystems. Treating them as epistemic agents, we develop completely axiomatized and decidable logics that express the information flow between them in a dynamic and distributed environment. The knowledge of an epistemic agent, is understood as the information, locally available to our observer, about the overall-global system. By combining the knowledge of different observers we can specify properties of the whole system. Dynamic Epistemic Spatial Logics are decidable against a semantics based on a fragment of CCS for which the classical spatial logics have been proved to be undecidable. Eventually model-checking and satisfiability/validity-checking algorithms are presented.
