BRICS RS-01-19 J. Srba: On the Power of Labels in Transition Systems BRICS

Basic Research in Computer Science

On the Power of Labels in Transition Systems

Jiří Srba BRICS Report Series RS-01-19 ISSN 0909-0878 June 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Jiří Srba.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/19/

On the Power of Labels in Transition Systems^{⋆}

Jiří Srba^{⋆⋆}
BRICS^{⋆ ⋆ ⋆}

Department of Computer Science University of Aarhus Denmark

                        srba@brics.dk

Abstract. In this paper we discuss the role of labels in transition systems with regard to bisimilarity and model checking problems. We suggest a general reduction from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of μ-calculus formulas. We apply the reduction to the class of transition systems generated by Petri nets and pushdown automata, and obtain several decidability/complexity corollaries for unlabelled systems. Probably the most interesting result is undecidability of strong bisimilarity for unlabelled Petri nets.

1 Introduction

Formal methods for verification of infinite-state systems have been an active area of research with a number of positive decidability results. In particular, verification techniques for concurrent systems defined by process algebras like CCS [Mil89], ACP [BW90] or CSP [Hoa85], pushdown systems, Petri nets, process rewrite systems [May00b] and others have attracted a lot of attention. There are two central questions about decidability (complexity) of equivalence and model checking problems:

– Equivalence checking (see [Mol96]): Given two (infinite-state) systems, are they equal with regard to some equivalence notion?

– Model checking (see [BE97]):

Given an (infinite-state) transition system and a formula ϕ of some suitable logic, does the system satisfy the property described by ϕ?

⋆ Full and extended version of [Srb01]. ⋆⋆ The author is supported in part by the GACR, grant No. 201/00/0400.

⋆ ⋆ ⋆

Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Both these problems have an interesting and unifying aspect in common. They can be defined independently on the computational model by means of labelled transition systems. All the models mentioned above give rise to a certain type of (infinite) labelled transition system and this is considered to be their desired semantics. Equivalence and model checking problems can be defined purely in terms of these transition systems.

In the first part of the paper we discuss the role of labels of such transition systems. There are two aspects of the branching structure described by a labelled transition system T. First, given a state of T, there can be several outgoing edges with different labels. Second, given a state of T and a label a, there can be several outgoing edges under the same label a. We claim that for our purposes only the second property is the essential one. In other words, given a labelled transition system, we can construct another transition system where all edges are labelled by the same label, i.e., the labels are in fact completely irrelevant. We call such systems unlabelled transition systems. What is important is the fact that our construction preserves the answers to both the questions we are interested in — equivalence checking (and we have chosen strong bisimilarity as the notion of equivalence) and model checking with action-based modal μ-calculus as the chosen logic for expressing properties of labelled transition systems.

In the second part we focus on two specific classes of infinite-state systems, namely Petri nets and pushdown systems. Petri nets are a typical example of fully parallel models of computation, whereas pushdown systems can model sequential stack-like process behaviours. Both Petri nets and pushdown systems generate (in general infinite) labelled transition systems. The question is whether the transformed unlabelled transition systems (given by the construction mentioned in the previous paragraph) are still definable by the chosen formalism of Petri nets resp. pushdown automata. The answer is shown to be positive for both our models — there are even polynomial time transformations. This implies several decidability/complexity results about bisimilarity and model checking problems for unlabelled Petri nets and pushdown systems.

Probably the most interesting corollary is the application of the transformation to Petri nets. We prove that strong bisimilarity for unlabelled Petri nets (where the set of labels is a singleton set) is undecidable. This is stronger result than undecidability of strong bisimilarity for labelled Petri nets given by Jancar [Jan95]. The undecidability for unlabelled Petri nets contrasts to a positive decidability result for the subclass of Petri nets which are deterministic [Jan95,Vog92], i.e., for any marking M and a label a there is at most one outgoing transition from M labelled by a. This again demonstrates that the role of labels is not important for decidability questions and what is crucial is the branching structure induced by transitions with the same label.

In the end we briefly discuss other popular process algebras — BPA (Basic Process Algebra) [BK85] and BPP (Basic Parallel Process) [Chr93]. BPA is a strict subclass of pushdown systems and BPP is a strict subclass of Petri nets (also called communication-free Petri nets). Unfortunately, it is sketched that these models — unlike pushdown systems and Petri nets — are not strong enough to express deadlock behaviour which is essential for the transformation. In other words, the corresponding unlabelled transition system of a given BPA (BPP) transition graph is not necessarily definable in the BPA (BPP) syntax.

2 Basic definitions

First, we define labelled transition systems [Plo81,Mol96].

Definition 1 (Labelled transition system). A labelled transition system is a triple T = (S, Act, ⟶) where

– S is a set of states (or processes)

– Act is a set of labels (or actions) such that S ∩ Act = ∅ and

– ⟶⊆ S × Act × S is a transition relation, written α ⟶^{a} β for (α, a, β) ∈⟶.

In what follows we assume that Act is a finite set. As usual we extend the transition relation to the elements of Act^{∗} (α ⟶^{ϵ} α and inductively

α ⟶^{aw} β iff ∃γ : α ⟶^{a} γ and γ ⟶^{w} β where α, β, γ ∈ S, a ∈ Act and

w ∈ Act^{∗}). We also write α ⟶^{∗} β iff ∃w ∈ Act^{∗} such that α ⟶^{w} β. A state β is reachable from a state α, iff α ⟶^{∗} β. Moreover, we write α −̸→ for α ∈ S iff there is no β ∈ S and a ∈ Act such that α ⟶^{a} β.

We call a labelled transition system T normed iff ∀s ∈ S. ∃s′ ∈ S such that s ⟶^{∗} s′ −̸→.

Definition 2. Let T = (S, Act, ⟶) be a labelled transition system and s ∈ S. By T_{s} we denote a labelled transition system restricted to states of T reachable from s. More precisely, T_{s} = (S_{s}, Act, ⟶_{s}) where S_{s} =

{s′ ∈ S | s ⟶^{∗} s′} and s_{1} ⟶^{a}_{s} s_{2} iff s_{1} ⟶^{a} s_{2} and s_{1}, s_{2} ∈ S_{s}.

Now, we introduce the notion of (strong) bisimilarity [Par81,Mil89].

Definition 3 (Bisimulation). Let T = (S, Act, ⟶) be a labelled transition system. A binary relation R ⊆ S × S is a relation of bisimulation iff whenever (α, β) ∈ R then for each a ∈ Act:

– if α ⟶^{a} α′ then β ⟶^{a} β′ for some β′ such that (α′, β′) ∈ R

– if β ⟶^{a} β′ then α ⟶^{a} α′ for some α′ such that (α′, β′) ∈ R.

Two states α, β ∈ S are bisimilar in T, written α ∼_{T} β, iff there is a bisimulation R such that (α, β) ∈ R.

Bisimilarity has also an elegant characterisation in terms of bisimulation games [Tho93,Sti95]. A bisimulation game on a pair of states α, β ∈ S is a two-player game of an “attacker” and a “defender”. The attacker chooses one of the states and makes an ⟶^{a}-move for some a ∈ Act. The defender must respond by making an ⟶^{a}-move from the other state under the same label a. Now the game repeats, starting from the new processes. If one player cannot move, the other player wins. If the game is infinite, the defender wins. States α and β are bisimilar iff the defender has a winning strategy (and non-bisimilar iff the attacker has a winning strategy).

We introduce unlabelled transition systems in the following definition.

Definition 4 (Unlabelled transition system). Let T = (S, Act, ⟶) be a labelled transition system. We call T unlabelled transition system whenever Act is a singleton set, i.e., |Act| = 1.

