Model Checking of non-finite state processes by Finite Approximations

N. De Francesco^{♣}, A. Fantechi^{♣} ^{♢}, S. Gnesi^{♢} and P. Inverardi^{♢} ^{♡}

♣ Dipartimento di Ingegneria dell’Informazione, Univ. di Pisa, Italy, e-mail: nico@iet.unipi.it, fantechi@iet.unipi.it

♢ Istituto di Elaborazione dell’Informazione, C.N.R. Pisa, Italy, e-mail: gnesi@iei.pi.cnr.it ♡ Dip. di Matematica Applicata, Univ. dell’Aquila, Italy, e-mail:inverard@iei.pi.cnr.it

Abstract

In this paper we present a verification methodology, using an action-based logic, able to check properties for full CCS terms, allowing also verification on infinite state systems. Obviously, for some properties we are only able to give a semidecision procedure. The idea is to use (a sequence of) finite state transition systems which approximate the, possibly infinite state, transition system corresponding to a term. To this end we define a particular notion of approximation, which is stronger than simulation, suitable to define and prove liveness and safety properties of the process terms.

1 Introduction

Many verification environments are presently available which can be used to automatically verify properties of reactive systems specified by means of process algebras, with respect to behavioural relations and logical properties. Most of these environments [7, 12, 13, 19] are based on the hypothesis that the system can be modelled as a finite state Labelled Transition Systems (LTS) and that the logic properties are regular properties. That is, no means are provided to deal with non-finite state LTS’s. Usually, in these environments, to avoid the nontermination of the generation phase a term must satisfy some finiteness syntactic conditions: in the case of CCS, for example, terms where a process variable x occurs in a parallel composition belonging to the definition of x are not handled [22].

We are interested here to deal with non finite-state systems; approaches have been proposed to this aim, which are not based on LTS’s [1, 4, 14, 15, 16]; we consider instead LTS based verification. The idea is to use, for proving a logical property, a sequence of finite state LTSs approximating the, possibly infinite state, LTS corresponding to a term by the standard CCS semantics.

In this paper we present a verification methodology to check properties expressed in ACTL, an action based logic [11], on full CCS terms (with no syntactic restriction), thus allowing complete generality of the class of reactive systems to be specified. We are able to carry on the verification even though the ”usual” LTS generation fails. Obviously, for some of the properties, we are able to give only a semidecision procedure. This procedure is based on a notion of approximation and on the study of the ACTL properties preserved by the approximation. In this way, we can infer the satisfaction of a property by the whole system from the satisfaction of the property by a chain of approximations. In particular, we define an approximation chain, denoted as {N_{i}}, which is very expressive with respect to liveness properties.

In order to reason on the properties that we are able to prove with approximation chains, we start giving a syntactic characterization of different kinds of properties. Moreover, we define a

Act \overline{μ.p →^{μ} p}  Con \frac{p →^{μ} p′, x =^{def} p}{x →^{μ} p′}
Sum \frac{p →^{μ} p′}{p + q →^{μ} p′ and q + p →^{μ} p′}  Par \frac{p →^{μ} p′}{p|q →^{μ} p′|q and q|p →^{μ} q|p′}
Com \frac{p →^{α} p′, q →^{\overline{α}} q′}{p|q →^{τ} p′|q′}  Res \frac{p →^{μ} p′, μ, \overline{μ} ∉ A}{p\A →^{μ} p′\A}
Rel \frac{p →^{μ} p′}{p[f] →^{f(μ)} p′[f]}

Figure 1: The SOS rules

criterion to compare the suitability of approximation chains to prove properties. Following this notion, we formalize the fact that a chain is ”better” than another one, if its set of provable properties is greater. Our work differs from the abstract interpretation approaches for model checking of transition systems [2, 6, 8] since we do not build an abstract (with respect to values) model on which the properties are proved, but a suitable chain of finite labelled transition systems based on the operational semantics: when dealing with infinite systems, this allows us to choose the approximation level case by case.

2 Background

2.1 CCS

We summarize the most relevant definitions regarding CCS, and refer to [21] for more details. The CCS syntax is the following: p ::= μ.p | nil | p + p | p|p | p\A | x | p[f]

Terms generated by p (T erms) are called process terms (called also processes or terms); x ranges over a set {X, Y, ..}, of process variables. A process variable is defined by a process definition x =^{def} p,

(p is called the expansion of x). As usual, there is a set of visible actions V is = \{a, \overline{a}, b, \overline{b}, ...\} over which α ranges, while μ, ν range over Act = V is∪{τ}, where τ denotes the so-called internal action. We denote by \overline{α} the action complement: if α = a, then \overline{α} = \overline{a}, while if α = \overline{a}, then \overline{α} = a. By nil we denote the empty process. The operators to build process terms are prefixing (μ.p), summation (p + p), parallel composition (p|p), restriction (p\A) and relabelling (p[f]), where A ⊆ V is and f : V is → V is. Given a term p, an occurrence of a process variable x is guarded in p if it is within some sub-term of the form μ.q. We assume that (i) V is is finite; (ii) for each definition x =^{def} p, each occurrence of each process variable is guarded in p; (iii) all terms are closed, i.e. all variables occurring in a term are defined.

An operational semantics OP is a set of inference rules defining a relation D ⊆ T erms × Act × T erms. The relation is the least relation satisfying the rules. If (p, μ, q) ∈ D, we write p →^{μ}_{OP} q. The rules defining the semantics of CCS [21], from now on referred to as SOS, are recalled in Figure 1.

A labelled transition system (or simply transition system) T S is a quadruple (S, T, D, s_{0}), where S is a set of states, T is a set of transition labels, s_{0} ∈ S is the initial state, and D ⊆ S × T × S. A transition system is finite if D is finite.

A finite computation of a transition system is a sequence μ_{1}μ_{2}..μ_{n} of labels such that:

s_{0} →^{μ_{1}}_{OP} .. →^{μ_{n}}_{OP} s_{n}.

Given a term p (and a set of process variable definitions), and an operational semantics OP, OP (p) is the transition system (T erms, Act, D, p), where D is the relation defined by OP.

Let T S_{1} = (S_{1}, T_{1}, D_{1}, s_{0_{1}}) and T S_{2} = (S_{2}, T_{2}, D_{2}, s_{0_{2}}) be transition systems and let s_{1} ∈ S_{1} and s_{2} ∈ S_{2}. s_{1} and s_{2} are strongly equivalent (or simply equivalent) (s_{1} ∼ s_{2}) if there exists a strong bisimulation that relates s_{1} and s_{2}. B ⊆ S_{1} × S_{2} is a strong bisimulation if ∀(s_{1}, s_{2}) ∈ B (where μ ∈ T_{1} ∪ T_{2}),

• s_{1} →^{μ}_{1} s′_{1} implies ∃s′_{2} : s_{2} →^{μ}_{2} s′_{2} and (s′_{1}, s′_{2}) ∈ B; s_{2} →^{μ}_{2} s′_{2} implies s_{1} →^{μ}_{1} s′_{1} and (s′_{1}, s′_{2}) ∈ B

s_{2} simulates s_{1} if there exists a strong simulation that relates s_{1} and s_{2}. R ⊆ S_{1} ×S_{2} is a strong

simulation if ∀(s_{1}, s_{2}) ∈ R (where μ ∈ T_{1} ∪ T_{2}): s_{1} →^{μ}_{1} s′_{1} implies ∃s′_{2} : s_{2} →^{μ}_{2} s′_{2} and (s′_{1}, s′_{2}) ∈ R.

T S_{1} and T S_{2} are said to be equivalent (T S_{1} ∼ T S_{2}) if a strong bisimulation exists for s_{0_{1}} and s_{0_{2}}. Two CCS terms p and q are equivalent (p ∼ q) if SOS(p) ∼ SOS(q).

T S_{2} simulates T S_{1} if a strong simulation R exists such that (s_{01}, s_{02}) ∈ R.

Given a state s of a transition system T S = (S, T, D, s_{0}), we say that s ↛ if no s′ ∈ S and μ ∈ T exist such that (s, μ, s′) ∈ D.

CCS can be used to define a wide class of systems, that ranges from Turing machines to finite systems [22]; therefore, in general, CCS terms cannot be represented as finite state systems.

2.2 ACTL

We introduce now the action based branching temporal logic ACTL defined in [11]. This logic is suitable to express properties of reactive systems defined by means of TS’s. ACTL is in agreement with the notion of bisimulation defined above. Before defining syntax and semantics of ACTL operators, let us introduce some notions and definitions which will be used in the sequel.

For A ⊆ Act, we let D_{A}(s) denote the set {s′: there exists α ∈ A such that (s, α, s′) ∈ D}. We will also use the action name, instead of the corresponding singleton denotation, as subscript. Moreover, we let D(s) denote in short D_{Act}(s) and D_{A_{τ}} (s) denote D_{A∪{τ}}(s). For A, B ⊆ Act, we let A/B denote the set A − (A ∩ B). Given a LTS TS=(S,T,D,s_{0}), we define:

• σ is a path from r_{0} ∈ S if either σ = r_{0} (the empty path from r_{0}) or σ is a (possibly infinite) sequence (r_{0}, α_{1}, r_{1})(r_{1}, α_{2}, r_{2}) … such that (r_{i}, α_{i+1}, r_{i+1}) ∈ D for each i ≥ 0.

• A path σ is called maximal if either it is infinite or it is finite and its last state r has no successor states (D(r) = ∅). The set of maximal paths from r_{0} will be denoted by Π(r_{0}).

• If σ is infinite, then |σ| = ω.

If σ = r_{0}, then |σ| = 0.

If σ = (r_{0}, α_{1}, r_{1})(r_{1}, α_{2}, r_{2}) … (r_{n}, α_{n+1}, r_{n+1}), n ≥ 0, then |σ| = n + 1. Moreover, we will denote the i^{th} state in the sequence, i.e. r_{i}, by σ(i). ⊓ ⊔

To define the logic ACTL [11], an auxiliary logic of actions is introduced. The collection AF of action formulae over V is is defined by the following grammar where χ, χ′, range over action formulae, and α ∈ V is:

χ ::= α|¬χ|χ ∧ χ

We write ff for α_{0} ∧ ¬α_{0}, where a_{0} is some chosen action, and tt stands for ¬ff. Moreover, we will write χ ∨ χ′ for ¬(¬χ ∧ χ′). An action formula permits the expression of constraints on the actions that can be observed (along a path or after next step); for instance, α ∨ β says that the only possible observations are α or β, while tt stands for ”all actions are allowed” and ff for ”no actions can be observed”, that is only silent actions can be performed.

The satisfaction of an action formula χ by an action α, α ⊧ χ, is defined inductively by:

•α ⊧ β iff α = β;  •α ⊧ ¬χ iff not α ⊧ χ;  •α ⊧ χ ∧ χ′ iff α ⊧ χ and α ⊧ χ′

