Relating Paths in Transition Systems: The Fall of the Modal Mil-Calculus

摘要

We revisit Janin and Walukiewicz's classic result on the expressive completeness of the modal mu-calculus with respect to Monadic Second Order Logic (MSO), which is where the mu-calculus corresponds precisely to the fragment of MSO that is invariant under bisimulation. We show that adding binary relations over finite paths in the picture may alter the situation. We consider a general setting where finite paths of transition systems are linked by means of a fixed binary relation. This setting gives rise to natural extensions of MSO and the mu-calculus, that we call the MSO with paths relation and the jumping mu-calculus, the expressivities of which we aim at comparing. We first show that "bounded-memory" binary relations bring about no additional expressivity to either of the two logics, and thus preserve expressive completeness. In contrast, we show that for a natural, classic "infinite-memory" binary relation stemming from games with imperfect information, the existence of a winning strategy in such games, though expressible in the bisimulation-invariant fragment of MSO with paths relation, cannot be expressed in the jumping mu-calculus. Expressive completeness thus fails for this relation. These results crucially rely on our observation that the jumping mu-calculus has a tree automata counterpart: the jumping tree automata, hence the name of the jumping mu-calculus. We also prove that for observable winning conditions, the existence of winning strategies in games with imperfect information is expressible in the jumping mu-calculus. Finally, we derive from our main theorem that jumping automata cannot be projected, and ATL with imperfect information does not admit expansion laws.