Remark 1. If it is the case that |Act| = 1 then (for our purposes) we simply write ⟶ instead of ⟶^{a}. We also forget about the second component in the definition of a labelled transition system, i.e., we can denote an unlabelled transition system by T = (S, ⟶) where ⟶⊆ S × S.

Now, we define a powerful logic for labelled transition systems — modal μ-calculus [Koz83,Pra82].

Definition 5 (Syntax of modal μ-calculus). Let Var be a set of variables and Act a set of action labels such that Var ∩ Act = ∅. The syntax of modal μ-calculus is defined as follows:

ϕ ::= tt | X | ϕ_{1} ∧ ϕ_{2} | ¬ϕ | ⟨a⟩ϕ | μX.ϕ

where tt stands for “true”, X ranges over Var and a over Act. There is a standard restriction on the formulas: we consider only formulas where each occurrence of a variable X is within a scope of an even number of negation symbols.

Given a labelled transition system T = (S, Act, ⟶), we interpret a formula ϕ as follows. Assume a valuation Val : Var → 2^{S}.

\begin{aligned}[[tt]]_{Val,T} & = & S \\ [[X]]_{Val,T} & = & Val(X) \\ [[ϕ_{1} ∧ ϕ_{2}]]_{Val,T} & = & [[ϕ_{1}]]_{Val,T} ∩ [[ϕ_{2}]]_{Val,T} \\ [[¬ϕ]]_{Val,T} & = & S ∖ [[ϕ]]_{Val,T} \\ [[⟨a⟩ϕ]]_{Val,T} & = & \{s | ∃s′. (s ⟶^{a} s′ ∧ s′ ∈ [[ϕ]]_{Val,T})\} \\ [[μX.ϕ]]_{Val,T} & = & ⋂\{S′ ⊆ S | [[ϕ]]_{Val[S′/X],T} ⊆ S′\} \end{aligned}

Here Val[S′/X] stands for a valuation function such that Val[S′/X](X) = S′ and Val[S′/X](Y) = Val(Y) for X ≠ Y. We say that a formula ϕ is satisfied in a state s of T, and we write T, s ⊧ ϕ, if for all valuations Val we have s ∈ [[ϕ]]_{Val,T}.

Remark 2. The logic defined above without the fixed-point operator μX.ϕ is called Hennessy-Milner logic [HM85].

3 From labelled to unlabelled transition systems

In this section we present a transformation from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of μcalculus formulas.

Let T = (S, Act, ⟶) be a labelled transition system. We define a transformed unlabelled transition system T̂ = (Ŝ, ⟶). We reuse the relation symbol ⟶ without causing confusion, since in the system T it is a ternary relation and in T̂ it is a binary relation. Without loss of generality we assume that Act = {1, 2, …, n} for some n > 0. We define the system T̂ = (Ŝ, ⟶) as follows:

Ŝ = S ∪ {r_{(s,a,s′)}^{k} | 0 ≤ k ≤ a ∧ s ⟶^{a} s′} ∪

{d_{s}^{k} | s ∈ S ∧ 0 ≤ k ≤ n}

⟶ = {(s, r_{(s,a,s′)}^{0}), (r_{(s,a,s′)}^{0}, s′) | s ⟶^{a} s′} ∪

{(r_{(s,a,s′)}^{k}, r_{(s,a,s′)}^{k+1}) | s ⟶^{a} s′ ∧ 0 ≤ k < a} ∪

{(s, d_{s}^{0}) | s ∈ S} ∪

{(d_{s}^{k}, d_{s}^{k+1}) | s ∈ S ∧ 0 ≤ k < n}.

For a better understanding of the transformation take a look at Figure 1 where a way how to transform a transition s ⟶^{a} s′ is drawn. The idea consists in splitting each transition s ⟶^{a} s′ labelled by a ∈ ℕ_{0} with an intermediate state (the r_{(s,a,s′)}^{0} state) out of which goes a newly added

[figure: s; a; s′; ⇓; d_{s}^{n}; …; d_{s}^{0}; d_{s′}^{0}; …; d_{s′}^{n}; s; r_{(s,a,s′)}^{0}; s′; r_{(s,a,s′)}^{1}; r_{(s,a,s′)}^{2}; …; …; r_{(s,a,s′)}^{a}]

Fig. 1. Transformation of a transition s ⟶^{a} s′

linear path of length a. The d_{s} states add a linear path of length n + 1 to each state from S and serve for distinguishing the r-states from the original ones.

Notice that if T is a finite-state system then the size of T̂ is polynomially bounded by the size of T. In fact, we could add only one linear path of length n + 1 with appropriate links into the path starting in the states from S and in the r^{0}-states. However, for technical convenience in Section 4, we use the previously described construction.

Remark 3. It is an easy observation that T̂ is a normed transition system.

3.1 Bisimilarity

Let T = (S, Act, ⟶) be a labelled transition system and let s ∈ S. We define a set of finite norms of s by

N (s) = {|w| | ∃s′ ∈ S : s ⟶^{w} s′ −̸→}

where |w| is the length of w. The following proposition is a standard one.

Proposition 1. Let T = (S, Act, ⟶) be a labelled transition system and s_{1}, s_{2} ∈ S. Then s_{1} ∼_{T} s_{2} implies that N (s_{1}) = N (s_{2}).

Our aim is to show that for a pair of states s_{1} and s_{2} of a labelled transition system T holds that s_{1} ∼_{T} s_{2} if and only if s_{1} ∼T̂ s_{2}.

Lemma 1. Let T = (S, Act, ⟶) be a labelled transition system and s_{1}, s_{2} ∈ S be a pair of states. If s_{1} ∼_{T} s_{2} then s_{1} ∼T̂ s_{2}.

Proof. Suppose that the defender has a winning strategy in T starting from the pair s_{1} and s_{2}. We show that the defender in T̂ has also a winning strategy starting from the pair s_{1} and s_{2}. Any attacker’s move in T̂ of the form s_{i} ⟶ d_{s_{i}}^{0} (for i ∈ {1, 2}) can be matched by a defender’s move s_{3−i} ⟶ d_{s_{3−i}}^{0}. The states d_{s_{1}}^{0} and d_{s_{2}}^{0} are trivially bisimilar. Let the attacker’s move in T̂ be s_{i} ⟶ r_{(s_{i},a,s′_{i})}^{0} for i ∈ {1, 2}. Of course, the

following attacker’s move is possible in T as well: s_{i} ⟶^{a} s′_{i}. We assume defender’s answer in T by performing s_{3−i} ⟶^{a} s′_{3−i} such that

s′_{1} ∼_{T} s′_{2}.  (1)

The defender’s response in T̂ is then s_{3−i} ⟶ r_{(s_{3−i},a,s′_{3−i})}^{0}. Now the game

in T̂ continues from the states r_{(s_{1},a,s′_{1})}^{0} and r_{(s_{2},a,s′_{2})}^{0}. Given i ∈ {1, 2}, only two transitions are possible from r_{(s_{i},a,s′_{i})}^{0}. Either the attacker can choose r_{(s_{i},a,s′_{i})}^{0} ⟶ s′_{i} or r_{(s_{i},a,s′_{i})}^{0} ⟶ r_{(s_{i},a,s′_{i})}^{1}. If he chooses the second option then he looses since the defender answers with r_{(s_{3−i},a,s′_{3−i})}^{0} ⟶ r_{(s_{3−i},a,s′_{3−i})}^{1} and these reached states are easily seen to be bisimilar. Should the attacker’s choice be r_{(s_{i},a,s′_{i})}^{0} ⟶ s′_{i} then the defender’s answer is r_{(s_{3−i},a,s′_{3−i})}^{0} ⟶ s′_{3−i}. Since s′_{1}, s′_{2} ∈ S and the defender in T has a winning strategy from these states because of (1), we have established a winning strategy for the defender in T̂. ⊓ ⊔

Before showing the other implication, we prove the following property.

Property 1. The attacker in T̂ has a winning strategy from any pair of states s_{1}, s_{2} ∈ Ŝ such that s_{1} ∉ S and s_{2} ∈ S, or s_{1} ∈ S and s_{2} ∉ S.

Proof. Assume w.l.o.g. that s_{1} ∉ S and s_{2} ∈ S. The other case is symmetric. There are three possibilities if s_{1} ∉ S.

– Let s_{1} = d_{s}^{k} for some s ∈ S and 0 ≤ k ≤ n, or s_{1} = r_{(s,a,s′)}^{k} for some s, s′ ∈ S, a ∈ Act and 0 < k ≤ a. In both these cases n + 1 ∉ N (s_{1}) and n + 1 ∈ N (s_{2}). Because of Proposition 1 we get s_{1} ≁T̂ s_{2} and the attacker in T̂ has a winning strategy.

– Let s_{1} = r_{(s,a,s′)}^{0} for some s, s′ ∈ S and a ∈ Act. Now the attacker has the following winning strategy in T̂. He makes a move r_{(s,a,s′)}^{0} ⟶ r_{(s,a,s′)}^{1}. Assume a defender’s answer s_{2} ⟶ s′_{2} for an arbitrary s′_{2} ∈ Ŝ. Obviously either n ∈ N (s′_{2}) or n + 2 ∈ N (s′_{2}) and max [N (r_{(s,a,s′)}^{1})] < n. Again, using Proposition 1, the attacker has a winning strategy. ⊓ ⊔ Lemma 2. Let T = (S, Act, ⟶) be a labelled transition system and s_{1}, s_{2} ∈ S be a pair of states. If s_{1} ∼T̂ s_{2} then s_{1} ∼_{T} s_{2}.

Proof. Knowing that the defender has a winning strategy in T̂ from s_{1} and s_{2}, we establish a winning strategy for the defender in T from s_{1} and s_{2}. Suppose that the attacker’s move in T is s_{i} ⟶^{a} s′_{i} for i ∈ {1, 2}. Then it is possible to perform a series of two moves s_{i} ⟶ r_{(s_{i},a,s′_{i})}^{0} ⟶ s′_{i} in T̂.

Because of Property 1, the defender in T̂ has a response to this series of moves only by performing s_{3−i} ⟶ r_{(s_{3−i},b,s′_{3−i})}^{0} ⟶ s′_{3−i} for some b ∈ Act and s′_{3−i} ∈ S where

s′_{1} ∼T̂ s′_{2}.  (2)

Notice that a = b, otherwise the attacker has a winning strategy in T̂ from r_{(s_{i},a,s′_{i})}^{0} and r_{(s_{3−i},b,s′_{3−i})}^{0} by performing a move r_{(s_{i},a,s′_{i})}^{0} ⟶ r_{(s_{i},a,s′_{i})}^{1}. Using Property 1, the defender must answer with r_{(s_{3−i},b,s′_{3−i})}^{0} ⟶ r_{(s_{3−i},b,s′_{3−i})}^{1}. However, the attacker has a winning strategy now since a−1 ∈ N (r_{(s_{i},a,s′_{i})}^{1}) and a−1 ∉ N (r_{(s_{3−i},b,s′_{3−i})}^{1}) whenever a ≠ b — Proposition 1. This implies

that the defender in T can perform s_{3−i} ⟶^{a} s′_{3−i} and because of (2), the defender in T has a winning strategy from s′_{1} and s′_{2}. Thus s_{1} ∼_{T} s_{2}. ⊓ ⊔

From Lemma 1 and Lemma 2 we can conclude with the following theorem.

Theorem 1. Let T = (S, Act, ⟶) be a labelled transition system and s_{1}, s_{2} ∈ S be a pair of states. Let T̂ be the corresponding unlabelled transition system. Then

s_{1} ∼_{T} s_{2} if and only if s_{1} ∼T̂ s_{2}.

3.2 Model checking

We turn our attention to the model checking problem now. We show that there is a polynomial time transformation of any μ-calculus formula ϕ into ϕ̂ such that T, s ⊧ ϕ iff T̂, s ⊧ ϕ̂. When interpreting a μ-calculus formula on an unlabelled transition system T̂, we write ♢ instead of ⟨a⟩, since a ∈ Act is the only label and hence it is irrelevant. We also define a dual operator □ as □ϕ ≡ ¬♢¬ϕ and ff as ff ≡ ¬tt.

Let T = (S, Act, ⟶) be a labelled transition system such that Act = {1, 2, …, n} and let T̂ = (Ŝ, ⟶) be the corresponding unlabelled system. First of all, we write a formula L(a) such that

[[L(a)]]_{Val′,T̂} = {r_{(s,a,s′)}^{0} | ∃s, s′ ∈ S : s ⟶^{a} s′}  (3)

for any valuation Val′ : Var → 2Ŝ. We define

L(a) ≡ ♢^{n+1}tt ∧ ♢(□^{a}ff ∧ ♢^{a−1}tt)

where ♢^{0}ϕ ≡ ϕ and ♢^{k+1}ϕ ≡ ♢(♢^{k}ϕ), and similarly □^{0}ϕ ≡ ϕ and □^{k+1}ϕ ≡ □(□^{k}ϕ).

Let T̂, s_{1} ⊧ L(a). The left subformula in L(a), namely ♢^{n+1}tt, ensures that the state s_{1} is not of the form r_{(s,b,s′)}^{k} for k > 0, nor of the form d_{s}^{k} for k ≥ 0. The second subformula in the conjunction says that there is a one step transition from s_{1}, reaching a state s′_{1} of the form r_{(s,b,s′)}^{1} — should s′_{1} ∈ S, or s′_{1} be of the form r_{(s,b,s′)}^{0}, or s′_{1} be of the form d_{s}^{0}, then the formula □^{a}ff can never be satisfied. Moreover, the formula □^{a}ff guarantees that there are at most a − 1 transitions from r_{(s,b,s′)}^{1} and the formula ♢^{a−1}tt finally ensures that at least a − 1 transitions can be performed from r_{(s,b,s′)}^{1}. Hence a = b and (3) is established.

Let us consider another formula called State and defined by

State ≡ ♢tt ∧ □♢^{n}tt.

Obviously, [[State]]_{Val′,T̂} = S for any valuation Val′ : Var → 2Ŝ. We are now ready to define ϕ̂ for a given μ-calculus formula ϕ. The definition follows:

\begin{aligned}t̂t & = & tt ∧ State \\ X̂ & = & X ∧ State \\ { \atop ϕ_{1} ∧ ϕ_{2}} & = & ϕ̂_{1} ∧ ϕ̂_{2} ∧ State \\ ˆ¬ϕ & = & ¬ϕ̂ ∧ State \\ { \atop μX.ϕ} & = & (μX.ϕ̂) ∧ State \\ ˆ⟨a⟩ϕ & = & ♢(L(a) ∧ ♢ϕ̂) ∧ State. \end{aligned}

Theorem 2. Let T = (S, Act, ⟶) be a labelled transition system and s ∈ S. Let ϕ be a μ-calculus formula. Then

T, s ⊧ ϕ if and only if T̂, s ⊧ ϕ̂.

Proof. By structural induction on ϕ we prove that

[[ϕ]]_{Val,T} = [[ϕ̂]]_{Val′,T̂}  (4)

for arbitrary valuations Val : Var → 2^{S} and Val′ : Var → 2Ŝ such that Val(X) = Val′(X) ∩ S for all X ∈ Var.

Base case:

– Case tt. Obviously, [[tt]]_{Val,T} = S = [[tt]]_{Val′,T̂} ∩ S = [[tt ∧ State]]_{Val′,T̂}.

– Case X. Because of our assumptions on Val and Val′ we get [[X]]_{Val,T} = Val(X) = Val′(X) ∩ S = [[X ∧ State]]_{Val′,T̂}.

Inductive step:

– Case ϕ_{1} ∧ ϕ_{2}. By definition [[ϕ_{1} ∧ ϕ_{2}]]_{Val,T} = [[ϕ_{1}]]_{Val,T} ∩ [[ϕ_{2}]]_{Val,T}. Using induction hypothesis this equals to [[ϕ̂_{1}]]_{Val′,T̂} ∩ [[ϕ̂_{2}]]_{Val′,T̂} which gives again by definition [[ϕ̂_{1} ∧ ϕ̂_{2}]]_{Val′,T̂}. Since [[ϕ_{1} ∧ ϕ_{2}]]_{Val,T} = [[ϕ̂_{1} ∧ ϕ̂_{2}]]_{Val′,T̂} ⊆ S, we get [[ϕ̂_{1} ∧ ϕ̂_{2}]]_{Val′,T̂} = [[ϕ̂_{1} ∧ ϕ̂_{2} ∧ State]]_{Val′,T̂} which equals to [[{ \atop ϕ_{1} ∧ ϕ_{2}}]]_{Val′,T̂}.

– Case ¬ϕ. By definition [[¬ϕ]]_{Val,T} = S ∖ [[ϕ]]_{Val,T}. Using induction hypothesis this equals to S ∖ [[ϕ̂]]_{Val′,T̂} which is the same as (Ŝ ∖ [[ϕ̂]]_{Val′,T̂}) ∩ S = [[¬ϕ̂]]_{Val′,T̂} ∩ S = [[¬ϕ̂ ∧ State]]_{Val′,T̂}. This is by definition [[ ˆ¬ϕ]]_{Val′,T̂}.

– Case μX.ϕ. By definition we know that [[μX.ϕ]]_{Val,T} = ⋂{S′ ⊆ S | [[ϕ]]_{Val[S′/X],T} ⊆ S′} and this equals by induction hypothesis to ⋂{S′ ⊆ S | [[ϕ̂]]_{Val′[S′/X],T̂} ⊆ S′}. Notice that [[ϕ̂]]_{Val′[S′/X],T̂} = [[ϕ̂]]_{Val′[S′′/X],T̂} ⊆ S for any S′ ⊆ S and S′′ ⊆ Ŝ such that S′ = S′′ ∩ S. Thus ⋂{S′ ⊆ S | [[ϕ̂]]_{Val′[S′/X],T̂} ⊆ S′} = ⋂{S′′ ⊆ Ŝ | [[ϕ̂]]_{Val′[S′′/X],T̂} ⊆ S′′} ∩ S. This is the same as [[(μX.ϕ̂) ∧ State]]_{Val′,T̂} and equals by definition to

[[{ \atop μX.ϕ}]]_{Val′,T̂}.

– Case ⟨a⟩ϕ. First, we show that [[⟨a⟩ϕ]]_{Val,T} ⊆ [[ ˆ⟨a⟩ϕ]]_{Val′,T̂}. Let s ∈ [[⟨a⟩ϕ]]_{Val,T} which means that there is some s′ ∈ S such that s ⟶^{a} s′ and s′ ∈ [[ϕ]]_{Val,T}. By induction hypothesis s′ ∈ [[ϕ̂]]_{Val′,T̂}. We show that s ∈ [[ ˆ⟨a⟩ϕ]]_{Val′,T̂}. However, r_{(s,a,s′)}^{0} ∈ [[♢ϕ̂]]_{Val′,T̂}. Moreover, r_{(s,a,s′)}^{0} ∈ [[L(a)]]_{Val′,T̂} using (3) and of course s ∈ [[State]]_{Val′,T̂}. This implies that s ∈ [[♢(L(a) ∧ ♢ϕ̂) ∧ State]]_{Val′,T̂} = [[ ˆ⟨a⟩ϕ]]_{Val′,T̂}. Second, we show that [[ ˆ⟨a⟩ϕ]]_{Val′,T̂} ⊆ [[⟨a⟩ϕ]]_{Val,T}. Let s ∈ [[ ˆ⟨a⟩ϕ]]_{Val′,T̂} = [[♢(L(a)∧♢ϕ̂)∧State]]_{Val′,T̂} which means that s ∈ S and s ⟶ s′′ such that s′′ ∈ [[L(a) ∧ ♢ϕ̂]]_{Val′,T̂}. Because of (3) we know that s′′ = r_{(s,a,s′)}^{0} for some s′ ∈ S. We remind that r_{(s,a,s′)}^{0} ⟶ s′. Since [[ϕ̂]]_{Val′,T̂} ⊆ S and r_{(s,a,s′)}^{1} ∉ S, we get that s′ ∈ [[ϕ̂]]_{Val′,T̂}. This implies by induction hypothesis that s′ ∈ [[ϕ]]_{Val,T} and moreover s ⟶^{a} s′. Hence s ∈ [[⟨a⟩ϕ]]_{Val,T}.

Thus we have established (4) and proved the theorem. ⊓ ⊔

Remark 4. Let us consider temporal operators EF ϕ and EGϕ defined by EF ϕ ≡ μX.ϕ ∨ ⟨−⟩X and EGϕ ≡ ¬μX.¬ϕ ∨ (¬⟨−⟩¬X ∧ ⟨−⟩tt) where ⟨−⟩ϕ ≡ ⋁_{a∈Act} ⟨a⟩ϕ. We define the transformed formulas { \atop EF ϕ} (using only EF operator) and { \atop EGϕ} (using only EG operator) as follows:

\begin{aligned}{ \atop EF ϕ} & = & EF ϕ̂ ∧ State \\ { \atop EGϕ} & = & EG ((State ∨ ⋁_{a∈Act} L(a)) ∧ State ⟹ ϕ̂) ∧ State. \end{aligned}

Note that still [[ϕ̂]]_{Val′,T̂} ⊆ S for any formula ϕ and any valuation Val′ :

Var → 2Ŝ. Let s ∈ S. Then T, s ⊧ EF ϕ iff T̂, s ⊧ { \atop EF ϕ}. If moreover T_{s}

satisfies condition

∀s′ ∈ S_{s}. ∃s′′ ∈ S_{s}. ∃a ∈ Act : s′ ⟶^{a} s′′  (5)

then T, s ⊧ EGϕ iff T̂, s ⊧ { \atop EGϕ}. This enables to transform formulas of even weaker logics than modal μ-calculus (such as Hennessy-Milner logic, possibly equipped with the operator EF, respectively EG) into unlabelled formulas of the same logic. Hennessy-Milner logic with the operators EF and EG is called unified system of branching-time logic (UB) [BAMP83] and the fragments of UB containing only the operator EF ϕ (EGϕ) are referred to as EF -logic (EG-logic).

Similarly, the until operators E [ϕUψ] and A [ϕUψ] of CTL [CE81]

— defined by E [ϕUψ] ≡ μX.ψ ∨ (ϕ ∧ ⟨−⟩X) and A [ϕUψ] ≡ μX.ψ ∨ (ϕ ∧ ⟨−⟩tt ∧ ¬⟨−⟩¬X) — can be transformed:

\begin{aligned}{ \atop E [ϕUψ]} & = & E [(State ⟹ ϕ̂) U ψ̂] ∧ State \\ { \atop A [ϕUψ]} & = & χ̂^{AU} where χ^{AU} = ¬(E [¬ψ U (¬ϕ ∧ ¬ψ)] ∨ EG(¬ψ)). \end{aligned}

In the case of A [ϕUψ] we use the equivalence A [ϕUψ] ⟺ χ^{AU} from [CES86]. Again, for any s ∈ S it holds that T, s ⊧ E [ϕUψ] iff

T̂, s ⊧ { \atop E [ϕUψ]}. Moreover T, s ⊧ A [ϕUψ] iff T̂, s ⊧ { \atop A [ϕUψ]} under

the assumption of condition (5). This enables to transform also the logic CTL.

4 Applications

In this section we show how the previous results can be applied to equivalence/model checking of infinite-state systems. We focus in particular on a typical representative of parallel models — Petri nets (see e.g. [Pet81])

— and sequential processes — pushdown systems (see e.g. [Mol96]). We have to show that the class of transition systems generated by these models is closed under the transformation from labelled to unlabelled systems as presented in the previous section.

Let us now define bisimilarity and model checking problems.

Problem: Bisimilarity checking problem

Instance: Labelled transition system T = (S, Act, ⟶) and

s_{1}, s_{2} ∈ S.

Question: s_{1} ∼_{T} s_{2} ?

Problem: Model checking problem with logic L Instance: Labelled transition system T = (S, Act, ⟶), s ∈ S and a formula ϕ of the logic L.

Question: T, s ⊧ ϕ ?

First of all, we remind the reader of the fact that our transformation works immediately for finite-state transition systems. In the following corollary we consider the model checking problem with these logics: Hennessy-Milner logic, EF -logic, EG-logic, UB, CTL and modal μ-calculus.

Corollary 1. Let T = (S, Act, ⟶) be a finite-state labelled transition system, i.e., |S|, |Act| < ∞. There is a polynomial time reduction from the bisimilarity (model) checking problem for T to the bisimilarity (model) checking problem for T̂, where T̂ is an unlabelled (and finite-state) transition system.

Proof. Immediately from Theorem 1, Theorem 2 and Remark 4. In the case of EG-logic, UB and CTL we can ensure the validity of condition (5) of Remark 4 by adding a self-loop s ⟶^{u} s (u is a fresh action) to every state s ∈ S such that s −̸→. This does not influence satisfiability of EG, UB and CTL formulas. ⊓ ⊔

4.1 Petri nets

It is a well known fact that the bisimilarity checking problem is undecidable for labelled Petri nets [Jan95]. The technique of the proof is based on a reduction from the counter machine of Minsky [Min67] and the labelling is essential for the reduction. It is also known that bisimilarity is decidable for the class of Petri nets which are deterministic up to bisimilarity [Jan95], i.e., F-deterministic nets of Vogler [Vog92]. Bisimilarity between a labelled Petri net and a finite-state system is decidable [JM95,JKM98] and EXPSPACE-hard (see e.g. comments in [May00a]).

Model checking of even weak temporal logics on labelled transition systems generated by Petri nets is quite pessimistic. The only decidable logic is (trivially) Hennessy-Milner logic. The EF -logic is undecidable [Esp97] and model checking with EG is also undecidable, even for BPP [EK95] — BPP is a strict subclass of labelled Petri nets where each transition has exactly one input place.

We examine the bisimilarity and model checking problems for unlabelled Petri nets in this subsection.

Definition 6 (Labelled Petri net). A labelled Petri net is a tuple N = (P, T, F, L, λ), where P is a finite set of places, T is a finite set of transitions such that T ∩ P = ∅, F ⊆ (P × T) ∪ (T × P) is a flow relation, L is a finite set of labels and λ : T → L is a labelling function.

A marking M of a net N is a mapping M : P → ℕ_{0}, i.e., each place is assigned a nonnegative number of tokens. We define ^{•}t = {p | (p, t) ∈ F } and t^{•} = {p | (t, p) ∈ F } for a transition t ∈ T. We say that t ∈ T is enabled in a marking M iff ∀p ∈ ^{•}t. M(p) > 0. If t is enabled in M then it can be fired, producing a marking M′ such that:

– M′(p) = M(p) for all p ∈ (P ∖ (^{•}t ∪ t^{•})) ∪ (^{•}t ∩ t^{•})

– M′(p) = M(p) − 1 for all p ∈ ^{•}t ∖ t^{•}

– M′(p) = M(p) + 1 for all p ∈ t^{•} ∖^{•}t.

