RAIRO-Theor. Inf. Appl.
Volume 35, Number 1, January/February 2001Coalgebraic Methods in Computer Science
|Page(s)||31 - 59|
|Published online||15 April 2002|
Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study
Department of Computer Science, University of Nijmegen,
P.O. Box 9010, 6500 GL Nijmegen, The Netherlands; e-mail: firstname.lastname@example.org URL: http://www.cs.kun.nl/~bart
Accepted: 9 March 2001
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.
Mathematics Subject Classification: 03G05 / 03G30 / 06E25
Key words: Modal logic / coalgebra / Boolean algebra with operators.
© EDP Sciences, 2001
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.