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.
@article{ITA_2001__35_1_31_0,
author = {Jacobs, Bart},
title = {Many-sorted coalgebraic modal logic : a model-theoretic study},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
volume = {35},
year = {2001},
pages = {31-59},
mrnumber = {1845874},
zbl = {0984.03019},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2001__35_1_31_0}
}
Jacobs, Bart. Many-sorted coalgebraic modal logic : a model-theoretic study. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 35 (2001) pp. 31-59. http://gdmltest.u-ga.fr/item/ITA_2001__35_1_31_0/
[1] , A logic for coalgebraic simulation, edited by H. Reichel, Coalgebraic Methods in Computer Science. Elsevier, Amsterdam, Electon. Notes Theor. Comput. Sci. 33 (2000). | MR 1787573 | Zbl 0959.03501
[2] and, Introduction to Lattices and Order, Math. Textbooks. Cambridge Univ. Press (1990). | MR 1058437 | Zbl 0701.06001
[3] , Mathematics of Modality. Stanford, CSLI Lecture Notes 43 (1993). | MR 1317099 | Zbl 0942.03516
[4] , Duality for some categories of coalgebras. Algebra Universalis (to appear). | MR 1857205 | Zbl 1061.18004
[5] , What is the coalgebraic analogue of Birkhoff's variety theorem? Theoret. Comput. Sci. (to appear). | MR 1850291 | Zbl 0989.68099
[6] and, 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. | MR 589012 | Zbl 0441.68018
[7] ,,, and, 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] and, Structural induction and coinduction in a fibrational setting. Inform. and Comput. 145 (1998) 107-152. | MR 1641597 | Zbl 0941.18006
[9] , 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] , Categorical Logic and Type Theory. North Holland, Amsterdam (1999). | MR 1674451 | Zbl 0911.03001
[11] , The temporal logic of coalgebras via Galois algebras, Technical Report CSI-R9906. Comput. Sci. Inst. Univ. of Nijmegen, Math. Structures Comput. Sci. (to appear). | MR 1947808 | Zbl 1030.03017
[12] , 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). | MR 1787578 | Zbl 0959.03503
[13] and, A tutorial on (co)algebras and (co)induction. EATCS Bull. 62 (1997) 222-259. | Zbl 0880.68070
[14] ,,,, and, Reasoning about classes in Java (preliminary report), in Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM Press (1998) 329-340.
[15] , Stone Spaces. Cambridge Univ. Press, Cambridge Stud. Adv. Math. 3 (1982). | MR 698074 | Zbl 0499.54001
[16] and, Boolean algebras with operators I. Amer. J. Math. 73 (1951) 891-939. | MR 44502 | Zbl 0045.31505
[17] , Specifying coalgebras with modal logic. Theoret. Comput. Sci. (to appear). | MR 1827935 | Zbl 0974.68034
[18] , Functorial semantics. Proc. Nat. Acad. Sci. U.S.A. 50 (1963) 869-872. | MR 158921 | Zbl 0119.25901
[19] , Algebraic semantics for modal logics II. J. Symbolic Logic 31 (1966) 191-218. | MR 205835 | Zbl 0147.24805
[20] , Coalgebraic logic. Ann. Pure Appl. Logic 96 (1999) 277-317; Erratum in Ann. Pure Appl. Logic 99 (1999) 241-259. | MR 1673305 | Zbl 0969.03026
[21] , An approach to object semantics based on terminal co-algebras. Math. Structures Comput. Sci. 5 (1995) 129-152. | MR 1368919 | Zbl 0854.18006
[22] , 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). | MR 1689449 | Zbl 0918.68028
[23] , Coalgebras and modal logic, edited by H. Reichel, Coalgebraic Methods in Computer Science. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 33 (2000). | MR 1787583 | Zbl 0959.03502
[24] , From modal logic to terminal coalgebras. Theoret. Comput. Sci. (to appear). | MR 1827938 | Zbl 0973.68177
[25] , and, The coalgebraic class specification language CCSL. J. Universal Comput. Sci. 7 (2001). | MR 1829826 | Zbl 0970.68104
[26] , Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249 (2000) 3-80. | MR 1791953 | Zbl 0951.68038
[27] , The theory of representations for Boolean algebra. Trans. Amer. Math. Soc. 40 (1936) 37-111. | MR 1501865 | Zbl 0014.34002
[28] , Applications of the theory of Boolean rings to general topology. Trans. Amer. Math. Soc. 41 (1937) 375-481. | JFM 63.1173.01 | MR 1501905
[29] and, On the foundations of final semantics: non-standard sets, metric spaces and partial orders. Math. Structures Comput. Sci. 8 (1998) 481-540. | MR 1652714 | Zbl 0917.68140
[30] , Points, lines and diamonds: a two-sorted modal logic for projective planes. J. Logic Comput. 9 (1999) 601-621. | MR 1727211 | Zbl 0941.03020
[31] , Topology Via Logic. Cambridge Univ. Press, Tracts Theor. Comput. Sci. 5 (1989). | MR 1002193 | Zbl 0668.54001