Filetype PDF | Posted on 25 Jan 2023 | 2 years ago
Authentication
digital resources
170x Filetype PDF File size 0.63 MB Source: johannesmarti.com
1 Succinct Graph Representations of µ-Calculus
2 Formulas
3 Clemens Kupke !
4 University of Strathclyde, Scotland
5 Johannes Marti !
6 University of Amsterdam, The Netherlands
7 Yde Venema !
8 University of Amsterdam, The Netherlands
9 Abstract
10 Manyalgorithmicresults on the modal mu-calculus use representations of formulas such as alternating
11 tree automata or hierarchical equation systems. At closer inspection, these results are not always
12 optimal, since the exact relation between the formula and its representation is not clearly understood.
13 In particular, there has been confusion about the deĄnition of the fundamental notion of the size of
14 a mu-calculus formula.
15 Wepropose the notion of a parity formula as a natural way of representing a mu-calculus formula,
16 and as a yardstick for measuring its complexity. We discuss the close connection of this concept
17 with alternating tree automata, hierarchical equation systems and parity games. We show that
18 well-known size measures for mu-calculus formulas correspond to a parity formula representation of
19 the formula using its syntax tree, subformula graph or closure graph, respectively. Building on work
20 by Bruse, Friedmann & Lange we argue that for optimal complexity results one needs to work with
21 the closure graph, and thus deĄne the size of a formula in terms of its Fischer-Ladner closure. As a
22 new observation, we show that the common assumption of a formula being clean, that is, with every
23 variable bound in at most one subformula, incurs an exponential blow-up of the size of the closure.
24 To realise the optimal upper complexity bound of model checking for all formulas, our main
25 result is to provide a construction of a parity formula that (a) is based on the closure graph of a
26 given formula, (b) preserves the alternation-depth but (c) does not assume the input formula to be
27 clean.
28 2012 ACM Subject ClassiĄcation Theory of computation → Modal and temporal logics; Theory of
29 computation → Logic and veriĄcation
30 Keywords and phrases modal mu-calculus, model checking, alternating tree automata, hierachical
31 equation systems
32 Digital Object IdentiĄer 10.4230/LIPIcs.CVIT.2016.23
33 Related Version This paper is largely based on our technical report [15].
34 Funding Clemens Kupke: Supported by Leverhulme Trust Research Project Grant RPG-2020-232.
35 Johannes Marti: The research of this author has been made possible by a grant from the Dutch
36 Research Council NWO, project nr. 617.001.857.
37 1 Introduction
38 The modal µ-calculus, introduced by Kozen [14] and surveyed in for instance [2, 12, 4, 9],
39 is a logic for describing properties of processes that are modelled by labelled transition
40 systems. It extends the expressive power of propositional modal logic by means of least and
41 greatest Ąxpoint operators. This addition permits the expression of all bisimulation-invariant
42 monadic second order properties of such processes [13]. As a logic, µML has many desirable
43 properties, such as a natural complete axiomatisation [14, 19], uniform interpolation and
© Clemens Kupke, Johannes Marti and Yde Venema;
licensed under Creative Commons License CC-BY 4.0
42nd Conference on Very Important Topics (CVIT 2016).
Editors: John Q. Open and Joan R. Access; Article No.23; pp.23:1Ű23:17
Leibniz International Proceedings in Informatics
Schloss Dagstuhl Ű Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
23:2 Succinct Graph Representations of µ-Calculus Formulas
44 other interesting model-theoretical properties [8, 11], and a complete cut-free proof system [1].
45 Here we will be interested in some of its computational properties.
46 The µ-calculus is generally regarded as a universal speciĄcation language for reactive
47 systems, since it embeds most other logics that are used for this purpose, such as ltl, ctl,
∗
48 ctl and pdl. Given this status, the computational complexity of its model checking and
49 satisĄability problems is of central importance. While the satisĄability problem has been
50 shown to be exptime-complete [10] already thirty years ago, the precise complexity of
51 its model checking problem turned out to be a challenging problem. A breakthrough was
52 obtained by Calude et alii [7] who gave a quasi-polynomial algorithm for deciding parity
53 games; since model checking for the modal µ-calculus can be determined by such games, this
54 indicates a quasi-polynomial upper bound of the complexity of the model checking problem.
55 Generally, to determine the complexity of a proposed algorithm operating on µ-calculus
56 formulas, one needs sensible measures of the complexity of the formula that is (part of)
57 the input to the algorithm; the most important of these concern size and alternation depth.
58 Different notions of size have been used, depending on how precisely formulas are represented
59 in the input. Standard size measures include: (1) length, corresponding to a representation of
60 the formula as a string or syntax tree; (2) subformula size, corresponding to a representation of
61 the formula as the directed acyclic graph of its subformulas; and (3) closure size, corresponding
62 to a similar representation of a formula via its (Fischer-Ladner) closure.
63 The choice between these representations is non-trivial because the subformula size
64 of a formula may be exponentially smaller than its length, and, as was shown by Bruse,
65 Friedmann & Lange [6], its closure size may be exponentially smaller than its subformula size.
66 Consequently, complexity results about the µ-calculus may be suboptimal when expressed
67 in terms of subformula size, in the sense that a stronger version of the result holds when
68 formulated in terms of closure size. In other words, it is desirable to design algorithms that
69 operate on a representation of a formula that is based on its closure.
70 At closer inspection it turns out that generally, the literature on algorithmic aspects of the
71 µ-calculus is crystal clear in terms of the structures on which the algorithms operate, but less
72 so on the precise way in which these structures represent formulas. As a consequence, when
73 formulated in terms of the actual formulas, complexity results as given may be suboptimal or
74 somewhat fuzzy. Our long-term goal is to study the representation of µ-calculus formulas in
75 more detail, and to develop a framework in which various approaches can easily be compared,
76 and in which complexity results can be formulated and proved optimally and unambiguously.
77 As a starting point, we note that in the literature different frameworks are used to
78 represent µ-calculus formulas. The parity games that feature in model checking algorithms
79 are usually based on an arena which is some kind of Cartesian product of a graph that
80 represents the formula with the model where this formula is evaluated. Other prominent ways
81 to represent formulas are (alternating) tree automata and (hierarchical) equation systems; as
82 we shall see further on, in these cases we can think of the structures that represent formulas
83 in graph-theoretic terms as well. In all cases then, the mathematically fundamental structure
84 representing a formula is a graph, whose nodes are labelled with logical connectives or
85 atomic formulas, and with priorities that are used to determine some winning or acceptance
86 condition. The graph itself can be based on the syntax tree, the subformula dag or the
87 closure graph of the formula that it represents.
88 Wemakethis fundamental labelled graph structure explicit and call the resulting concept
89 a parity formula.1 Intuitively, parity formulas generalise standard formulas by dropping the
1 Parity formulas are almost the same structures as the alternating binary tree automata of Emerson &
C. Kupke, J. Marti and Y. Venema 23:3
90 requirement that the underlying graph structure of the formula is a tree with back edges,
91 and adding an explicit parity acceptance condition. A good way to think about a parity
92 formula is as the formula component of a model checking game. As we shall see below,
93 parity formulas are closely related to alternating tree automata and hierarchical equation
94 systems. Compared to these however, parity formulas have a very simple mathematical
95 structure, which allows for a straightforward and unambiguous deĄnition of its size and its
96 index (alternation depth).
97 The explicit introduction of this notion is not a goal in itself. We intend to use it as a
98 tool to analyse some underexposed sides of the theory of the modal µ-calculus. In this paper
99 we discuss some key constructions turning standard formulas into parity formulas and vice
100 versa. Along the way we make two observations that we consider the key contributions of
101 this paper:
102 1) A common assumption in the literature on the µ-calculus is that one may assume,
103 without loss of generality, that formulas are clean or well-named, in the sense that bound
104 variables are disjoint from free variables, and each bound variable determines a unique
105 subformula. In Proposition 10 we show that this assumption may lead to an exponential
106 blow-up in terms of closure-size. This means that, if one is interested in optimal complexity
107 results, one should not assume the input formula to be clean.
108 2) To the best of our knowledge, all representations of µ-calculus formulas known from
109 the literature, are suboptimal in one way or another: they are based on the subformula dag,
110 they presuppose cleanness, or they use a priority function which yields an unnecessarily big
111 index. The main result of our paper, Theorem 12, concerns a construction that provides, for
112 every µ-calculus formula, an equivalent parity formula that is based on its closure graph,
113 and has an index that matches its alternation depth. The fact that we do not assume the
2
114 input formula to be clean makes our proof non-trivial.
115 Because of Proposition 10, Theorem 12 has an impact on the quasi-polynomial time
116 complexity of the model checking problem for the modal µ-calculus. If one wants to formulate
117 an optimal version of this complexity result, by the observations of Bruse, Friedmann &
118 Lange [6] one needs to measure the formula in terms of closure-size; but then Theorem 12 is
119 needed to ensure that the result applies to all formulas, not just to the ones that are clean.
120 2 Preliminaries
121 In this section we brieĆy review the syntax and semantics of the modal µ-calculus.
122 Syntax It will be convenient to assume that µ-calculus formulas are in negation normal
123 form. That is, the formulas of the modal µ-calculus µML are given by the following grammar:
124 µML ∋ φ ::= p ♣ p ♣ ⊥ ♣ ⊤ ♣ (φ∨φ) ♣ (φ∧φ) ♣ ✸φ ♣ ✷φ ♣ µxφ ♣ νxφ,
125 where p,x are variables, and the formation of the formulas µxφ and νxφ is subject to the
126 constraint that φ is positive in x, i.e., there are no occurrences of x in φ. Elements of µML
127 will be called µ-calculus formulas or standard formulas. Formulas of the form µx:φ or νx:φ
128 will be called Ąxpoint formulas. We deĄne Lit(Q) := ¶p,p ♣ p ∈ Q♢ as the set of literals over
129 Q, and At(Q) := ¶⊥,⊤♢∪Lit(Q) as the set of atomic formulas over Q. We will associate µ
Jutla [10] and as the version of WilkeŠs alternating tree automata where the transition conditions are
basic formulas, i.e., contain at most one logical connective [20, 12].
2 Proof details, which we could not include here for lack of space, can be found in the technical report [15].
CVIT 2016
23:4 Succinct Graph Representations of µ-Calculus Formulas
130 and ν with the odd and even numbers, respectively, and for η ∈ ¶µ,ν♢ deĄne η by putting
131 µ:=ν and ν := µ. The notion of subformula is deĄned as usual; we write φ P ψ if φ is a
132 subformula of ψ, and deĄne Sfor(ψ) as the set of subformulas of ψ.
133 Weuse standard terminology related to the binding of variables. We write BV(ξ) and
134 FV(ξ) for, respectively, the set of bound and free variables of a formula ξ. A formula ξ is
135 tidy3 if FV(ξ) ∩ BV(ξ) = ∅. We Ąx a set Q of proposition letters and let µML(Q) denote
136 the set of formulas ξ with FV(ξ) ⊆ Q. We let φ[ψ/x] denote the formula φ, with every
137 free occurrence of x replaced by the formula ψ; we will make sure that we only apply this
138 substitution operation if ψ is free for x in φ (meaning that no free variable of ψ gets bound
139 after substituting). This saves us from involving alphabetical variants when substituting.
140 The unfolding of a formula ηx:χ is the formula χ[ηx:χ/x]; this formula is tidy if χ is so.
141 Semantics The modal µ-calculus is interpreted over Kripke structures. A (Kripke) model is
142 a triple S = (S,R,V) where S is the set of states or points of S, R ⊆ S ×S is its accessibility
143 relation, and V : Q → P(S) its valuation. A pointed model is a pair (S,s) where s is a
S
144 designated state of S. Inductively we deĄne the meaning [[φ]] ⊆ S of a formula φ ∈ µML(Q)
145 in a model S as follows:
[[p]]S := V(p) [[p]]S := S\V(p)
[[⊥]]S := ∅ [[⊤]]S := S
146 S S S S S S
[[φ ∨ ψ]] := [[φ]] ∪[[ψ]] [[φ ∧ ψ]] := [[φ]] ∩[[ψ]]
[[✸φ]]S := ¶s∈S♣R[s]∩[[φ]]S ̸= ∅♢ [[✷φ]]S := ¶s∈S♣R[s]⊆[[φ]]S♢
S T S[x7→U] S S S[x7→U]
[[µx:φ]] := ¶U ⊆S ♣ [[φ]] ⊆U♢ [[νx:φ]] := ¶U ⊆S ♣ [[φ]] ⊇U♢:
147 Here S[x 7→ U] := (S,R,V[x 7→ U] where V[x 7→ U] is the Q∪¶x♢-valuation mapping x to
S
148 U and any p ̸= x to V (p). If a state s ∈ S belongs to the set [[φ]] , we write S,s ⊩ φ, and say
149 that s satisĄes φ.
150 Complexity measures The size of a formula ξ ∈ µML can be measured in at least three
ℓ
151 different ways. First, its length ♣ξ♣ is deĄned as the number of symbols that occur in ξ.
s
152 Second, we deĄne its subformula size ♣ξ♣ := ♣Sfor(ξ)♣ as the number of distinct subformulas
153 of ξ.
154 Third, we can measure the size of ξ by counting the number of formulas in its (Fischer-
155 Ladner) closure. We need some notation and terminology here, where we assume that ξ is
156 tidy. The set Clos0(ξ) is deĄned by the following case distinction:
Clos0(φ) := ∅ if φ ∈ At(Q)
Clos (φ ⊙φ ) := ¶φ ,φ ♢ where ⊙ ∈ ¶∧,∨♢
157 0 0 1 0 1
Clos0(♡φ) := ¶φ♢ where ♡ ∈ ¶✸,✷♢
Clos0(ηx:φ) := ¶φ[ηx:φ/x]♢ where η ∈ ¶µ,ν♢:
158 We write ξ → φ if φ ∈ Clos (ξ) and call → the trace relation on µML. We let ↠
C 0 C C
159 denote the reĆexive and transitive closure of → , and deĄne the closure of ξ as the set
C
160 Clos(ξ) := ¶φ ♣ ξ ↠ φ♢. The closure graph of ξ is the directed graph (Clos(ξ),→ ). The
C C
c c
161 closure size ♣ξ♣ of ξ is given as ♣ξ♣ := ♣Clos(ξ)♣.
3 In the literature, some authors make a distinction between proposition letters (which can only occur
freely in a formula), and propositional variables, which can be bound. Our tidy formulas correspond to
sentences in this approach, that is, formulas without free variables.
no reviews yet
Please Login to review.
