Abstract
In computer science, scenarios with interacting agents are often developed using modal logic. We show how to interpret modal logic of knowledge in relation algebra. This allows the use of the RelView tool for the purpose of investigating finite models and for visualizing certain properties. Our approach is illustrated with the well-known ‘muddy children’ puzzle using modal logic of knowledge. We also sketch how to treat other non-classical logics in this way. In particular, we explore our approach for computational tree logic and illustrate it with the ‘mutual exclusion’ example.
The authors thank Harrie de Swart and the anonymous referees for their comments. The work was supported by EU COST Action 274 (Tarski).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berghammer, R., Behnke, R., Meyer, E., Schneider, P.: RELVIEW - A system for calculating with relations and relational programming. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 318–321. Springer, Heidelberg (1998)
Berghammer, R., Kempf, P., Schmidt, G., Ströhlein, T.: Relational algebra and logic of programs. In: Andréka, H., Monk, J.D., Németi, I. (eds.) Algebraic Logic. Colloq. Math. Soc. J. Bolyai, vol. 54, pp. 37–58. North-Holland, Amsterdam (1991)
Berghammer, R., Leoniuk, B., Milanese, U.: Implementation of relational algebra using binary decision diagrams. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol. 2561, pp. 241–257. Springer, Heidelberg (2002)
Berghammer, R., Neumann, F.: RelView – An OBDD-based Computer Algebra system for relations. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2005. LNCS, vol. 3718, pp. 40–51. Springer, Heidelberg (2005)
Blackburn, P., de Rijke, M., Venema, V.: Modal Logic. Cambridge Univ. Press, Cambridge (2001)
Brink, C., Britz, K., Schmidt, R.A.: Peirce algebras. Formal Aspects of Computing 6(3), 339–358 (1994)
Chellas, B.F.: Modal Logic: An Introduction. Cambridge Univ. Press, Cambridge (1980)
Clarke, E., Grumberg, O., Peled, D.: Modal Checking. MIT Press, Cambridge (2000)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about knowledge. MIT Press, Cambridge (1995)
Goldblatt, R.: Logics of Time and Computation. In: CSLI Lecture Notes, vol. 7, Chicago Univ. Press, Chicago (1987)
Hughes, G.E., Cresswell, M.J.: A New Introduction to Modal Logic. Routledge, London (1996)
Huth, M., Ryan, M.: Logic in Computer Science. In: Modelling and Reasoning About Systems. Cambridge Univ. Press, Cambridge (2000)
Jónsson, B., Tarski, A.: Boolean algebras with operators, Part I. American Journal of Mathematics 73, 891–939 (1951)
Nabialek, W., Niewiadomski, A., Penczek, W., Polrola, A., Szreter, M.: Verics 2004: A model checker for real time and multi-agent systems. In: Proc. International Workshop on Concurrency, Specification, and Programming. Informatik-Berichte, vol. 170, pp. 88–99. Humbold University, Berlin (2004)
Kacprzak, M., Lomusico, A., Niewiadomski, A., Szreter, M., Penczek, W., Raimondi, F.: Comparing BDD and SAT based techniques for model checking Chaum’s Dining Cryptographers protocol. Fundamenta Informaticae (to appear, 2006)
Kozen, D.: A representation theorem for models of *-free PDL. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 351–362. Springer, Heidelberg (1980)
Leoniuk, B.: ROBDD-based implementation of relational algebra with applications (in German). Ph.D. thesis, Institut für Informatik und Praktische Mathematik, Universität Kiel (2001)
Lomuscio, A., Raimondi, F.: Mcmas: a tool for verifying multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)
Meyer, J.-J.C., van der Hoek, W.: Epistemic Logic for AI and Computer Science. Cambridge Univ. Press, Cambridge (1995)
Milanese, U.: On the implementation of a ROBDD-based tool for the manipulation and visualization of relations (in German). Ph.D. thesis, Institut für Informatik und Praktische Mathematik, Universität Kiel (2003)
Müller-Olm, M., Schmidt, D., Steffen, B.: Model-checking: A tutorial introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330–354. Springer, Heidelberg (1999)
Ng, K.C., Tarski, A.: Relation algebras with transitive closure, abstract 742-02-09. Notices Amer. Math. Soc., A29–A30 (1977)
Orlowska, E.: Relational formalisation of nonclassical logics. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science. Advances in Computing, pp. 90–105. Springer, Wien (1997)
Pratt, V.R.: Dynamic algebras: Examples, constructions, applications. Technical Report MIT/LCS/TM-138, MIT Laboratory for Computer Science (1979)
Schmidt, G., Ströhlein, T.: Relations and Graphs. Discrete Mathematics for Computer Scientists. Springer, Berlin (1993)
Tarski, A.: On the calculus of relations. J. Symbolic Logic 6(3), 73–89 (1941)
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285–309 (1955)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berghammer, R., Schmidt, R.A. (2006). Investigating Finite Models of Non-classical Logics with Relation Algebra and RelView . In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds) Theory and Applications of Relational Structures as Knowledge Instruments II. Lecture Notes in Computer Science(), vol 4342. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11964810_2
Download citation
DOI: https://doi.org/10.1007/11964810_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69223-2
Online ISBN: 978-3-540-69224-9
eBook Packages: Computer ScienceComputer Science (R0)