Abstract
Deciding formulas that mix arithmetic and uninterpreted predicates is of practical interest, notably for applications in verification. Some decision procedures consist in building by structural induction an automaton that recognizes the set of models of the formula under analysis, and then testing whether this automaton accepts a non-empty language. A drawback is that universal quantification is usually handled by a reduction to existential quantification and complementation. For logical formalisms in which models are encoded as infinite words, this hinders the practical use of this method due to the difficulty of complementing infinite-word automata. The contribution of this paper is to introduce an algorithm for directly computing the effect of universal first-order quantifiers on automata recognizing sets of models, for formulas involving natural numbers encoded in unary notation. This paves the way to implementable decision procedures for various arithmetic theories.
Research reported in this paper was supported in part by an Amazon Research Award, Fall 2022 CFP. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not reflect the views of Amazon.
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
References
Boigelot, B., Fontaine, P., Vergain, B.: Universal first-order quantification over automata. arXiv:2306.04210 [cs.LO] (2023)
Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Tr. Comp. Logic 6(3), 614–633 (2005)
Boigelot, B., Latour, L.: Counting the solutions of Presburger equations without enumerating them. Theo. Comp. Sc. 313(1), 17–29 (2004)
Bruyère, V., Carton, O.: Automata on linear orderings. J. Comput. Syst. Sci. 74(1), 1–24 (2007)
Büchi, J.R.: Weak second-order arithmetic and finite automata. Math. Logic Q. 6(1–6), 66–92 (1960)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings International Congress on Logic, Methodology and Philosophy of Science, pp. 1–12 (1962)
Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Harvard University, Technical Report (1972)
Halpern, J.Y.: Presburger arithmetic with unary predicates is \(\Pi _1^1\) complete. Journal Symbolic Logic 56(2), 637–642 (1991)
Klarlund, N.: Mona & Fido: The logic-automaton connection in practice. In: Nielsen, M., Thomas, W. (eds.) CSL 1997. LNCS, vol. 1414, pp. 311–326. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028022
Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fundamenta Mathematicae 59(1), 109–116 (1966)
McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9(5), 512–530 (1966)
Okhotin, A.: The dual of concatenation. Theo. Comp. Sc. 345(2–3), 425–447 (2005)
Safra, S.: On the complexity of omega-automata. In: Proceedings of 29th FOCS, pp. 319–327. IEEE Computer Society (1988)
Shiple, T.R., Kukula, J.H., Ranjan, R.K.: A comparison of Presburger engines for EFSM reachability. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 280–292. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028752
Speranski, S.O.: A note on definability in fragments of arithmetic with free unary predicates. Arch. Math. Logic 52(5–6), 507–516 (2013)
Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B, pp. 133–191. Elsevier and MIT Press (1990)
Vardi, M.Y.: The Büchi complementation saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 12–22. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-70918-3_2
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Boigelot, B., Fontaine, P., Vergain, B. (2023). Universal First-Order Quantification over Automata. In: Nagy, B. (eds) Implementation and Application of Automata. CIAA 2023. Lecture Notes in Computer Science, vol 14151. Springer, Cham. https://doi.org/10.1007/978-3-031-40247-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-031-40247-0_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-40246-3
Online ISBN: 978-3-031-40247-0
eBook Packages: Computer ScienceComputer Science (R0)