Document Open Access Logo

Nominal Büchi Automata with Name Allocation

Authors Henning Urbat , Daniel Hausmann , Stefan Milius , Lutz Schröder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.4.pdf
  • Filesize: 0.75 MB
  • 16 pages

Document Identifiers

Author Details

Henning Urbat
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Daniel Hausmann
  • Gothenburg University, Göteborg, Sweden
Stefan Milius
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Urbat, Henning: Supported by Deutsche Forschungsgemeinschaft (DFG) under project SCHR 1118/15-1.
  • Hausmann, Daniel: Supported by Deutsche Forschungsgemeinschaft (DFG) under project MI 717/7-1 and by the European Research Council (ERC) under project 772459.
  • Milius, Stefan: Supported by Deutsche Forschungsgemeinschaft (DFG) under project MI 717/7-1.
  • Schröder, Lutz: Supported by Deutsche Forschungsgemeinschaft (DFG) under project SCHR 1118/15-1.

Cite AsGet BibTex

Henning Urbat, Daniel Hausmann, Stefan Milius, and Lutz Schröder. Nominal Büchi Automata with Name Allocation. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.4

Abstract

Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach ω-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Data languages
  • infinite words
  • nominal sets
  • inclusion checking

Metrics

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

Related Versions

References

  1. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  2. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. URL: http://dx.doi.org/10.1145/1970398.1970403.
  3. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(3:4)2014.
  4. Benedikt Bollig, Peter Habermehl, Martin Leucker, and Benjamin Monmege. A robust class of data languages and an application to learning. Log. Meth. Comput. Sci., 10(4), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(4:19)2014.
  5. Vincenzo Ciancia and Matteo Sammartino. A class of automata for the verification of infinite, resource-allocating behaviours. In Trustworthy Global Computing, TGC 2014, volume 8902 of LNCS, pages 97-111. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-45917-1_7.
  6. Thomas Colcombet and Amaldev Manuel. Generalized data automata and fixpoint logic. In Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, volume 29 of LIPIcs, pages 267-278. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.267.
  7. Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. J. ACM, 68(1):7:1-7:28, 2021. URL: http://dx.doi.org/10.1145/3422822.
  8. Wojciech Czerwiński and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. CoRR, 2021. URL: http://arxiv.org/abs/2104.13866.
  9. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: http://dx.doi.org/10.1145/1507244.1507246.
  10. Murdoch J. Gabbay. Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bull. Symb. Log., 17(2):161-229, 2011. URL: http://dx.doi.org/10.2178/bsl/1305810911.
  11. Murdoch J. Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In Foundations of Software Science and Computation Structures, FOSSACS 2011, volume 6604 of LNCS, pages 365-380. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19805-2.
  12. Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In Logic in Computer Science, LICS 1999, pages 214-224. IEEE Computer Society, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782617.
  13. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-36387-4.
  14. Radu Grigore, Dino Distefano, Rasmus Petersen, and Nikos Tzevelekos. Runtime verification based on register automata. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, volume 7795 of LNCS, pages 260-276. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-36742-7_19.
  15. Orna Grumberg, Orna Kupferman, and Sarai Sheinvald. Variable automata over infinite alphabets. In Language and Automata Theory and Applications, LATA 2010, volume 6031 of LNCS, pages 561-572. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13089-2.
  16. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: http://dx.doi.org/10.1016/0304-3975(94)90242-9.
  17. Ahmet Kara, Thomas Schwentick, and Tony Tan. Feasible automata for two-variable logic with successor on data words. In Language and Automata Theory and Applications, LATA 2012, volume 7183 of LNCS, pages 351-362. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28332-1_30.
  18. Orna Kupferman and Moshe Y. Vardi. Verification of fair transisiton systems. In Computer Aided Verification, CAV 1996, volume 1102 of LNCS, pages 372-382. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-61474-5_84.
  19. Klaas Kürtz, Ralf Küsters, and Thomas Wilke. Selecting theories and nonce generation for recursive protocols. In Formal methods in security engineering, FMSE 2007, pages 61-70. ACM, 2007. URL: http://dx.doi.org/10.1145/1314436.1314445.
  20. Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Nominal coalgebraic data types with applications to lambda calculus. Log. Methods Comput. Sci., 9(4), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(4:20)2013.
  21. Ranko Lazić. Safely freezing LTL. In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006, volume 4337 of LNCS, pages 381-392. Springer, 2006. URL: http://dx.doi.org/10.1007/11944836_35.
  22. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. CoRR, 2021. URL: http://arxiv.org/abs/2104.12695.
  23. Stefan Milius and Henning Urbat. Equational axiomatization of algebras with structure. In Foundations of Software Science and Computation Structures, FOSSACS 2019, volume 11425 of LNCS, pages 400-417. Springer, 2019. Full version available at https://arxiv.org/abs/1812.02016. URL: http://dx.doi.org/10.1007/978-3-030-17127-8_23.
  24. Daniela Petrişan. Investigations into Algebra and Topology over Nominal Sets. PhD thesis, University of Leicester, 2011. Google Scholar
  25. Andrew Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  26. Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. Nominal automata with name binding. In Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of LNCS, pages 124-142, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_8.
  27. Christoph Stockhusen and Till Tantau. Completeness results for parameterized space classes. In Parameterized and Exact Computation, IPEC 2013, volume 8246 of LNCS, pages 335-347. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-03898-8.
  28. Nikos Tzevelekos. Nominal Game Semantics. PhD thesis, University of Oxford, 2008. Google Scholar
  29. Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic trace semantics for buechi and parity automata. In Concurrency Theory, CONCUR 2016, volume 59 of LIPIcs, pages 24:1-24:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.24.
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