Then we write M[t⟩M′. Without loss of generality we assume that if M[t_{1}⟩M′ and M[t_{2}⟩M′ then λ(t_{1}) ≠ λ(t_{2}) for any pair of markings M, M′ and transitions t_{1} and t_{2}.

Definition 7 (Labelled transition system T (N)). Let N = (P, T, F, L, λ) be a labelled Petri net. We define a corresponding labelled transition system T (N) as T (N) = ([P → ℕ_{0}], L, ⟶) where M ⟶^{a} M′ whenever M[t⟩M′ and a = λ(t) for M, M′ ∈ [P → ℕ_{0}] and t ∈ T.

Now, we define unlabelled Petri nets.

Definition 8 (Unlabelled Petri net). An unlabelled Petri net is a labelled Petri net N = (P, T, F, L, λ) such that |L| = 1.

Remark 5. Whenever |L| = 1, let us say L = {a}, we can omit L and λ from the definition of the net N and instead of M ⟶^{a} M′ in T (N) we simply write M ⟶ M′.

Let N = (P, T, F, L, λ) be a labelled Petri net. Without loss of generality assume that L = {1, …, n} for some n > 0. We construct an unlabelled Petri net N′ = (P′, T′, F′) and a mapping ψ : (P → ℕ_{0}) → (P′ → ℕ_{0}) such that { \atop T (N)_{M_{1}}} and T (N′)_{ψ(M_{1})} are isomorphic unlabelled transition systems for any marking M_{1} of N. Let us recall that { \atop T (N)_{M_{1}}} is the transition system restricted to markings reachable from M_{1} and T (N′)_{ψ(M_{1})} is restricted to markings reachable from ψ(M_{1}) — see Definition 2. The net N′ is defined as follows:

P′ = P ∪ {p_{t}^{k} | t ∈ T ∧ 0 ≤ k ≤ λ(t)} ∪ {p_{c}} ∪ {d^{k} | 0 ≤ k ≤ n}
T′ = {t^{in}, t^{out} | t ∈ T } ∪ {l_{t}^{k} | t ∈ T ∧ 0 ≤ k < λ(t)} ∪ {l^{k} | 0 ≤ k ≤ n}
F′ = {(p, t^{in}) | (p, t) ∈ F } ∪ {(t^{out}, p) | (t, p) ∈ F } ∪
{(t^{in}, p_{t}^{0}), (p_{t}^{0}, t^{out}) | t ∈ T } ∪
{(p_{t}^{k}, l_{t}^{k}), (l_{t}^{k}, p_{t}^{k+1}) | t ∈ T ∧ 0 ≤ k < λ(t)} ∪
{(p_{c}, t^{in}), (t^{out}, p_{c}) | t ∈ T } ∪
{(p_{c}, l^{0})} ∪ {(l^{k}, d^{k}), (d^{k}, l^{k+1}) | 0 ≤ k < n} ∪ {(l^{n}, d^{n})}.

In this construction each transition t with input places p_{1}, …, p_{k_{1}} and output places q_{1}, …, q_{k_{2}} is transformed into a set of transitions shown in Figure 2. Now, we give the mapping ψ. Let M ∈ (P → ℕ_{0}). Then ψ(M) : P′ → ℕ_{0} is defined by

ψ(M)(p) = \begin{cases}1 & if p = p_{c} \\ M(p) & if p ∈ P \\ 0 & otherwise. \end{cases}

Lemma 3. Let N = (P, T, F, L, λ) be a labelled Petri net and N′ = (P′, T′, F′) the unlabelled Petri net defined above. Then { \atop T (N)_{M_{1}}} and T (N′)_{ψ(M_{1})} are isomorphic unlabelled transition systems for any M_{1} ∈ [P → ℕ_{0}].

Proof. Assume that { \atop T (N)_{M_{1}}} = (S_{1}, ⟶_{1}) and T (N′)_{ψ(M_{1})} = (S_{2}, ⟶_{2}). Recall that S_{1} ⊆ [P → ℕ_{0}] ∪ {r_{(M,λ(t),M′)}^{k} | M[t⟩M′ ∧ 0 ≤ k ≤ λ(t)} ∪ {d_{M}^{k} | M ∈ [P → ℕ_{0}] ∧ 0 ≤ k ≤ n} and S_{2} ⊆ [P′ → ℕ_{0}]. We define a

[figure: p_{1}; q_{1}; ⋮; t; ⋮; p_{k_{1}}; q_{k_{2}}; ⇓; l^{0}; d^{0}; l^{1}; …; d^{n}; p_{1}; p_{c}; q_{1}; ⋮; t^{in}; p_{t}^{0}; t^{out}; ⋮; p_{k_{1}}; l_{t}^{0}; q_{k_{2}}; p_{t}^{1}; l_{t}^{1}; p_{t}^{2}; ⋯; p_{t}^{λ(t)}]

Fig. 2. Transformation of a transition t

mapping f : S_{1} → S_{2} by

f(s_{1}) = \begin{cases}ψ(s_{1}) & if s_{1} ∈ [P → ℕ_{0}] \\ \overline{M} & if s_{1} = r_{(M,λ(t),M′)}^{k} such that M[t⟩M′ \\ \overline{\overline{M}} & if s_{1} = d_{M}^{k} such that M ∈ [P → ℕ_{0}] \end{cases}

where

\overline{M}(p) = \begin{cases}M(p) & if p ∈ P ∖^{•}t \\ M(p) − 1 & if p ∈ ^{•}t \\ 1 & if p = p_{t}^{k} \\ 0 & otherwise \end{cases} and \overline{\overline{M}}(p) = \begin{cases}M(p) & if p ∈ P \\ 1 & if p = d^{k} \\ 0 & otherwise. \end{cases}

Let s_{1} ⟶_{1} s′_{1} for some s_{1}, s′_{1} ∈ S_{1}. It can be easily seen that f(s_{1}) ⟶_{2} f(s′_{1}). On the other hand, let M_{2} ⟶_{2} M′_{2} and M_{2} = f(s_{1}) for some s_{1} ∈ S_{1} and M_{2}, M′_{2} ∈ S_{2}. Then there exists s′_{1} ∈ S_{1} such that M′_{2} = f(s′_{1}) and s_{1} ⟶_{1} s′_{1}. This implies that f is surjective and moreover f is trivially injective. Hence, { \atop T (N)_{M_{1}}} and T (N′)_{ψ(M_{1})} are isomorphic unlabelled transition systems. ⊓ ⊔

Theorem 3. Let N be a labelled Petri net, and M_{1}, M_{2} a pair of markings in N and ϕ a μ-calculus formula. There is a polynomial time reduction producing an unlabelled and normed Petri net N′, a pair of markings ψ(M_{1}), ψ(M_{2}) in N′ and a μ-calculus formula ϕ̂ such that

M_{1} ∼_{T (N)} M_{2} if and only if ψ(M_{1}) ∼_{T (N′)} ψ(M_{2})

and

T (N), M_{1} ⊧ ϕ if and only if T (N′), ψ(M_{1}) ⊧ ϕ̂.

Proof. From Lemma 3 and Theorems 1 and 2. Normedness is because of Remark 3. ⊓ ⊔

Since the bisimilarity checking problem and model checking problems with EF -logic and EG-logic are undecidable [Jan95,Esp97,EK95] for labelled Petri nets, we obtain the following undecidability results for unlabelled and normed Petri nets. In the case of model checking problems we use Remark 4 and the fact that undecidability of model checking with EG-logic can be proved by standard “weak” simulation of a 2-counter machine and we can easily ensure the validity of condition (5) for the Petri net simulating the 2-counter machine.

Corollary 2. Bisimilarity checking problem for unlabelled and normed Petri nets is undecidable.

Corollary 3. Model checking problems with EF -logic and EG-logic for unlabelled and normed Petri nets are undecidable.

Since the bisimilarity checking problem between a labelled Petri net and a finite-state system is EXPSPACE-hard (see comments e.g. in [May00a]), we get also the following corollary.

Corollary 4. Bisimilarity checking problem between an unlabelled and normed Petri net and a finite-state system is EXPSPACE-hard.

4.2 Pushdown systems

It is known that the bisimilarity checking problem for pushdown processes is decidable [Sén98] and PSPACE-hard [May00a]. PSPACE-hard is also the bisimilarity checking problem between a pushdown process and a finite-state system [May00a] — this problem is moreover in EXPTIME [JKM98].

Model checking pushdown processes with modal μ-calculus is decidable and EXPTIME-complete [Wal96]. This means that the model checking problem with EF -logic, EG-logic and CTL is also in EXPTIME. The model checking problems with these logics are PSPACE-hard — see e.g. [May98]. Moreover, model checking with EF -logic and CTL is known ([Wal00]) to be PSPACE-complete and EXPTIME-complete, respectively. The exact complexity of model checking with EG-logic is unknown, however, it seems to be EXPTIME-complete by modification of arguments from [Wal00].

We examine the bisimilarity and model checking problems for unlabelled pushdown systems in this subsection.

Definition 9 (Pushdown system). A pushdown system Δ is a tuple Δ = (Q, Γ, Act, ⟶_{Δ}) where

– Q is a finite set of control states,

– Γ is a finite stack alphabet such that Q ∩ Γ = ∅,

– Act is a finite input alphabet and

– ⟶_{Δ}⊆ Q × Γ × Act × Q × Γ^{∗} is a finite (|⟶_{Δ}| < ∞) transition relation, written pA ⟶^{a}_{Δ} qα for (p, A, a, q, α) ∈⟶_{Δ}.

Definition 10 (Labelled transition system T (Δ)). Let Δ = (Q, Γ, Act, ⟶_{Δ}) be a pushdown system. We define a corresponding labelled transition system T (Δ) as T (Δ) = (S, Act, ⟶) where

S = {pβ | p ∈ Q ∧ β ∈ Γ^{∗}} and pβ ⟶^{a} qγ iff β = Aβ′, γ = αβ′ and

pA ⟶^{a}_{Δ} qα.

Our aim is to transform Δ into an unlabelled pushdown system such that bisimilarity and model checking are preserved. For technical convenience, we assume from now on that Γ contains a distinct “dummy” symbol Z such that pZ −̸→ for any p ∈ Q. Then trivially

p_{1}β_{1} ∼_{T (Δ)} p_{2}β_{2} if and only if p_{1}β_{1}Z ∼_{T (Δ)} p_{2}β_{2}Z  (6)

and

T (Δ), p_{1}β_{1} ⊧ ϕ if and only if T (Δ), p_{1}β_{1}Z ⊧ ϕ  (7)

for any p_{1}, p_{2} ∈ Q, β_{1}, β_{2} ∈ Γ^{∗} and a μ-calculus formula ϕ. In particular, all reachable states from pβZ are of the form qβ′Z where p, q ∈ Q and β, β′ ∈ Γ^{∗}.

Definition 11 (Unlabelled pushdown system). An unlabelled pushdown system is a pushdown system Δ = (Q, Γ, Act, ⟶_{Δ}) such that |Act| = 1.

Remark 6. Whenever |Act| = 1, let us say Act = {a}, we can omit Act from the definition of the pushdown system Δ and instead of pA ⟶^{a}_{Δ} qα we simply write pA ⟶_{Δ′} qα where Δ′ = (Q, Γ, ⟶_{Δ′}) and ⟶_{Δ′}⊆ Q × Γ × Q × Γ^{∗}.

Let Δ = (Q, Γ, Act, ⟶_{Δ}) be a pushdown system such that Z ∈ Γ is the “dummy” stack symbol. Without loss of generality assume that Act = {1, …, n} for some n > 0. We construct an unlabelled pushdown system

Δ′ = (Q, Γ′, ⟶_{Δ′}) where Γ ⊆ Γ′ such that { \atop T (Δ)_{p_{1}α_{1}Z}} and T (Δ′)_{p_{1}α_{1}Z}

are isomorphic unlabelled transition systems for any p_{1} ∈ Q and α_{1} ∈ Γ^{∗}. Again, see Definition 2 for the notation of transition systems restricted to reachable states from p_{1}α_{1}Z. The system Δ′ is defined as follows:

Γ′ = Γ ∪ {X_{(pA,a,qα)}^{k} | pA ⟶^{a}_{Δ} qα ∧ 0 ≤ k ≤ a} ∪ {D^{k} | 0 ≤ k ≤ n}
⟶_{Δ′} = {(p, A, p, X_{(pA,a,qα)}^{0}), (p, X_{(pA,a,qα)}^{0}, q, α) | pA ⟶^{a}_{Δ} qα} ∪

{(p, X_{(pA,a,qα)}^{k}, p, X_{(pA,a,qα)}^{k+1}) | pA ⟶^{a}_{Δ} qα ∧ 0 ≤ k < a} ∪

{(p, A, p, D^{0}A) | p ∈ Q ∧ A ∈ Γ } ∪ {(p, D^{k}, p, D^{k+1}) | p ∈ Q ∧ 0 ≤ k < n}.

Notice that in particular pX_{(pA,a,qα)}^{a}βZ −̸→ and pD^{n}βZ −̸→ for any β ∈ Γ′^{∗}. Graphical representation showing the transformation of pAβZ ⟶^{a} qαβZ where β ∈ Γ^{∗} and pA ⟶^{a}_{Δ} qα can be seen in Figure 3.

Lemma 4. Let Δ = (Q, Γ, Act, ⟶_{Δ}) be a pushdown system containing Z ∈ Γ. Let Δ′ = (Q, Γ′, ⟶_{Δ′}) be the unlabelled pushdown system defined above. Then { \atop T (Δ)_{p_{1}α_{1}Z}} and T (Δ′)_{p_{1}α_{1}Z} are isomorphic unlabelled transition systems for any p_{1} ∈ Q and α_{1} ∈ Γ^{∗}.

Proof. Immediately from the construction. Notice that it is important that any reachable state in T (Δ′)_{p_{1}α_{1}Z} ends with Z. In particular, from any state of the form pβZ where p ∈ Q and β ∈ Γ^{∗} (even if β = ϵ) the following transition is possible in T (Δ′): pβZ ⟶ pD^{0}βZ. ⊓ ⊔

Theorem 4. Let Δ be a pushdown system, and p_{1}β_{1}, p_{2}β_{2} a pair of states in T (Δ) and ϕ a μ-calculus formula. There is a polynomial time reduction

[figure: pAβZ; a; qαβZ; ⇓; pD^{n}AβZ; pD^{0}AβZ; qD^{0}αβZ; qD^{n}αβZ; pAβZ; pX_{(pA,a,qα)}^{0}βZ; qαβZ; pX_{(pA,a,qα)}^{1}βZ; pX_{(pA,a,qα)}^{2}βZ; pX_{(pA,a,qα)}^{a}βZ]

Fig. 3. Transformation of a transition pAβZ ⟶^{a} qαβZ

producing an unlabelled and normed pushdown system Δ′, a pair of states ψ(p_{1}β_{1}), ψ(p_{2}β_{2}) in T (Δ′) and a μ-calculus formula ϕ̂ such that

p_{1}β_{1} ∼_{T (Δ)} p_{2}β_{2} if and only if ψ(p_{1}β_{1}) ∼_{T (Δ′)} ψ(p_{2}β_{2})

and

T (Δ), p_{1}β_{1} ⊧ ϕ if and only if T (Δ′), ψ(p_{1}β_{1}) ⊧ ϕ̂.

Proof. Directly from Lemma 4 together with (6) and (7) — producing the mapping ψ such that ψ(pβ) = pβZ for p ∈ Q and β ∈ Γ^{∗} — and from Theorems 1 and 2. Normedness is because of Remark 3. ⊓ ⊔

Since the bisimilarity checking problem between a pushdown system and a finite-state system is PSPACE-hard [May00a] (this is trivially also a lower bound for two pushdown systems), and because the model checking problems with CTL and Hennessy-Milner logic are EXPTIME-complete resp. PSPACE-complete [Wal00,May98], we obtain the following corollaries. In the case of CTL we use Remark 4 and the fact that we can easily ensure the validity of condition (5) similarly as in the proof of Corollary 1.

Corollary 5. Bisimilarity checking problem between an unlabelled and normed pushdown system and a finite-state system (or another unlabelled and normed pushdown system) is PSPACE-hard.

Corollary 6. Model checking problems with CTL and Hennessy-Milner logic for unlabelled and normed pushdown systems are EXPTIME-complete and PSPACE-complete, respectively.

The bisimilarity checking problem between a pushdown system and a finite-state system is in EXPTIME [JKM98] and PSPACE-hard [May00a]. In order to establish its containment in e.g. PSPACE, it is enough to show it for unlabelled and normed pushdown systems.

4.3 BPA and BPP

By imposing a special restriction on the number of control states of a pushdown system to be a singleton set, let us say Q = {p}, we obtain a BPA system [BK85] with deadlocks — we call it a BPA_{δ} system. In this case, a deadlock δ is a stack symbol which has no defining equation, i.e., pδ −̸→. The class of labelled transition systems generated by BPA_{δ} systems is strictly more expressive (w.r.t. bisimilarity) than the BPA class without such deadlocks [Srb98]. Observe that the class BPA_{δ} is closed under the transformation from labelled transition systems to unlabelled ones — the number of control states of a pushdown system Δ is the same as the number of control states of the transformed unlabelled pushdown system Δ′. However, the class BPA is not closed under such transformation: let Δ = ({p}, {A, Z}, {a, b}, ⟶_{Δ}) be a BPA system such that

pA ⟶^{a}_{Δ} pAA, pA ⟶^{b}_{Δ} p.

The minimal norm of any reachable state in { \atop T (Δ)_{pAZ}} is less or equal to 3 where 3 = |\{a, b\}| + 1. Moreover pA^{k}Z ≁{ \atop T (Δ)_{pAZ}} pA^{k′}Z for any k, k′ ∈ ℕ_{0} such that k ≠ k′. On the other hand there are only finitely many states with norm less or equal to 3 in any BPA system . Thus { \atop T (Δ)_{pAZ}} cannot be described by any BPA system. Similarly the class BPP [Chr93] (subclass of Petri nets where each transition has exactly one input place) is not closed under the transformation — it is enough to replace in our system Δ the sequential composition with a parallel one. This demonstrates that process algebras BPA and BPP are not strong enough to describe deadlock behaviour which is essential for our reduction.

Bisimilarity checking problem for BPA is in 2-EXPTIME [BCS95] and there is no known lower bound yet. Again, in order to prove the containment of the problem in some lower complexity class (PSPACE, NP or even P), it is enough to demonstrate a decision algorithm (running with the corresponding complexity) for normed and unlabelled BPA_{δ} systems. This is especially interesting because the bisimilarity checking problem for normed BPA (without deadlocks) is known to be decidable in polynomial time [HJM96].

Acknowledgements: I would like to thank Mogens Nielsen for his kind supervision and Daniel Polansky for his comments and suggestions.

References

[BAMP83] M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica, 20(3):207–226, 1983.

[BCS95] O. Burkart, D. Caucal, and B. Steffen. An elementary decision procedure for arbitrary context-free processes. In Proceedings of MFCS’95, volume 969 of LNCS, pages 423–433. Springer-Verlag, 1995.

[BE97] O. Burkart and J. Esparza. More infinite results. Bulletin of the European Association for Theoretical Computer Science, 62:138–159, June 1997. Columns: Concurrency.

[BK85] J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77–121, 1985.

[BW90] J.C.M. Baeten and W.P. Weijland. Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.

[CE81] E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs Workshop, volume 131 of LNCS, pages 52–71. Springer-Verlag, 1981.

[CES86] E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.

[Chr93] S. Christensen. Decidability and Decomposition in Process Algebras. PhD thesis, The University of Edinburgh, 1993.

[EK95] J. Esparza and A. Kiehn. On the model checking problem for branching time logics and basic parallel processes. In International Conference on Computer-Aided Verification (CAV’95), volume 939 of LNCS, pages 353– 366, 1995.

[Esp97] J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997.

[HJM96] Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science, 158(1–2):143–159, 1996.

[HM85] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, 32(1):137–161, 1985.

[Hoa85] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

[Jan95] P. Jancar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, 148(2):281–301, 1995.

[JKM98] P. Jancar, A. Kucera, and R. Mayr. Deciding bisimulation-like equivalences with finite-state processes. In Proceedings of the Annual International Colloquium on Automata, Languages and Programming (ICALP’98), volume 1443 of LNCS. Springer-Verlag, 1998.

[JM95] P. Jancar and F. Moller. Checking regular properties of Petri nets. In Proceedings of CONCUR’95, volume 962 of LNCS, pages 348–362. Springer-Verlag, 1995.

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

[May98] R. Mayr. Strict lower bounds for model checking BPA. In Proceedings of the MFCS’98 Workshop on Concurrency, volume 18 of ENTCS. Springer-Verlag, 1998.

[May00a] R. Mayr. On the complexity of bisimulation problems for pushdown automata. In IFIP International Conference on Theoretical Computer Science (IFIP TCS’2000), volume 1872 of LNCS. Springer-Verlag, 2000.

[May00b] R. Mayr. Process rewrite systems. Information and Computation, 156(1):264–286, 2000.

[Mil89] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

[Min67] M.L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967.

[Mol96] F. Moller. Infinite results. In Proceedings of CONCUR’96, volume 1119 of LNCS, pages 195–216. Springer-Verlag, 1996.

[Par81] D.M.R. Park. Concurrency and automata on infinite sequences. In Proceedings 5^{th} GI Conference, volume 104 of LNCS, pages 167–183. Springer-Verlag, 1981.

[Pet81] J.L. Peterson. Petri Net Theory and the Modelling of Systems. Prentice-Hall, 1981.

[Plo81] G. Plotkin. A structural approach to operational semantics. Technical Report Daimi FN-19, Department of Computer Science, University of Aarhus, 1981.

[Pra82] V. Pratt. A decidable mu-calculus. In 22nd IEEE Symposium on Foundations of Computer Science, pages 421–427, 1982.

[Sén98] G. Sénizergues. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In Proceedings of the 39th Annual Symposium on Foundations of Computer Science(FOCS-98), pages 120–129. IEEE Computer Society, 1998.

[Srb98] J. Srba. Deadlocking states in context-free process algebra. In Proceedings of 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS’98), volume 1450 of LNCS, pages 388–398. Springer-Verlag, 1998. To appear in Theoretical Computer Science.

[Srb01] J. Srba. On the power of labels in transition systems. In Proceedings of 12th International Conference on Concurrency Theory (CONCUR’01), LNCS. Springer-Verlag, 2001. To appear.

[Sti95] C. Stirling. Local model checking games. In Proceedings of the 6th International Conference on Concurrency Theory (CONCUR’95), volume 962 of LNCS, pages 1–11. Springer-Verlag, 1995.

[Tho93] W. Thomas. On the Ehrenfeucht-Fraïssé game in theoretical computer science (extended abstract). In Proceedings of the 4th International Joint Conference CAAP/FASE, Theory and Practice of Software Development (TAP-SOFT’93), volume 668 of LNCS, pages 559–568. Springer-Verlag, 1993.

[Vog92] W. Vogler. Modular construction and partial order semantics of Petri nets, volume 625 of LNCS. Springer-Verlag, 1992.

[Wal96] I. Walukiewicz. Pushdown processes: Games and model checking. In International Conference on Computer-Aided Verification (CAV’96), volume 1102 of LNCS, pages 62–74, 1996. To appear in Information and Computation.

[Wal00] I. Walukiewicz. Model checking CTL properties of pushdown systems. In Proceedings Foundations of Software Technology and Theoretical Computer Science (FSTTCS’00), volume 1974 of LNCS, pages 127–138. Springer-Verlag, 2000.

Recent BRICS Report Series Publications

RS-01-19 Jiří Srba. On the Power of Labels in Transition Systems. June 2001. 23 pp. Full and extended version of Larsen and Nielsen, editors, Concurrency Theory: 12th International Conference, CONCUR ’01 Proceedings, LNCS, 2001.

RS-01-18 Katalin M. Hangos, Zsolt Tuza, and Anders Yeo. Some Complexity Problems on Single Input Double Output Controllers. 2001. 27 pp.

RS-01-17 Claus Brabrand, Anders Møller, Steffan Olesen, and Michael I. Schwartzbach. Language-Based Caching of Dynamically Generated HTML. May 2001. 18 pp.

RS-01-16 Olivier Danvy, Morten Rhiger, and Kristoffer H. Rose. Normalization by Evaluation with Typed Abstract Syntax. May 2001. 9 pp. To appear in Journal of Functional Programming.

RS-01-15 Luigi Santocanale. A Calculus of Circular Proofs and its Categorical Semantics. May 2001. 30 pp.

RS-01-14 Ulrich Kohlenbach and Paulo B. Oliva. Effective Bounds on Strong Unicity in L_{1}-Approximation. May 2001. 38 pp.

RS-01-13 Federico Crazzolara and Glynn Winskel. Events in Security Protocols. April 2001. 30 pp.

RS-01-12 Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær. The Abstraction and Instantiation of String-Matching Programs. April 2001.

RS-01-11 Alexandre David and M. Oliver Möller. From HUppaal to Uppaal: A Translation from Hierarchical Timed Automata to Flat Timed Automata. March 2001. 40 pp.

RS-01-10 Daniel Fridlender and Mia Indrika. Do we Need Dependent Types? March 2001. 6 pp. Appears in Journal of Functional Programming, 10(4):409–415, 2000. Superseeds BRICS Report RS-98-38.

RS-01-9 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. Static Validation of Dynamically Generated HTML. February 2001. 18 pp.

RS-01-8 Ulrik Frendrup and Jesper Nyholm Jensen. Checking for Open Bisimilarity in the π-Calculus. February 2001. 61 pp.