BRICS RS-04-7 Křetínský et al.: On the Expressive Power of Extended Process Rewrite Systems BRICS

Basic Research in Computer Science

On the Expressive Power of Extended Process Rewrite Systems

Mojmír Křetínský Vojtěch Řehák Jan Strejček BRICS Report Series RS-04-7 ISSN 0909-0878 April 2004 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2004, Mojmír Křetínský & Vojtěch Řehák & Jan

Strejček. 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/04/7/

On the Expressive Power of Extended Process Rewrite Systems^{∗}

M. Křetínský, V. Řehák^{†}, and J. Strejček

Department of Computer Science, Faculty of Informatics Masaryk University Brno, Czech Republic

         {kretinsky,rehak,strejcek}@fi.muni.cz

April, 2004

Abstract

We provide a unified view on three extensions of Process rewrite systems (PRS) and compare their and PRS’s expressive power. We show that the class of Petri Nets is less expressible up to bisimulation than the class of Process Algebra extended with finite state control unit. Further we show our main result that the reachability problem for PRS extended with a so called weak finite state unit is decidable.

1 Introduction

An automatic verification of current software systems often needs to model them as infinite-state systems, i.e. systems with an evolving structure and operating on unbounded data types: a network of mobile phones is a concurrent system with evolving structure which dynamically changes its size (and can become very large). Robustness of the network requires that underlying protocols should work for an arbitrarily large (i.e. potentially infinite) number of client processes. A JAVA applet dynamically downloads classes over the network and executes their methods, the stack of activation records should be seen as potentially infinite.

∗This work has been supported by GAČR, grant No. 201/03/1161.

†The co-author is supported by Marie Curie Fellowship of the European Community Programme Improving the Human Research Potential and the Socio-economic Knowledge Base under contract number HPMT-CT-2000-00093.

Infinite-state systems can be specified in a number of ways with their respective advantages and limitations. Petri nets, pushdown automata, and process algebras like BPA, BPP, or PA all serve to exemplify this. Here we employ the classes of infinite-state systems defined by term rewrite systems and called PRS (Process Rewrite Systems) as introduced by Mayr [12]. PRS subsume a variety of the formalisms studied in the context of formal verification (e.g. all the models mentioned above).

A Process Rewrite System is a finite set of rules t ⟶^{a} t′ where a is an action under which a subterm t can be reduced onto a subterm t′. Terms are build up from an empty process ε and a set of process constants using (associative) sequential “.” and (associative and commutative) parallel “∥” operators. The semantics of PRS can be defined by labelled transition systems (LTS) – labelled directed graphs whose nodes (states of the system) correspond to terms modulo properties of “.” and “∥” and edges correspond to individual actions (computational steps) which can be performed in a given state. The relevance of various subclasses of PRS for modelling and analysing programs is shown e.g. in [7], for automatic verification see for example surveys [5, 18].

Mayr [12] has also shown that the reachability problem (i.e. given terms t, t′: is t reducible to t′?) for PRSs is decidable. This property is important to automatic verification as many verification problems, e.g. verification of safety properties, reduce to the reachability problem. Most research (with some recent exceptions, e.g. [3, 7]) has been devoted to the PRS classes from the lower part of the PRS hierarchy, especially to pushdown automata (PDA), Petri nets (PN) and their respective subclasses. We mention the successes of PDA in modeling recursive programs (without process creation), PN modeling dynamic creation of concurrent processes (without recursive calls), and CPDS (communicating pushdown systems [2]) modeling both features. All of these formalisms subsume a notion of a finite state unit (FSU) keeping some kind of global information which is accessible by the ready to be reduced components of a PRS term – hence a FSU can regulate rewriting. On the other hand, using a FSU to extend the PRS rewriting mechanism is very powerful since the state-extended version of PA (sePA) processes has a full Turing-power [1] – the decidability of reachability is lost for sePA, all its superclasses (see Fig. 1), and CPDS as well.

In brief, the purpose of this paper is to present suitable models for some real-life patterns of software systems such that reachability remains decidable. We have proposed two PRS extensions, namely fcPRS ([19], inspired by concurrent constraint programming [17]) and wPRS ([9] for PRS equipped with weak FSU inspired by weak automata [16]). It is shown that they increase the expressive power of those PRS subclasses which do not subsume the notion of finite control. By our opinion (sub)classes of wPRS are suitable for modeling some software systems which can be found in the areas of real-time control programs and communication and cryptographic protocols. In wPRS rewriting, FSU can cycle in any control state, but it can change its state only finitely many times. Hence an LTS generated by wPRS models the consecutive execution of the respective (and differently working) phases of the mentioned software systems.

The outline of the paper is a follows: after some preliminaries we introduce a uniform framework for specifying all extended PRS formalisms in Section 3 and compare their relative expressibility with respect to strong bisimulation in Section 4. Here we also solve (to the best of our knowledge) an open problem of the relationship between PN and sePA classes by showing that PN are less expressible (up to bisimulation) than sePA. In Section 5 we show that all classes of our fcPRS and wPRS extensions keep the reachability problem decidable. The last section summarises our results.

Related work: In the context of reachability analysis one can see at least two approaches: (i) abstraction (approximate) analysis techniques on stronger ’models’ such as sePA and its superclasses with undecidable reachability, e.g. see a recent work [2], and (ii) precise techniques for ’weaker’ models, e.g. PRS classes with decidable reachability, e.g. [10] and another recent work [3]. In the latter one, symbolic representations of set of reachable states are built with respect to various term structural equivalences. Among others it is shown that for the PAD class and the same equivalence as in this paper, when properties of sequential and parallel compositions are taken into account, one can construct nonregular representations based on counter tree automata.

2 Preliminaries

A labelled transition system (LTS) L is a tuple (S, Act, ⟶, α_{0}), where S is a set of states or processes, Act is a set of atomic actions or labels, ⟶⊆ S × Act × S is a transition relation (written α ⟶^{a} β instead of (α, a, β) ∈⟶), α_{0} ∈ S is a distinguished initial state.

We use the natural generalization α ⟶^{σ} β for finite sequences of actions σ ∈ Act^{∗}. The state α is reachable if there is σ ∈ Act^{∗} such that α_{0} ⟶^{σ} α. Let Const = {X, …} be a countably infinite set of process constants. The set T of process terms (ranged over by t, …) is defined by the abstract syntax t = ε | X | t_{1}.t_{2} | t_{1}∥t_{2}, where ε is the empty term, X ∈ Const is a process constant (used as an atomic process), ’∥’ and ’.’ mean parallel and sequential compositions respectively.

The set Const(t) is the set of all constants occurring in a process term t. We always work with equivalence classes of terms modulo commutativity and associativity of ’∥’ and modulo associativity of ’.’ We also define ε.t = t = t.ε and t∥ε = t.

We distinguish four classes of process terms: ’1’ stands for terms consisting of a single process constant only (i.e. ε ∉ 1), ’S’ are sequential terms – without parallel composition, ’P’ are parallel terms – without sequential composition, ’G’ are general terms – with arbitrarily nested sequential and parallel compositions.

Definition 2.1. Let Act = {a, b, ⋯ } be a countably infinite set of atomic actions, α, β ∈ {1, S, P, G} such that α ⊆ β. An (α, β)-PRS (process rewrite system) Δ is a pair (R, t_{0}), where

• R is a finite set of rewrite rules of the form t_{1} ⟶^{a} t_{2}, where t_{1} ∈ α, t_{1} ≠ ε, t_{2} ∈ β are process terms and a ∈ Act is an atomic action,

• t_{0} ∈ β is an initial state.

Given PRS Δ we define Const(Δ) as the set of all constants occurring in the rewrite rules of Δ or in its initial state, and Act(Δ) as the set of all actions occurring in the rewrite rules of Δ. We sometimes write

(t_{1} ⟶^{a} t_{2}) ∈ Δ instead of (t_{1} ⟶^{a} t_{2})∈R.

The semantics of Δ is given by the LTS (S, Act(Δ), ⟶, t_{0}), where S = {t ∈ β | Const(t) ⊆ Const(Δ)} and ⟶ is the least relation satisfying the inference rules:

\frac{(t_{1} ⟶^{a} t_{2}) ∈ Δ}{t_{1} ⟶^{a} t_{2}}, \frac{t_{1} ⟶^{a} t′_{1}}{t_{1}∥t_{2} ⟶^{a} t′_{1}∥t_{2}} , \frac{t_{1} ⟶^{a} t′_{1}}{t_{1}.t_{2} ⟶^{a} t′_{1}.t_{2}} .

If no confusion arises, we sometimes speak about a “process rewrite system” meaning a “labelled transition system generated by process rewrite system”.

Some classes of (α, β)-PRS correspond to widely known models as finite state systems (FS), basic process algebras (BPA), basic parallel processes (BPP), process algebras (PA), pushdown processes (PDA, see [6] for justification), and Petri nets (PN). The other classes were introduced (and named as PAD, PAN, and PRS) by Mayr [12]. The correspondence between (α, β)-PRS classes and acronyms just mentioned can be seen in Figure 1.

3 Extended PRS

In this section we recall the definitions of three different extensions of process rewrite systems, namely state-extended PRS (sePRS) [8], PRS with a finite constraint system (fcPRS) [19], and PRS with a weak finitestate unit (wPRS) [9]. In all cases, the PRS formalism is extended with a finite state unit of some kind.

sePRS State-extended PRS corresponds to PRS extended with s finite state unit without any other restrictions. The well-known example of this extension is the state-extended BPA class (also known as pushdown processes).

wPRS The notion of weakness employed in wPRS formalism corresponds to weak automaton [16] in automata theory. The behaviour of a weak state unit is acyclic, i.e. states of state unit are ordered and nonincreasing during every sequence of actions. As the state unit is finite, its state can be changed only finitely many times during every sequence of actions.

fcPRS The extension of PRS with finite constraint systems is motivated by concurrent constraint programming (CCP) (see e.g. [17]). In CCP the processes work with a shared store (seen as a constraint on values that variables can represent) via two operations, tell and ask. The tell adds a constraint to the store provided the store remains consistent. The ask is a test on the store – it can be executed only if the current store implies a specified constraint.

Formally, values of store form a bounded lattice (called a constraint system) with the lub operation ∧ (least upper bound), the least element tt, and the greatest element ff. The execution of tell(n) changes the value of the store from o to o ∧ n (provided o ∧ n ≠ ff – consistency check). The ask(m) can be executed if the current value of the store o is greater than m.

The state unit of fcPRS has the same properties as the store in CCP. We add two constraints (m, n) to each rewrite rule. The application of a rule corresponds to the concurrent execution of ask(m), tell(n), and rewriting:

• a rule can be applied only if the actual store o satisfies m ≤ o and o ∧ n ≠ ff,

• the application of the rule rewrites the process term and changes the store to o ∧ n.

At first we define the common syntax of extended PRS and then we specify the individual restrictions on state units.

Definition 3.1. Let Act = {a, b, ⋯ } be a countably infinite set of atomic actions, α, β ∈ {1, S, P, G} such that α ⊆ β. An extended (α, β)- PRS Δ is a tuple (M, ≤, R, m_{0}, t_{0}), where

• M is a finite set of states of state unit,

• ≤ is a binary relation over M,

• R is a finite set of rewrite rules of the form (m, t_{1}) ⟶^{a} (n, t_{2}), where t_{1} ∈ α, t_{1} ≠ ε, t_{2} ∈ β, m, n ∈ M, and a ∈ Act,

• Pair (m_{0}, t_{0}) ∈ M × β forms a distinguished initial state of the system.

The specific type of extended (α, β)-PRS is given by further requirements on ≤. An extended (α, β)-PRS is

• (α, β)-sePRS without any requirements.^{1}

• (α, β)-wPRS iff (M, ≤) is a partially ordered set.

• (α, β)-fcPRS iff (M, ≤) is a bounded lattice. The lub operation (least upper bound) is denoted by ∧, the least and the greatest elements are denoted by tt and ff, respectively. We also assume that m_{0} ≠ ff.

1In this case, the relation ≤ can be omitted from the definition.

To shorten our notation we prefer mt over (m, t). As in the PRS case, instead of (mt_{1} ⟶^{a} nt_{2}) ∈ R where Δ = (M, ≤, R, m_{0}, t_{0}), we usually write (mt_{1} ⟶^{a} nt_{2}) ∈ Δ. The meaning of Const(Δ) (process constants used in rewrite rules) and Act(Δ) (actions occurring in rewrite rules) for a given extended PRS Δ is also the same as in the PRS case.

The semantics of extended (α, β)-PRS Δ is given by the corresponding labelled transition system (S, Act(Δ), ⟶, m_{0}t_{0}), where S = M×{t ∈ β | Const(t) ⊆ Const(Δ)}^{2} and the relation ⟶ is defined as the least relation satisfying the inference rule corresponding to the application of rewrite rules (and dependent on the concrete formalism):

sePRS  \frac{(mt_{1} ⟶^{a} nt_{2}) ∈ Δ}{mt_{1} ⟶^{a} nt_{2}}

wPRS  \frac{(mt_{1} ⟶^{a} nt_{2}) ∈ Δ}{mt_{1} ⟶^{a} nt_{2}} if n ≤ m

fcPRS  \frac{(mt_{1} ⟶^{a} nt_{2}) ∈ Δ}{ot_{1} ⟶^{a} (o ∧ n)t_{2}} if m ≤ o and o ∧ n ≠ ff

and two common inference rules

\frac{mt_{1} ⟶^{a} nt′_{1}}{mt_{1}∥t_{2} ⟶^{a} nt′_{1}∥t_{2}} , \frac{mt_{1} ⟶^{a} nt′_{1}}{mt_{1}.t_{2} ⟶^{a} nt′_{1}.t_{2}} ,

where t_{1}, t_{2}, t′_{1} ∈ T and m, n, o ∈ M.

Instead of (1, S)-sePRS, (1, S)-wPRS, (1, S)-fcPRS, … we use a more natural notation seBPA, wBPA, fcBPA, etc. The class seBPP is also known as parallel pushdown automata (PPDA) or multiset automata (MSA), see [14].

4 Expressiveness

Figure 1 describes the hierarchy of PRS classes and their extended counterparts with respect to bisimulation equivalence. If any process in class X can be also defined (up to bisimulation) in class Y we write X ⊆ Y. If additionally Y ⊈ X holds, we write X ⊊ Y and say X is less expressive than Y. This is depicted by the line(s) connecting X and Y with Y

2If Δ is an fcPRS, we eliminate the states with ff as they are unreachable.

sePRS

wPRS

[figure] [figure]

fcPRS

[figure] [figure]

PRS_{(G, G)-PRS}

[figure] [figure]

sePAD

sePAN

wPAD

[figure]

wPAN

[figure]

fcPAD

[figure]

fcPAN

[figure]

PAD_{(S, G)-PRS}

[figure]

PAN_{(P, G)-PRS}

[figure]

sePA

[figure] [figure]

wPA

[figure] [figure]

fcPA

[figure] [figure]

{se,w,fc}PDA=PDA=seBPA

(S, S)-PRS

PA_{(1, G)-PRS}

[figure] [figure]

{se,w,fc}PN=PN

(P, P)-PRS

seBPP=MSA

wBPA

wBPP

fcBPA

fcBPP

BPA_{(1, S)-PRS}

[figure]

BPP_{(1, P)-PRS}

[figure]

{se,w,fc}FS=FS

(1, 1)-PRS

Figure 1: The hierarchy of classes defined by (extended) rewrite formalisms.

placed higher than X in Figure 1. The dotted lines represent the facts X ⊆ Y, where we just conjecture that X ⊊ Y hold.

