2026-07-25T15:15:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6172 2024-03-06T10:38:31Z ddc:004 open_access

Global Caching for the Alternation-free µ-Calculus Hausmann, Daniel Schröder, Lutz Egger, Christoph modal logic fixpoint logic satisfiability global caching coalgebraic logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Daniel Hausmann and Lutz Schröder and Christoph Egger 2016 Is Part Of LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2016.34 urn:nbn:de:0030-drops-61724 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.34 eng https://creativecommons.org/licenses/by/3.0/legalcode