当前位置：文档库 › On the Expressive Power of Extended Process Rewrite Systems

On the Expressive Power of Extended Process Rewrite Systems

BRICS RS-04-7 Kˇr et′

?nsk′y et al.: On the Expressive

Power

of Extended

Process Rewrite Systems

BRICS ISSN0909-0878April2004

Strejˇc ek.

BRICS,Department of Computer Science

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,building540

DK–8000Aarhus C

Denmark

Telephone:+4589423360

Telefax:+4589423255

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ˇr et′?nsk′y,V.ˇReh′a k?,and J.Strejˇc 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 uni?ed 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?-

nite state control unit.Further we show our main result that the

reachability problem for PRS extended with a so called weak?nite

state unit is decidable.

1Introduction

An automatic veri?cation of current software systems often needs to model them as in?nite-state systems,i.e.systems with an evolving struc-ture 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 re-quires that underlying protocols should work for an arbitrarily large

(i.e.potentially in?nite)number of client processes.A JAVA applet dy-namically downloads classes over the network and executes their meth-ods,the stack of activation records should be seen as potentially in?nite.

In?nite-state systems can be speci?ed 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 in?nite-state systems de?ned 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 veri?cation(e.g.all the models mentioned above).

A Process Rewrite System is a?nite 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 de?ned 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 veri?cation 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 veri?cation as many veri?cation problems,e.g. veri?cation 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 push-down automata(PDA),Petri nets(PN)and their respective subclasses. We mention the successes of PDA in modeling recursive programs(with-out process creation),PN modeling dynamic creation of concurrent pro-cesses(without recursive calls),and CPDS(communicating pushdown systems[2])modeling both features.All of these formalisms subsume a notion of a?nite state unit(FSU)keeping some kind of global informa-tion 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?nite 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 com-munication and cryptographic protocols.In wPRS rewriting,FSU can cycle in any control state,but it can change its state only?nitely many times.Hence an LTS generated by wPRS models the consecutive execu-tion of the respective(and di?erently 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 for-malisms in Section3and compare their relative expressibility with re-spect to strong bisimulation in Section4.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 bisim-ulation)than sePA.In Section5we 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 par-allel compositions are taken into account,one can construct nonregular representations based on counter tree automata.

2Preliminaries

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?nite sequences of actionsσ∈Act?.The stateαis reachable if there isσ∈Act?such that α0σ?→α.Let Const={X,...}be a countably in?nite set of process constants.The set T of process terms(ranged over by t,...)is de?ned by the abstract syntax t=ε|X|t1.t2|t1 t2,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 com-mutativity and associativity of’ ’and modulo associativity of’.’We also de?neε.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.

De?nition 2.1.Let Act={a,b,···}be a countably in?nite set of atomic actions,α,β∈{1,S,P,G}such thatα?β.An(α,β)-PRS (process rewrite system)?is a pair(R,t0),where

?R is a?nite set of rewrite rules of the form t1a?→t2,where t1∈α, t1=ε,t2∈βare process terms and a∈Act is an atomic action,?t0∈βis an initial state.

Given PRS?we de?ne 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 (t1a?→t2)∈?instead of(t1a?→t2)∈R.

The semantics of?is given by the LTS(S,Act(?),?→,t0),where S={t∈β|Const(t)?Const(?)}and?→is the least relation satisfying the inference rules:

(t1a?→t2)∈?

t1 t2a?→t′1 t2,

t1a?→t′1

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?-nite state systems(FS),basic process algebras(BPA),basic parallel pro-cesses(BPP),process algebras(PA),pushdown processes(PDA,see[6] for justi?cation),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 Figure1.

3Extended PRS

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

sePRS State-extended PRS corresponds to PRS extended with s?-nite 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 corre-sponds 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 non-increasing during every sequence of actions.As the state unit is?nite, its state can be changed only?nitely many times during every sequence of actions.

fcPRS The extension of PRS with?nite constraint systems is mo-tivated by concurrent constraint programming(CCP)(see e.g.[17]).In CCP the processes work with a shared store(seen as a constraint on val-ues 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 speci?ed 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 satis?es m≤o and o∧n=ff,

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

At?rst we de?ne the common syntax of extended PRS and then we specify the individual restrictions on state units.

De?nition 3.1.Let Act={a,b,···}be a countably in?nite set of atomic actions,α,β∈{1,S,P,G}such thatα?β.An extended(α,β)-PRS?is a tuple(M,≤,R,m0,t0),where

?M is a?nite set of states of state unit,

?≤is a binary relation over M,

?R is a?nite set of rewrite rules of the form(m,t1)a?→(n,t2), where t1∈α,t1=ε,t2∈β,m,n∈M,and a∈Act,

?Pair(m0,t0)∈M×βforms a distinguished initial state of the system.

The speci?c type of extended(α,β)-PRS is given by further require-ments on≤.An extended(α,β)-PRS is

?(α,β)-sePRS without any requirements.1

?(α,β)-wPRS i?(M,≤)is a partially ordered set.

?(α,β)-fcPRS i?(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 m0=ff.

To shorten our notation we prefer mt over(m,t).As in the PRS case, instead of(mt1a?→nt2)∈R where?=(M,≤,R,m0,t0),we usually write(mt1a?→nt2)∈?.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 correspond-ing labelled transition system(S,Act(?),?→,m0t0),where S=M×{t∈β|Const(t)?Const(?)}2and the relation?→is de?ned as the least relation satisfying the inference rule corresponding to the application of rewrite rules(and dependent on the concrete formalism):

sePRS

(mt1a?→nt2)∈?

mt1a?→nt2

if n≤m

fcPRS

(mt1a?→nt2)∈?

mt1 t2a?→nt′1 t2,

mt1a?→nt′1

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

sePRS

J J J J J J J J J J J J J J J J J J J J J J J J J J J wPAN u u u u u u u u u u u u u u u u u u u u u u u u u J J J J J J J J J J J J J J J J J J J J J J J J J J fcPAN u u u u u u u u u u u u u u u u u u u u u u u u u J J J J J J J J J J J J J J J J J J J J J J J J J J PAN (P,G )-PRS v v v v v v v v v v v v v v v v v v v v v v v v N N N N N N N N N N N N N N N N N N N N wPA t t t t t t t t t t t t t t t t t t t t t t t t t t t H

H H H H H H H H H H H H H H H H H H H H H H H H {se,w,fc }PDA=PDA=seBPA (S,S )-PRS seBPP=MSA wBPP fcBPP

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.5and 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 Figure1–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 col-lapse”of(S,S)-PRS and PDA proved by Caucal[6](up to isomorphism). The right-part counterpart is slightly di?erent due to the previously men-tioned MSA PN.In the next subsection we prove PN sePA(in fact it su?ces to show PN?sePA as the strictness is obvious).

4.1P N seP A

We now show that Petri nets are less expressive(with respect to bisim-ulation)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?nite sets of la-belled transitions and places).A state of a PN is a marking of the places P1,P2,...,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?nite-state control unit(FSU).Each state of FSU is the product of three parts as: {1,...,k}×({?M1,...,2?M1}×...×{?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 to2?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 de?ne2k 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α=(p1,p2,...,p k)of a PN?we construct the following initial state of the sePA?′

1(m1,m2,...,m k)(e1,e2,...,e k)t1 t2 ··· t k

where m i=p i mod M i,if n=0then e i=1else e i=0,and t i=X n i 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((l1,l2,...,l k)a?→(r1,r2,...,r k))∈?we construct the set of sePA rules

s(m1,...,m k)(e1,...,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′

∈{?M i,...,2?M i},e i,e′i∈{0,1},

–if e i=1then 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?rst 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 manipu-lating the s-th stack.

Rule m s?l s+r s∈t′

B s1

B s0

X s0

Lemma4.1.?M i+L i?1

Lemma4.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 de?ni-tion.The inductive step proving the lemma for other reachable states is a straightforward consequence of the m′i and t′conditions in the de?nition of sePA rules.

Lemma4.2shows 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β.

Lemma4.3.p i≥l i i?(e i=0or 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 to0,then p i≥M i.There are k?1states to the next updating.Hence p i≥M i?(k?1)?L i=L i in all these states and according to the de?nition of L i,L i≥l i and so p i≥l i.

Theorem4.4.PN sePA with respect to bisimulation.

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

5Reachability for wPRS is decidable

In the following we show that for a given wPRS?and its states rt1,st2 it is decidable whether st2is reachable from rt1or not(st2is reachable from rt1if a sequence of actionsσsuch that rt1σ?→st2)exists.

Our proof exhibits a similar structure to the proof of decidability of the reachability problem for PRS[12];at?rst 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 rt1??st2to denote that in wPRS?the state st2is reachable from rt1.Further,states of weak state unit are called weak states.

De?nition5.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.

Lemma5.2.For wPRS?,terms t1,t2,and weak states r,s,there are terms t′1,t′2of wPRS?′in normal form satisfying rt1??st2??

rt′

1??′st′2.Moreover,wPRS?′and terms t′1,t′2can be e?ectively con-

structed.

Proof.In this proof we assume that the sequential composition is left-associative.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(rt1?→st2)∈?that are neither parallel nor sequential and size(rt1?→st2)=i,where size(rt1?→st2)=size(t1)+size(t2).Thus,?is in normal form i?k i=0for 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?nite).We de?ne norm(?)to be the pair(n,k n).

Now we describe a procedure transforming?(if it is not in a nor-mal form)onto a wPRS?′and terms t1,t2onto terms t′1,t′2such that norm(?′)

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 t1and t2by 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′1and t′2where the constant X serves as an abbreviation for the term t.By the de?nition of norm we get norm(?′)

rt1??st2??rt′1??′st′2

The implication?=is obvious.For the opposite direction we show that every rewriting step in?from pl1to ql2under the rule(pl?→ql′)∈?corresponds to a sequence of several rewriting steps in?′leading from

pl′

1to ql′2,where l′1,l′2equal to l1,l2with all occurrences of t replaced by

X.Let us assume the rule pl?→ql′modi?es a subterm t of pl1,and/or a subterm t appears in ql2after the rule application(other cases are trivial).If the rule modi?es a subterm t of l1there 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 l1and thus the application of the corresponding rule in ?′on pl′1is preceded by an application of the added rule pX?→pt. The situation when subterm t appears in ql2after 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 l2and 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?nally get a wPRS?′′in normal form and terms t′′1,t′′2satisfying rt1??st2??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 e?ect of rewriting under sequential rules in a parallel environment and vice versa. Intuitively,whenever there is a rewriting sequence

X Y?→(X1.X2) Y?→(X1.X2) Z?→X2 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?→X1.X2?→X2and Y?→Z.This does not hold for wPRS in nor-mal form as the rewriting on one parallel component can in?uence 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.

De?nition5.3.A?nite sequence of weak states pairs PS={(p i,q i)}n i=1 satisfying p1>q1≥p2>q2≥···≥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 t1,t2and weak states r,s we write

rt1??+PS

triv

st2i?rt1??+PS st2via trivial rules,

rt1??+PS

seq

st2i?rt1??+PS st2via sequential rules,

rt1??+PS

par

st2i?rt1??+PS st2via parallel rules.

Informally,rt1??+PS st2means that the state rt1can be rewritten onto state st2provided a weak state can be passively changed from p to q for every passive step(p,q)in PS.Thanks to the?niteness of a weak state unit,the number of di?erent passive steps is?nite.

De?nition5.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??+PS

triv sY

then?is in?atted normal form,

?rX??+PS

seq sY=?rX??+PS

triv

then?is in sequential?atted normal form,

?rX??+PS

par sY=?rX??+PS

triv

then?is in parallel?atted normal form.

The following lemma says that it is su?cient to check reachability via sequential rules and via parallel rules in order to construct a wPRS in?atted 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).

Lemma5.5.If a wPRS is in both sequential and parallel?atted normal form then it is in?atted normal form as well.

Proof.We assume the contrary and derive a contradiction.Let?be a wPRS in sequential and parallel?atted normal form.Now let us choose passive steps PS and a rewriting sequence in?+P S leading from rX to

sY such that rX??+PS

triv 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?atted normal form,

rX??+PS

seq sY and rX??+PS

par

sY.Hence,both sequential and parallel

operators occur in the rewriting sequence.There are two cases.

1.Assume that a sequential operator appears?rst.The parallel op-

erator is then introduced by a rule in the form pU?→qU1 U2 applied to a state pU.t,where t∈S.From q(U1 U2).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 con-sidered,the term(U1 U2)is rewritten onto a process constant(say V)?rst.Let PS′be PS in this case.

2.Assume that a parallel operator appears?rst.The sequential op-

erator is then introduced by a rule in the form pU?→qU1.U2 applied to a state pU t,where t∈P.The rest of the sequence subsumes steps rewriting the term U1.U2onto a process constant (say V).Contrary to the previous case,these steps can be inter-leaved 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??+PS′

triv oV.This contradicts our choice

of rX,sY,and PS.

Lemma5.6.For every wPRS system?in normal form,terms t1,t2over Const(?),and weak states r,s of?a wPRS?′can be constructed such that?′is in?atted normal form satisfying rt1??st2??rt1??′st2. Proof.To obtain?′we enrich?by trivial rewrite rules transforming the system into sequential and parallel?atted normal forms,which su?ces thanks to https://www.wendangku.net/doc/c61832871.html,ing 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)}n i=1(satisfying r≥p1

and q n≥s as weak states pairs beyond this range are of no use here)

such that rX??+PS

seq sY∨rX??+PS

par

sY and rX??+PS

triv

sY.We

?nish if the answer is negative.Otherwise we add to?rules rX?→p1Z1,q i Z i?→p i+1Z i+1for i=1,...,n?1,and q n Z n?→sY,where Z1,...,Z n are fresh process constants(if n=0then we add just the rule rX?→sY).The algorithm then repeats this procedure on the system with added rules with one di?erence;the X,Y ranges over the constants of the original system?.This is su?cient as new constants occur only in trivial rules3.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 in?uence on reachability.

Theorem5.7.The reachability problem for wPRS is decidable. Proof.Let?be a wPRS and rt1,st2its states.We want to decide whether rt1??st2or not.Clearly rt1??st2??rX??′sY, where X,Y are fresh constants and?′arises from?by the addition of the rules rX?→rt1and st2?→sY4.Hence we can directly assume that t1,t2are process constants,say X,Y.Lemma5.2and Lemma5.6 successively reduce the question whether rX??sY to question whether rX??′sY,where?′is in?atted normal form–note that Lemma5.2 does not change terms t1,t2if they are process constants.The de?nition of?atted normal form implies rX??′sY??rX??′triv sY.Finally the relation rX??′triv sY is easy to check.

6Conclusions

We have presented a uni?ed view on some(non-conservative)extensions of Process Rewrite https://www.wendangku.net/doc/c61832871.html,paring 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?nite 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.

References

[1]A.Bouajjani,R.Echahed,and P.Habermehl.On the veri?ca-

tion 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.Interna-tional 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,volume2914of LNCS,pages 74–87.Springer,2003.

[4]J.R.B¨u chi.Regular canonical systems.Arch.Math.Logik u.Grund-

lagenforschung,6:91–111,1964.

[5]O.Burkart,D.Caucal,F.Moller,and B.Ste?en.Veri?cation on

in?nite structures.In Handbook of Process Algebra,pages545–623.

Elsevier,2001.

[6]D.Caucal.On the regular structure of pre?x rewriting.Theoretical

Computer Science,106:61–86,1992.

[7]J.Esparza.Grammars as processes.In Formal and Natural Com-

puting,volume2300of LNCS.Springer,2002.

[8]P.Janˇc ar, A.Kuˇc era,and R.Mayr.Deciding bisimulation-like

equivalences with?nite-state processes.Theoretical Computer Sci-ence,258:409–433,2001.

[9]M.Kˇr et′?nsk′y,V.ˇReh′a k,and J.Strejˇc 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 INFINITY03.

[10]D.Lugiez and Ph.Schnoebelen.The regular viewpoint on PA-

processes.In Proc.of CONCUR’98,volume1466of LNCS,pages 50–66,1998.

[11]E.W.Mayr.An algorithm for the general petri net reachability

problem.In Proc.of13th Symp.on Theory of Computing,pages 238–246.ACM Press,1981.

[12]R.Mayr.Process rewrite https://www.wendangku.net/doc/c61832871.html,rmation and Computation,

156(1):264–286,2000.

[13]https://www.wendangku.net/doc/c61832871.html,munication and Concurrency.Prentice-Hall,1989.

[14]F.Moller.In?nite results.In Proc.of CONCUR’96,volume1119of

LNCS,pages195–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 https://www.wendangku.net/doc/c61832871.html,puter Science,97(1–2):233–244,1992.

[17]V.A.Saraswat and M.Rinard.Concurrent constraint programming.

In Proc.of17th POPL,pages232–245.ACM Press,1990.

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

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

[19]J.Strejˇc ek.Rewrite systems with constraints,EXPRESS’01.Elec-

tronic Notes in Theoretical Computer Science,52,2002.