Given an action formula χ, the set of the actions satisfying χ can be given by the function κ : AF(V is) → 2^{V is} as follows:

•κ(tt) = V is;  •κ(α) = {α};  •κ(¬χ) = V is/κ(χ);  •κ(χ ∨ χ′) = κ(χ) ∪ κ(χ′).

The syntax of ACTL is defined by the state formulae generated by the following grammar: ϕ ::= tt | ϕ ∧ ϕ | ¬ϕ | Eγ | Aγ γ ::= X_{χ}ϕ | X_{τ} ϕ | ϕ_{χ}U ϕ | ϕ_{χ}U_{χ′} ϕ

where χ, χ′ range over action formulae, E and A are path quantifiers, X and U are next and until operators respectively.

Let T S = (S, Act, D, s_{0}) be a LTS. Satisfaction of a state formula ϕ (path formula γ) by a state s (path σ), notation s ⊧_{T S} ϕ (σ ⊧_{T S} γ) is given inductively by :

s ⊧_{T S} tt always; s ⊧_{T S} ϕ ∧ ϕ′ iff s ⊧_{T S} ϕ and s ⊧_{T S} ϕ′; s ⊧_{T S} ¬ϕ iff not s ⊧_{T S} ϕ; s ⊧_{T S} Eγ iff there exists a path σ ∈ Π(s) such that σ ⊧_{T S} γ; s ⊧_{T S} Aγ iff for all maximal paths σ ∈ Π(s), σ ⊧_{T S} γ; σ ⊧_{T S} X_{χ}ϕ iff |σ| ≥ 1 and σ(2) ∈ D_{κ(χ)}(σ(1)) and σ(2) ⊧_{T S} ϕ; σ ⊧_{T S} X_{τ} ϕ iff |σ| ≥ 1 and σ(2) ∈ D_{{τ}}(σ(1)) and σ(2) ⊧_{T S} ϕ; σ ⊧_{T S} ϕ_{χ}Uϕ′ iff there exists i ≥ 1 such that σ(i) ⊧_{T S} ϕ′, and for all

1 ≤ j ≤ i − 1: σ(j) ⊧_{T S} ϕ and σ(j + 1) ∈ D_{κ(χ)_{τ}} (σ(j));

σ ⊧_{T S} ϕ_{χ}U_{χ′}ϕ′ iff there exists i ≥ 2 such that σ(i) ⊧_{T S} ϕ′ and σ(i) ∈ D_{κ(χ′)}(σ(i − 1)), and for all

1 ≤ j ≤ i − 1: σ(j) ⊧_{T S} ϕ and σ(j) ∈ D_{κ(χ)_{τ}} (σ(j − 1)).

Several useful modalities can be defined, starting from the basic ones. In particular, we will write:

• EF ϕ for E(tt_{tt}U ϕ), and AF ϕ for A(tt_{tt}U ϕ); these are called the eventually operators.

• EGϕ for ¬AF ¬ϕ, and AGϕ for ¬EF ¬ϕ; these are called the always operators.

ACTL can be used to define liveness (something good eventually happen) and safety (nothing bad can happen) properties of reactive systems. In a branching time logic both liveness and safety properties could be divided into two classes: universal liveness (safety) properties and existential liveness (safety) properties. The former state that a condition holds at some (all) states of all computation paths. The latter state that a condition holds at some (all) states of one computation path. Moreover liveness properties can be better classified as in the following [17, 20]:

Termination properties: ”a good thing happens at some states of a (all) computation(s)”. Recurrence properties: ”a good thing happens at infinitely many states of a (all) computation(s)”. Persistence property: ”a good thing happens at all but finitely many states of a (all) computation(s)”. We can also talk of finite properties, that state some condition on the finite initial part of the behaviour of the system.

2.3 Infinite state systems and logical properties

We know that all ACTL formulae are decidable on finite state transition systems and the linear time ACTL model checker [10] can be used to do this job. Hence, when we have a CCS description of a system and we want to prove on it ACTL properties, the labeled transition system associated to it needs to be built. This will be the model on which the satisfiability of the formulae will be checked. Problems, obviously, arise when the system to be modelled has an infinite state representation, due for example to the interplay between parallel composition and recursion operators.

As an example, let us consider the CCS definition of a bag containing two kinds of elements:

X = p1.(g1.nil|X) + p2.(g2.nil|X)

where p_{1} and p_{2} represent insertions and g_{1} and g_{2} deletions of the two kinds of elements, respectively. It is known that X is neither finite state nor context-free. Some typical properties of a bag could be requested to be checked on this specification, in order to validate it:

1) The bag is not a set, therefore it is possible to put twice the same value in the bag consecutively: AF AX_{p_{1}}EX_{p_{1}}tt.

2) It is possible, on all (but finitely many) states to do a put action immediately followed by a get action: EF EG(EX_{p_{1}}EX_{g_{1}}tt).

3) There exists a computation path on which it is possible to do infinitely often put actions: EGAF (EX_{p_{1}∨p_{2}}tt).

4) It is always possible to perform a put action: AGEX_{p_{1}∨p_{2}}tt.

3 Verification by approximations

Let us first present a syntactic characterization, as ACTL formulae, of the logical properties we will deal with. We then introduce the general notion of chain of finite approximations of the transition system of a term p. Finally, we introduce a notion of approximation suitable to prove liveness properties.

3.1 Temporal properties

Definition 3.1 (Positive formula) We say that π′ is a positive formula if it is an ACTL formula without negations.

