LIPIcs.MFCS.2021.58.pdf
- Filesize: 0.81 MB
- 18 pages
Document
A Linear-Time Nominal μ-Calculus with Name Allocation
Authors
Daniel Hausmann 
,
Stefan Milius ,
Lutz Schröder
-
Part of:
Volume:
46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Mathematical Foundations of Computer Science (MFCS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-08-18
File
Document Identifiers
Author Details
Cite AsGet BibTex
Daniel Hausmann, Stefan Milius, and Lutz Schröder. A Linear-Time Nominal μ-Calculus with Name Allocation. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 58:1-58:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.58
https://doi.org/10.4230/LIPIcs.MFCS.2021.58
Abstract
Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as {regular nondeterministic nominal automata (RNNAs)} have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-μTL} for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-μTL} allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-μTL} over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter.
Subject Classification
ACM Subject Classification
- Theory of computation → Modal and temporal logics
- Theory of computation → Verification by model checking
Keywords
- Model checking
- linear-time logic
- nominal sets
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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.
- 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.
- 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.
- Benedikt Bollig, Karin Quaas, and Arnaud Sangnier. The complexity of flat freeze LTL. Log. Methods Comput. Sci., 15(3), 2019. URL: http://dx.doi.org/10.23638/LMCS-15(3:33)2019.
- Thomas Colcombet. Unambiguity in automata theory. In Descriptional Complexity of Formal Systems, DCFS 2015, volume 9118 of LNCS, pages 3-18. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-19225-3.
- Thomas Colcombet and Amaldev Manuel. Generalized data automata and fixpoint logic. In Foundations 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.
- Thomas Colcombet and Amaldev Manuel. μ-calculus on data words. CoRR, 2014. URL: http://arxiv.org/abs/1404.4827.
- Thomas Colcombet and Amaldev Manuel. Fragments of fixpoint logic on data words. In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2015, volume 45 of LIPIcs, pages 98-111. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.98.
- 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.
- Wojciech Czerwiński and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. CoRR, 2021. URL: http://arxiv.org/abs/2104.13866.
- 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.
- Stéphane Demri and Arnaud Sangnier. When model-checking freeze LTL over counter machines becomes decidable. In Foundations of Software Science and Computation Structures, FOSSACS 2010, volume 6014 of LNCS, pages 176-190. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-12032-9_13.
- Diego Figueira and Luc Segoufin. Future-looking logics on data words and trees. In Mathematical Foundations of Computer Science, MFCS 2009, volume 5734 of LNCS, pages 331-343. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-03816-7_29.
- 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.
- 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.
- Murdoch James 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.
- Giuseppe De Giacomo and Moshe Vardi. Linear temporal logic and linear dynamic logic on finite traces. In International Joint Conference on Artificial Intelligence, IJCAI 2013, pages 854-860. IJCAI/AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997.
- 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.
- Jan Groote and Radu Mateescu. Verification of temporal properties of processes in a setting with data. In Algebraic Methodology and Software Technology, AMAST 1998, volume 1548 of LNCS, pages 74-90. Springer, 1998. URL: http://dx.doi.org/10.1007/3-540-49253-4_8.
- Jan Groote and Tim Willemse. Model-checking processes with data. Sci. Comput. Prog., 56(3):251-273, 2005. URL: http://dx.doi.org/10.1016/j.scico.2004.08.002.
- Orna Grumberg, Orna Kupferman, and Sarai Sheinvald. Model checking systems and specifications with parameterized atomic apropositions. In Automated Technology for Verification and Analysis, ATVA 2012, volume 7561 of LNCS, pages 122-136. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-33386-6_11.
- Daniel Hausmann, Stefan Milius, and Lutz Schröder. Harnessing LTL with freeze quantification. CoRR, 2020. URL: http://arxiv.org/abs/2010.10912.
- Falk Howar, Bengt Jonsson, and Frits Vaandrager. Combining black-box and white-box techniques for learning register automata. In Computing and Software Science - State of the Art and Perspectives, volume 10000 of LNCS, pages 563-588. Springer, 2019. URL: http://dx.doi.org/10.1007/978-3-319-91908-9_26.
- 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.
- Bartek Klin, Sławomir Lasota, and Szymon Toruńczyk. Nondeterministic and co-nondeterministic implies deterministic, for data languages. In Foundations of Software Science and Computation Structures, FOSSACS 2021, volume 12650 of LNCS, pages 365-384. Springer, 2021. URL: http://dx.doi.org/10.1007/978-3-030-71995-1_19.
- Bartek Klin and Mateusz Łełyk. Scalar and vectorial μ-calculus with atoms. Log. Methods Comput. Sci., 15(4), 2019. URL: http://dx.doi.org/10.23638/LMCS-15(4:5)2019.
- Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: http://dx.doi.org/10.1016/0304-3975(82)90125-6.
- Dexter Kozen, Konstantinos Mamouras, Daniela Petrisan, and Alexandra Silva. Nominal Kleene coalgebra. In Automata, Languages, and Programming, ICALP 2015, volume 9135 of LNCS, pages 286-298. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6.
- Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in nominal kleene algebra. In Relational and Algebraic Methods in Computer Science, RAMiCS 2015, volume 9348 of LNCS, pages 51-66. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-24704-5.
- 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.
- 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.
- Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. CoRR, 2021. URL: http://arxiv.org/abs/2104.12695.
- Amaldev Manuel, Anca Muscholl, and Gabriele Puppis. Walking on data words. Theory Comput. Sys., 59(2):180-208, 2016. URL: http://dx.doi.org/10.1007/s00224-014-9603-3.
- Antoine Mottet and Karin Quaas. The containment problem for unambiguous register automata. In Theoretical Aspects of Computer Science, STACS 2019, volume 126 of LIPIcs, pages 53:1-53:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2019.53.
- Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 5(3):403-435, 2004. URL: http://dx.doi.org/10.1145/1013560.1013562.
-
Andrew Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013.
- Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. Nominal automata with name binding. CoRR, 2016. URL: http://arxiv.org/abs/1603.01455.
- 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.
- Fu Song and Zhilin Wu. On temporal logics with data variable quantifications: Decidability and complexity. Inf. Comput., 251:104-139, 2016. URL: http://dx.doi.org/10.1016/j.ic.2016.08.002.
- David Turner and Glynn Winskel. Nominal domain theory for concurrency. In Computer Science Logic, CSL 2009, pages 546-560, 2009. URL: http://dx.doi.org/10.1007/978-3-642-04027-6_39.