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-Gordon-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.
Work partially supported by EU-IST project 016004 SENSORIA.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bergstra, J.A.: Handbook of Process Algebra. Elsevier Science Inc., New York (2001)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. JACM 32(1), 137–161 (1985)
Stirling, C.: Modal and temporal properties of processes. Springer, New York (2001)
Milner, R., Parrow, J., Walker, D.: Modal logics for mobile processes. Theoretical Computer Science 114, 149–171 (1993)
Dam, M.: Proof systems for π-calculus. In: de Queiroz, (ed.) Logic for Concurrency and Synchronisation, Studies in Logic and Computation. Oxford University Press, Oxford (to appear)
Dam, M.: Model checking mobile processes. Information and Computation 129(1), 35–51 (1996)
Caires, L., Cardelli, L.: A spatial logic for concurrency (part i). Information and Computation 186/2, 194–235 (2003)
Cardelli, L., Gordon, A.D.: Ambient logic. Mathematical Structures in Computer Science (to appear, 2003)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients, 365–377 (2000)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 140. Springer, Heidelberg (1998)
Caires, L., Lozes, É.: Elimination of quantifiers and undecidability in spatial logics for concurrency. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 240–257. Springer, Heidelberg (2004)
Charatonik, W., Talbot, J.-M.: The decidability of model checking mobile ambients. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 339–354. Springer, Heidelberg (2001)
Charatonik, W., Gordon, A.D., Talbot, J.-M.: Finite-control mobile ambients. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 295–313. Springer, Heidelberg (2002)
Milner, R.: A Calculus of Communicating Systems. Springer, New York (1982)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Baltag, A., Moss, L.S.: Logics for epistemic programs. In: Symons, J., Hintikka, J. (eds.) Synthese: Knowledge, Rationality and Action, vol. 139 (2), pp. 165–224. Springer, Heidelberg (2004)
Gerbrandy, J., Groeneveld, W.: Reasoning about information change. Journal of Logic, Language and Information 6, 146–169 (1997)
van Benthem, J.F.A.K.: Games in dynamic epistemic logic. Bulletin of Economic Research 53(4), 219–248 (2001)
Syverson, P.F., Cervesato, I.: The logic of authentication protocols. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, p. 63. Springer, Heidelberg (2001)
Mardare, R., Priami, C.: Dynamic epistemic spatial logics. Technical Report, 03/2006, Microsoft Research Center for Computational and Systems Biology, Trento, Italy (2006)
Mardare, R., Priami, C.: A decidable extension of hennessy-milner logic with spatial operators. Technical Report DIT-06-009, Informatica e Telecomunicationi, University of Trento (2006)
Mardare, R.: Logical analysis of complex systems: Dynamic epistemic spatial logics. PhD. thesis, DIT, University of Trento, Italy (March 2006), http://www.dit.unitn.it/~mardare/publications.htm
Calcagno, C., Cardelli, L., Gordon, A.D.: Deciding validity in a spatial logic for trees, 62–73 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Mardare, R., Priami, C. (2006). Decidable Extensions of Hennessy-Milner Logic. In: Najm, E., Pradat-Peyre, JF., Donzeau-Gouge, V.V. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2006. FORTE 2006. Lecture Notes in Computer Science, vol 4229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11888116_16
Download citation
DOI: https://doi.org/10.1007/11888116_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46219-4
Online ISBN: 978-3-540-46220-0
eBook Packages: Computer ScienceComputer Science (R0)