Document

**Published in:** LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

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.

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)

Copy BibTex To Clipboard

@InProceedings{hausmann_et_al:LIPIcs.MFCS.2021.58, author = {Hausmann, Daniel and Milius, Stefan and Schr\"{o}der, Lutz}, title = {{A Linear-Time Nominal \mu-Calculus with Name Allocation}}, booktitle = {46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)}, pages = {58:1--58:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-201-3}, ISSN = {1868-8969}, year = {2021}, volume = {202}, editor = {Bonchi, Filippo and Puglisi, Simon J.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.58}, URN = {urn:nbn:de:0030-drops-144987}, doi = {10.4230/LIPIcs.MFCS.2021.58}, annote = {Keywords: Model checking, linear-time logic, nominal sets} }

Document

**Published in:** LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

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.

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)

Copy BibTex To Clipboard

@InProceedings{urbat_et_al:LIPIcs.CONCUR.2021.4, author = {Urbat, Henning and Hausmann, Daniel and Milius, Stefan and Schr\"{o}der, Lutz}, title = {{Nominal B\"{u}chi Automata with Name Allocation}}, booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)}, pages = {4:1--4:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-203-7}, ISSN = {1868-8969}, year = {2021}, volume = {203}, editor = {Haddad, Serge and Varacca, Daniele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.4}, URN = {urn:nbn:de:0030-drops-143813}, doi = {10.4230/LIPIcs.CONCUR.2021.4}, annote = {Keywords: Data languages, infinite words, nominal sets, inclusion checking} }

Document

**Published in:** LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

The coalgebraic mu-calculus is a generic framework for fixpoint logics with varying branching types that subsumes, besides the standard relational mu-calculus, such diverse logics as the graded mu-calculus, the monotone mu-calculus, the probabilistic mu-calculus, and the alternating-time mu-calculus. In the present work, we give a local model checking algorithm for the coalgebraic mu-calculus using a coalgebraic variant of parity games that runs, under mild assumptions on the complexity of the so-called one-step satisfaction problem, in time p^k where p is a polynomial in the formula and model size and where k is the alternation depth of the formula. We show moreover that under the same assumptions, the model checking problem is in both NP and coNP, improving the complexity in all mentioned non-relational cases. If one-step satisfaction can be solved by means of small finite games, we moreover obtain standard parity games, ensuring quasi-polynomial run time. This applies in particular to the monotone mu-calculus, the alternating-time mu-calculus, and the graded mu-calculus with grades coded in unary.

Daniel Hausmann and Lutz Schröder. Game-Based Local Model Checking for the Coalgebraic mu-Calculus. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{hausmann_et_al:LIPIcs.CONCUR.2019.35, author = {Hausmann, Daniel and Schr\"{o}der, Lutz}, title = {{Game-Based Local Model Checking for the Coalgebraic mu-Calculus}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {35:1--35:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.35}, URN = {urn:nbn:de:0030-drops-109373}, doi = {10.4230/LIPIcs.CONCUR.2019.35}, annote = {Keywords: Model checking, mu-calculus, coalgebraic logic, graded mu-calculus, probabilistic mu-calculus, parity games} }

Document

**Published in:** LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

We present a sound, complete, and optimal single-pass tableau algorithm for the alternation-free mu-calculus. The algorithm supports global caching with intermediate propagation and runs in time 2^O(n). In game-theoretic terms, our algorithm integrates the steps for constructing and solving the Büchi game arising from the input tableau into a single procedure; this is done on-the-fly, i.e. may terminate before the game has been fully constructed. This suggests a slogan to the effect that global caching = game solving on-the-fly. A prototypical implementation shows promising initial results.

Daniel Hausmann, Lutz Schröder, and Christoph Egger. Global Caching for the Alternation-free µ-Calculus. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{hausmann_et_al:LIPIcs.CONCUR.2016.34, author = {Hausmann, Daniel and Schr\"{o}der, Lutz and Egger, Christoph}, title = {{Global Caching for the Alternation-free µ-Calculus}}, booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)}, pages = {34:1--34:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-017-0}, ISSN = {1868-8969}, year = {2016}, volume = {59}, editor = {Desharnais, Jos\'{e}e and Jagadeesan, Radha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.34}, URN = {urn:nbn:de:0030-drops-61724}, doi = {10.4230/LIPIcs.CONCUR.2016.34}, annote = {Keywords: modal logic, fixpoint logic, satisfiability, global caching, coalgebraic logic} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail