Document Open Access Logo

Characterizing Definability in Decidable Fixpoint Logics

Authors Michael Benedikt, Pierre Bourhis, Michael Vanden Boom

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2017.107.pdf
  • Filesize: 0.54 MB
  • 14 pages

Document Identifiers

Author Details

Michael Benedikt
Pierre Bourhis
Michael Vanden Boom

Cite AsGet BibTex

Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. Characterizing Definability in Decidable Fixpoint Logics. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 107:1-107:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ICALP.2017.107

Abstract

We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back-and-forth between relational logics and logics over trees.
Keywords
  • Guarded logics
  • bisimulation
  • definability
  • automata

Metrics

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

References

  1. Hajnal Andréka, Johan van Benthem, and István Németi. Modal languages and bounded fragments of predicate logic. J. Phil. Logic, 27:217-274, 1998. Google Scholar
  2. Andre Arnold and Damin Niwinski. Rudiments of mu-calculus. Elsevier, 2001. Google Scholar
  3. Vince Bárány, Balder Ten Cate, and Luc Segoufin. Guarded negation. J. ACM, 62(3), 2015. URL: http://dx.doi.org/10.1145/2701414.
  4. Vince Bárány, Georg Gottlob, and Martin Otto. Querying the guarded fragment. In LMCS, volume 10, 2014. URL: http://dx.doi.org/10.2168/LMCS-10(2:3)2014.
  5. Vince Bárány, Balder ten Cate, and Luc Segoufin. Guarded negation. In ICALP, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22012-8_28.
  6. Pablo Barceló, Georg Gottlob, and Andreas Pieris. Semantic acyclicity under constraints. In PODS, 2016. URL: http://dx.doi.org/10.1145/2902251.2902302.
  7. Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. A step up in expressiveness of decidable fixpoint logics. In LICS, 2016. URL: http://dx.doi.org/10.1145/2933575.2933592.
  8. Michael Benedikt, Balder ten Cate, Thomas Colcombet, and Michael Vanden Boom. The complexity of boundedness for guarded logics. In LICS, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.36.
  9. Michael Benedikt, Balder ten Cate, and Michael Vanden Boom. Interpolation with decidable fixpoint logics. In LICS, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.43.
  10. Achim Blumensath, Martin Otto, and Mark Weyer. Decidability results for the boundedness problem. Logical Methods in Computer Science, 10(3), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(3:2)2014.
  11. Giovanna D'Agostino and Marco Hollenberg. Logical Questions Concerning The mu-Calculus: Interpolation, Lyndon and Los-Tarski. The Journal of Symbolic Logic, 65(1):310-332, 2000. URL: http://dx.doi.org/10.2307/2586539.
  12. Giovanna D'Agostino and Giacomo Lenzi. Bisimulation quantifiers and uniform interpolation for guarded first order logic. Theor. Comput. Sci., 563:75-85, 2015. URL: http://dx.doi.org/10.1016/j.tcs.2014.08.015.
  13. Diego Figueira. Semantically acyclic conjunctive queries under functional dependencies. In LICS, 2016. URL: http://dx.doi.org/10.1145/2933575.2933580.
  14. Georg Gottlob, Erich Grädel, and Helmut Veith. Datalog LITE: a deductive query language with linear time model checking. ACM Trans. Comput. Log., 3(1):42-79, 2002. URL: http://dx.doi.org/10.1145/504077.504079.
  15. Georg Gottlob, Nicola Leone, and Francesco Scarcello. Robbers, marshals, and guards: game theoretic and logical characterizations of hypertree width. J. Comput. Syst. Sci., 66(4):775-808, 2003. URL: http://dx.doi.org/10.1016/S0022-0000(03)00030-8.
  16. Erich Grädel, Colin Hirsch, and Martin Otto. Back and forth between guarded and modal logics. ACM TOCL, 3(3):418-463, 2002. URL: http://dx.doi.org/10.1145/507382.507388.
  17. Erich Grädel and Martin Otto. The freedoms of (guarded) bisimulation. In Johan van Benthem on Logic and Information Dynamics, pages 3-31. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-06025-5_1.
  18. Erich Grädel and Igor Walukiewicz. Guarded fixed point logic. In LICS, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782585.
  19. Eva Hoogland, Maarten Marx, and Martin Otto. Beth definability for the guarded fragment. In LPAR, 1999. URL: http://dx.doi.org/10.1007/3-540-48242-3_17.
  20. David Janin and Igor Walukiewicz. Automata for the modal mu-calculus and related results. In MFCS, 1995. URL: http://dx.doi.org/10.1007/3-540-60246-1_160.
  21. David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In CONCUR, 1996. URL: http://dx.doi.org/10.1007/3-540-61604-7_60.
  22. Martin Otto. Eliminating recursion in the μ-calculus. In STACS, 1999. URL: http://dx.doi.org/10.1007/3-540-49116-3_50.
  23. Balder ten Cate and Luc Segoufin. Unary negation. In STACS, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2011.344.
  24. J. F. A. K. van Benthem. Modal Logic and Classical Logic. Humanities Pr, 1983. Google Scholar
  25. Moshe Y. Vardi. "Why is Modal Logic so Robustly Decidable". In Descriptive Complexity and Finite Models, pages 149-184, 1997. Google Scholar
  26. Mihalis Yannakakis. Algorithms for acyclic database schemes. In VLDB, 1981. 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 Imprint Privacy Contact