Abstract
We revisit Janin and Walukiewicz’s classic result on the expressive completeness of the modal mu-calculus w.r.t. MSO, when transition systems are equipped with a binary relation over paths. We obtain two natural extensions of MSO and the mu-calculus: MSO with path relation and the jumping mu-calculus. While “bounded-memory” binary relations bring about no extra expressivity to either of the two logics, “unbounded-memory” binary relations make the bisimulation-invariant fragment of MSO with path relation more expressive than the jumping mu-calculus: the existence of winning strategies in games with imperfectinformation inhabits the gap.
Cite
CITATION STYLE
Dima, C., Maubert, B., & Pinchinat, S. (2015). Relating paths in transition systems: The fall of the modal mu-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9234, pp. 179–191). Springer Verlag. https://doi.org/10.1007/978-3-662-48057-1_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
