Model Checking the Full Modal Mu-Calculus for Infinite Sequential Processes

Olaf Burkart^{∗} LFCS, University of Edinburgh JCMB, King’s Buildings Edinburgh EH9 3JZ, UK

<olaf@dcs.ed.ac.uk>

Bernhard Steffen FMI, Universität Passau Innstraße 33 94032 Passau, Germany

<steffen@fmi.uni-passau.de>

Infinite-state systems, context-free processes, pushdown processes, regular graphs, modal mu-calculus, model-checking.

Abstract

In this paper we develop a new elementary algorithm for model-checking infinite sequential processes, including context-free processes, pushdown processes, and regular graphs, that decides the full modal mu-calculus. Whereas the actual model checking algorithm results from considering conditional semantics together with backtracking caused by alternation, the corresponding correctness proof requires a stronger framework, which uses dynamic environments modelled by finite-state automata.

1 Introduction

Over the past decade model-checking has emerged as a powerful tool for the automatic analysis of concurrent systems. Whereas model-checking for finite-state systems is nowadays well-established, the theory for infinite systems is a current research topic (cf. [Esp96]). Since even weak branching time logics are undecidable for infinite-state systems incorporating parallel operators [Esp94, EK95], much work has focused on the verification of sequential processes. The strongest results obtained so far show the decidability of monadic second order logic (MSOL) for the infinite binary tree [Rab69], pushdown transition graphs [MS85], regular graphs [Cou90], and rational restricted recognizable graphs [Cau96]. However, all decision procedures are non-elementary and thus not applicable to practical problems. Moreover, MSOL is usually too expressive, since it allows to distinguish even bisimilar models. For these reasons, the modal mu-calculus, a powerful temporal logic combining modal operators with least and greatest fixpoints, is seen as an attractive alternative for specifying behavioural properties. Choosing the modal mu-calculus, we do not even loose expressiveness wrt. bisimulation semantics, since recently, this logic was identified as the bisimulation closed fragment of MSOL [JW96].

∗This work was supported during my stay at IRISA by the European Community under HCM grant ERBCHBGCT 920017, and during my stay at the LFCS by the DAAD under grant D/95/14834 of the NATO science committee.

The model-checking problem for sequential processes and the modal mu-calculus was first considered in [BS92]. The authors developed an iterative model-checking algorithm that decides the alternation-free part of the modal μ-calculus for context-free processes based on a conditional formulation of the semantics of μ-formulas. Moreover, in [HS94] it is shown how this can be done using tableaux-based techniques, allowing local model checking. Finally, the approach was also extended to the strictly larger classes of pushdown processes [BS95] and regular graphs [BQ96]. Since alternation of fixpoints gives, however, rise to a strict hierarchy [Bra96] the problem of model-checking the full modal mu-calculus has still been open. Only recently, Walukiewicz presented a first elementary modelchecking algorithm for pushdown processes based on games [Wal96].

In this paper we develop an alternative algorithm which, essentially, arises as a combination of extending the standard iterative model-checking techniques with conditional reasoning, in order to capture sequential model structures in an alternation-free setting [BS92, BS95, BQ96], and the observation that alternating fixpoints require some kind of backtracking, as it is known from regular model checking (cf. e.g. [CKS92]).

Whereas the actual model checker results directly from this combination, the corresponding correctness proof requires a stronger framework, which uses dynamic environments. In contrast to the “standard” assertions, which suffice algorithmically, dynamic environments also explicitly model valuations of variables that occur free in the actual fixpoint computation. This explicit treatment is necessary in order to establish the link between the result of the fixpoint iteration and the semantics of the full modal mu-calculus.

Fortunately, all this additional complexity is only required for the proof and need not be considered for an implementation. In fact, the actual algorithm can be implemented on top of the algorithms of [BS92, BS95, BQ96] covering the alternation-free case. Taking |C| as the number of transitions, and |Q| as the branching degree in the finite sequential process representation, as well as |Φ| as the size of the formula, and ad as the alternation depth of the formula under consideration, the overall complexity^{1} is

O( |Φ| ∗ (|Q| ∗ |C|)^{ad(Φ)+1} ∗ 2^{|Φ|∗(ad(Φ)+|Q|)} ).

The plan of the paper is now as follows. The next section describes the class of processes we will consider, and presents the full modal mu-calculus. Subsequently, we develop our model-checking algorithm which is proved to be correct in Section 4. The final section contains our conclusions and directions for future research.

1In this paper we neglect the optimization of [LBC^{+}94] which exploits monotonicity arguments and would reduce ad(Φ) to ad(Φ)/2.

2 Processes and Specifications

Infinite sequential processes comprise context-free processes, pushdown processes, and regular graphs. In this paper we will mainly concentrate on the model-checking problem for context-free processes, as the extension to pushdown processes, respectively regular graphs, can be obtained following the lines of [BS95], respectively [BQ96].

2.1 Context-Free Processes

As usual, we consider labelled transition graphs as models for the behaviour of concurrent systems, since they allow to represent the underlying interleaving semantics of many process calculi.

Definition 2.1 A labelled transition graph is a triple T = (S, Act, →) where S is the set of states, Act is the set of transition labels (or actions), and → ⊆ S × Act × S is the transition relation.

In particular, we are interested in classes of infinite transition graphs which can be finitely represented by labelled rewrite systems.

Definition 2.2 A labelled rewrite system is a triple R = (V, Act, R) where V is an alphabet, Act is a set of labels, and R ⊆ V^{∗} × Act × V^{∗} is a finite set of rewrite rules. If the rewrite rules are of the form R ⊆ V × Act × V^{∗} the rewrite system is called alphabetic.

In the remainder of the paper, a rewrite rule (u, a, v) ∈ R is also written as u →^{a} v. Moreover, we will denote a rewrite system simply by R if V and Act are clear from the context. In general, rewrite systems are used to define a rewrite relation on words of V^{∗} where a rewrite rule may be applied at any position. The technical development of this paper concentrates on rewritings of the following restricted form.

Definition 2.3 Let R = (V, Act, R) be a rewrite system. Then the prefix rewriting relation of R is defined by

⟼_{R} =_{df} { (uw, a, vw) | (u →^{a} v) ∈ R, w ∈ V^{∗} },

and the labelled transition graph T_{R} =_{df} (V^{∗}, Act, ⟼_{R}) is called the prefix transition graph of R. By abuse of notation, we will henceforth write uw →^{a} vw instead of uw ⟼_{R}^{a} vw.

An alphabetic rewrite system which is interpreted wrt. prefix rewriting is called a context-free system, and a context-free process is then the rooted prefix transition graph of a context-free system. Note that the states of a context-free process are words over V, and we will henceforth use lower greek letters α, β, … to denote them. One standard example for a context-free process is the prefix transition graph of C_{ex} = { A →^{a} AB, A →^{b} ϵ, B →^{b} ϵ } rooted at A. According to the prefix rewriting defined above the variable A generates the labelled transition graph of Figure 1.

Figure 1: The prefix transition graph for the alphabetic rewrite system C_{ex}.

2.2 The Modal μ-Calculus

Nowadays it is widely accepted that system properties can conveniently be expressed by temporal logic formulas. Particularly, the modal μ-calculus as introduced by Kozen [Koz83] is a powerful branching time logic. It combines standard modal logic with least and greatest fixpoint operators which allows to express very complex temporal properties within this formalism. Due to its expressiveness and its conciseness the μ-calculus can be regarded as the “assembly language” of temporal logics. Formulas of the μ-calculus, given in positive form, are defined by the following grammar

Φ ::= tt | ff | X | Φ ∨ Φ | Φ ∧ Φ | [a]Φ | ⟨a⟩Φ | μX.Φ | νX.Φ

where X ranges over a (countable) set of variables Var, and a over a set of actions Act. We will use Lμ to denote the set of all μ-calculus formulas.

2.2.1 Standard Semantics

Usually, formulas are interpreted with respect to a labelled transition graph, and the meaning of a formula is then the set of states where the formula is true. The more specific, equivalent interpretation given in the following only applies to transition graphs of context-free systems, although it may also be generalized to arbitrary labelled transition graphs.

Given T_{R} = (V^{∗}, Act, →), and a valuation V : Var → 2^{V^{∗}}, the inductive definition below stipulates when a context-free process α ∈ V^{∗} has the property Φ, written as α ⊧_{V} Φ. If α fails to satisfy Φ, we will write α |̸=_{V} Φ.

α ⊧_{V} tt α |̸=_{V} ff

α ⊧_{V} X  iff α ∈ V(X)
α ⊧_{V} Φ_{1} ∨ Φ_{2} iff α ⊧_{V} Φ_{1} or α ⊧_{V} Φ_{2}
α ⊧_{V} Φ_{1} ∧ Φ_{2} iff α ⊧_{V} Φ_{1} and α ⊧_{V} Φ_{2}
α ⊧_{V} ⟨a⟩Φ  iff ∃ α′. α →^{a} α′ and α′ ⊧_{V} Φ
α ⊧_{V} [a]Φ  iff ∀ α′. α →^{a} α′ implies α′ ⊧_{V} Φ
α ⊧_{V} μX.Φ  iff ∀ S ⊆ V^{∗}. (∀ β ∈ V^{∗}. β ⊧_{V[ X↦S]} Φ implies β ∈ S) implies α ∈ S
α ⊧_{V} νX.Φ  iff ∃ S ⊆ V^{∗}. (∀ β ∈ V^{∗}. β ∈ S implies β ⊧_{V[ X↦S]} Φ) and α ∈ S

where V[ X ↦ S] is the valuation resulting from V by updating the binding of X to S.

The clauses for the fixpoints are a reformulation of the Tarski-Knaster theorem which states that the least fixpoint is the intersection of all pre-fixpoints and the greatest fixpoint is the union of all post-fixpoints. As a consequence, states satisfy a fixpoint formula iff they satisfy the unfolding of the formula, i.e. α ⊧_{V} σX.Φ iff α ⊧_{V} Φ[σX.Φ/X] where σ ∈ { μ, ν } and Φ[Ψ/X] denotes the simultaneous replacement of all free occurrences of X in Φ by Ψ.

The satisfaction relation defined above is independent of the valuation if the considered formula has no free variables in which case we will drop the index V. We extend our satisfaction relation, moreover, to sets of formulas by writing α ⊧ Γ if α ⊧ Φ, for all Φ ∈ Γ. Finally, we observe that the usual denotation of formulas as the set of states where the formula holds is obtained in our presentation by [[Φ]]_{V} = { α | α ⊧_{V} Φ }.

Next we define some standard notions which will allow us to deal with occurrences of subformulas in a given formula.

Definition 2.4 (Binding) A formula Φ is called well named if every fixpoint operator in Φ binds a distinct variable, and free variables are distinct from bound variables. With each well named formula Φ we then associate its binding function D_{Φ} which assigns to every bound variable X of Φ the unique subformula σX.Ψ(X) of Φ, called the binding definition of X in Φ.

From now on we assume that every formula is well named.

Definition 2.5 (Dependency order, Expansion) Given a formula Φ, we define the dependency order over the bound variables of Φ, denoted by ≤_{Φ}, as the least partial order such that if X occurs free in D_{Φ}(Y) then X ≤_{Φ} Y. Moreover, for every subformula Ψ of Φ, we define the expansion of Ψ with respect to D_{Φ} as:

⟨[Ψ]⟩_{D_{Φ}} =_{df} Ψ [ D_{Φ}(X_{n})/X_{n}] … [ D_{Φ}(X_{1})/X_{1} ]

where the sequence (X_{1}, …, X_{n}) is a linear ordering of all bound variables of Φ compatible with the dependency order, i.e. if X_{i} ≤_{Φ} X_{j} then i ≤ j.

Definition 2.6 (Subformula relation, Closure) The subformula relation on Lμ, denoted by ⪯, is the least partial order on Lμ such that Ψ_{i} ⪯ Ψ_{1} ∨ Ψ_{2}, Ψ_{i} ⪯ Ψ_{1} ∧ Ψ_{2}, Ψ ⪯ ⟨a⟩Ψ, Ψ ⪯ [a]Ψ, Ψ ⪯ μX.Ψ, and Ψ ⪯ νX.Ψ, for i = 1, 2 and a ∈ Act. Given a formula Φ, we define the closure of Φ as CL(Φ) = { Ψ | Ψ ⪯ Φ }. Furthermore, if CL(Φ) = { Ψ_{1}, …, Ψ_{n} } we will henceforth assume that the subformulas Ψ_{i} are linearly ordered compatible with ⪯, i.e. if Ψ_{i} ⪯ Ψ_{j} then i ≥ j.

Finally, we define a measure for the complexity of a formula depending on the number of intertwined alternating fixpoint operators.

Definition 2.7 (Alternation Depth) A formula Φ is said to be in the classes Σ_{0} and Π_{0} iff it contains no fixpoint operators. To form the class Σ_{n+1}, take Σ_{n} ∪ Π_{n}, and close under (i) boolean and modal combinators, (ii) μX.Φ, for Φ ∈ Σ_{n+1}, and (iii) substitution of Φ′ ∈ Σ_{n+1} for a free variable of Φ ∈ Σ_{n+1} provided that no free variable of Φ′ is captured by Φ; and dually for Π_{n+1}. The (Niwinski) alternation depth of a formula Φ, denoted by ad(Φ), is then the least n such that Φ ∈ Σ_{n+1} ∩ Π_{n+1}.

Example 2.8 Consider the closed formula Φ_{ex} = μX.νY.[b]X ∧ [a]Y which expresses intuitively that “on every (infinite) { a, b }-path only finitely many b-transitions can occur”. This formula has alternation depth 2, and its closure is the set of formulas { Ψ_{1}, Ψ_{2}, Ψ_{3}, Ψ_{4}, Ψ_{5}, Ψ_{6}, Ψ_{7} } where

Ψ_{1} = μX.νY.[b]X ∧ [a]Y  Ψ_{4} = [b]X  Ψ_{6} = X
Ψ_{2} = νY.[b]X ∧ [a]Y  Ψ_{5} = [a]Y  Ψ_{7} = Y
Ψ_{3} = [b]X ∧ [a]Y

When interpreted with respect to the transition graph of Figure 1 the semantics of Φ_{ex} is the set of states AB^{∗}∪B^{∗}. Note, however, that the semantics of the inner fixpoint formula νY.[b]X ∧ [a]Y is not continuous wrt. the valuation of X. This can be seen by applying

f(S) =_{df} [[νY.[b]X ∧ [a]Y]]_{[ X↦S]}^{T}

to the finite approximants B^{0...j} =_{df} { ϵ, B, B^{2}, …, B^{j} }. Since f(B^{0...j}) = B^{0...j+1}, for any j, we obtain ⋃_{j≥0} f(B^{0...j}) = B^{∗} as the limit of iteration over the naturals, while one further iteration yields f(B^{∗}) = AB^{∗} ∪ B^{∗}. Hence the function f is not continuous.

2.2.2 Assertion-Based Semantics

As pointed out in [BS92], context-free processes can be verified by considering Hoare-logic style pre-condition/post-condition pairs of sets of formulas for each of the nonterminals occurring in the context-free system. A triple { Γ } α { Δ } is then interpreted as α satisfies all formulas of Γ if we assert that after termination of α exactly the set of formulas Δ holds. This intuition is formally captured by the following definition of assertion-based semantics which generalises standard semantics by taking into account the set of formulas which hold after termination of a process.

Given T_{C} = (V^{∗}, Act, ⟼_{C}), and a valuation V : Var → 2^{V^{∗}}, the inductive definition below stipulates when a context-free process α ∈ V^{∗} has the property Φ under the hypothesis that after termination of α the formulas Δ hold, written as α ⊧_{V} (Φ, Δ). If α fails to satisfy Φ under the hypothesis Δ, we will write α |̸=_{V} (Φ, Δ). First we have

ϵ ⊧_{V} (Φ, Δ) iff Φ ∈ Δ

and then, for α ≠ ϵ, α ⊧_{V} (tt, Δ) α |̸=_{V} (ff, Δ)

α ⊧_{V} (X, Δ)  iff α ∈ V(X)
α ⊧_{V} (Φ_{1} ∨ Φ_{2}, Δ) iff α ⊧_{V} (Φ_{1}, Δ) or α ⊧_{V} (Φ_{2}, Δ)
α ⊧_{V} (Φ_{1} ∧ Φ_{2}, Δ) iff α ⊧_{V} (Φ_{1}, Δ) and α ⊧_{V} (Φ_{2}, Δ)
α ⊧_{V} (⟨a⟩Φ, Δ)  iff ∃ α′. α →^{a} α′ and α′ ⊧_{V} (Φ, Δ)
α ⊧_{V} ([a]Φ, Δ)  iff ∀ α′. α →^{a} α′ implies α′ ⊧_{V} (Φ, Δ)
α ⊧_{V} (μX.Φ, Δ)  iff ∀ S ⊆ V^{∗}. (∀ β ∈ V^{∗}. β ⊧_{V[ X↦S]} (Φ, Δ) implies β ∈ S)
implies α ∈ S
α ⊧_{V} (νX.Φ, Δ)  iff ∃ S ⊆ V^{∗}. (∀ β ∈ V^{∗}. β ∈ S implies β ⊧_{V[ X↦S]} (Φ, Δ))
and α ∈ S

As in the case of the standard semantics, we will use α ⊧_{V} (Γ, Δ) to denote α ⊧_{V} (Φ, Δ), for all Φ ∈ Γ.

The usefulness of the assertion-based semantics is underpined by the following proposition [BS92] which states that, firstly, the assertion-based semantics extend the standard semantics, and secondly, that they allow to reason compositionally about context-free processes.

Proposition 2.9 The assertion-based semantics is

1. an extension of standard semantics, i.e. given a closed formula Φ, we have,

α ⊧ Φ iff α ⊧ (Φ, Δ_{ϵ})

for Δ_{ϵ} = { Ψ ∈ CL(Φ) | ϵ ⊧ ⟨[Ψ]⟩_{D_{Φ}} }.

2. compositional wrt. context-free processes, i.e. for all Δ, Γ ⊆ Lμ,

αβ ⊧ (Γ, Δ) iff ∃ Σ ⊆ Lμ. α ⊧ (Γ, Σ) and β ⊧ (Σ, Δ)

The effectiveness of our algorithm, which is presented in the next section, relies, in particular, on Proposition 2.9.1, as it shows that Φ can be verified by taking into account merely the semantics of all subformulas of Φ.

3 The Model-Checking Algorithm

In this section we develop our model-checking algorithm which allows us to verify closed μformulas with arbitrary alternation depth for context-free processes in exponential time. In fact, the algorithm coincides with a backtracking extension of the model-checker of [BS92] which deals only with the alternation-free fragment of the modal μ-calculus. The correctness proof, presented in Section 4, requires, however, a stronger new framework involving dynamic environments which capture the valuations of free variables on the context-free transition graph.

[[A]]_{V}^{tt}  = λ(Δ).1  [[A]]_{V}^{Ψ_{1}∨Ψ_{2}} = [[A]]_{V}^{Ψ_{1}} ⊔ [[A]]_{V}^{Ψ_{2}}
[[A]]_{V}^{ff}  = λ(Δ).0  [[A]]_{V}^{Ψ_{1}∧Ψ_{2}} = [[A]]_{V}^{Ψ_{1}} ⊓ [[A]]_{V}^{Ψ_{2}}
[[A]]_{V}^{X}  = λ(Δ).V(X, A)  [[A]]_{V}^{⟨a⟩Ψ} = ⊔_{A→^{a}α}[[α]]_{V}^{Ψ}
[[A]]_{V}^{[a]Ψ} = ⊓_{A→^{a}α}[[α]]_{V}^{Ψ}
[[A]]_{V}^{μX.Ψ} = sel_{A}(⊓{ (h_{A_{1}}^{X}, …, h_{A_{n}}^{X}) | ∀_{1≤i≤n} [[A_{i}]]_{V[ (X,A_{j})↦h_{A_{j}}^{X} ,1≤j≤n]}^{Ψ} ⊑ h_{A_{i}}^{X} })
[[A]]_{V}^{νX.Ψ} = sel_{A}(⊔{ (h_{A_{1}}^{X}, …, h_{A_{n}}^{X}) | ∀_{1≤i≤n} h_{A_{i}}^{X} ⊑ [[A_{i}]]_{V[ (X,A_{j})↦h_{A_{j}}^{X} ,1≤j≤n]}^{Ψ} })
[[ϵ]]_{V}^{Ψ}(Δ) = mem_{Ψ}(Δ)
[[Aα]]_{V}^{Ψ}(Δ) = [[A]]_{V}^{Ψ}({ Υ ∈ CL(Φ) | [[α]]_{V}^{Υ}(Δ) = 1 })

Figure 2: The property transformer scheme.

3.1 The Property Transformer Scheme

Given a context-free system C and a closed formula Φ, each nonterminal A ∈ V = { A_{1}, …, A_{n} } defines a mapping [[A]] : 2^{CL(Φ)} → 2^{CL(Φ)} from post- to pre-conditions. As we are, however, in particular interested in the question whether a given subformula Ψ ∈ CL(Φ) belongs to the pre-condition set or not, we refine this notion by defining the following functions, called characteristic property transformers (CPT).

[[A]]^{Ψ}(Δ) =_{df} \{ \begin{matrix}1 & if A ⊧ (Ψ, Δ) \\ 0 & otherwise \end{matrix}

Writing IB for the usual lattice of boolean values, characteristic property transformers are elements of the boolean lattice consisting of all functions from 2^{CL(Φ)} to IB, where the ordering, and the meet and join operations respectively, are defined argument-wise.

More importantly, they can be obtained as a fixpoint solution of an appropriate function scheme, called the property transformer scheme (PTS). This scheme is defined by the rules given in Figure 2, and consists of two parts. The first part copes with the structure of the context-free system, as well as with the semantics of the formula, and defines an equation for each pair (A, Ψ) ∈ V × CL(Φ). The second part deals with the empty process according to the first clause of the assertion-based semantics, as well as with composed processes according to Proposition 2.9.2. Whereas the rules for the basic cases mimic directly the semantics of the subformula, the fixpoint related equations are slightly more complicated and require a simultaneous computation of all their corresponding transformers^{2}. sel_{A} then simply selects the A component of the resulting tuple. The other auxiliary function, mem_{Ψ}, tests the membership of Ψ in the given set of formulas. It returns 1 if Ψ ∈ Δ and 0 otherwise.

The overall structure of the model-checking algorithm consists now of the following three steps.

2Note that valuations map now pairs of variables and nonterminals to characteristic property transformers.

1. Given a context-free system C and a closed μ-formula Φ construct the property transformer scheme according to the rules given in Figure 2.

2. Solve the (finite) fixpoint problem for the property transformer scheme.

3. Check whether [[A_{1}]]^{Φ}(Δ_{ϵ}) = 1 where A_{1} is the root of the context-free system, and Δ_{ϵ} = { Ψ ∈ CL(Φ) | ϵ ⊧ ⟨[Ψ]⟩_{D_{Φ}} }.

In Section 4 we prove that the second step of the algorithm computes transformers which reflect the assertion-based semantics, while Proposition 2.9.1 now ensures that the third step solves the model-checking problem, as we have

[[A_{1}]]^{Φ}(Δ_{ϵ}) = 1 iff A_{1} ⊧ (Φ, Δ_{ϵ}) iff A_{1} ⊧ Φ

Moreover, the ordinary semantics of Φ can be obtained from the set of CPT’s by means of [[Φ]] = { α ∈ V^{∗} | [[α]]^{Φ}(Δ_{ϵ}) = 1 }. In particular, the semantics of Φ is always a regular set of states.

3.2 Complexity

As expected, the required backtracking for alternating μ-formulas yield a worst-case time complexity for the algorithm, which is exponentially worse (in the alternation depth) than the estimation given for the alternation-free case [BS92, BS95].

Theorem 3.1 (Complexity) Let C be a context-free system, and Φ be a closed μ-formula. Then the worst-case time complexity of solving the property transformer scheme is

O( |Φ| ∗ (|C| ∗ 2^{|Φ|})^{ad(Φ)+1} )

Proof: For the complexity analysis we assume wlog. that the context-free system is given in 3-GNF, i.e. that each right-hand side of the context-free system has length at most 2.

First observe that the right-hand side of a single PTS-equation can be computed argument-wise for each of the 2^{|Φ|} arguments Δ ∈ CL(Φ). The most expensive right-hand side computations result from PTS-equations related to formulas containing a modality. In this case any evaluation of [[α]]_{V}^{Ψ} takes time O( |Φ|), and for a fixed Ψ, we have at most |C| of these composed expressions. Thus fixing a subformula Ψ_{k}, the evaluation of all its PTS right-hand sides for all arguments has time complexity O( |C| ∗ |Φ| ∗ 2^{|Φ|}).

Moreover, there are now at most |C| CPT’s each having a maximal chain length of approximants of 2^{|Φ|}. Thus the overall worst-case time complexity for computing the fixpoint at level k ∈ [1, n] can be estimated by

T C_{k} = O( |C| ∗ 2^{|Φ|} ∗ (T C_{k+1} + |C| ∗ |Φ| ∗ 2^{|Φ|}) )

where T C_{n+1} = 0. Using induction, and thereafter standard techniques to refine the fixpoint computation by dealing with subformulas occurring in between alternation simultaneously we hence obtain the overall time complexity

T C_{1} = O( |Φ| ∗ (|C| ∗ 2^{|Φ|})^{ad(Φ)+1} )
□

3.3 An Example

In this section we illustrate our model-checking algorithm by verifying the μ-formula Φ_{ex} of Example 2.8 for the context-free process C_{ex} given in Figure 1. Figure 3 shows the property transformer scheme P T S_{ex} constructed from C_{ex} and Φ_{ex}, as well as the corresponding fixpoint computation. To shorten the example we have evaluated { Ψ_{2}, …, Ψ_{7} } simultaneously, as they occur in the same alternation level, and we have used simply Ψ_{6} instead of mem_{Ψ_{6}}. At the bottom of the figure we, finally, apply the resulting characteristic property transformer [[A]]^{Ψ_{1}} to the set of subformulas satisfied by ϵ. Since the application yields true, we have thus verified that A satisfies indeed the property represented by Ψ_{1}.

4 The Correctness Proof

The observation that the fixpoint computation for μ-formulas with only one sort of fixpoint can be done simultaneously was used in [BS92, BS95] to verify closed alternation-free formulas by merely exploring the assertion-based semantics. For formulas with alternation, however, we need a stronger framework which takes also into account the bindings of free variables where the parity may alternate. These bindings will be dealt with by dynamic environments which are decribed in terms of deterministic finite-state automata introduced in Section 4.1. Subsequently, in Section 4.2 we show that dynamic environments may represent the semantic solution of the model-checking problem, and that there exists an iterative algorithm which admits the computation of the semantic solution.

4.1 Dynamic Environments

In the presence of formulas containing free variables the simple composition property of Proposition 2.9.1 no longer captures correctly the behaviour of context-free processes wrt. the specification at hand. This defect is eliminated by the slight modification given below.

{ Γ, V′ } αβ { Δ, V } iff ∃ Σ, V′′ { Γ, V′ } α { Σ, V′′ } and { Σ, V′′ } β { Δ, V }

Intuitively, the modified composition rule expresses that in addition to assertions also environments must be adapted when considered at intermediate states. In general, the valuation V′′ is obtained from V by right cancellation of β, i.e. for all X ∈ dom(V), V′′(X) = (V(X) ∩ V^{∗}β)β^{−1}. As an example, αβ ∈ V(X) would imply α ∈ V′′(X).

In the remainder of this section we fix now a context-free system C, and a formula Φ with closure { Ψ_{1}, …, Ψ_{n} }. Our aim is to develop a formalism, the dynamic environments, which faithfully models the adaptations of valuations needed for composition. Dynamic environments will be partitioned into levels k ∈ [1, n] where a dynamic environment of level k defines the valuations for { Ψ_{1}, …, Ψ_{k} }. This change from valuations for variables to valuations for subformulas is reflected in the semanics by adding the rule “if Ψ ∈ dom(V) then (α ⊧_{V} (Ψ, Δ) if α ∈ V(Ψ))”. The original model-checking problem is then reduced to a corresponding fixpoint problem on the finite domain of dynamic

C_{ex} = \{ \begin{matrix}A & →^{a} & AB \\ A & →^{b} & ϵ \\ B & →^{b} & ϵ \end{matrix} \} Φ_{ex} = \{ \begin{matrix}Ψ_{1} & =^{μ} & Ψ_{2} \\ Ψ_{2} & =^{ν} & Ψ_{3} \\ Ψ_{3} & = & Ψ_{4} ∧ Ψ_{5} \\ Ψ_{4} & = & [b]Ψ_{6} \\ Ψ_{5} & = & [a]Ψ_{7} \\ Ψ_{6} & = & Ψ_{1} \\ Ψ_{7} & = & Ψ_{2} \end{matrix} \} P T S_{ex} = \{ \begin{matrix}[[A]]^{Ψ_{1}} & =^{μ} & [[A]]^{Ψ_{2}} & [[B]]^{Ψ_{1}} & =^{μ} & [[B]]^{Ψ_{2}} \\ [[A]]^{Ψ_{2}} & =^{ν} & [[A]]^{Ψ_{3}} & [[B]]^{Ψ_{2}} & =^{ν} & [[B]]^{Ψ_{3}} \\ [[A]]^{Ψ_{3}} & = & [[A]]^{Ψ_{4}} ⊓ [[A]]^{Ψ_{5}} & [[B]]^{Ψ_{3}} & = & [[B]]^{Ψ_{4}} ⊓ [[B]]^{Ψ_{5}} \\ [[A]]^{Ψ_{4}} & = & [[ϵ]]^{Ψ_{6}} & [[B]]^{Ψ_{4}} & = & [[ϵ]]^{Ψ_{6}} \\ [[A]]^{Ψ_{5}} & = & [[AB]]^{Ψ_{7}} & [[B]]^{Ψ_{5}} & = & 1 \\ [[A]]^{Ψ_{6}} & = & [[A]]^{Ψ_{1}} & [[B]]^{Ψ_{6}} & = & [[B]]^{Ψ_{1}} \\ [[A]]^{Ψ_{7}} & = & [[A]]^{Ψ_{2}} & [[B]]^{Ψ_{7}} & = & [[B]]^{Ψ_{2}} \end{matrix} \}

Fixpoint computation for P T S_{ex}:

[[A]]^{Ψ_{1}} [[A]]^{Ψ_{2}} [[A]]^{Ψ_{3}} [[A]]^{Ψ_{4}} [[A]]^{Ψ_{5}} [[A]]^{Ψ_{6}} [[A]]^{Ψ_{7}} [[B]]^{Ψ_{1}} [[B]]^{Ψ_{2}} [[B]]^{Ψ_{3}} [[B]]^{Ψ_{4}} [[B]]^{Ψ_{5}} [[B]]^{Ψ_{6}} [[B]]^{Ψ_{7}}
1 0  1  1  1  1  1  1  0  1  1  1  1  1  1
2  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  0  1  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  0  1
3  0  0  Ψ_{6}  0  0  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  0  Ψ_{6}
4  0  0  Ψ_{6}  0  0  0  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  0  Ψ_{6}
5 0  1  1  1  1  1  1  Ψ_{6}  1  1  1  1  1  1
6  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  0  1  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  Ψ_{6}  1
7  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  0  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  Ψ_{6}  Ψ_{6}
8 Ψ_{6}  1  1  1  1  1  1  Ψ_{6}  1  1  1  1  1  1
9  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  Ψ_{6}  1  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  Ψ_{6}  1
10  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  Ψ_{6}  1  Ψ_{6}  Ψ_{6}

Standard model-checking for ϵ delivers ϵ ⊧ Δ_{ϵ} =_{df} { Ψ_{1}, Ψ_{2}, Ψ_{3}, Ψ_{4}, Ψ_{5}, Ψ_{6}, Ψ_{7} }. Overall we thus obtain:

A ⊧ Ψ_{1} iff A ⊧ (Ψ_{1}, Δ_{ϵ}) iff [[A]]^{Ψ_{1}}(Δ_{ϵ}) = 1 iff mem_{Ψ_{6}}(Δ_{ϵ}) = 1 iff Ψ_{6} ∈ Δ_{ϵ} Figure 3: The verification of Φ_{ex} for C_{ex}.

11 environments, such that the semantics of the original formula is captured by the final environment of level n.

Definition 4.1 (Dynamic Environment) A dynamic environment Ā_{k} of level k ∈ [1, n] is a sequence of deterministic finite-state automata A_{i} = (Q_{A_{i}}, V, δ_{A_{i}}, F_{A_{i}}), i = 1, …, k, where

• Q_{A_{i}} = (2^{CL(Φ)})^{i} are the state sets of the automata,

• V is the input alphabet,

• δ_{A_{i}} : Q_{A_{i}} × V → Q_{A_{i}} are the transition functions obeying the constraints

δ_{A_{i}}(Δ̄_{i}, A) = Γ̄_{i} implies δ_{A_{i−1}}(Δ̄_{i−1}, A) = Γ̄_{i−1}

where Δ̄_{i} denotes (Δ_{1}, …, Δ_{i}), and

• F_{A_{i}} = { Δ̄_{i} ∈ Q_{A_{i}} | Ψ_{i} ∈ Δ_{i} } is the set of accepting states.

Denoting the transitive closure of δ_{A_{i}}, as usual, also by δ_{A_{i}} the language accepted by A_{i} starting in the state Δ̄_{i} is L_{A_{i}}(Δ̄_{i}) = { α ∈ V^{∗} | δ_{A_{i}}(Δ̄_{i}, α̃) ∈ F_{A_{i}} } where α̃ is the reverse of α^{3}.

A dynamic environment Ā_{k} together with a state Δ̄_{k} is then interpreted as an environment which defines valuations for Ψ_{1}, …, Ψ_{k} by means of

Ā_{1}⟨Δ̄_{1}⟩ =_{df} [ Ψ_{1} ↦ L_{A_{1}}(Δ̄_{1}) ]
Ā_{k}⟨Δ̄_{k}⟩ =_{df} Ā_{k−1}⟨Δ̄_{k−1}⟩ [ Ψ_{k} ↦ L_{A_{k}}(Δ̄_{k}) ] for 2 ≤ k ≤ n

Dynamic environments are a convenient formalism to describe the semantics of μformulas on context-free processes since they model compositionality simply by transitions in the finite automata.

Lemma 4.2 Let { Γ, V′ } A { Δ, Ā_{k}⟨Δ̄_{k}⟩ }. Then

1. For all i ≤ k, Ψ_{i} ∈ Γ iff A ∈ Ā_{k}⟨Δ̄_{k}⟩(Ψ_{i}), and

2. V′ = Ā_{k}⟨δ_{A_{k}}(Δ̄_{k}, A)⟩.

The first property expresses that a dynamic environment of level k captures the semantics of all subformulas up to level k, while the second property states that the environment to be considered in the pre-condition of A coincides with the interpretation of the A-successor of Δ̄_{k} in A_{k}.

3Here we have to use α̃ as the automaton has to model the above mentioned right cancellation

The granularity of the transition functions of dynamic environments is not sufficient to obtain a match between the semantic and the iterative intuition behind the model checking problem. We therefore split these transition functions into characteristic transition functions (CTF) δ^{i,j} as follows.

δ^{i,j}(Δ̄_{i}, A) = \{ \begin{matrix}1 & if Ψ_{j} ∈ δ_{A_{i}}^{i}(Δ̄_{i}, A) \\ 0 & otherwise \end{matrix}

where δ_{A_{i}}^{j}(Δ̄_{i}, A) =_{df} Γ_{j} if δ_{A_{i}}(Δ̄_{i}, A) = Γ̄_{i}. CTF’s can naturally be extended to words over V by means of

δ^{i,j}(Δ̄_{i}, ϵ) = mem_{Ψ_{j}}(Δ_{i})
δ^{i,j}(Δ̄_{i}, αA) = δ^{i,j}(δ_{A_{i}}(Δ̄_{i}, A), α)

The split into characteristic transition functions allows us to view a dynamic environment Ā_{k} as a matrix of CTF’s as depicted below.

δ^{1,1} δ^{1,2} … δ^{1,k} … δ^{1,n}
⋮  ...  ⋮
δ^{k,1} δ^{k,2} … δ^{k,k} … δ^{k,n}

This matrix can be systematically extended to a matrix for Ā_{k+1} with new row (δ^{k+1,1}, …, δ^{k+1,n}) by means of a fixpoint computation such that the final result will capture the semantics of the formula Φ on the given process. During this computation we need to update a characteristic transition function by a function of the same column. The arity of the function is then adapted by either suppressing or by replicating arguments. Formally, we define

(δ^{i,j} ↑ k) (Δ̄_{k}, A) =_{df} δ^{i,j}(Δ̄_{i}, A) where k ≥ i, and
(δ^{i,j} ↓ k) (Δ̄_{k}, A) =_{df} δ^{i,j}(Δ̄_{i}, A) where k ≤ i and Δ_{j} = Δ_{k}, for j = k + 1, …, i.

Intuitively, the first line describes that a CTF of level i which is used at level k ≥ i ignores the local formula sets Δ_{i+1}, …, Δ_{k}, while the second line expresses that a CTF of level i which is used at level k ≤ i takes as arguments Δ_{1}, …, Δ_{k}, and replicates Δ_{k} i − k times. To simplify the subsequent presentation of the algorithm we will, however, use δ^{i,j} also for the adapted CTF’s.

As will be elaborated on in the next subsection, the matrices defined above are adequate for proving our main result, Theorem 4.7, i.e. the equivalence of the semantic and the iterative algorithm presented in Section 4.2, because it is possible to “synchronize” their corresponding computations on the diagonal.

4.2 Semantic and Iterative Solutions

Given the semantics of the formulas Ψ_{1}, …, Ψ_{k−1} in terms of a dynamic environment Ā_{k−1} we will now consider the semantics of the remaining formulas Ψ_{k}, …, Ψ_{n}.

Definition 4.3 (Semantic Solutions) We call Ā_{k}, for k ∈ [1, n], the semantic solution of Ā_{k−1}, written as S(Ā_{k−1}), if the transition function of A_{k} satisfies

δ_{A_{k}}(Δ̄_{k}, A) = Γ̄_{k} iff (Γ_{k}, Ā_{k−1}⟨Γ̄_{k−1}⟩) A (Δ_{k}, Ā_{k−1}⟨Δ̄_{k−1}⟩).

Moreover, we call (Ā_{k}, …, Ā_{n}) the semantic solutions of Ā_{k−1}, denoted by S̄(Ā_{k−1}), if Ā_{i} = S(Ā_{i−1}), for i ∈ [k, n].

It turns out that the semantic solution respects the standard substitution lemma.

Lemma 4.4 Let (Γ_{k}, Ā_{k−1}⟨Γ̄_{k−1}⟩) A (Δ_{k}, Ā_{k−1}⟨Δ̄_{k−1}⟩) and let Ā_{k} be the semantic solution of Ā_{k−1}. Then

(Γ_{k}, Ā_{k−1}⟨Γ̄_{k−1}⟩[ Ψ_{k} ↦ L_{A_{k}}(Γ̄_{k}) ]) A (Δ_{k}, Ā_{k−1}⟨Δ̄_{k−1}⟩[ Ψ_{k} ↦ L_{A_{k}}(Δ̄_{k}) ])

Corollary 4.5 (Diagonal Consistency) If Ā_{k}, …, Ā_{n} are the semantic solutions of Ā_{k−1} then δ^{i,j} = δ^{j,j}, for i ∈ [k, n], j ∈ [1, n].

Due to this corollary we may simply identify the semantic solutions Ā_{k}, …, Ā_{n} with the characteristic transition functions δ^{k,k}, …, δ^{n,n}. Conversely, given Ā_{k−1} and (arbitrary) δ^{k,k}, …, δ^{n,n} we define

• Ā_{k−1} ⊕ (δ^{k,k}, …, δ^{n,n}) as Ā_{k−1} augmented by δ^{k,j} =_{df} δ^{j,j}, for j ∈ [1, n], and

• Ā_{k−1} ⊗ (δ^{k,k}, …, δ^{n,n}) as Ā_{k−1} augmented by δ^{i,j} =_{df} δ^{j,j}, for i ∈ [k, n], j ∈ [1, n].

Let us finally sketch the resulting (conceptual) algorithm which iteratively computes the semantic solutions for Ā_{k−1}. Given Ā_{k−1}, we would like to compute δ^{i,j} for i ∈ [k, n], j ∈ [1, n]. By Corollary 4.5 we already know that δ^{i,j} = δ^{j,j} for i ∈ [k, n], j ∈ [1, k − 1]. The remaining characteristic transition functions are then computed levelwise by a two-level fixpoint computation. During the inner-level computation we have fixed some approximant δ^{k,k} and vary the values of δ^{k,k+1}, …, δ^{k,n}. The idea is that (δ^{k,1}, …, δ^{k,n}) together with Ā_{k−1} defines a dynamic environment Ā_{k} for which we can compute the semantic solutions θ^{k+1,k+1}, …, θ^{n,n} by induction. We may therefore update δ^{k,k+1}, …, δ^{k,n} by θ^{k+1,k+1}, …, θ^{n,n}, and repeat this iteration until we reach consistency. In the outer-level fixpoint computation we may now update the fixed δ^{k,k} by evaluating the characteristic transition function for the “unfolding” of Ψ_{k} in the current setting, and start the inner fixpoint computation again. Our main theorem then states that if we have reached consistency also at the outer-level then the iterative and the semantic solutions for Ā_{k−1} coincide.

Formally, given a dynamic environment Ā_{k−1}, we define a monotone function GI_{k}(δ^{k,k}) called the global iteration function at level k with respect to δ^{k,k} by

GI_{k}(δ^{k,k})(δ^{k+1,k+1}, …, δ^{n,n}) =_{df} (θ^{k+1,k+1}, …, θ^{n,n}).

where (θ^{k+1,k+1}, …, θ^{n,n}) are the semantic solutions of Ā_{k} = Ā_{k−1} ⊕ (δ^{k,k}, …, δ^{n,n}). Accordingly, μGI_{k}(δ^{k,k}) denotes now the least fixpoint of GI_{k}(δ^{k,k}), while νGI_{k}(δ^{k,k}) denotes the greatest. Notice, moreover, that both fixpoints are monotone wrt. δ^{k,k}.

In order to define in a second step the local iteration function LI_{k} at level k we first consider the CTF [[[Ψ_{k}]]]Ā_{n} : Q_{A_{k}} × V → { 0, 1 } representing the “unfolding” of a formula Ψ_{k} wrt. a dynamic environment Ā_{n}. It is given by

[[[Ψ_{k}]]]Ā_{n} =_{df} \{ \begin{matrix}λ(Δ̄_{k}, A).1 & if Ψ_{k} = tt \\ λ(Δ̄_{k}, A).0 & if Ψ_{k} = ff \\ Ā_{n}[i, i] & if Ψ_{k} = X and Ψ_{i} = σX.Ψ_{j} \\ Ā_{n}[i, i] ⊔ Ā_{n}[j, j] & if Ψ_{k} = Ψ_{i} ∨ Ψ_{j} \\ Ā_{n}[i, i] ⊓ Ā_{n}[j, j] & if Ψ_{k} = Ψ_{i} ∧ Ψ_{j} \\ λ(Δ̄_{k}, A). ⊔_{A→^{a}α} Ā_{n}[i, i](Δ̄_{k}, α) & if Ψ_{k} = ⟨a⟩Ψ_{i} \\ λ(Δ̄_{k}, A). ⊓_{A→^{a}α} Ā_{n}[i, i](Δ̄_{k}, α) & if Ψ_{k} = [a]Ψ_{i} \\ Ā_{n}[i, i] & if Ψ_{k} = σX.Ψ_{i} \end{matrix}

where Ā_{n}[i, j] denotes the CTF of Ā_{n} ocurring in row i, and in column j.

Now let σ be the parity^{4} of Ψ_{k}, σGI_{k}(δ^{k,k}) = (δ^{k+1,k+1}, …, δ^{n,n}), and (Ā_{k+1}, …, Ā_{n}) be the semantic solutions of Ā_{k} = Ā_{k−1} ⊕ (δ^{k,k}, …, δ^{n,n}). Then we define

LI_{k}(δ^{k,k}) =_{df} [[[Ψ_{k}]]]Ā_{n}

As LI_{k} is again monotone, we may build its least fixpoint μLI_{k}, as well as its greatest fixpoint νLI_{k}. Finally, we use GI_{k} and LI_{k} to define the iterative solutions of Ā_{k−1}, written as Ī(Ā_{k−1}), by

Ī(Ā_{k−1}) =_{df} (ϑ^{k,k}, …, ϑ^{n,n})

where σ is the parity of Ψ_{k}, ϑ^{k,k} = σLI_{k}, and (ϑ^{k+1,k+1}, …, ϑ^{n,n}) = σGI_{k}(ϑ^{k,k}).

Based on the following lemma, which states that the semantic solutions are a fixpoint of GI_{k} and LI_{k}, the key to our algorithm is now an iterative characterization of the semantic solutions.

Lemma 4.6 Let S̄(Ā_{k−1}) = (Ā_{k}, …, Ā_{n}) with CTF’s (θ^{k,k}, …, θ^{n,n}). Then we have

1. GI_{k}(θ^{k,k})(θ^{k+1,k+1}, …, θ^{n,n}) = (θ^{k+1,k+1}, …, θ^{n,n}), and

2. LI_{k}(θ^{k,k}) = θ^{k,k}.

Theorem 4.7 For any given dynamic environment Ā_{k} the semantic and the iterative solutions coincides, i.e. S̄(Ā_{k}) = Ī(Ā_{k}).

4For non-fixpoint formulas we can take σ to be either μ or ν as the semantics of the subformulas of Ψ_{k} do not depend on the semantics of Ψ_{k} itself.

Proof: The theorem is shown by induction on k. For the induction base where k = n there is nothing to show, as S̄(Ā_{n}) = () = Ī(Ā_{n}). Now consider a dynamic environment Ā_{k−1} with k − 1 < n, and assume the theorem holds for all i ∈ [k, n]. The induction step for Ψ_{k} = tt, ff, X, Ψ_{i} ∨ Ψ_{j}, Ψ_{i} ∧ Ψ_{j}, ⟨a⟩Ψ_{i}, and [a]Ψ_{i} is proved using the definition of LI_{k} and the fact that the semantics of occurring proper subformulas do not depend on the semantics of Ψ_{k} itself. We therefore prove the induction step only for the case where Ψ_{k} is a minimal fixpoint operator μX.Ψ_{l}, since the case for maximal fixpoints is completely dual.

Let θ = (θ^{k,k}, …, θ^{n,n}) be the semantic solutions of Ā_{k−1}, and S̄_{k} = Ā_{k−1} ⊕ θ. Moreover, let ϑ = (ϑ^{k,k}, …, ϑ^{n,n}) be the iterative solutions of Ā_{k−1}, i.e. ϑ^{k,k} = μLI_{k} and (ϑ^{k+1,k+1}, …, ϑ^{n,n}) = μGI_{k}(ϑ^{k,k}), as well as Ī_{k} = Ā_{k−1} ⊕ ϑ.

(I) (ϑ^{k,k}, …, ϑ^{n,n}) ⊑ (θ^{k,k}, …, θ^{n,n})

To show the inequality we construct inductively a chain of dynamic environments Ā_{n}^{(i)}, for i ≥ 0, as follows. Let

Ā_{n}^{(i)} = Ā_{k−1} ⊗ (ϑ^{(i)k,k}, …, ϑ^{(i)n,n})

where

\begin{aligned}ϑ^{(0)k,k} & = & θ^{k,k}, & (ϑ^{(0)k+1,k+1}, …, ϑ^{(0)n,n}) & = & μGI_{k}(ϑ^{(0)k,k}) \\ ϑ^{(i+1)k,k} & = & [[[Ψ_{k}]]]Ā_{n}^{(i)}, & (ϑ^{(i+1)k+1,k+1}, …, ϑ^{(i+1)n,n}) & = & μGI_{k}(ϑ^{(i+1)k,k}) \end{aligned}

Claim : Ā_{n}^{(i)}, for i ≥ 0, is a descending chain of dynamic environments.

Proof: First note that ϑ^{(i)k,k} ⊒ ϑ^{(i+1)k,k} implies Ā_{n}^{(i)} ⊒ Ā_{n}^{(i+1)}, since by definition

(ϑ^{(i)k+1,k+1}, …, ϑ^{(i)n,n}) = μGI_{k}(ϑ^{(i)k,k}) ⊒ μGI_{k}(ϑ^{(i+1)k,k}) = (ϑ^{(i+1)k+1,k+1}, …, ϑ^{(i+1)n,n}).

The claim is then proved by showing

(4.7.1) Ā_{n}^{(0)} ⊒ Ā_{n}^{(1)}, and
(4.7.2) Ā_{n}^{(i−1)} ⊒ Ā_{n}^{(i)} implies Ā_{n}^{(i)} ⊒ Ā_{n}^{(i+1)}.

(4.7.1) Since by Lemma 4.6.1 GI_{k}(θ^{k,k})(θ^{k+1,k+1}, …, θ^{n,n}) = (θ^{k+1,k+1}, …, θ^{n,n}) we see that

(θ^{k+1,k+1}, …, θ^{n,n}) ⊒ μGI_{k}(θ^{k,k}) = (ϑ^{(0)k+1,k+1}, …, ϑ^{(0)n,n}),

and hence

ϑ^{(0)k,k} = θ^{k,k} = [[[Ψ_{k}]]]Ā_{n}^{θ} ⊒ [[[Ψ_{k}]]]Ā_{n}^{(0)} = ϑ^{(1)k,k}.

Thus we obtain Ā_{n}^{(0)} ⊒ Ā_{n}^{(1)}.

(4.7.2) Now let Ā_{n}^{(i−1)} ⊒ Ā_{n}^{(i)}, for some i ≥ 1. Since

ϑ^{(i)k,k} = [[[Ψ_{k}]]]Ā_{n}^{(i−1)} ⊒ [[[Ψ_{k}]]]Ā_{n}^{(i)} = ϑ^{(i+1)k,k}

by definition, we immediately obtain Ā_{n}^{(i)} ⊒ Ā_{n}^{(i+1)}, as desired. □

Since the domain of all dynamic environments wrt. Φ and C is finite, we eventually reach a fixpoint Ā_{n}^{(fix)} for which we conclude

(ϑ^{k,k}, …, ϑ^{n,n}) ⊑ (ϑ^{(fix)k,k}, …, ϑ^{(fix)n,n}) ⊑ (ϑ^{(0)k,k}, …, ϑ^{(0)n,n}) ⊑ (θ^{k,k}, …, θ^{n,n}).

(II) LĪ_{k}(Δ̄_{k}) ⊇ LS̄_{k}(Δ̄_{k}), for any consistent Δ̄_{k}

Δ̄_{k} is said to be consistent if each Δ_{i}, for i ∈ [1, k], is consistent, and Δ_{i} is called consistent if it satisfies the following conditions: ff ∉ Δ_{i}, Ψ_{1} ∨ Ψ_{2} ∈ Δ_{i} iff Ψ_{1} ∈ Δ_{i} or Ψ_{2} ∈ Δ_{i}, Ψ_{1} ∧ Ψ_{2} ∈ Δ_{i} iff Ψ_{1} ∈ Δ_{i} and Ψ_{2} ∈ Δ_{i}, and σX.Ψ ∈ Δ_{i} iff X ∈ Δ_{i} iff Ψ ∈ Δ_{i}.

As Ψ_{k} = μX.Ψ_{l}, (II) follows now from the fixpoint property

α ⊧_{Ī_{k}⟨Δ̄_{k}⟩} (Ψ_{l}, Δ_{k}) iff α ∈ L_{I_{k}}(Δ̄_{k})

which is proved by induction on the length of processes. For the induction base we have

ϵ ⊧_{Ī_{k}⟨Δ̄_{k}⟩} (Ψ_{l}, Δ_{k})
iff Ψ_{l} ∈ Δ_{k}
iff Ψ_{k} ∈ Δ_{k}  by consistency of Δ_{k}
iff ϵ ∈ L_{I_{k}}(Δ̄_{k})

The induction step then follows from

αA ⊧_{Ī_{k}⟨Δ̄_{k}⟩} (Ψ_{l}, Δ_{k})

iff α ⊧_{Ī_{k}⟨δ_{I_{k}} (Δ̄_{k},A)⟩} (Ψ_{l}, δ_{I_{k}}^{k}(Δ̄_{k}, A)) by induction hypothesis on k
iff α ∈ L_{I_{k}}(δ_{I_{k}}(Δ̄_{k}, A))  by induction hypothesis on the length of α
iff αA ∈ L_{I_{k}}(Δ̄_{k})

(III) Since (I) implies LĪ_{k}(Δ̄_{k}) ⊆ LĪ_{k}(Δ̄_{k}), we conclude from (II) LĪ_{k}(Δ̄_{k}) ⊆ LĪ_{k}(Δ̄_{k}), for any consistent Δ̄_{k}. We have hence ϑ^{k,k} = θ^{k,k}, and by induction hypothesis on k also ϑ^{i,i} = θ^{i,i}, for i ∈ [k + 1, n].

As Δ_{ϵ} is consistent, and characteristic transition functions preserve consistency, this concludes the proof. □

The observation that only the characteristic transition functions on the diagonal have to be taken into account when updating δ^{k,k} wrt. the current dynamic environment Ā_{n}, allows us to replace the “conceptual” algorithm used in the correctness proof to the “actual” model-checking algorithm presented in the previous section. This optimization is, finally, the key for proving the claimed complexity result.

5 Conclusions and Further Research

In this paper we have presented an iterative, elementary model-checking algorithm for context-free processes which deals with the full modal μ-calculus. This basic algorithm can be extended to the class of pushdown processes following the lines of [BS95], as well as to the class of regular graphs following the lines of [BQ96], respectively. Essentially, both extensions are obtained by taking into account the arity Q of pushdown processes (which corresponds to the number of states in the finite control), respectively regular graphs (which corresponds to the maximal arity of a hyperedge), which yields characteristic property transformers with multiple arguments. For these extensions our algorithm has the worst-time complexity

O( |Φ| ∗ (|Q| ∗ |C|)^{ad(Φ)+1} ∗ 2^{|Φ|∗(ad(Φ)+|Q|)} ).

Recently, Walukiewicz presented another model-checker for pushdown processes which uses games [Wal96]. His algorithm has a dramatically different complexity estimation. In particular it behaves much worse for increasing degrees of alternation depths.

O( |C| ∗ (2^{|Q|∗|Φ|∗ad(Φ)})^{ad(Φ)} )

Whereas our algorithm directly mimics the behavioural intuition behind sequential processes and, in particular, keeps process and formula structure transparent, which gives a direct handle to extending the underlying process structure, Walukiewics’ algorithm intertwines these structures, which, at least, complicates the identification of the modifications necessary for the extensions.

This structural distinction has also an impact on the further extensions we are planning: First, to extend model-checking to the class of rational restricted recognizable graphs as introduced in [Cau96], and second, to develop a local variant. Both extensions will exploit the structural transparency of our approach and, in particular, use the framework of dynamic environments.

References

[BQ96] O. Burkart and Y.-M. Quemener. Model-Checking of Infinite Graphs Defined by Graph Grammars. In INFINITY ’96, MIP-9614, pages 56–70. Universität Passau, July 1996.

[Bra96] J.C. Bradfield. The Modal mu-Calculus Alternation Hierarchy is Strict. In CONCUR ’96, LNCS 1119, pages 233–246. Springer, 1996.

[BS92] O. Burkart and B. Steffen. Model Checking for Context-Free Processes. In CONCUR ’92, LNCS 630, pages 123–137. Springer, 1992.

[BS95] O. Burkart and B. Steffen. Composition, Decomposition and Model-Checking of Pushdown Processes. Nordic Journal of Computing, 2:89–125, 1995.

[Cau96] D. Caucal. On Infinite Transition Graphs Having a Decidable Monadic Theory. In ICALP ’96, LNCS 1099, pages 194–205. Springer, 1996.

[CKS92] R. Cleaveland, M. Klein, and B. Steffen. Faster Model Checking for the Modal Mu-Calculus. In CAV ’92, LNCS 663, pages 410–422, 1992.

[Cou90] B. Courcelle. Graph Rewriting: An Algebraic and Logic Approach. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 5, pages 193–242. Elsevier Science Publisher B.V., 1990.

[EK95] J. Esparza and A. Kiehn. On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes. In CAV ’95, LNCS 939, pages 353–366. Springer, 1995.

[Esp94] J. Esparza. On the Decidability of Model Checking for Several μ-calculi and Petri Nets. In CAAP ’94, LNCS 787, pages 115–129. Springer, 1994.

[Esp96] J. Esparza. More Infinite Results. In INFINITY ’96, MIP-9614, pages 4–20. Universität Passau, July 1996.

[HS94] H. Hungar and B. Steffen. Local Model-Checking for Context-Free Processes. Nordic Journal of Computing, 1(3):364–385, 1994.

[JW96] D. Janin and I. Walukiewicz. On the Expressive Completeness of the Propositional mu-Calculus wrt. Monadic Second Order Logic. In CONCUR ’96, LNCS 1119, pages 263–277. Springer, 1996.

[Koz83] D. Kozen. Results on the Propositional μ-Calculus. Theoretical Computer Science, 27:333–354, 1983.

[LBC^{+}94] D.E. Long, A. Browne, E.M. Clarke, S. Jha, and W.R. Marrero. An Improved Algorithm for the Evaluation of Fixpoint Expressions. In CAV ’94, LNCS 818, pages 338–350. Springer, 1994.

[MS85] D.E. Muller and P.E. Schupp. The Theory of Ends, Pushdown Automata, and Second-Order Logic. Theoretical Computer Science, 37:51–75, 1985.

[Rab69] R.O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the AMS, 141:1–35, 1969.

[Wal96] I. Walukiewicz. Pushdown Processes: Games and Model-Checking. In CAV ’96, LNCS 1102. Springer, 1996.