This is an extended abstract of a paper presented at MFCS 2015 [11]. Monadic second-order logic (MSO) is considered as a standard for comparing 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 regularitypreserving 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 MSOeqlwhere, 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 system, 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 purposes.
is concerned with the expressivity, decidability and axiomatizability of logics of
knowledge and time [
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 [
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 [
In this work, we develop a general setting in which models are transition systems, i.e. directed graphs with atomic propositions, or predicates, on vertices/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 indistinguishability 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 [
As in the classic setting of [
We first show that, just like alternating tree automata are equivalent to the
μ-calculus, the jumping tree automata recently defined in [
We establish the following results: Theorem 1. For any recognizable path relation, the jumping μ-calculus is expressive 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 [
To establish Theorem 2 we consider the case of the so-called synchronous
perfect recall relation over paths [
Our expressivity incompleteness result has several impacts.
First, we obtain that the class of jumping tree automata is not closed under projection. Indeed, the (bisimulation-closed) second-order-quantification-free fragment of MSO with path relation can be embedded into jumping tree automata. 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
perfect information, the μ-calculus subsumes these logics (see for instance [
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.