Document Open Access Logo

Expressivity Within Second-Order Transitive-Closure Logic

Authors Flavio Ferrarotti , Jan Van den Bussche , Jonni Virtema

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.22.pdf
  • Filesize: 499 kB
  • 18 pages

Document Identifiers

Author Details

Flavio Ferrarotti
  • Software Competence Center Hagenberg, Hagenberg, Austria
Jan Van den Bussche
  • Hasselt University, Hasselt, Belgium
Jonni Virtema
  • Hasselt University, Hasselt, Belgium

Funding

The research reported in this paper results from the joint project Higher-Order Logics and Structures supported by the Austrian Science Fund (FWF: [I2420-N31]) and the Research Foundation Flanders (FWO: [G0G6516N]).

Cite AsGet BibTex

Flavio Ferrarotti, Jan Van den Bussche, and Jonni Virtema. Expressivity Within Second-Order Transitive-Closure Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.22

Abstract

Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. This paper focuses on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(exists); in 2TC, the TC operator binds only tuples of relation variables. We establish that, with respect to expressive power, SO(2TC)(exists) collapses to existential first-order logic. In addition we study the relationship of MSO(TC) to an extension of MSO(TC) with counting features (CMSO(TC)) as well as to order-invariant MSO. We show that the expressive powers of CMSO(TC) and MSO(TC) coincide. Moreover we establish that, over unary vocabularies, MSO(TC) strictly subsumes order-invariant MSO.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • Expressive power
  • Higher order logics
  • Descriptive complexity

Metrics

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