Definition 3.2 (Liveness property) We say that ψ is a liveness property if one of the following holds, where π′ is a positive formula:

• ψ = AF π′ or ψ = EF π′ (termination property)

• ψ = AF AGπ′, ψ = EF AGπ′, ψ = AF EGπ′ or ψ = EF EGπ′ (persistence property)

• ψ = AGAF π′, ψ = EGAF π′, ψ = AGEF π′ or ψ = EGEF π′ (recurrence property)

Definition 3.3 (Finite property) We say that σ is a finite property if it can be expressed by an ACTL formula defined by the following grammar: σ ::= tt | σ ∧ σ | σ ∨ σ | ¬σ | Eγ | Aγ γ ::= X_{χ}σ | X_{τ} σ

Definition 3.4 (Positive finite property) We say that π is a positive finite property if it is a finite property without negations.

Definition 3.5 (Safety property) We say that θ is a safety property if θ = AGπ or θ = EGπ and π is a positive finite property.

The given syntactical presentation of liveness and safety properties does not obviously cover all the liveness and safety properties expressible by means of all the ACTL operators as the negation operator. Indeed, negation makes the syntactic classification of formulae difficult. Following this classification, we have that properties 1) to 3) of the bag example are liveness properties, while 4) is a safety one.

Finite, liveness and safety properties are decidable on a finite state LTS. In general, while finite properties are provable, liveness (including termination, persistence and recurrence) and safety properties can be undecidable for a non-finite state term p.

3.2 Approximation chains

Given a CCS term p, we define chains of finite LTSs which more and more accurately simulate the behaviour of SOS(p). Since each LTS in a chain is finite proof checking methodologies for finite LTSs can be used. First we define in the most general way the concept of approximation chain. In the following we denote, with T and T, the set of all LTSs and a generic LTS, respectively.

Definition 3.6 (Approximation chain) Let ⪯ a preorder over T . We say that T_{1} approximates by ⪯ (⪯-approximates) T_{2} iff T_{1} ⪯ T_{2}. Given a term p, a chain {T_{i}(p)|i ≥ 0} on (T , ⪯) is called approximation chain for p by ⪯ (⪯-approximation chain) iff:

• for each i, T_{i}(p) is finite;

• for each i, T_{i}(p) ⪯ T_{i+1}(p);

• ⊔{T_{i}(p)} ∼ SOS(p).

Note that, if we have a finite approximation chain {T_{i}(p)|r ≥ i ≥ 0}, then T_{r}(p) ∼ SOS(p).

[figure: ⪯_{s}; ⪯̸_{bc}; T S_{2}; T S_{1}; a; b; a]

Figure 2: Simulation vs. BC-simulation.

Definition 3.7 (Properties preserved by ⪯) A preorder ⪯ preserves a property ϕ if whenever T_{1} verifies ϕ and T_{1} ⪯ T_{2} then T_{2} verifies ϕ.

The above definitions allow us to define a procedure for proving the validity of a property on an infinite state-system, by checking the property on the elements of an approximation chain, starting from the first one, until we find that the property is verified. The procedure is sound if the chain preserves the property, i.e. it must happen that, if we are able to prove ϕ on an element of the chain, we can assert the validity of ϕ on SOS(p). This means that the property must be monotonic on the preorder. The first result we show is that simulation, from now on denoted by ⪯_{s}, is not suitable to prove all liveness properties.

Proposition 3.1 ⪯_{s} does not preserve all liveness properties. Proof Let us consider the following liveness property: Each path contains a state from which all the outcoming arcs are labelled by a, expressed by (AF AX_{a}tt) and the transition systems T S_{1} and T S_{2} in Figure 2. We have that T S_{1} ⪯_{s} T S_{2}, but T S_{1} verifies the property and T S_{2} does not.

In order to manage all liveness properties, we now introduce a stronger notion of simulation between transition systems. This notion, in contrast to simulation, permits the definition of approximation chains that preserve the branching structure, that is, for each approximation, if a node has been exploded, all its branches have been developed.

Definition 3.8 (Branching Complete Simulation) Let T S_{1} = (S_{1}, T_{1}, D_{1}, s_{0_{1}}) and T S_{2} = (S_{2}, T_{2}, D_{2}, s_{0_{2}}) be transition systems and let s_{1} ∈ S_{1} and s_{2} ∈ S_{2}. s_{2} BC-simulates s_{1} if there exists a strong BC-simulation that relates s_{1} and s_{2}. R ⊆ S_{1} × S_{2} is a strong BC-simulation if ∀(s_{1}, s_{2}) ∈ R, μ ∈ T_{1} ∪ T_{2},

• s_{1} →^{μ}_{1} s′_{1} implies ∃s′_{2} : s_{2} →^{μ}_{2} s′_{2} and (s′_{1}, s′_{2}) ∈ R.

• s_{2} →^{μ}_{2} s′_{2} implies either s_{1} ↛_{1} or s_{1} →^{μ}_{1} s′_{1} and (s′_{1}, s′_{2}) ∈ R.

T S_{2} BC-simulates T S_{1} (T S_{1} ⪯_{bc} T S_{2}) if a branching complete simulation R exists such that (s_{0_{1}}, s_{0_{2}}) ∈ R.

It is easy to see that T S_{1} ⪯_{bc} T S_{2} implies T S_{1} ⪯_{s} T S_{2}, but the converse is not true in general. For example, T S_{2} does not BC-simulate T S_{1} in Figure 2.

The following proposition holds.

Proposition 3.2 ⪯_{bc} is a preorder. Proof Sketch. It is reflexive and transitive.