Some observations (even up to isomorphism) are immediate, for example (i) collapses of the classes FS, PDA and PN with their extended analogues, (ii) if e ∈ {se, w, fc} and X ⊆ Y then eX ⊆ eY, and (iii) (α, β)-PRS ⊆ (α, β)-fcPRS ⊆ (α, β)-wPRS ⊆ (α, β)-sePRS for every (α, β)-PRS class.

The strictness (’⊊’) of the PRS-hierarchy has been proved by Mayr [12], that of the corresponding classes of PRS and fcPRS has been proved in [19], and that of relating fcPRSs, wPRSs, and MSA is shown in [9]. Note the strictness relations wX ⊊ seX hold for all X = PA, PAD, PAN, PRS due to our reachability result for wPRS given in Sec. 5 and due to the full Turing-power of sePA [1].

These proofs together with Moller’s result establishing MSA ⊊ PN [15] complete the strictness proof of Figure 1 – with one exception, namely the relation between PN and sePA classes. Looking at two lines leaving sePA down to the left and down to the right, we note the “left-part collapse” of (S, S)-PRS and PDA proved by Caucal [6] (up to isomorphism). The right-part counterpart is slightly different due to the previously mentioned MSA ⊊ PN. In the next subsection we prove PN ⊊ sePA (in fact it suffices to show PN ⊆ sePA as the strictness is obvious).

4.1 P N ⊊ seP A

We now show that Petri nets are less expressive (with respect to bisimulation) than state-extended Process Algebras. The proof is done by a construction of a sePA Δ′ bisimilar to a given PN Δ. In this section, a Petri net is considered in traditional notation (via finite sets of labelled transitions and places). A state of a PN is a marking of the places P_{1}, P_{2}, …, P_{k}, k = |Const(Δ)| and it is given as a k-tuple, where the i-th component stands for the number of tokens at place P_{i}.

Let L_{i} be the maximal number of arrows between any transition and place P_{i}. We put M_{i} = k ∗ L_{i}.

Each state of sePA Δ′ will consist of a term (a parallel composition of k counters for corresponding marking) and a state of a finite-state control unit (FSU). Each state of FSU is the product of three parts as:

{1, …, k} × ({−M_{1}, …, 2∗M_{1}}×…×{−M_{k}, …, 2∗M_{k}}) × {0, 1}^{k}

update controller  modulo counter  empty info

The update controller goes around the range and refers to the counter being updated in the next step. The modulo counter is k-tuple of counters with values from −M_{i} to 2 ∗ M_{i}. Each of them saves the number of tokens in one state counted modulo M_{i}. The empty info says which term counters are empty.

We define 2k process constants B_{i}, X_{i} ∈ Const(Δ′), B_{i} representing the bottom of i-th counter and X_{i} representing M_{i} tokens at place P_{i}.

For a given initial marking α = (p_{1}, p_{2}, …, p_{k}) of a PN Δ we construct the following initial state of the sePA Δ′

1(m_{1}, m_{2}, …, m_{k})(e_{1}, e_{2}, …, e_{k})t_{1}∥t_{2}∥ ⋯ ∥t_{k}

where m_{i} = p_{i} mod M_{i}, if n = 0 then e_{i} = 1 else e_{i} = 0, and t_{i} = X_{i}^{n}B_{i}, where n = p_{i} div M_{i}. In other words we have p_{i} = m_{i} + n ∗ M_{i}.

For each PN transition ((l_{1}, l_{2}, …, l_{k}) ⟶^{a} (r_{1}, r_{2}, …, r_{k})) ∈ Δ we construct the set of sePA rules

s(m_{1}, …, m_{k})(e_{1}, …, e_{k})t ⟶^{a} s′(m′_{1}, …, m′_{k})(e′_{1}, …, e′_{k})t′

such that they obey the following conditions:

• Update controller conditions: s ∈ {1, …, k} and s′ = (s mod k)+1.

• The general conditions for modulo counters and empty infos (1 ≤ i ≤ k):

– m_{i}, m′_{i} ∈ {−M_{i}, …, 2 ∗ M_{i}}, e_{i}, e′_{i} ∈ {0, 1},

– if e_{i} = 1 then m_{i} ≥ l_{i} (i.e. the transition can be performed),

– if i ≠ s then m′_{i} = m_{i} − l_{i} + r_{i}, e′_{i} = e_{i} else m′_{s} = (m_{s} − l_{s} + r_{s}) mod M_{s}

We now specify e′_{s} and the terms t, t′. The first two Bottom rules, t = B_{s}, are the rules for working with the empty stack. The next three Top rules, t = X_{s}, describe the rewriting of a process constant X_{s}. Depending on the values of m_{s} − l_{s} + r_{s}, there are dec, inc, and basic variants manipulating the s-th stack.

Rule  t  m_{s} − l_{s} + r_{s} ∈  e′_{s}  t′
Bottom-basic rule B_{s}  {0, …, M_{s} − 1}  1  B_{s}
Bottom-inc rule  B_{s} {M_{s}, …, 2 ∗ M_{s}} 0 X_{s}.B_{s}
Top-dec rule  X_{s}  {−M_{s}, …, −1}  0  ε
Top-basic rule  X_{s} {0, …, M_{s} − 1}  0  X_{s}
Top-inc rule  X_{s} {M_{s}, …, 2 ∗ M_{s}} 0 X_{s}.X_{s}

