Many-sorted coalgebraic modal logic : a model-theoretic study

Bart Jacobs

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2001)

  • Volume: 35, Issue: 1, page 31-59
  • ISSN: 0988-3754

Abstract

top
This paper gives a semantical underpinning for a many-sorted modal logic associated with certain dynamical systems, like transition systems, automata or classes in object-oriented languages. These systems will be described as coalgebras of so-called polynomial functors, built up from constants and identities, using products, coproducts and powersets. The semantical account involves Boolean algebras with operators indexed by polynomial functors, called MBAOs, for Many-sorted Boolean Algebras with Operators, combining standard (categorical) models of modal logic and of many-sorted predicate logic. In this setting we will see Lindenbaum MBAO models as initial objects, and canonical coalgebraic models of maximally consistent sets of formulas as final objects. They will be used to (re)prove completeness results, and Hennessey–Milner style characterisation results for the modal logic, first established by Rößiger.

How to cite

top

Jacobs, Bart. "Many-sorted coalgebraic modal logic : a model-theoretic study." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 35.1 (2001): 31-59. <http://eudml.org/doc/92654>.

@article{Jacobs2001,
abstract = {This paper gives a semantical underpinning for a many-sorted modal logic associated with certain dynamical systems, like transition systems, automata or classes in object-oriented languages. These systems will be described as coalgebras of so-called polynomial functors, built up from constants and identities, using products, coproducts and powersets. The semantical account involves Boolean algebras with operators indexed by polynomial functors, called MBAOs, for Many-sorted Boolean Algebras with Operators, combining standard (categorical) models of modal logic and of many-sorted predicate logic. In this setting we will see Lindenbaum MBAO models as initial objects, and canonical coalgebraic models of maximally consistent sets of formulas as final objects. They will be used to (re)prove completeness results, and Hennessey–Milner style characterisation results for the modal logic, first established by Rößiger.},
author = {Jacobs, Bart},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {modal logic; coalgebra; boolean algebra with operators; coalgebras; many-sorted logic; many-sorted Boolean algebras with operators},
language = {eng},
number = {1},
pages = {31-59},
publisher = {EDP-Sciences},
title = {Many-sorted coalgebraic modal logic : a model-theoretic study},
url = {http://eudml.org/doc/92654},
volume = {35},
year = {2001},
}

TY - JOUR
AU - Jacobs, Bart
TI - Many-sorted coalgebraic modal logic : a model-theoretic study
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2001
PB - EDP-Sciences
VL - 35
IS - 1
SP - 31
EP - 59
AB - This paper gives a semantical underpinning for a many-sorted modal logic associated with certain dynamical systems, like transition systems, automata or classes in object-oriented languages. These systems will be described as coalgebras of so-called polynomial functors, built up from constants and identities, using products, coproducts and powersets. The semantical account involves Boolean algebras with operators indexed by polynomial functors, called MBAOs, for Many-sorted Boolean Algebras with Operators, combining standard (categorical) models of modal logic and of many-sorted predicate logic. In this setting we will see Lindenbaum MBAO models as initial objects, and canonical coalgebraic models of maximally consistent sets of formulas as final objects. They will be used to (re)prove completeness results, and Hennessey–Milner style characterisation results for the modal logic, first established by Rößiger.
LA - eng
KW - modal logic; coalgebra; boolean algebra with operators; coalgebras; many-sorted logic; many-sorted Boolean algebras with operators
UR - http://eudml.org/doc/92654
ER -

References

top
  1. [1] A. Baltag, A logic for coalgebraic simulation, edited by H. Reichel, Coalgebraic Methods in Computer Science. Elsevier, Amsterdam, Electon. Notes Theor. Comput. Sci. 33 (2000). Zbl0959.03501MR1787573
  2. [2] B.A. Davey and H.A. Priestley, Introduction to Lattices and Order, Math. Textbooks. Cambridge Univ. Press (1990). Zbl0701.06001MR1058437
  3. [3] R. Goldblatt, Mathematics of Modality. Stanford, CSLI Lecture Notes 43 (1993). Zbl0942.03516MR1317099
  4. [4] R. Goldblatt, Duality for some categories of coalgebras. Algebra Universalis (to appear). Zbl1061.18004MR1857205
  5. [5] R. Goldblatt, What is the coalgebraic analogue of Birkhoff’s variety theorem? Theoret. Comput. Sci. (to appear). Zbl0989.68099
  6. [6] M. Hennessy and R. Milner, On observing non-determinism and concurrency, edited by J.W. de Bakker and J. van Leeuwen, Mathematical Foundations of Computer Science. Springer, Berlin, Lecture Notes in Comput. Sci. 85 (1980) 299-309. Zbl0441.68018MR589012
  7. [7] U. Hensel, M. Huisman, B. Jacobs, and H. Tews, Reasoning about classes in object-oriented languages: Logical models and tools, edited by Ch. Hankin, European Symposium on Programming. Springer, Berlin, Lecture Notes in Comput. Sci. 1381 (1998) 105-121. 
  8. [8] C. Hermida and B. Jacobs, Structural induction and coinduction in a fibrational setting. Inform. and Comput. 145 (1998) 107-152. Zbl0941.18006MR1641597
  9. [9] B. Jacobs, Objects and classes, co-algebraically, edited by B. Freitag, C.B. Jones, C. Lengauer and H.-J. Schek, Object-Orientation with Parallelism and Persistence. Kluwer Acad. Publ. (1996) 83-103. 
  10. [10] B. Jacobs, Categorical Logic and Type Theory. North Holland, Amsterdam (1999). Zbl0911.03001MR1674451
  11. [11] B. Jacobs, The temporal logic of coalgebras via Galois algebras, Technical Report CSI-R9906. Comput. Sci. Inst. Univ. of Nijmegen, Math. Structures Comput. Sci. (to appear). Zbl1030.03017MR1947808
  12. [12] B. Jacobs, Towards a duality result in coalgebraic modal logic, edited by H. Reichel, Coalgebraic Methods in Computer Science. Elsevier, Amsterdam, Electon. Notes Theor. Comput. Sci. 33 (2000). Zbl0959.03503MR1787578
  13. [13] B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. EATCS Bull. 62 (1997) 222-259. Zbl0880.68070
  14. [14] B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel and H. Tews, Reasoning about classes in Java (preliminary report), in Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press (1998) 329-340. 
  15. [15] P.T. Johnstone, Stone Spaces. Cambridge Univ. Press, Cambridge Stud. Adv. Math. 3 (1982). Zbl0499.54001MR698074
  16. [16] B. Jónsson and A. Tarski, Boolean algebras with operators I. Amer. J. Math. 73 (1951) 891-939. Zbl0045.31505MR44502
  17. [17] A. Kurz, Specifying coalgebras with modal logic. Theoret. Comput. Sci. (to appear). Zbl0974.68034MR1827935
  18. [18] F.W. Lawvere, Functorial semantics. Proc. Nat. Acad. Sci. U.S.A. 50 (1963) 869-872. Zbl0119.25901MR158921
  19. [19] E.J. Lemmon, Algebraic semantics for modal logics II. J. Symbolic Logic 31 (1966) 191-218. Zbl0147.24805MR205835
  20. [20] L.S. Moss, Coalgebraic logic. Ann. Pure Appl. Logic 96 (1999) 277-317; Erratum in Ann. Pure Appl. Logic 99 (1999) 241-259. Zbl0969.03026MR1673305
  21. [21] H. Reichel, An approach to object semantics based on terminal co-algebras. Math. Structures Comput. Sci. 5 (1995) 129-152. Zbl0854.18006MR1368919
  22. [22] M. Rößiger, Languages for coalgebras on datafunctors, edited by B. Jacobs and J. Rutten, Coalgebraic Methods in Computer Science. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 19 (1999). Zbl0918.68028MR1689449
  23. [23] M. Rößiger, Coalgebras and modal logic, edited by H. Reichel, Coalgebraic Methods in Computer Science. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 33 (2000). Zbl0959.03502MR1787583
  24. [24] M. Rößiger, From modal logic to terminal coalgebras. Theoret. Comput. Sci. (to appear). Zbl0973.68177MR1827938
  25. [25] J. Rothe, H. Tews and B. Jacobs, The coalgebraic class specification language CCSL. J. Universal Comput. Sci. 7 (2001). Zbl0970.68104MR1829826
  26. [26] J. Rutten, Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249 (2000) 3-80. Zbl0951.68038MR1791953
  27. [27] M.H. Stone, The theory of representations for Boolean algebra. Trans. Amer. Math. Soc. 40 (1936) 37-111. Zbl0014.34002MR1501865
  28. [28] M.H. Stone, Applications of the theory of Boolean rings to general topology. Trans. Amer. Math. Soc. 41 (1937) 375-481. Zbl0017.13502MR1501905JFM63.1173.01
  29. [29] D. Turi and J. Rutten, On the foundations of final semantics: non-standard sets, metric spaces and partial orders. Math. Structures Comput. Sci. 8 (1998) 481-540. Zbl0917.68140MR1652714
  30. [30] Y. Venema, Points, lines and diamonds: a two-sorted modal logic for projective planes. J. Logic Comput. 9 (1999) 601-621. Zbl0941.03020MR1727211
  31. [31] S. Vickers, Topology Via Logic. Cambridge Univ. Press, Tracts Theor. Comput. Sci. 5 (1989). Zbl0668.54001MR1002193

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.