Universal First-Order Quantification over Automata

[en] Deciding formulas that mix arithmetic and uninterpreted predicates is of practical interest, notably for applications in veriﬁcation. 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 quantiﬁcation is usually handled by a reduction to existential quantiﬁcation and complementation. For logical formalisms in which models are encoded as inﬁnite words, this hinders the practical use of this method due to the diﬃculty of complementing inﬁnite-word automata. The contribution of this paper is to introduce an algorithm for directly computing the eﬀect of universal ﬁrst-order quantiﬁers 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.

Disciplines :

Computer science

Author, co-author :

Boigelot, Bernard ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Informatique

Fontaine, Pascal ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Systèmes informatiques distribués

Vergain, Baptiste ; Université de Liège - ULiège > Montefiore Institute of Electrical Engineering and Computer Science

Language :

English

Title :

Universal First-Order Quantification over Automata

Publication date :

September 2023

Event name :

27th International Conference on Implementation and Application of Automata (CIAA 2023)

Event organizer :

Eastern Mediterranean University

Event place :

Famagusta, Cyprus

Event date :

September 19-22, 2023

Audience :

International

Main work title :

Implementation and Application of Automata

Publisher :

Springer Nature Switzerland

ISBN/EAN :

978-3-03-140247-0
978-3-03-140246-3

Pages :

Peer reviewed :

Peer reviewed

Additional URL :

https://link.springer.com/content/pdf/10.1007/978-3-031-40247-0_6

Funders :

Amazon [US-WA] [US-WA]

Funding text :

Research reported in this paper was supported in part by an Amazon Research Award, Fall 2022 CFP. Any opinions, ﬁndings, and conclusions or recommendations expressed in this material are those of the authors and do not reﬂect the views of Amazon.

Available on ORBi :

since 06 September 2023

Statistics

Number of views

56 (6 by ULiège)

Number of downloads

40 (5 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

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 Π11 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