# Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study

RAIRO - Theoretical Informatics and Applications (2010)

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

## Access Full Article

top## Abstract

top## How to cite

topJacobs, Bart. "Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study." RAIRO - Theoretical Informatics and Applications 35.1 (2010): 31-59. <http://eudml.org/doc/222078>.

@article{Jacobs2010,

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},

keywords = {Modal logic; coalgebra; Boolean algebra with operators.; modal logic; coalgebras; many-sorted logic; many-sorted Boolean algebras with operators},

language = {eng},

month = {3},

number = {1},

pages = {31-59},

publisher = {EDP Sciences},

title = {Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study},

url = {http://eudml.org/doc/222078},

volume = {35},

year = {2010},

}

TY - JOUR

AU - Jacobs, Bart

TI - Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

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.; modal logic; coalgebras; many-sorted logic; many-sorted Boolean algebras with operators

UR - http://eudml.org/doc/222078

ER -

## References

top- 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.03501
- B.A. Davey and H.A. Priestley, Introduction to Lattices and Order, Math. Textbooks. Cambridge Univ. Press (1990). Zbl0701.06001
- R. Goldblatt, Mathematics of Modality. Stanford, CSLI Lecture Notes 43 (1993).
- R. Goldblatt, Duality for some categories of coalgebras. Algebra Universalis (to appear). Zbl1061.18004
- R. Goldblatt, What is the coalgebraic analogue of Birkhoff's variety theorem? Theoret. Comput. Sci. (to appear). Zbl0989.68099
- 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.68018
- 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.
- C. Hermida and B. Jacobs, Structural induction and coinduction in a fibrational setting. Inform. and Comput.145 (1998) 107-152. Zbl0941.18006
- 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.
- B. Jacobs, Categorical Logic and Type Theory. North Holland, Amsterdam (1999). Zbl0911.03001
- 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.03017
- 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.03503
- B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. EATCS Bull.62 (1997) 222-259. Zbl0880.68070
- 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.
- P.T. Johnstone, Stone Spaces. Cambridge Univ. Press, Cambridge Stud. Adv. Math. 3 (1982).
- B. Jónsson and A. Tarski, Boolean algebras with operators I. Amer. J. Math.73 (1951) 891-939. Zbl0045.31505
- A. Kurz, Specifying coalgebras with modal logic. Theoret. Comput. Sci. (to appear). Zbl0974.68034
- F.W. Lawvere, Functorial semantics. Proc. Nat. Acad. Sci. U.S.A.50 (1963) 869-872. Zbl0119.25901
- E.J. Lemmon, Algebraic semantics for modal logics II. J. Symbolic Logic31 (1966) 191-218. Zbl0147.24805
- L.S. Moss, Coalgebraic logic. Ann. Pure Appl. Logic96 (1999) 277-317; Erratum in Ann. Pure Appl. Logic 99 (1999) 241-259. Zbl0969.03026
- H. Reichel, An approach to object semantics based on terminal co-algebras. Math. Structures Comput. Sci.5 (1995) 129-152. Zbl0854.18006
- 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.68028
- 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.03502
- M. Rößiger, From modal logic to terminal coalgebras. Theoret. Comput. Sci. (to appear). Zbl0959.03502
- J. Rothe, H. Tews and B. Jacobs, The coalgebraic class specification language CCSL. J. Universal Comput. Sci. 7 (2001). Zbl0970.68104
- J. Rutten, Universal coalgebra: A theory of systems. Theoret. Comput. Sci.249 (2000) 3-80. Zbl0951.68038
- M.H. Stone, The theory of representations for Boolean algebra. Trans. Amer. Math. Soc.40 (1936) 37-111. Zbl0014.34002
- M.H. Stone, Applications of the theory of Boolean rings to general topology. Trans. Amer. Math. Soc.41 (1937) 375-481. Zbl0017.13502
- 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.68140
- Y. Venema, Points, lines and diamonds: a two-sorted modal logic for projective planes. J. Logic Comput.9 (1999) 601-621. Zbl0941.03020
- S. Vickers, Topology Via Logic. Cambridge Univ. Press, Tracts Theor. Comput. Sci.5 (1989).

## NotesEmbed ?

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