Notation. In the following Lemmata 4.1 to 4.3 let β be a reachable state of sePA Δ′, β = s(m_{1}, m_{2}, …, m_{k})(e_{1}, e_{2}, …, e_{k})t_{1}∥t_{2}∥ … ∥t_{k}, and n_{i} to be the number of constants X_{i} in the term t_{i} of β. We also refer to α as a marking of PN Δ corresponding to the state β, and p_{i} is the number of tokens at the i-th place of the marking α, and

((l_{1}, l_{2}, … l_{k}) ⟶^{a} (r_{1}, r_{2}, … r_{k})) ∈ Δ is a PN rule.

The following lemma shows that modulo counters never overflow.

Lemma 4.1. −M_{i} + L_{i} − 1 < m_{i} < 2 ∗ M_{i} − L_{i} for all reachable states.

Proof. If the i-th stack has been just updated, then −1 < m_{i} < M_{i}. As there are exactly k − 1 states to the next updating and each transition works with at most L_{i} tokens of P_{i}, each of the states differs from the updated one by at most (k − 1) ∗ L_{i} tokens at P_{i}. As M_{i} = k ∗ L_{i}, the lemma holds.

Lemma 4.2. p_{i} = m_{i} + n_{i} ∗ M_{i} for all reachable states.

Proof. For the initial state the lemma is implied directly from the definition. The inductive step proving the lemma for other reachable states is a straightforward consequence of the m′_{i} and t′ conditions in the definition of sePA rules.

Lemma 4.2 shows that every sePA state β saves the numbers of tokens of α. The following lemma proves that every transition of Δ can be performed in α if and only if there is a corresponding rewrite rule that can be used in β.

Lemma 4.3. p_{i} ≥ l_{i} iff (e_{i} = 0 or m_{i} ≥ l_{i}) for all reachable states.

Proof. If the i-th stack has just been updated and e_{i} = 1, a Bottom-basic rule was used and so m_{i} = p_{i}. These conditions stay unchanged till the next updating.

If e_{i} has been updated to 0, then p_{i} ≥ M_{i}. There are k − 1 states to the next updating. Hence p_{i} ≥ M_{i} − (k − 1) ∗ L_{i} = L_{i} in all these states and according to the definition of L_{i}, L_{i} ≥ l_{i} and so p_{i} ≥ l_{i}.

Theorem 4.4. PN ⊊ sePA with respect to bisimulation.

Proof. Lemma 4.1 and Lemma 4.2 show that the construction of sePA presented here, saves every marking correctly, while Lemma 4.3 proves that the corresponding states are bisimilar. Hence, PN ⊆ sePA (with respect to bisimulation). Strictness follows from two of the results mentioned in the introduction, namely the full Turing-power of sePA [1] and the decidability of reachability for PRS [12].

5 Reachability for wPRS is decidable

In the following we show that for a given wPRS Δ and its states rt_{1}, st_{2} it is decidable whether st_{2} is reachable from rt_{1} or not (st_{2} is reachable from rt_{1} if a sequence of actions σ such that rt_{1} ⟶^{σ} st_{2}) exists.

Our proof exhibits a similar structure to the proof of decidability of the reachability problem for PRS [12]; at first we reduce the general problem to the reachability problem for wPRS with rules containing at most one occurrence of a sequential or parallel operator, and then we solve this subproblem using the fact that reachability problems for both PN and PDA are decidable [11, 4]. The latter part of the proof is based on a new idea of passive steps presented later.

As the labels on rewrite rules are not relevant here, we omit them in this section. To distinguish between rules and rewriting sequences we use rt_{1} ≻^{Δ} st_{2} to denote that in wPRS Δ the state st_{2} is reachable from rt_{1}. Further, states of weak state unit are called weak states.

Definition 5.1. Let Δ be a wPRS. A rewrite rule in Δ is parallel or sequential if it has one of the following forms:

parallel: pX ⟶ qY ∥Z pX∥Y ⟶ qZ pX ⟶ qY pX ⟶ qε,
sequential: pX ⟶ qY.Z pX.Y ⟶ qZ pX ⟶ qY pX ⟶ qε,

where X, Y, Z are process constants and p, q are weak states. A rule is trivial if it is both parallel and sequential (i.e. it has the form pX ⟶ qY or pX ⟶ qε). A wPRS Δ is in normal form if every rewrite rule in Δ is parallel or sequential.

Lemma 5.2. For wPRS Δ, terms t_{1}, t_{2}, and weak states r, s, there are terms t′_{1}, t′_{2} of wPRS Δ′ in normal form satisfying rt_{1} ≻^{Δ} st_{2} ⟺ rt′_{1} ≻^{Δ′} st′_{2}. Moreover, wPRS Δ′ and terms t′_{1}, t′_{2} can be effectively constructed.

Proof. In this proof we assume that the sequential composition is leftassociative. It means that the term X.Y.Z is (X.Y).Z and so its subterms are X, Y, Z, and X.Y, but not Y.Z. However, the term Y ∥Z is a subterm of X.(Y ∥Z).

Let size(t) denote the number of sequential and parallel operators in term t. For every wPRS Δ, let k_{i} be the number of rules (rt_{1} ⟶ st_{2}) ∈ Δ that are neither parallel nor sequential and size(rt_{1} ⟶ st_{2}) = i, where size(rt_{1} ⟶ st_{2}) = size(t_{1}) + size(t_{2}). Thus, Δ is in normal form iff k_{i} = 0 for every i. In this case, let n = 0. Otherwise, let n be the maximal i such that k_{i} ≠ 0 (n existing as the set of rules is finite). We define norm(Δ) to be the pair (n, k_{n}).

Now we describe a procedure transforming Δ (if it is not in a normal form) onto a wPRS Δ′ and terms t_{1}, t_{2} onto terms t′_{1}, t′_{2} such that norm(Δ′) < norm(Δ) (with respect to lexicographical ordering) and rt_{1} ≻^{Δ} st_{2} ⟺ rt′_{1} ≻^{Δ′} st′_{2}.

Let us assume that wPRS Δ is not in normal form. Then there is a rule that is neither sequential nor parallel and has the maximal size. Take a non-atomic subterm t of this rule and replace every subterm t in Δ (i.e. in rewrite rules and initial term) and in t_{1} and t_{2} by a fresh constant X. Then add two rules pX ⟶ pt and pt ⟶ pX for each weak state p. This yields a new wPRS Δ′ and terms t′_{1} and t′_{2} where the constant X serves as an abbreviation for the term t. By the definition of norm we get norm(Δ′) < norm(Δ). The correctness of our transformation remains to be demonstrated:

rt_{1} ≻^{Δ} st_{2} ⟺ rt′_{1} ≻^{Δ′} st′_{2}

The implication ⟸ is obvious. For the opposite direction we show that every rewriting step in Δ from pl_{1} to ql_{2} under the rule (pl ⟶ ql′) ∈ Δ corresponds to a sequence of several rewriting steps in Δ′ leading from pl′_{1} to ql′_{2}, where l′_{1}, l′_{2} equal to l_{1}, l_{2} with all occurrences of t replaced by X. Let us assume the rule pl ⟶ ql′ modifies a subterm t of pl_{1}, and/or a subterm t appears in ql_{2} after the rule application (other cases are trivial). If the rule modifies a subterm t of l_{1} there are two cases. Either l subsumes whole t and then the corresponding rule in Δ′ (with t replaced by X) can be applied directly on pl′_{1}, or due to the left-associativity of sequential operator, t is not a subterm of the right part of any sequential composition in l_{1} and thus the application of the corresponding rule in Δ′ on pl′_{1} is preceded by an application of the added rule pX ⟶ pt. The situation when subterm t appears in ql_{2} after the application of the considered rule is similar. Either l′ subsumes whole t and then the application of the corresponding rule in Δ′ results directly in ql′_{2}, or t is not a subterm of the right part of any sequential composition in l_{2} and thus the application of the corresponding rule in Δ′ is followed by an application of the added rule qt ⟶ qX reaching the state ql′_{2}.

By repeating this procedure we finally get a wPRS Δ′′ in normal form and terms t′′_{1},t′′_{2} satisfying rt_{1} ≻^{Δ} st_{2} ⟺ rt′′_{1} ≻^{Δ′′} st′′_{2}.

Mayr’s proof of the reachability problem for PRS now completes the PRS Δ in normal form into so-called transitive normal form satisfying (X ⟶ Y) ∈ Δ whenever X ≻^{Δ} Y. This step employs the local effect of rewriting under sequential rules in a parallel environment and vice versa. Intuitively, whenever there is a rewriting sequence

X∥Y ⟶ (X_{1}.X_{2})∥Y ⟶ (X_{1}.X_{2})∥Z ⟶ X_{2}∥Z

in PRS in normal form, then the rewriting of each parallel component is independent in the sense that there are also rewriting sequences X ⟶ X_{1}.X_{2} ⟶ X_{2} and Y ⟶ Z. This does not hold for wPRS in normal form as the rewriting on one parallel component can influence the rewriting on other parallel components via a weak state unit. To get its independence back we introduce the concept of passive steps emulating changes of a weak state produced by the environment.

Definition 5.3. A finite sequence of weak states pairs PS = {(p_{i}, q_{i})}_{i=1}^{n} satisfying p_{1} > q_{1} ≥ p_{2} > q_{2} ≥ ⋯ ≥ p_{n} > q_{n} is called passive steps.

Let Δ be a wPRS and PS be passive steps. By Δ + PS we denote a system Δ with an added rule pX ⟶ qX for each (p, q) in PS and X ∈ Const(Δ). For all terms t_{1}, t_{2} and weak states r, s we write

rt_{1} ≻_{triv}^{Δ+PS} st_{2} iff rt_{1} ≻^{Δ+PS} st_{2} via trivial rules,
rt_{1} ≻_{seq}^{Δ+PS} st_{2} iff rt_{1} ≻^{Δ+PS} st_{2} via sequential rules,
rt_{1} ≻_{par}^{Δ+PS} st_{2} iff rt_{1} ≻^{Δ+PS} st_{2} via parallel rules.

Informally, rt_{1} ≻^{Δ+PS} st_{2} means that the state rt_{1} can be rewritten onto state st_{2} provided a weak state can be passively changed from p to q for every passive step (p, q) in PS. Thanks to the finiteness of a weak state unit, the number of different passive steps is finite.

Definition 5.4. Let wPRS Δ be in normal form. If for every X, Y ∈ Const(Δ), weak states r, s, and passive steps PS it holds that

• rX ≻^{Δ+PS} sY ⟹ rX ≻_{triv}^{Δ+PS} sY then Δ is in flatted normal form,

• rX ≻_{seq}^{Δ+PS} sY ⟹ rX ≻_{triv}^{Δ+PS} sY then Δ is in sequential flatted normal form,

• rX ≻_{par}^{Δ+PS} sY ⟹ rX ≻_{triv}^{Δ+PS} sY then Δ is in parallel flatted normal form.

The following lemma says that it is sufficient to check reachability via sequential rules and via parallel rules in order to construct a wPRS in flatted normal form. This allows to reduce the reachability problem for wPRS to the reachability problems for wPN and wPDA (i.e. to the reachability problems for PN and PDA).

Lemma 5.5. If a wPRS is in both sequential and parallel flatted normal form then it is in flatted normal form as well.

Proof. We assume the contrary and derive a contradiction. Let Δ be a wPRS in sequential and parallel flatted normal form. Now let us choose passive steps PS and a rewriting sequence in Δ + P S leading from rX to sY such that rX ⊁_{triv}^{Δ+PS} sY and the number of applications of non-trivial rewrite rules used in the sequence is minimal.

As the wPRS Δ is in both sequential and parallel flatted normal form, rX ⊁_{seq}^{Δ+PS} sY and rX ⊁_{par}^{Δ+PS} sY. Hence, both sequential and parallel operators occur in the rewriting sequence. There are two cases.

1. Assume that a sequential operator appears first. The parallel operator is then introduced by a rule in the form pU ⟶ qU_{1}∥U_{2} applied to a state pU.t, where t ∈ S. From q(U_{1}∥U_{2}).t ≻^{Δ+PS} sY and the fact that at most one process constant can be removed in one rewriting step, it follows that in the rest of the sequence considered, the term (U_{1}∥U_{2}) is rewritten onto a process constant (say V) first. Let PS′ be PS in this case.

2. Assume that a parallel operator appears first. The sequential operator is then introduced by a rule in the form pU ⟶ qU_{1}.U_{2} applied to a state pU∥t, where t ∈ P. The rest of the sequence subsumes steps rewriting the term U_{1}.U_{2} onto a process constant (say V). Contrary to the previous case, these steps can be interleaved with steps rewriting other parallel components and possibly changing weak state. Let PS′ be passive steps PS merged with these changes of weak states.

Consequently, we have a rewriting sequence in Δ + PS′ from pU to oV (for some o) with fewer applications of non-trivial rewrite rules. As the number of applications of non-trivial rewrite rules used in the original sequence is minimal we get pU ⊁_{triv}^{Δ+PS′} oV. This contradicts our choice of rX, sY, and PS.

Lemma 5.6. For every wPRS system Δ in normal form, terms t_{1}, t_{2} over Const(Δ), and weak states r, s of Δ a wPRS Δ′ can be constructed such that Δ′ is in flatted normal form satisfying rt_{1} ≻^{Δ} st_{2} ⟺ rt_{1} ≻^{Δ′} st_{2}.

Proof. To obtain Δ′ we enrich Δ by trivial rewrite rules transforming the system into sequential and parallel flatted normal forms, which suffices thanks to Lemma 5.5. Using algorithms deciding reachability for PDA and PN, the algorithm checks if there are some weak states r, s, constants X, Y ∈ Const(Δ), and passive steps PS = {(p_{i}, q_{i})}_{i=1}^{n} (satisfying r ≥ p_{1} and q_{n} ≥ s as weak states pairs beyond this range are of no use here) such that rX ≻_{seq}^{Δ+PS} sY ∨ rX ≻_{par}^{Δ+PS} sY and rX ⊁_{triv}^{Δ+PS} sY. We finish if the answer is negative. Otherwise we add to Δ rules rX ⟶ p_{1}Z_{1}, q_{i}Z_{i} ⟶ p_{i+1}Z_{i+1} for i = 1, …, n − 1, and q_{n}Z_{n} ⟶ sY, where Z_{1}, …, Z_{n} are fresh process constants (if n = 0 then we add just the rule rX ⟶ sY). The algorithm then repeats this procedure on the system with added rules with one difference; the X, Y ranges over the constants of the original system Δ. This is sufficient as new constants occur only in trivial rules^{3}. The algorithm terminates as the number of iterations is bounded by the number of pairs of states rX, sY of Δ, times the number of passive steps PS. The correctness follows from the fact that added rules have no influence on reachability.

Theorem 5.7. The reachability problem for wPRS is decidable.

Proof. Let Δ be a wPRS and rt_{1}, st_{2} its states. We want to decide whether rt_{1} ≻^{Δ} st_{2} or not. Clearly rt_{1} ≻^{Δ} st_{2} ⟺ rX ≻^{Δ′} sY, where X, Y are fresh constants and Δ′ arises from Δ by the addition of the rules rX ⟶ rt_{1} and st_{2} ⟶ sY^{4}. Hence we can directly assume that t_{1}, t_{2} are process constants, say X, Y. Lemma 5.2 and Lemma 5.6 successively reduce the question whether rX ≻^{Δ} sY to question whether rX ≻^{Δ′} sY, where Δ′ is in flatted normal form – note that Lemma 5.2 does not change terms t_{1}, t_{2} if they are process constants. The definition of flatted normal form implies rX ≻^{Δ′} sY ⟺ rX ≻_{triv}^{Δ′} sY. Finally the relation rX ≻_{triv}^{Δ′} sY is easy to check.

