Abstract
We present a modular approach to defining logics for a wide variety of state-based systems. We use coalgebras to model the behaviour of systems, and modal logics to specify behavioural properties of systems. We show that the syntax, semantics and proof systems associated to such logics can all be derived in a modular way. Moreover, we show that the logics thus obtained inherit soundness, completeness and expressiveness properties from their building blocks. We apply these techniques to derive sound, complete and expressive logics for a wide variety of probabilistic systems.
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
Aczel, P., Mendler, N.: A final coalgebra theorem. In: Dybjer, P., Pitts, A.M., Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 389. Springer, Heidelberg (1989)
Bartels, F.: On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam (2004)
Bartels, F., Sokolova, A., de Vink, E.: A hierarchy of probabilistic system types. In: Gumm, H.P. (ed.) Proc. CMCS 2003. ENTCS, vol. 82. Elsevier, Amsterdam (2003)
Bidoit, M., Cengarle, M.V., Hennicker, R.: Proof systems for structured specifications and their refinements. In: Kreowski, H.J., Astesiano, E., Krieg-Brückner, B. (eds.) Algebraic Foundations of Systems Specification, IFIP State-of-the-Art Reports, pp. 385–434. Springer, Heidelberg (1999)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2000)
Borzyszkowski, T.: Logical systems for structured specifications. Theoret. Comput. Sci. 286(2), 197–245 (2002)
Caleiro, C.: Combining Logics. PhD thesis (2002)
Cîrstea, C.: On expressivity and compositionality in logics for coalgebras. In: Gumm, H.P. (ed.) Proc. CMCS 2003. ENTCS, vol. 82. Elsevier, Amsterdam (2003)
Clarke, E., Emerson, E.: Synthesis of synchronisation skeletons for branching temporal logics. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131. Springer, Heidelberg (1982)
de Vink, E., Rutten, J.: Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoret. Comput. Sci. 221, 271–293 (1999)
Gabbay, D.: Fibring Logics. Oxford University Press, Oxford (1998)
Heifetz, A., Mongin, P.: Probability logic for type spaces. Games and Economic Behaviour 35, 31–53 (2001)
Jacobs, B.: Many-sorted coalgebraic modal logic: a model-theoretic study. Theor. Inform. Appl. 35(1), 31–59 (2001)
Kick, M.: Bialgebraic modelling of timed processes. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, p. 525. Springer, Heidelberg (2002)
Kozen, D.: Results on the propositional mu-calculus. Theoret. Comput. Sci. 27, 333–354 (1983)
Kurz, A.: Specifying Coalgebras with Modal Logic. Theoret. Comput. Sci. 260(1–2), 119–138 (2001)
Kurz, A., Pattinson, D.: Definability, canonical models, and compactness for finitary coalgebraic modal logic. In: Moss, L.S. (ed.) Proc. CMCS 2002. ENTCS, vol. 65. Elsevier, Amsterdam (2002)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inform. and Comput. 94, 1–28 (1991)
Milner, R.: Communication and Concurrency. International series in computer science. Prentice Hall, Englewood Cliffs (1989)
Moss, L.S.: Coalgebraic logic. Ann. Pure Appl. Logic 96, 277–317 (1999)
Naur, P., Randell, B. (eds.): Software Engineering: Report of a conference sponsored by the NATO Science Committee, Garmisch, Germany, 7-11 October 1968. Scientific Affairs Division, NATO (1969)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104. Springer, Heidelberg (1981)
Pattinson, D.: Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoret. Comput. Sci. 309(1–3), 177–193 (2003)
Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic (to appear, 2004)
Rockafellar, R.T.: Convex Analysis. Princeton University Press, Princeton (1970)
Rößiger, M.: From Modal Logic to Terminal Coalgebras. Theoret. Comput. Sci. 260, 209–228 (2001)
Rutten, J.J.M.M.: Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249, 3–80 (2000)
Segala, R.: Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Proc. 12th LICS Conference, pp. 280–291. IEEE Computer Society Press, Los Alamitos (1999)
Wirsing, M.: Algebraic specification. In: van Leuween, J. (ed.) Handbook of Theoretical Computer Science. Elsevier, Amsterdam (1990)
Worrell, J.: On the Final Sequence of an Accessible Set Functor. Theoret. Comput. Sci. (to appear, 2003)
Zanardo, A., Sernadas, A., Sernadas, C.: Fibring: Completeness preservation. J. Symbolic Logic 66(1), 414–439 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cîrstea, C., Pattinson, D. (2004). Modular Construction of Modal Logics. In: Gardner, P., Yoshida, N. (eds) CONCUR 2004 - Concurrency Theory. CONCUR 2004. Lecture Notes in Computer Science, vol 3170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28644-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-28644-8_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22940-7
Online ISBN: 978-3-540-28644-8
eBook Packages: Springer Book Archive