Document Open Access Logo

Uniform Interpolation for Coalgebraic Fixpoint Logic

Authors Johannes Marti, Fatemeh Seifan, Yde Venema

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2015.238.pdf
  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Author Details

Johannes Marti
Fatemeh Seifan
Yde Venema

Cite As Get BibTex

Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform Interpolation for Coalgebraic Fixpoint Logic. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 238-252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CALCO.2015.238

Abstract

We use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoys uniform interpolation. To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e., functors with quasifunctorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.

Subject Classification

Keywords
  • mu-calculus
  • uniform interpolation
  • coalgebra
  • automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jiří Adámek and Věra Trnková. Automata and algebras in categories, volume 37 of Mathematics and its Applications (East European Series). Kluwer Academic Publishers Group, Dordrecht, 1990. Google Scholar
  2. A. Arnold and D. Niwiński. Rudiments of μ-calculus, volume 146 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 2001. Google Scholar
  3. J. Richard Büchi. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math., 6:66-92, 1960. Google Scholar
  4. William Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic, 22:269-285, 1957. Google Scholar
  5. Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the μ-calculus: interpolation, Lyndon and Łoś-Tarski. J. Symbolic Logic, 65(1):310-332, 2000. Google Scholar
  6. Calvin C. Elgot. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98:21-51, 1961. Google Scholar
  7. Silvio Ghilardi. An algebraic theory of normal forms. Ann. Pure Appl. Logic, 71(3):189-245, 1995. Google Scholar
  8. Silvio Ghilardi and Marek Zawadowski. Undefinability of propositional quantifiers in the modal system S4. Studia Logica, 55(2):259-271, 1995. Google Scholar
  9. Leon Henkin. An extension of the Craig-Lyndon interpolation theorem. J. Symbolic Logic, 28:201-216, 1963. Google Scholar
  10. David Janin and Igor Walukiewicz. Automata for the modal μ-calculus and related results. In Mathematical foundations of computer science 1995 (Prague), volume 969 of Lecture Notes in Comput. Sci., pages 552-562. Springer, Berlin, 1995. Google Scholar
  11. Christian Kissig and Yde Venema. Complementation of coalgebra automata. In Algebra and coalgebra in computer science, volume 5728 of Lecture Notes in Comput. Sci., pages 81-96. Springer, Berlin, 2009. Google Scholar
  12. Clemens Kupke and Yde Venema. Coalgebraic automata theory: basic results. Log. Methods Comput. Sci., 4(4):4:10, 43, 2008. Google Scholar
  13. Johannes Marti. Relation liftings in coalgebraic modal logic. Master’s thesis, Universiteit van Amsterdam, 2011. Google Scholar
  14. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. System Sci., 81(5):880-900, 2015. Google Scholar
  15. Lawrence S. Moss. Coalgebraic logic. Ann. Pure Appl. Logic, 96(1-3):277-317, 1999. Festschrift on the occasion of Professor Rohit Parikh’s 60th birthday. Google Scholar
  16. Dirk Pattinson. The logic of exact covers: Completeness and uniform interpolation. In Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on, pages 418-427. IEEE, 2013. Google Scholar
  17. Andrew M. Pitts. On an interpretation of second-order quantification in first-order intuitionistic propositional logic. J. Symbolic Logic, 57(1):33-52, 1992. Google Scholar
  18. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1-35, 1969. Google Scholar
  19. J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000. Modern algebra and its applications (Nashville, TN, 1996). Google Scholar
  20. Luigi Santocanale and Yde Venema. Uniform interpolation for monotone modal logic. In Advances in modal logic. Volume 8, pages 350-370. Coll. Publ., London, 2010. Google Scholar
  21. Vladimir Yurievich Shavrukov. Adventures in diagonalizable algebras. ILLC Publications, 1994. Google Scholar
  22. Yde Venema. Automata and fixed point logics for coalgebras. In Proceedings of the Workshop on Coalgebraic Methods in Computer Science, volume 106 of Electron. Notes Theor. Comput. Sci., pages 355-375 (electronic). Elsevier, Amsterdam, 2004. Google Scholar
  23. Albert Visser. Uniform interpolation and layered bisimulation. In Gödel'96 (Brno, 1996), volume 6 of Lecture Notes Logic, pages 139-164. Springer, Berlin, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact