Dynamic Epistemic Spatial Logic

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 overall-global 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. This is the preliminary version of a paper that was published in Proceedings of International Conference on Formal Methods for Networked and Distributed Systems (FORTE 2006), LNCS 4229, Springer, 2006. The original publication is available at www.springerlink.com