6 Conclusions

We have presented a unified view on some (non-conservative) extensions of Process Rewrite Systems. Comparing the mutual expressiveness of the respective subclasses up to bisimulation equivalence, we have added some new strict relations, including the class of Petri Nets being less expressible than the class of Process Algebra extended with finite state control unit. We have shown that our extensions keep the reachability problem decidable and we believe that they may be suitable for modeling some real-life software systems.

3If the system with added rules is not in sequential or parallel flatted normal form, then there is a counterexample with the constants X, Y of the original system Δ.

4If t_{2} = ε then this is not a correct rule. In this case we need to add to Δ′ a rule pt ⟶ qY for each rule (pt ⟶ qε) ∈ Δ.

References

[1] A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregular properties for nonregular processes. In Proc. of LICS’95. IEEE, 1995.

[2] A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. International Journal on Foundations of Computer Science, 14(4):551–582, 2003.

[3] A. Bouajjani and T. Touili. Reachability Analysis of Process Rewrite Systems. In Proc. of FST&TCS-2003, volume 2914 of LNCS, pages 74–87. Springer, 2003.

[4] J. R. Büchi. Regular canonical systems. Arch. Math. Logik u. Grundlagenforschung, 6:91–111, 1964.

[5] O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In Handbook of Process Algebra, pages 545–623. Elsevier, 2001.

[6] D. Caucal. On the regular structure of prefix rewriting. Theoretical Computer Science, 106:61–86, 1992.

[7] J. Esparza. Grammars as processes. In Formal and Natural Computing, volume 2300 of LNCS. Springer, 2002.

[8] P. Jančar, A. Kučera, and R. Mayr. Deciding bisimulation-like equivalences with finite-state processes. Theoretical Computer Science, 258:409–433, 2001.

[9] M. Křetínský, V. Řehák, and J. Strejček. Process Rewrite Systems with Weak Finite-State Unit. Technical Report FIMU-RS-2003-05, Masaryk University Brno, 2003. to appear in ENTCS as Proc.of INFINITY 03.

[10] D. Lugiez and Ph. Schnoebelen. The regular viewpoint on PAprocesses. In Proc. of CONCUR’98, volume 1466 of LNCS, pages 50–66, 1998.

[11] E. W. Mayr. An algorithm for the general petri net reachability problem. In Proc. of 13th Symp. on Theory of Computing, pages 238–246. ACM Press, 1981.

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

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

[14] F. Moller. Infinite results. In Proc. of CONCUR’96, volume 1119 of LNCS, pages 195–216. Springer, 1996.

[15] F. Moller. Pushdown Automata, Multiset Automata and Petri Nets, MFCS Workshop on concurrency. Electronic Notes in Theoretical Computer Science, 18, 1998.

[16] D. Muller, A. Saoudi, and P. Schupp. Alternating automata, the weak monadic theory of trees and its complexity. Theoret. Computer Science, 97(1–2):233–244, 1992.

[17] V. A. Saraswat and M. Rinard. Concurrent constraint programming. In Proc. of 17th POPL, pages 232–245. ACM Press, 1990.

[18] J. Srba. Roadmap of infinite results. EATCS Bulletin, (78):163–175,

2002. http://www.brics.dk/~srba/roadmap/.

[19] J. Strejček. Rewrite systems with constraints, EXPRESS’01. Electronic Notes in Theoretical Computer Science, 52, 2002.

Recent BRICS Report Series Publications

RS-04-7 Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček. On the Expressive Power of Extended Process Rewrite Systems. April 2004. 18 pp.

RS-04-6 Gudmund Skovbjerg Frandsen and Igor E. Shparlinski. On Reducing a System of Equations to a Single Equation. March 2004. 11 pp. To appear in Schicho and Singer, editors, ACM SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC ’04 Proceedings, 2004.

RS-04-5 Biernacki Dariusz and Danvy Olivier. From Interpreter to Logic Engine by Defunctionalization. March 2004. 20 pp. To appear in Bruynooghe, editor, International Symposium on Logic Based Program Development and Transformation, LOPSTR ’03 Proceedings, Revised Selected Papers, LNCS, 2003. This report supersedes the earlier BRICS report RS-03-25.

RS-04-4 Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal Strategies in Priced Timed Game Automata. February 2004. 32 pp.

RS-04-3 Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines. February 2004. 17 pp. This report supersedes the earlier BRICS report RS-03-24. Extended version of an article to appear in Information Processing Letters.

RS-04-2 Gerth Stølting Brodal, Rolf Fagerberg, Ulrich Meyer, and Norbert Zeh. Cache-Oblivious Data Structures and Algorithms for Undirected Breadth-First Search and Shortest Paths. February 2004. 19 pp.

RS-04-1 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy’s Merge. January 2004. 16 pp.

RS-03-53 Kyung-Goo Doh and Peter D. Mosses. Composing Programming Languages by Combining Action-Semantics Modules. December 2003. 39 pp. Appears in Science of Computer Programming, 47(1):2–36, 2003.