The notion of approximation chain based on BC-simulation preserves the branching structure of the transition systems all along the chain. This allow us to prove properties not provable on a chain based on simulation. One of the main results of the paper is the following:

Proposition 3.3 ⪯_{bc} preserves liveness properties. Proof sketch By structural induction on the structure of the liveness formulae and taking into account that the liveness properties are defined on a positive fragment of ACTL and that the BCsimulation forces the simulating transition system to exactly mantain all the (bisimilar) branches of the simulated one, if any.

It is now easy to relate approximation chains, based on BC-simulation, with liveness properties. The following proposition is the basis of our verification method.

[figure: a; a; b; a; T S_{1}; T S_{3}; ⪯_{bc}; ⪯_{s}]

Figure 3: Simulation and BC-simulation.

Proposition 3.4 Let p be a term and {T_{i}(p)} a ⪯_{bc}-approximation chain for p. If ϕ is a liveness property, it holds that: if s_{0} ⊧_{T_{i}(p)} ϕ for some i, then s_{0} ⊧_{SOS(p)} ϕ. Proof. It follows by proposition 3.3.

For safety properties, the following proposition holds :

Proposition 3.5 ⪯_{s} and ⪯_{bc} do not preserve safety properties. Proof Let us consider the safety property ”It is always possible to perform an action a ” , expressed by AGAX_{a}tt, and the transition systems T S_{1} and T S_{3} in Figure 3. Then T S_{1} ⪯_{bc} T S_{3} and T S_{1} ⪯_{s} T S_{3}, but T S_{1} verifies the property and T S_{3} does not.

This means that we cannot define a semidecision procedure based on approximation chains for the satisfaction of safety properties; on the converse, the following proposition gives a method to prove that a safety property does not hold for SOS(p).

Proposition 3.6 Let p be a term and {T_{i}(p)} a ⪯_{bc}-approximation chain for p. If ψ is a safety property, it holds that: if s_{0} |̸=_{T_{i}(p)} ψ for some i, then s_{0} |̸=_{SOS(p)} ψ. Proof sketch For duality from Prop. 3.4

Prop. 3.6 corresponds, according to the definition of safety properties in [20, 17], to say that if a finite approximation of a term p violates the property, then p itself violates the property.

Let us now consider finite properties. The following holds:

Proposition 3.7 ⪯_{s} does not preserve all finite properties. Proof sketch Consider the finite property: Each path starts with an action a (AX_{a}tt), with T S_{1} and T S_{2} of Figure 2. We have that T S_{1} ⪯_{s} T S_{2}, but T S_{1} verifies the property and T S_{2} does not.

Since finite properties represent a particular class of liveness properties we have a semidecision procedure for testing the validity of these properties by using approximation chains based on ⪯_{bc}. We can do more, as one should have expected, and provide a decision procedure for finite properties. To this end, we furtherly constrain our chains. Let us consider, for example, the following finite property for SOS(p) for some p: All paths start with the action b and contain at least an action a as a second action (AX_{b}EX_{a}tt).

Approximation chains based on ⪯_{bc} are not suitable to give a positive or negative answer if SOS(p) is infinite: in fact a new path of length 2 may appear in whatever element of the chain. The property is decidable if, instead, each transition system T_{i}(p) of the chain grows on all possible paths with respect to T_{i−1}(p). This suggests the following notion:

Definition 3.9 (Transition system path-approximation) Let T S_{1} and T S_{2} be transition systems. We say that T S_{1} is an n-path-approximation of T S_{2} (T S_{1} ⪯_{n} T S_{2}) if

• T S_{1} ⪯_{bc} T S_{2};

• either T S_{1} ∼ T S_{2} or the paths of length ≤ n of T S_{1} and T S_{2} coincide.

We can now state the following:

Proposition 3.8 Let π be a finite property of depth n, that is with only n nested next operators, and {T_{i}(p)} a ⪯_{bc}-approximation chain for a term p such that T_{i}(p) ⪯_{i} SOS(p) for each i. Then s_{0} ⊧_{SOS(p)} π iff s_{0} ⊧_{T_{n}(p)} π. Proof sketch We have that T_{n}(p) has all the paths of length n of SOS(p).

4 How to build approximations

In this section, we present some ways of constructing approximation chains. In order to obtain correct approximations for a term p, the idea is to derive p using the operational semantics until some stopping condition, thus obtaining a partial transition system, which is furtherly expanded to obtain the successive elements of the chain. The first chain we present, described in the following sub-secton, is based on the standard SOS semantics. In order to obtain better approximations, we then introduce a second chain, which is based on a different semantics, able to produce ”more expressive” transition systems.

4.1 SOS approximations

Definition 4.1 ({M_{i}(p)}) Given a term p, the chain {M_{i}(p) = (S_{M_{i}}, Act, D_{M_{i}}, s_{0})} is inductively defined as follows:

• M_{0}(p) = ({p}, Act, {}, p)

• M_{i+1}(p) = (S_{M_{i+1}}, Act, D_{M_{i+1}}, p) where

– S_{M_{i+1}} = S_{M_{i}} ∪ {q|p ∈ S_{M_{i}} and μ ∈ Act exist such that p →^{μ}_{SOS} q};

– D_{M_{i+1}} = D_{M_{i}} ∪ {(p, μ, q)|p ∈ S_{M_{i}} and μ ∈ Act exist such that p →^{μ}_{SOS} q}.

