The μ-calculus can be viewed as essentially the "ultimate" program logic, as it expressively subsumes all propositional program logics, including dynamic logics, process logics, and temporal logics. It is known that the satisfiability problem for the μ-calculus is EXPTIME-complete. This upper bound, however, is known for a version of the logic that has only forward modalities, which express weakest preconditions, but not backward modalities, which express strongest postconditions. Our main result in this paper is an exponential time upper bound for the satisfiability problem of the μ-calculus with both forward and backward modalities. To get this result we develop a theory of two-way alternating automata on infinite trees.
CITATION STYLE
Vardi, M. Y. (1998). Reasoning about the past with two-way automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1443 LNCS, pp. 628–641). Springer Verlag. https://doi.org/10.1007/bfb0055090
Mendeley helps you to discover research relevant for your work.