×

Coalgebraic logic. (English) Zbl 0969.03026

Ann. Pure Appl. Logic 96, No. 1-3, 277-317 (1999); erratum ibid. 99, No. 1-3, 241-259 (1999).
A starting point of the paper is the characterization theorem for infinitary modal logic stating that two points in Kripke models satisfy the same infinitary modal formulas iff they are bisimilar; moreover, every bisimulation type is determined by a single formula [J. Barwise and L. S. Moss, Vicious circles (CSLI Lect. Notes 60), CSLI, Stanford (1996; Zbl 0865.03002)].
Coalgebraic logics are generalizations of infinitary modal logics. Such a logic is determined by a functor on sets with some properties; formulas are interpreted in coalgebras of that functor. Coalgebraic logics generalize modal logics as well as various logics of transition systems [J. J. M. M. Rutten, “A calculus of transition systems: towards universal coalgebra”, in: A. Ponse, M. de Rijke, Y. Venema (eds.), Modal logic and process algebra: a bisimulation perspective, CSLI Lect. Notes 53, 231-256 (1995; Zbl 0943.68508)].
The paper introduces a semantics for coalgebraic logics and proves soundness for the ‘minimal F-logic’ (completeness remains an open problem). Moreover, it proves characterization results and a representation theorem stating that every final F-coalgebra can be extracted from an F-algebra with a complete semilattice ordering.

MSC:

03B45 Modal logic (including the logic of norms)
03G30 Categorical logic, topoi
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aczel, P., Non-Well-Founded Sets, (CSLI Lecture Notes Number, vol. 14 (1988), CSLI Publications: CSLI Publications Stanford) · Zbl 0668.04001
[2] Aczel, P.; Mendler, N., A final coalgebra theorem, (Pitt, D. H.; etal., Category Theory and Computer Science (1989), Springer: Springer Heidelberg), 357-365 · Zbl 1496.03206
[3] S. Aliyari, Personal correspondence. Email message of 24 September, 1997.; S. Aliyari, Personal correspondence. Email message of 24 September, 1997.
[4] Baltag, A., Alexandru, Modal characterisation for sets and Kripke models (1996), Indiana University, Unpublished manuscript
[5] Barr, M., Terminal coalgebras in well-founded set theory, Theoret. Comput. Sci., 114, 2, 299-315 (1993) · Zbl 0779.18004
[6] Barr, M., Additions and corrections to “terminal coalgebras in well-founded set theory”, Theoret. Comput. Sci., 124, 1, 189-192 (1994) · Zbl 0788.18001
[7] Blute, R.; Desharnais, J.; Edalat, A.; Panangaden, P., Bisimulation for labeled Markov processes, (proceedings of the 1997 CSI. meeting. proceedings of the 1997 CSI. meeting, Technical Report (1996), BRICS: BRICS Aarhus, Denmark), Paper also to appear in the
[8] Barwise, J.; Moss, L. S., Vicious Circles, CSLI Publications Number 60 (1996), Stanford · Zbl 0865.03002
[9] Barwise, J.; Moss, L. S., Modal correspondence for models, (Dekker, P.; Stokhof, M., Proc. 10th Amsterdam Colloquium. ILLC/Department of Philosophy (1996), University of Amsterdam), 41-56
[10] van Benthem, J., Modal correspondence theory, (Ph.D. Thesis (1976), Department of Mathematics, University of Amsterdam) · Zbl 0308.02023
[11] Corradini, A., A complete calculus for equational deduction in coalgebraic specification, (Technical Report (1997), CWI: CWI Amsterdam) · Zbl 0903.08007
[12] Fagin, R., A quantitative analysis of modal logic, J. Symbolic Logic, 59, 1, 209-252 (1994) · Zbl 0806.03017
[13] Gerbrandy, J., Characterizations of bisimulation and bounded bisimulations, (de Rijke, M., Workshop Proc. on Observational Equivalence and Logical Equivalence. European Summer School on Logic, Language, and Information. Workshop Proc. on Observational Equivalence and Logical Equivalence. European Summer School on Logic, Language, and Information, Prague (1996))
[14] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Inform. Comput., 94, 1-28 (1991) · Zbl 0756.68035
[15] Moss, L. S.; Danner, N., On the foundations of corecursion, Logic J. IGPL, 5, 3, 231-257 (1997) · Zbl 0872.03030
[16] Mislove, M. W.; Moss, L. S.; Oles, F. J., Non-well-founded sets modeled as ideal fixed points, Inform Comput., 93, 1, 16-54 (1991) · Zbl 0723.03031
[17] Paulson, L., A concrete final coalgebra theorem for ZF set theory, (Dybjer, P.; Nordstrom, B.; Smith, J., Types for Proofs and Programs ’94. Types for Proofs and Programs ’94, Lecture Notes in Computer Science, vol. 995 (1995), Springer: Springer Berlin), 120-139
[18] Rutten, J. J.M. M., A calculus of transition systems: towards universal coalgebra, (Ponsc, A.; de Rijke, M.; Venema, Y., Modal Logic and Process Algebra: a Bisimulation Perspective. Modal Logic and Process Algebra: a Bisimulation Perspective, CSLI Lecture Notes, vol. 53 (1995)), Stanford · Zbl 0951.68038
[19] Rutten, J. J.M. M., Universal coalgebra: a theory of systems, (CWI Report CS-R9652 (1996), CWI Computer Science Department: CWI Computer Science Department Amsterdam) · Zbl 0951.68038
[20] Turi, D., Functorial operational semantics and its denotational dual, (Ph.D. Thesis (1976), CWI: CWI Amsterdam)
[21] Turi, D.; Rutten, J. J.M. M., On the foundations of final semantics: non-standard sets, metric spaces. partial orders, (de Bakker, J. W.; de Roever, W.-P.; Rozenberg, G., Proc. REX Workshop on Semantics: Foundations and Applications. Proc. REX Workshop on Semantics: Foundations and Applications, Lecture Notes in Computer Science, vol. 666 (1993), Springer: Springer Berlin), 477-530, Revised version of a paper with the same title
[22] de Vink, E. P.; Rutten, J. J.M. M., Bisimulation for probabilistic transition systems: a coalgebraic approach, (Degano, P.; Gorrieri, R.; Marchetti-Spaccamela, A., Proc. 24th ICALP’97 (1997), Springer: Springer Berlin), 460-470, 1256 · Zbl 0930.68092
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.