Abstract
We introduce two versions of Presburger Automata with the Büchi acceptance condition, working over infinite, finite-branching trees. These automata, in addition to the classical ones, allow nodes for checking linear inequalities over labels of their children. We establish tight \(\textsc {NP}\) and \(\textsc {ExpTime}\) bounds on the complexity of the non-emptiness problem for the presented machines. We demonstrate the usefulness of our automata models by polynomially encoding the two-variable guarded fragment extended with Presburger constraints, improving the existing triply-exponential upper bound to a single exponential.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Constraints with \(\equiv _k\) can be eliminated [4].
- 2.
Of course we may always restrict ourselves to binary trees by employing standard tricks, but then the verification of Presburger constraints becomes a challenge.
- 3.
In the literature \(\mathcal {S}\) appears under the name of a syntactic closure.
References
Baader, F.: A new description logic with set constraints and cardinality constraints on role successors. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 43–59. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_3
Baader, F., Hladik, J., Peñaloza, R.: Automata can show PSPACE results for description logics. Inf. Comput. 206, 1045–1056 (2008)
Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press, Cambridge (2017)
Bednarczyk, B.: One-variable logic meets Presburger arithmetic. Theor. Comput. Sci. 802, 141–146 (2020)
Bednarczyk, B., Orlowska, M., Pacanowska, A., Tan, T.: On classical decidable logics extended with percentage quantifiers and arithmetics. In: FSTTCS 2021 (2021)
Boiret, A., Hugot, V., Niehren, J., Treinen, R.: Automata for unordered trees. Inf. Comput. 253, 304–335 (2017)
Boiret, A., Hugot, V., Niehren, J., Treinen, R.: Logics for unordered trees with data constraints. J. Comput. Syst. Sci. 104, 149–164 (2019)
Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The complexity of enriched mu-calculi. Log. Methods Comput. Sci. (2008)
Boneva, I., Talbot, J.-M.: Automata and logics for unranked and unordered trees. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 500–515. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_36
Borosh, I., Flahive, M., Treybig, B.: Small solutions of linear Diophantine equations. Discret. Math 58, 215–220 (1986)
Calvanese, D., Carbotta, D., Ortiz, M.: A practical automata-based technique for reasoning in expressive description logics. In: Walsh, T. (ed.) IJCAI 2011 (2011)
Calvanese, D., Eiter, T., Ortiz, M.: Answering regular path queries in expressive description logics via alternating tree-automata. Inf. Comput. 237, 12–55 (2014)
Chandra, A.K., Stockmeyer, L.J.: Alternation. In: FOCS 1976 (1976)
Comon, H., et al.: Tree automata techniques and applications (2008)
Demri, S., Lugiez, D.: Complexity of modal logics with Presburger constraints. J. Appl. Log. 8, 233–252 (2010)
Eisenbrand, F., Shmonin, G.: Carathéodory bounds for integer cones. Oper. Res. Lett. 34, 564–568 (2006)
El-Sappagh, S., Franda, F., Ali, F., Kwak, K.S.: SNOMED CT standard ontology based on the ontology for general medical science. BMC Med. Inform. Decis. Making 18, 1–19 (2018)
Grädel, E.: Description logics and guarded fragments of first order logic. In: DL (1998)
Kupke, C., Pattinson, D.: On modal logics of linear inequalities. In: Beklemishev, L.D., Goranko, V., Shehtman, V.B. (eds.) AIML 2010 (2010)
Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)
Papadimitriou, C.H.: On the complexity of integer programming. J. ACM (JACM) 28, 765–768 (1981)
Schwentick, T.: Trees, automata and XML. In: Beeri, C., Deutsch, A. (eds.) PODS 2004 (2004)
Seidl, H., Schwentick, T., Muscholl, A.: Counting in trees. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas] (2008)
Sipser, M.: Introduction to the theory of computation. ACM Sigact News 27, 27–29 (1996)
Acknowledgements
This work was supported by the Polish Ministry of Science and Higher Education program “Diamentowy Grant” no. DI2017 006447. We are grateful to Tim Lyon and Reijo Jaakkola for proofreading and language improvements.
Results from this paper will appear in the BSc thesis of Oskar Fiuk, written under informal supervision of Bartosz Bednarczyk at the University of Wrocław. Oskar Fiuk was supported by NCN grant No. 2021/41/B/ST6/00996.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Bednarczyk, B., Fiuk, O. (2022). Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting. In: Ciabattoni, A., Pimentel, E., de Queiroz, R.J.G.B. (eds) Logic, Language, Information, and Computation. WoLLIC 2022. Lecture Notes in Computer Science, vol 13468. Springer, Cham. https://doi.org/10.1007/978-3-031-15298-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-031-15298-6_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-15297-9
Online ISBN: 978-3-031-15298-6
eBook Packages: Computer ScienceComputer Science (R0)
