A Linear-Time Nominal μ-Calculus with Name Allocation
Hausmann D, Milius S, Schröder L (2021)
Publication Type: Conference contribution
Publication year: 2021
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 202
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Tallinn
ISBN: 9783959772013
DOI: 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.
Authors with CRIS profile
Stefan Milius
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Lutz Schröder
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Involved external institutions
Sweden (SE)How to cite
APA:
Hausmann, D., Milius, S., & Schröder, L. (2021). A Linear-Time Nominal μ-Calculus with Name Allocation. In Filippo Bonchi, Simon J. Puglisi (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Tallinn, EE: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Hausmann, Daniel, Stefan Milius, and Lutz Schröder. "A Linear-Time Nominal μ-Calculus with Name Allocation." Proceedings of the 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, Tallinn Ed. Filippo Bonchi, Simon J. Puglisi, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021.
BibTeX: Download