Abstract
In this paper we develop a new exponential algorithm for model-checking infinite sequential processes, including context-free processes, pushdown processes, and regular graphs, that decides the full modal mu-calculus. Whereas the actual model checking algorithm results from considering conditional semantics together with backtracking caused by alternation, the corresponding correctness proof requires a stronger framework, which uses dynamic environments modelled by finite-state automata.
Cite
CITATION STYLE
Burkart, O., & Steffen, B. (1997). Model checking the pull modal mu-calculus for infinite sequential processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1256, pp. 419–429). Springer Verlag. https://doi.org/10.1007/3-540-63165-8_198
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