References

  1. Serge Abiteboul and Victor Vianu. Fixpoint extensions of first-order logic and datalog-like languages. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 71-79. IEEE Computer Society, 1989. URL: http://dx.doi.org/10.1109/LICS.1989.39160.
  2. Jean-Raymond Abrial. The B-book - Assigning programs to meanings. Cambridge University Press, 2005. Google Scholar
  3. Jean-Raymond Abrial. Modeling in Event-B - System and Software Engineering. Cambridge University Press, 2010. Google Scholar
  4. Faisal N. Abu-Khzam and Michael A. Langston. Graph coloring and the immersion order. In Computing and Combinatorics, 9th Annual International Conference (COCOON 2003), pages 394-403, 2003. Google Scholar
  5. Meghyn Bienvenu, Balder ten Cate, Carsten Lutz, and Frank Wolter. Ontology-based data access: A study through disjunctive Datalog, CSP, and MMSNP. In Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS '13, pages 213-224, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2463664.2465223.
  6. Andreas Blass, Yuri Gurevich, and Jan Van den Bussche. Abstract state machines and computationally complete query languages. Information and Computation, 174(1):20-36, 2002. URL: http://dx.doi.org/10.1006/inco.2001.3067.
  7. Andreas Blass, Yuri Gurevich, and Saharon Shelah. Choiceless polynomial time. Annals of Pure and Applied Logic, 100(1):141-187, 1999. URL: http://dx.doi.org/10.1016/S0168-0072(99)00005-6.
  8. Joshua Blinkhorn and Olaf Beyersdorff. Shortening QBF proofs with dependency schemes. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, pages 263-280, Cham, 2017. Springer International Publishing. Google Scholar
  9. Béla Bollobás. Modern Graph Theory, volume 184 of Graduate Texts in Mathematics. Springer, 2002. Google Scholar
  10. E. Börger and R. F. Stärk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, 2003. Google Scholar
  11. Pierre Bourhis, Markus Krötzsch, and Sebastian Rudolph. Reasonable highly expressive query languages - IJCAI-15 distinguished paper (honorary mention). In Qiang Yang and Michael Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 2826-2832. AAAI Press, 2015. Google Scholar
  12. Bogdan S Chlebus. Domino-tiling games. J. Comput. Syst. Sci., 32(3):374-392, 1986. URL: http://dx.doi.org/10.1016/0022-0000(86)90036-X.
  13. Bruno Courcelle. The monadic second-order logic of graphs VIII: orientations. Ann. Pure Appl. Logic, 72(2):103-143, 1995. URL: http://dx.doi.org/10.1016/0168-0072(95)94698-V.
  14. Stephen Dill, Ravi Kumar, Kevin S. Mccurley, Sridhar Rajagopalan, D. Sivakumar, and Andrew Tomkins. Self-similarity in the web. ACM Trans. Internet Technol., 2(3):205-223, 2002. Google Scholar
  15. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  16. Flavio Ferrarotti. Expressibility of Higher-Order Logics on Relational Databases: Proper Hierarchies. PhD thesis, Massey University, Wellington, New Zealand, 2008. URL: http://hdl.handle.net/10179/799.
  17. Flavio Ferrarotti, Senén González, and José Maria Turull Torres. On fragments of higher order logics that on finite structures collapse to second order. In Juliette Kennedy and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings, volume 10388 of Lecture Notes in Computer Science, pages 125-139. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-662-55386-2_9.
  18. Flavio Ferrarotti, Wei Ren, and Jose Maria Turull Torres. Expressing properties in second- and third-order logic: hypercube graphs and SATQBF. Logic Journal of the IGPL, 22(2):355-386, 2014. URL: http://dx.doi.org/10.1093/jigpal/jzt025.
  19. Martin Grohe, Kenichi Kawarabayashi, Dániel Marx, and Paul Wollan. Finding topological subgraphs is fixed-parameter tractable. In Proceedings of the 43rd Annual ACM Symposium on Theory of Computing (STOC 2011), pages 479-488. ACM, 2011. Google Scholar
  20. R. Guimerà, L. Danon, A. Díaz-Guilera, F. Giralt, and A. Arenas. Self-similar community structure in a network of human interactions. Phys. Rev. E, 68:065103, Dec 2003. Google Scholar
  21. David Harel and David Peleg. On static logics, dynamic logics, and complexity classes. Information and Control, 60(1-3):86-102, 1984. URL: http://dx.doi.org/10.1016/S0019-9958(84)80023-6.
  22. Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. J. Autom. Reasoning, 58(1):97-125, 2017. URL: http://dx.doi.org/10.1007/s10817-016-9390-4.
  23. Neil Immerman. Languages that capture complexity classes. SIAM J. Comput., 16(4):760-778, aug 1987. URL: http://dx.doi.org/10.1137/0216051.
  24. Neil Immerman. Nondeterministic space is closed under complementation. SIAM J. Comput., 17(5):935-938, 1988. URL: http://dx.doi.org/10.1137/0217058.
  25. Neil Immerman. Descriptive Complexity. Springer, 1998. Google Scholar
  26. E. Kopczynski and A. W. To. Parikh images of grammars: Complexity and applications. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 80-89, July 2010. URL: http://dx.doi.org/10.1109/LICS.2010.21.
  27. Richard Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6:467-480, 1977. Google Scholar
  28. Leslie Lamport. Specifying Systems, The TLA^+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. Google Scholar
  29. C.H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. Google Scholar
  30. Rohit J. Parikh. On context-free languages. J. ACM, 13(4):570-581, 1966. URL: http://dx.doi.org/10.1145/321356.321364.
  31. Tomáš Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency learning for QBF. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, pages 298-313, Cham, 2017. Springer International Publishing. Google Scholar
  32. Albert Réka. Scale-free networks in cell biology. Journal of Cell Science, 118(21):4947-4957, 2005. Google Scholar
  33. Juan L. Reutter, Miguel Romero, and Moshe Y. Vardi. Regular queries on graph databases. In 18th International Conference on Database Theory, ICDT 2015, March 23-27, 2015, Brussels, Belgium, pages 177-194, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.ICDT.2015.177.
  34. David Richerby. Logical characterizations of PSPACE. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 370-384. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30124-0_29.
  35. E. Rosen. An existential fragment of second order logic. Archive for Mathematical Logic, 38(4-5):217-234, 1999. Google Scholar
  36. Sebastian Rudolph and Markus Krötzsch. Flag &check: Data access with monadically defined queries. In Proceedings of the 32Nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS '13, pages 151-162, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2463664.2465227.
  37. Chaoming Song, Shlomo Havlin, and Hernán A. Makse. Self-similarity of complex networks. Nature, 433:392-395, 2005. 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