Informally, M_{0}(p) has the only state p without transitions and M_{i+1}(p), i ≥ 0, is obtained from M_{i}(p), by adding to the states (and the related transitions) of M_{i}(p) all those states reachable from them with only one action. The following proposition holds:

Proposition 4.1 Given a term p, the chain {M_{i}(p)} is a ⪯_{bc}-approximation chain for p. Proof sketch. By induction on the length of the chain and by definig suitable BC-simulations.

Actually, the chain {M_{i}(p)} is the simplest chain derivable from SOS(p) which is a ⪯_{bc}- approximation chain. In fact the simpler approximation chain which at any step adds a single new transition to the previous element of the chain, is not a ⪯_{bc}-approximation chain.

Example 4.1 Let us now reconsider the bag example of section 2.3, and try to prove the properties on the chain {M_{i}(X)}. Since {M_{i}(X)} is a ⪯_{bc}-approximation chain, it preserves all properties from 1) to 3) and does not preserve the safety property 4). Thus, if we find that an approximation M_{i}(X) verifies a property among 1) and 3), we prove that the property holds for the bag (i.e. SOS(X)). M_{0}(X) is given by a transition system with only one state, i.e. X itself, while M_{1}(X) and M_{2}(X) are represented in Figures 4 and 5 respectively.

                              [figure: g2.nil|x; g1.nil|x; p2; p1; x]

Figure 4: M_{1}(X)

              [figure: g2.nil|g2.nil|x; g2.nil|g1.nil|x; g1.nil|g2.nil|x; g1.nil|g1.nil|x; g2; g1; p1; p2; p2; p1; x; p1; p2; g1.nil|x; g2.nil|x; nil|x]

Figure 5: M_{2}(X)

We have that property 1) is not satisfied by M_{1}(X), it is satisfied by M_{2}(X) and thus it is true for the bag. Moreover, property 4) is verified by M_{1}(X), but this does not mean that it is true for the bag, since it is a safety property. Properties 2) and 3) are not verified by M_{1}(X) neither by M_{2}(X). It is easy to see that these properties are not verified by any M_{i}(X), for each i. In fact their satisfiability implies detecting a cycle in the transition system: this cycle will never appear in the chain {M_{i}(X)}.

Thus, if we use this chain to approximate SOS(X), these properties are not provable, while they hold for SOS(X). Nothing can instead be asserted about property 4), following proposition 3.6. The following proposition states that each M_{i} is a ⪯_{i}-approximation of SOS(p), i.e. the size of the transition system grows.

Proposition 4.2 Given a term p, for each i ≥ 0, M_{i}(p) ⪯_{i} SOS(p). Proof. By proposition 4.1 it holds that M_{i}(p) ⪯_{bc} SOS(p). Moreover, by induction on the length of {M_{i}(p)}, we have by definition that M_{i}(p) has all the paths of length less or equal to i.

As a consequence, using {M_{i}(p)} we can decide any finite property of depth n of a term p: it sufficies to check the property on M_{n}(p).

4.2 SS Approximations

In this section, we present a way of approximating SOS(p) based on a different operational semantics, which allows us to prove a greater set of properties than those proved by {M_{i}(p)}. In [9] the semantics SS was defined, which is more abstract than SOS, since the SS rules have built in some behavioural equivalence axioms, i.e. they accomplish some simplifications on the terms during the derivations, with the purpose of obtaining, if possible, a finite-state transition system for p. The rules of SS are such that SS(p) is strongly equivalent to SOS(p). The definition of SS, whose rules are shown in figure 6, is based on the following considerations. Given the CCS syntax, those operators that, in presence of recursion, would give rise to the derivation of growing terms (and therefore to an infinite number of derivations) are parallel composition, restriction and relabelling. For restriction and relabelling, in a language with finite action set, the unlimited growth of terms can be prevented by using suitable inference rules. In fact, successive, possibly intermixed, occurrences of restriction and relabelling can be reduced to only one restriction, followed by only one relabelling. Moreover, the parallel operator can be deleted as soon as one of the two arguments terminates, i.e. is equivalent to nil. The SS inference rules accomplish these strong equivalence preserving simplifications during the derivation. The following notation is used in the rules:

p\\A =  p\A, if p ≠ q\B, p ≠ q[f]  q\A ∪ B, if p = q\B
q\f^{1}(A)[f], if p = q[f], q ≠ r\B q\f^{1}(A) ∪ B[f], if p = q\B[f]
p[[f]]=  p[f], if p ≠ q[g]  q[f ∘ g], if p = q[g]

S-Act=Act S-Con=Con S-Sum=Sum

S-Par_{1} \frac{p →^{μ} p′, not p′ ↛}{p|q →^{μ} p′|q and q|p →^{μ} q|p′}  S-Par_{2} \frac{p →^{μ} p′, p′ ↛}{q|p →^{μ} q and q|p →^{μ} q}
S-Com_{1} \frac{p →^{α} p′, q →^{\overline{α}} q′, not p′ ↛ and not q′ ↛}{p|q →^{τ} p′|q′}  S-Com_{2} \frac{p →^{α} p′, q →^{\overline{α}} q′, p′ ↛}{p|q →^{τ} q′ and q|p →^{τ} q′}
S-Res \frac{p →^{μ} p′, μ, \overline{μ} ∉ A}{p\A →^{μ} q\\A}  S-Rel \frac{p →^{μ} q}{p[f] →^{f(μ)} q[[f]]}

Figure 6: The SS rules

The chain {N_{i}(p)} is defined in a similar way to {M_{i}(p)}, but using the above rules:

Definition 4.2 ({N_{i}(p)}) Given a term p, the chain {N_{i}(p) = (S_{N_{i}}, Act, D_{N_{i}}, s_{0})} is inductively defined as follows:

• N_{0}(p) = ({p}, Act, {}, p)

• S_{N_{i+1}}(p) = (S_{N_{i+1}}, Act, D_{N_{i+1}}, p) where

– S_{N_{i+1}} = S_{N_{i}} ∪ {q|p ∈ S_{N_{i}} and μ ∈ Act exist such that p →^{μ}_{SS} q};

– D_{N_{i+1}} = D_{N_{i}} ∪ {(p, μ, q)|p ∈ S_{N_{i}} and μ ∈ Act exist such that p →^{μ}_{SS} q}.

If we reconsider the bag example, Figures 7, 8 show N_{1}(X) and N_{2}(X), respectively.

                              [figure: g2.nil|x; g1.nil|x; p2; p1; x]

Figure 7: N_{1}(X)

              [figure: g2.nil|g2.nil|x; g2.nil|g1.nil|x; g1.nil|g2.nil|x; g1.nil|g1.nil|x; g2; g1; p1; p2; p2; p1; x; p1; p2; g1.nil|x; g2.nil|x]

Figure 8: N_{2}(X)

The following proposition holds: Proposition 4.3 Given a term p,

• the chain {N_{i}(p)} is a ⪯_{bc}-approximation chain for p;

• for each i ≥ 0, N_{i}(p) ⪯_{i} SOS(p) Proof sketch Analogous to the proof of proposition 4.1 and 4.2 and since SOS(p) ∼ SS(p).

If we check the properties 1) … 4) on the chain {N_{i}(p)}, we have the same results as with {M_{i}(p)} for 1) and 4), but N_{2}(X) satisfies properties 2) and 3), which are then true for the bag, while their validity is not provable on the chain {M_{i}(X)}.

The following proposition relates the two chains we have introduced. Proposition 4.4 Given a CCS term p, for each i ≥ 0, ∃j such that M_{i}(p) ⪯_{bc} N_{j}(p). Proof. The finite paths are equal in M_{i}(p) and N_{i}(p), since they are both ⪯_{i} SOS(p). Moreover, it holds that: ∀s ∈ S_{M_{i}}, ∃s′ ∈ S_{N_{i}} such that s ∼ s′ and length(s′) ≤ lengh(s), where length(t) denotes the number of operators occurring in the term t. This holds since terms generated by SS are ”shorter” than terms generated by SOS. Consider an infinite path in M_{i}(p), i.e. a path leading from a state s ∈ S_{M_{i}} to itself and take n equal to the number of terms t equivalent to s and such that length(t) ≤ lengh(s). Take j = i + n.

Note that the converse of the above proposition is not true: if we consider the bag example, no M_{i}(X) exists which is ⪯_{bc} N_{2}(X).

5 Suitability of approximation chains

Let us consider a liveness property ϕ and a ⪯_{bc}-approximation chain {T_{i}(p)} for a term p. Proposition 3.4 above ensures that, if we are able to prove ϕ on an element of the chain, we can assert the validity of ϕ on SOS(p). Thus an algorithm to check the validity of a liveness property is that of checking it on the elements of the chain, starting from the first one, until we find that the property is verified. But the converse of proposition 3.4 is not true in general: if a liveness property ϕ is verified on SOS(p), this does not imply that it is true for some {T_{i}(p)}. Thus, given an approximation chain, the above algorithm (which checks a liveness property on the elements of the chain) is not in general a semidecision procedure for the validity of a formula. This is the case of the chain {M_{i}(p)} and the properties 2) and 3) of our example above. Moreover, different approximation chains for the same term can be used to check different sets of properties, in the sense that, given a property ϕ, it is possible that the above algorithm is a semidecision procedure for ϕ if using a chain, while it cannot be used to semidecide the validity ϕ with another chain. This suggests a comparison criterion on the suitability of approximation chains for proving liveness properties.

Definition 5.1 (Checkable properties) Let be given a term p and a ⪯_{bc} approximation chain {T_{i}(p)}. We say that a liveness property ϕ is checkable by {T_{i}(p)} if

• either ϕ is not verified by SOS(p) or

• (T_{r}(p) ∈ {T_{i}(p)}) exists such that s_{0} ⊧_{T_{r}(p)} ϕ.

The set of checkable properties of p by {T_{i}(p)} is denoted as P_{T_{i}}(p).

Thus P_{T_{i}}(p) includes the properties for whose validity there is a semidecision procedure using {T_{i}(p)}.

Definition 5.2 (Suitability of approximation chains) Let be given a term p and two ⪯_{bc} approximations chains {T_{i}(p)} and {S_{i}(p)}. We say that {T_{i}(p)} is more suitable or equal for p than {S_{i}(p)} if P_{S_{i}}(p) ⊆ P_{T_{i}}(p). Moreover, {T_{i}(p)} is strictly more suitable for p than {S_{i}(p)} if P_{S_{i}}(p) ⊂ P_{T_{i}}(p).

Note that the notion of suitability of approximation chains is different from a notion considering the ”growing rate” of the chains. Given, for example, an approximation chain {T_{i}(p)}, let us consider the chain containing a subset of the elements of {T_{i}(p)}, for example the elements of even position, i.e. {S_{i}(p)} = {T_{0}(p), T_{2}(p), T_{4}(p), ⋯}. We have that {S_{i}(p)} grows faster than {T_{i}(p)}, but it is not more suitable. As a consequence of the above definitions and propositions 4.4, we can state the following propositions:

Proposition 5.1 For each term p, P_{M_{i}}(p) ⊆ P_{N_{i}}(p). Proof sketch. By proposition 4.4.

The following proposition states that the converse of proposition 5.1 is not true in general.

Proposition 5.2 Given a term p, P_{M_{i}}(p) ⊂ P_{N_{i}}(p), i.e. {N_{i}(p)} is strictly more suitable than {M_{i}(p)}. Proof sketch Properties 2) and 3) in the bag example are checkable by {N_{i}(p)} but not by {M_{i}(p)}.

6 Implementation in the JACK environment

The JACK system [3] is a verification environment for process algebra description languages. It is able to cover a large extent of the formal software development process, such as rewriting techniques, behavioural equivalence proofs, graph transformations, and (ACTL) logic verification. In JACK a particular description format is used to represent TSs, the so called format commun fc2, that has been proposed as standard format for automata [18]. The ACTL model checker was built on the basis of an algorithm similar to that of the EMC model checker [5], so it guarantees model checking of an ACTL formula on a TS in a linear time complexity [10].

The JACK environment has been extended with a tool to build the chain {N_{i}(p)}. We now describe the methodology for proving properties. Let be given a CCS term p and a list of ACTL formulae to be checked on it. A verification session has the following steps:

1. The term is input to JACK. If the term satisfies the finiteness condition of the transition system generator inside JACK, a corresponding transition system T S is built and the list of ACTL formulae is checked on it. The session terminates.

2. If the syntactic finiteness conditions are not satisfied, then we call the chain generator of JACK. Once obtained the first approximation N_{1}(p), we put T S := N_{1}(p).

3. The list of ACTL formulae is input to the model checker which checks them on T S. If N_{i+1}(p) = T S, the session terminates, since T S ∼ SOS(p). Otherwise, the results of the model checker are analyzed according to propositions 3.4, 3.6 and 3.8. This means that, possibly, a new approximation is built, i.e. T S := N_{i+1}(p) and we repeat step 3.

Acknowledgement

We wish to acknowledge Luigi Polverini for its work on the implementation of the NSS approximation generator, Rocco De Nicola and Gioia Ristori for interesting discussion about the topics of this paper.

References

[1] J. C. M. Baeten, J. A. Bergstra, J. W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. Journal of ACM 40,3,1993, pp. 653-682.

[2] G. Bruns. A practical technique for process abstraction. CONCUR’93, LNCS 715, pp. 37-49.

[3] A. Bouali, S. Gnesi, S. Larosa. The integration Project for the JACK Environment. Bulletin of the EATCS, n.54, October 1994, pp.207-223.

[4] O. Burkart, B. Steffen. Pushdown processes: Parallel Composition and Model Checking. Proceedings, CONCUR 94, LNCS 836, 1994, pp.98-113.

[5] E.M. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Toplas, 8 (2), 1986, pp. 244-263.

[6] E.M.Clarke, O.Grumberg, D.E.Long. Model Checking and Abstraction. ACM Toplas, 16 (5), 1994, pp.1512-1542.

[7] R. Cleaveland, J. Parrow, B. Steffen. The Concurrency Workbench. Proceedings of Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science 407, Springer-Verlag, 1990, pp. 24-37.

[8] D.Dams, O.Grumberg, R.Gerth. Automatic Verification of Abstract Interpretation of Reactive Systems: Abstractions Preserving ∀CTL*, ∃CTL*, CTL*. IFIP working conference on Programming Concepts, Methods and Calculi (PROCOMET’94), 1994.

[9] N. De Francesco, P. Inverardi. Proving Finiteness of CCS Processes by Non-standard Semantics. Acta Informatica, 31 (1), 1994, pp. 55-80.

[10] R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Network and ISDN systems, Vol. 25, No.7, 1993, pp 761-778.

[11] R. De Nicola, F. W. Vaandrager. Action versus State based Logics for Transition Systems. Proceedings Ecole de Printemps on Semantics of Concurrency. LNCS 469, 1990, pp. 407-419.

[12] J.C. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, J. Sifakis. A Toolbox for the Verification of LOTOS Programs. 14th ICSE, Melbourne, 1992, pp. 246-261.

[13] J. C. Godskesen, K. G. Larsen, M. Zeeberg. TAV Users Manual. Internal Report, Aalborg University Center, Denmark, 1989.

[14] H. Hungar, B. Steffen. Local Model Checking for Context-Free Processes. Proceedings, ICALP 93, LNCS 700, 1993, pp.593-605.

[15] H. Hungar. Local Model Checking for Parallel Composition of Context-Free Processes. Proceedings, CONCUR 94, LNCS 836, 1994, pp.114-128.

[16] H. Huttel, C Stirling. Actions speak louder than words: Proving Bisimilarity for Context Free Processes. LICS 91, IEEE Computer Society Press, 1991, pp. 376-386.

[17] E. Kindler. Safety and Liveness Properties: A Survey. Bulletin of the EATCS, 53, 1994, pp.268-272.

[18] E. Madelaine. Verification Tools from the Concur Project. Bulletin of EATCS 47, 1992, pp. 110-120.

[19] E. Madelaine, D. Vergamini. AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. FORTE ’89, North-Holland, 1990, pp. 61-66.

[20] Z. Manna, A. Pnueli. The Anchored Version of the Temporal Framework, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Lecture Notes in Computer Science 354, Springer-Verlag, 1989, pp. 201-284.

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

[22] D. Taubner. Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. LNCS 369, 1989.