Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2016.34
URN: urn:nbn:de:0030-drops-61724
URL: https://drops.dagstuhl.de/opus/volltexte/2016/6172/
Hausmann, Daniel ; Schröder, Lutz ; Egger, Christoph
Global Caching for the Alternation-free µ-Calculus
| pdf-format: |
|
Abstract
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.
BibTeX - Entry
@InProceedings{hausmann_et_al:LIPIcs:2016:6172,
author = {Daniel Hausmann and Lutz Schr{\"o}der and Christoph Egger},
title = {{Global Caching for the Alternation-free {$mu$}-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 = {Jos{\'e}e Desharnais and Radha Jagadeesan},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6172},
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}
}
| Keywords: | modal logic, fixpoint logic, satisfiability, global caching, coalgebraic logic | |
| Seminar: | 27th International Conference on Concurrency Theory (CONCUR 2016) | |
| Issue date: | 2016 | |
| Date of publication: | 24.08.2016 |
