SpringerLink
Log in

Universal First-Order Quantification over Automata

  • Conference paper
  • First Online:
Implementation and Application of Automata (CIAA 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14151))

Included in the following conference series:

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

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 48.14
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 62.05
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Boigelot, B., Fontaine, P., Vergain, B.: Universal first-order quantification over automata. ar**v:2306.04210 [cs.LO] (2023)

  2. 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)

    Article  MathSciNet  MATH  Google Scholar 

  3. Boigelot, B., Latour, L.: Counting the solutions of Presburger equations without enumerating them. Theo. Comp. Sc. 313(1), 17–29 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bruyère, V., Carton, O.: Automata on linear orderings. J. Comput. Syst. Sci. 74(1), 1–24 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  5. Büchi, J.R.: Weak second-order arithmetic and finite automata. Math. Logic Q. 6(1–6), 66–92 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  6. 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)

    Google Scholar 

  7. Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Harvard University, Technical Report (1972)

    Google Scholar 

  8. Halpern, J.Y.: Presburger arithmetic with unary predicates is \(\Pi _1^1\) complete. Journal Symbolic Logic 56(2), 637–642 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  9. 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

    Chapter  MATH  Google Scholar 

  10. Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fundamenta Mathematicae 59(1), 109–116 (1966)

    Article  MathSciNet  MATH  Google Scholar 

  11. McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9(5), 512–530 (1966)

    Article  MathSciNet  MATH  Google Scholar 

  12. Okhotin, A.: The dual of concatenation. Theo. Comp. Sc. 345(2–3), 425–447 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  13. Safra, S.: On the complexity of omega-automata. In: Proceedings of 29th FOCS, pp. 319–327. IEEE Computer Society (1988)

    Google Scholar 

  14. 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

    Chapter  Google Scholar 

  15. Speranski, S.O.: A note on definability in fragments of arithmetic with free unary predicates. Arch. Math. Logic 52(5–6), 507–516 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  16. Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B, pp. 133–191. Elsevier and MIT Press (1990)

    Google Scholar 

  17. 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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Montefiore Institute, B28, University of Liège, Liège, Belgium

    Bernard Boigelot, Pascal Fontaine & Baptiste Vergain

Authors
  1. Bernard Boigelot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pascal Fontaine
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Baptiste Vergain
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bernard Boigelot .

Editor information

Editors and Affiliations

  1. Eastern Mediterranean University, Famagusta, Cyprus

    Benedek Nagy

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation