=Paper=
{{Paper
|id=Vol-1720/short4
|storemode=property
|title=Relating Paths in Transition Systems: the Fall of the Modal mu-Calculus
|pdfUrl=https://ceur-ws.org/Vol-1720/short4.pdf
|volume=Vol-1720
|authors=Catalin Dima,Bastien Maubert,Sophie Pinchinat
|dblpUrl=https://dblp.org/rec/conf/ictcs/DimaMP16
}}
==Relating Paths in Transition Systems: the Fall of the Modal mu-Calculus==
https://ceur-ws.org/Vol-1720/short4.pdf
Relating paths in transition systems:
the fall of the modal mu-calculus
Catalin Dima1 , Bastien Maubert2 , and Sophie Pinchinat3
1
Université Paris Est, LACL, UPEC, Créteil, France.
dima@u-pec.fr
2
Università degli Studi di Napoli Federico II
bastien.maubert@gmail.com
3
Université de Rennes 1, IRISA, Rennes, France.
sophie.pinchinat@irisa.fr
This is an extended abstract of a paper presented at MFCS 2015 [11].
Monadic second-order logic (MSO) is considered as a standard for compar-
ing expressiveness of logics of programs. Ground-breaking results concerning
expressiveness and decidability of MSO on infinite graphs were obtained first on
“freely-generated” structures (words, trees, tree-like structures, etc.) [28,30], then
on “non-free” structures like grids [18] or infinite graphs generated by regularity-
preserving transformations [10,8]. In all the above settings, the syntax of MSO
utilizes one or more binary relation symbols which are interpreted using the
binary edge relations of the graph structure. Additionally, much attention has
been brought to the study of enrichments of MSO with unary predicate symbols
or with the “equal level” binary predicate (MSOeql ) [12,27].
For many of these settings, MSO has been compared with automata and with
modal logics. Standard results on trees are Rabin’s expressiveness equivalence
between MSO with two successors and automata on binary trees [23], and Janin
and Walukiewicz’s result [16] showing that the bisimulation-invariant fragment of
MSO interpreted over transition coincides with the µ-calculus. Notable exceptions
to the classical trilogy between MSO, modal logics and automata are MSO on
infinite partial orders – where only partial results are known [5,9,25] – and MSOeql –
where, similarly, only partial results are known [27].
More recently, there has been an increased interest in the expressiveness and
decidability of logics defined on structures in which two “orthogonal” relations
are considered: the so-called temporal epistemic (multi-agent) logics [13], which
combine time-passage relations and epistemic relations on the histories of the
system. Time-passage relations classically represent the evolution of the sys-
tem, while each epistemic relation captures some agent’s partial observation of
the system by relating indistinguishable histories. They allow to reason about
what these agents know about the state of the system along its executions. We
may incidentally identify now an important sub-domain in verification which
Copyright c by the paper’s authors. Copying permitted for private and academic pur-
poses.
V. Biló, A. Caruso (Eds.): ICTCS 2016, Proceedings of the 17th Italian Conference on
Theoretical Computer Science, 73100 Lecce, Italy, September 7–9 2016, pp. 240–244
published in CEUR Workshop Proceedins Vol-1720 at http://ceur-ws.org/Vol-1720
Relating paths in transition systems: the fall of the modal mu-calculus 241
is concerned with the expressivity, decidability and axiomatizability of logics of
knowledge and time [15,6,29,13,14,17].
The natural question that arises regarding logics of agents that combine
time and knowledge is whether a similar trilogy can be established or not. In
particular, does there exist a natural extension of MSO, of the µ-calculus, and
of tree automata for the temporal epistemic framework, and how would they
compare? To the best of our knowledge, these questions remain open. Only
partial results exist on relations between some extensions of MSO, µ-calculus,
tree automata and other logics of knowledge and time [27,26,29,20].
The first observation is that appropriate extensions of MSO, of the µ-calculus
and of tree automata would rely on two sorts of binary relations: those related to
the behaviour of the system and those related to epistemic features. While the
temporal part of these logics naturally refer to a tree-like structure, the epistemic
part requires, in order to model e.g. powerful agents that remember the whole
past, to consider binary relations defined on histories. The models of such an
extension of MSO neither are tree-like structures, nor grid-like structures, nor
graphs within the Caucal hierarchy. The proposals in this direction that we know
about are [29,26,20] and [1]. [29] mentions an encoding of LTL with knowledge
into Chain Logic with equal-level predicate, which is a fragment of MSOeql . [26]
introduces the epistemic µ-calculus and studies its model-checking problem. [1]
studies an extension of the epistemic µ-calculus, and [20] proposes a generalization
of tree automata, called jumping tree automata, which is suited to the study of
temporal epistemic logics.
In this work, we develop a general setting in which models are transition
systems, i.e. directed graphs with atomic propositions, or predicates, on ver-
tices/states and labels on edges/transitions, together with a binary relation over
their finite executions, also called paths or histories. Such relations are called
path relations, and their definition is general enough to capture all indistinguisha-
bility relations considered in temporal epistemic logics, and more. We propose
extensions of MSO and of the µ-calculus, respectively called the monadic second
order logic with path relation and the jumping µ-calculus.
MSO with path relation is an extension of MSO interpreted over unfoldings of
transition systems equipped with a path relation, so that a first-order variable x
refers to a node in the tree-unfolding of a transition system, i.e. a finite execution
(or path, or history). The syntax is that of MSO on graphs with an additional
special binary relation symbol ;. A formula of the form x ; y holds in a
transition system if the path represented by x is related to the one represented
by y, according to the binary relation over paths that equips the system.
The jumping µ-calculus is a generalization of the epistemic µ-calculus defined
in [26]: it is also evaluated on tree-unfoldings of transition systems, and it features
a jumping modality ; whose semantics relies on the path relation that equips the
system. In case the path relation is seen as modelling histories’ indistinguishability
for some agent, this modality coincides with the classic knowledge operator K
for this agent.
242 Catalin Dima, Bastien Maubert, and Sophie Pinchinat
As in the classic setting of [16], definability in the jumping µ-calculus entails
definability in MSO with path relation. It is the converse statement that we
explore, that is the expressive completeness of jumping µ-calculus w.r.t. (the
bisimilar invariant fragment of) MSO with path relation.
We first show that, just like alternating tree automata are equivalent to the
µ-calculus, the jumping tree automata recently defined in [20] are equivalent to
the jumping µ-calculus, and the two-way translation does not depend on the a
priori fixed path relation. We then address, like in [16], the question whether
for bisimulation-closed classes of models, definability in MSO with path relation
implies definability in the jumping µ-calculus. A crucial parameter in this question
is the complexity of the path relation one considers. We recall that, given a finite
alphabet Σ, a binary relation over Σ ∗ is regular if there is a finite state automaton
with two tapes on which it progresses synchronously (a synchronous transducer)
that accepts a pair of words over Σ if, and only if, it is in the relation (see [2]
for details). An example is the epistemic relation of an agent with synchronous
perfect recall [3,4]. A relation over Σ ∗ is recognizable if there is a finite-state word
automaton over Σ ∪ {#}, where # is a special separator symbol, that accepts
precisely words of the form w#w0 where (w, w0 ) is in the relation (again refer to
[2] for details). For example, epistemic relations of agents whose memory can be
represented by finite state machines are recognizable relations (see [19]).
We establish the following results:
Theorem 1. For any recognizable path relation, the jumping µ-calculus is ex-
pressive complete with respect to MSO with path relation.
Theorem 2. There are regular binary relations for which the jumping µ-calculus
is not expressive complete with respect to MSO with path relation.
Theorem 1 follows simply from the fact that, since recognizable relations are
MSO definable, both our extensions of MSO and the µ-calculus collapse to the
classic MSO and µ-calculus, respectively, when the path relation is recognizable.
Concerning transition systems with bounded branching degree, we obtain in
addition that the jumping µ-calculus with recognizable path relation is at most
exponentially more succinct than the µ-calculus, while its satisfiability problem
is also E x p t i m e-complete. These results rely on the effective translation of
jumping tree automata equipped with recognizable path relations into alternating
two-way tree automata [20].
To establish Theorem 2 we consider the case of the so-called synchronous
perfect recall relation over paths [24,22], which is regular. We prove that the class
of reachability games with imperfect information and perfect recall (with a fixed
number of observations and actions) where the first player wins cannot be defined
in the jumping µ-calculus, while being closed by bisimulation and definable in
our extension of MSO. The proof heavily relies on the equivalence between the
jumping µ-calculus and jumping automata, on which we exploit the “pigeon-hole
principle”, as well as on the use of unobservable winning conditions. Indeed, we
prove that if winning conditions are assumed to be observable, then the class of
Relating paths in transition systems: the fall of the modal mu-calculus 243
imperfect-information (either reachability or parity) games where the first player
wins is definable in the jumping µ-calculus.
Our expressivity incompleteness result has several impacts.
First, we obtain that the class of jumping tree automata is not closed un-
der projection. Indeed, the (bisimulation-closed) second-order-quantification-free
fragment of MSO with path relation can be embedded into jumping tree au-
tomata. Their closure under projection would therefore imply that they coincide
with the full (bisimilar invariant) MSO with path relation, which contradicts our
expressivity incompleteness result.
Regarding logics of programs, there has been some interest in comparing
alternating-time temporal logics with fix-point logics. When agents have per-
fect information, the µ-calculus subsumes these logics (see for instance [21]).
For imperfect information, our results show that the picture changes: because
alternating-time temporal logics with imperfect information can express the
existence of winning strategies in reachability games with imperfect informa-
tion, Theorem 2 reveals that the powerful jumping µ-calculus does not subsume
alternating-time temporal logics with imperfect information when we consider
players with perfect recall.
We also believe that our incompleteness result impacts the axiomatizability of
alternating-time temporal logics with imperfect information: the impossibility to
express the existence of a winning strategy in reachability games with imperfect
information and perfect recall in the jumping µ-calculus strongly suggests the
absence of fix-point axioms for certain alternating temporal logics.
References
1. R. Alur, P. Černý, and S. Chaudhuri. Model checking on trees with path equiva-
lences. In TACAS’07, pages 664–678. Springer, 2007.
2. J. Berstel. Transductions and context-free languages, volume 4. Teubner Stuttgart,
1979.
3. D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, and Thomas A. Henzinger.
Strategy construction for parity games with imperfect information. Inf. Comput.,
208(10):1206–1220, 2010.
4. D. Berwanger and L. Kaiser. Information tracking in games on graphs. Journal of
Logic, Language and Information, 19(4):395–412, 2010.
5. B. Bollig and M. Leucker. Message-passing automata are expressively equivalent
to EMSO logic. Theor. Comput. Sci., 358(2-3):150–172, 2006.
6. N. Bulling, J. Dix, and W. Jamroga. Model checking logics of strategic ability:
Complexity. In M. Dastani, K. V. Hindriks, and J.-J. C. Meyer, editors, Specification
and Verification of Multi-Agent Systems, pages 125–160. Springer, 2010.
7. N. Bulling and W. Jamroga. Alternating epistemic mu-calculus. In Proceedings of
IJCAI’2011, pages 109–114. IJCAI/AAAI, 2011.
8. D. Caucal. On infinite transition graphs having a decidable monadic theory. Theor.
Comput. Sci., 290(1):79–115, 2003.
9. B. Courcelle and I. Durand. Automata for the verification of monadic second-order
graph properties. J. Applied Logic, 10(4):368–409, 2012.
244 Catalin Dima, Bastien Maubert, and Sophie Pinchinat
10. B. Courcelle and J. Engelfriet. Graph Structure and Monadic Second-Order Logic
- A Language-Theoretic Approach. Cambridge University Press, 2012.
11. Catalin Dima, Bastien Maubert, and Sophie Pinchinat. Relating paths in transition
systems: The fall of the modal mu-calculus. In Mathematical Foundations of
Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy,
August 24-28, 2015, Proceedings, Part I, pages 179–191, 2015.
12. C. C. Elgot and M. O. Rabin. Decidability and undecidability of extensions of
second (first) order theory of (generalized) successor. J. Symb. Log., 31(2):169–181,
1966.
13. R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning about knowledge. The
MIT Press, 2004.
14. J. Y. Halpern, R. van der Meyden, and M. Y. Vardi. Complete Axiomatizations for
Reasoning about Knowledge and Time. SIAM J. Comput., 33(3):674–703, 2004.
15. J. Y. Halpern and M. Y. Vardi. The complexity of reasoning about knowledge and
time. 1. Lower bounds. J. Comp. Sys. Sci., 38(1):195–237, 1989.
16. D. Janin and I. Walukiewicz. On the expressive completeness of the propositional
mu-calculus with respect to monadic second order logic. In Proceedings of CON-
CUR’96, pages 263–277. Springer, 1996.
17. A. Lomuscio and Fr. Raimondi. Mcmas: A model checker for multi-agent systems.
In Proceedings of TACAS’2006, volume 3920 of LNCS, pages 450–454, 2006.
18. O. Matz, N. Schweikardt, and W. Thomas. The monadic quantifier alternation
hierarchy over grids and graphs. Inf. Comput., 179(2):356–383, 2002.
19. B. Maubert. Logical foundations of games with imperfect information: uniform
strategies. PhD thesis, Université de Rennes 1, 2014.
20. B. Maubert and S. Pinchinat. Jumping automata for uniform strategies. In
Proceedings of FSTTCS’13, pages 287–298, 2013.
21. S. Pinchinat. A generic constructive solution for concurrent games with expres-
sive constraints on strategies. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo
Higashino, and Yoshio Okamura, editors, 5th International Symposium on Auto-
mated Technology for Verification and Analysis, volume 4762 of Lecture Notes in
Computer Science, pages 253–267. Springer-Verlag, 2007.
22. B. Puchala. Asynchronous omega-regular games with partial information. In
Proceedings of MFCS’2010, pages 592–603, 2010.
23. M. O. Rabin. Decidability of second-order theories and automata on infinite trees.
Transactions of the American Mathematical Society, pages 1–35, 1969.
24. J.-F. Raskin, K. Chatterjee, L. Doyen, and Th. A. Henzinger. Algorithms for
omega-regular games with imperfect information. LMCS, 3(3), 2007.
25. F. Reiter. Distributed graph automata. CoRR, abs/1404.6503, 2014.
26. N. V. Shilov and N. O. Garanina. Combining knowledge and fixpoints. Tech-
nical Report Preprint n.98, http://www.iis.nsk.su/files/preprints/098.pdf,
A.P. Ershov Institute of Informatics Systems, Novosibirsk, 2002.
27. W. Thomas. Infinite trees and automaton-definable relations over omega-words.
Theor. Comput. Sci., 103(1):143–159, 1992.
28. W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa,
editors, Handbook of Formal Languages, volume 3, Beyond Words, pages 389–455.
Springer Verlag, 1997.
29. R. van der Meyden and N. Shilov. Model checking knowledge and time in systems
with perfect recall (extended abstract). In Proceedings of FSTTCS’99, volume 1738
of LNCS, pages 432–445, 1999.
30. I. Walukiewicz. Monadic second-order logic on tree-like structures. Theor. Comput.
Sci., 275(1-2):311–346, 2002.