BRICS B R I C S R S - 0 5 - 3 3 BasicResearch inComputer Science A c e t o e t a l .: B i s i m i l a r i ty Bisimilarity is not Finitely Based over i s n BPA with Interrupt o t F i n i t e l y B a s e d o v e r B P A Luca Aceto w WillemJanFokkink i t h Anna Ingo´lfsdo´ttir I n SumitNain t e r r u p t BRICSReport Series RS-05-33 ISSN 0909-0878 October2005 Copyright(cid:13)c 2005, Luca Aceto & WillemJanFokkink& Anna Ingo´lfsdo´ttir& Sumit Nain. BRICS, Department ofComputer Science UniversityofAarhus. All rights reserved. Reproduction ofallorpart ofthis work ispermitted foreducational orresearch use onconditionthat this copyrightnotice is included inany copy. SeebackinnerpageforalistofrecentBRICSReportSeriespublications. Copies maybe obtainedby contacting: BRICS Department ofComputer Science University ofAarhus Ny Munkegade, building 540 DK–8000Aarhus C Denmark Telephone:+45 89423360 Telefax: +45 89423255 Internet: [email protected] BRICS publications are in general accessible through the World Wide Webandanonymous FTP through theseURLs: http://www.brics.dk ftp://ftp.brics.dk This document insubdirectory RS/05/33/ Bisimilarity is not Finitely Based over BPA with Interrupt ∗ c,a, e,b c,a Luca Aceto , Wan Fokkink , Anna Ingolfsdottir d Sumit Nain a BRICS(BasicResearchinComputerScience), CentreoftheDanishNationalResearch Foundation, DepartmentofComputerScience, AalborgUniversity, Fr.Bajersvej7B,9220 AalborgØ,Denmark. b CWI,DepartmentofSoftwareEngineering, Kruislaan 413,1098SJAmsterdam,The Netherlands. c DepartmentofComputerScience, SchoolofScience andEngineering, Reykjav´ık University, Ofanleiti2,103Reykjav´ık, Iceland. d DepartmentofComputerScience, MailStop132,RiceUniversity, 6100S.MainStreet, Houston,TX77005-1892, USA. e VrijeUniversiteit Amsterdam,DepartmentofComputerScience, SectionTheoretical ComputerScience, DeBoelelaan 1081a,1081HVAmsterdam,TheNetherlands. Abstract Thispapershowsthatbisimulationequivalencedoesnotaffordafiniteequationalaxiomati- zationoverthelanguageobtained byenriching BergstraandKlop’sBasicProcessAlgebra with the interrupt operator. Moreover, it is shown that the collection of closed equations overthislanguageisalsonotfinitelybased.Insharpcontrasttotheseresults,thecollection ofclosed equations overthe language BPAenriched withthedisrupt operator isproven to befinitelybased. Keywords: Concurrency, process algebra, BasicProcessAlgebra(BPA),interrupt, disrupt, bisimulation, equational logic,completeaxiomatizations, non-finitely based algebras, expressiveness 1991MSC:08A70,03B45,03C05,68Q10,68Q45,68Q55,68Q70 ∗ Corresponding author. Emailaddresses: [email protected],[email protected](LucaAceto), [email protected](WanFokkink),[email protected],[email protected](Anna Ingolfsdottir), [email protected](SumitNain). URLs:http://www.cs.aau.dk/˜luca(LucaAceto), http://www.cs.vu.nl/˜wanf(WanFokkink), http://www.cs.aau.dk/˜annai (AnnaIngolfsdottir). PreprintsubmittedtoElsevierScience 1 Introduction Programmingandspecificationlanguagesoftenincludeconstructstospecifymode switches (see, e.g., [8,11,23,24,26]). Indeed, some form of mode transfer in com- putation appears in the time-honoured theory of operating systems in the guise of, e.g., interrupts, in programming languages as exceptions, and in the behaviour of control programs and embedded systemsas discrete“modeswitches”triggered by changes inthestateoftheirenvironment. In light of the ubiquitousnature of mode changes in computation,it is not surpris- ing that classic process description languages either include primitiveoperators to describe mode changes—for example, LOTOS [15,23] offers the so-calleddisrup- tionoperator—or have been extended with variations on mode transfer operators. For instance, examples of such operators that may be added to CCS are discussed byMilnerin[25,pp.192–193],andthereference[17]offerssomediscussionofthe benefits ofaddingoneofthose,viz.thecheckpointingoperator, tothat language. In thesettingofBasic Process Algebra(BPA), as introducedby Bergstra andKlop in [12], some of these extensions, and their relativeexpressiveness, have been dis- cussed in the early paper [11]. That preprint of Bergstra’s has later been revised and extended in [7]. There, Baeten and Bergstra study the equational theory and expressivenessofBPA (theextensionofBPA withaconstantδ todescribe“dead- δ lock”) enriched with two mode transfer operators, viz. the disruptand interrupt operators. In particular, they offer an equational axiomatization of bisimulation equivalence [25,29] over the resulting extension of the language BPA . This ax- δ iomatizationisfinite, ifso istheunderlyingsetofactions—astateofaffairs thatis mostpleasingforprocessalgebraists. However, the axiomatization of bisimulation equivalence offered by Baeten and Bergstrain[7]reliesontheuseoffourauxiliaryoperators—twopermodetransfer operator. (Two of those auxiliary operators are, however, redundant since they are derivedBPA operators.)Althoughtheuseofauxiliaryoperators intheaxiomatiza- tion of behavioral equivalences over process description languages has been well established since Bergstra and Klop’s axiomatization of parallel composition us- ing theleft and communicationmerge operators [13], to ourmind,a result likethe aforementionedonealwaysbegsthequestionwhethertheuseofauxiliaryoperators isnecessary toobtainafiniteaxiomatizationofbisimulationequivalence. For the case of parallel composition, Moller showed in [27,28] that strong bisim- ulation equivalence is not finitely based over CCS [25] and PA [13] without the left merge operator. (The process algebra PA [13] contains a parallel composition operatorbasedonpureinterleavingwithoutcommunication,andtheleftmergeop- erator.) Thus auxiliary operators are necessary to obtain a finite axiomatization of parallelcomposition.But,istheuseofauxiliaryoperatorsnecessarytogiveafinite 2 axiomatization of bisimulation equivalence over the language BPA enriched with themodetransferoperators studiedby Baeten andBergstra in[7]? We address the above natural question in this paper. In particular, we mostly fo- cus on BPA enriched with the interrupt operator. Intuitively, “p interrupted by q” describes a process that normally behaves like p. However, at each point of the computation before p terminates, q can interrupt it, and begin its execution. If this happens,p resumes itscomputationuponterminationofq. We show that, in the presence of a single action, bisimulation equivalence is not finitely based over BPA with the interrupt operator. Moreover, we prove that the collectionofclosed equationsoverthislanguageisalso notfinitelybased.Thisre- sult provides evidence that the use of auxiliary operators in the technical develop- mentspresentedin[7]isindeednecessaryinordertoobtainafiniteaxiomatization ofbisimulationequivalence. Our main result adds the interrupt operator to the list of operators whose addition toaprocessalgebraspoilsfiniteaxiomatizabilitymodulobisimulationequivalence; see, e.g., [3,4,14,16,20,30,31] forother examplesofnon-finiteaxiomatizabilityre- sults over process algebras, and some of their precursors in the setting of formal language theory. Of special relevance for concurrency theory are the aforemen- tionedresultsofMoller’stotheeffectthattheprocessalgebrasCCSandPAwithout the auxiliary left merge operator from [12] do not have a finite equational axiom- atizationmodulobisimulationequivalence[27,28]. Recently, in collaborationwith Luttik,thefirstthreeauthorshaveshownin[5]thattheprocessalgebraobtainedby adding Hennessy’s merge operator from [22] to CCS does not have a finite equa- tionalaxiomatizationmodulobisimulationequivalence.Thisresultisinsharpcon- trastwithatheoremestablishedby FokkinkandLuttikin[18]to theeffect thatthe process algebra PA [13] affords an ω-completeaxiomatization that is finite if so is the underlyingset ofactions. Aceto, E´sik and Ingolfsdottirprovedin [2] that there is no finite equational axiomatization that is ω-complete for the max-plus algebra ofthenaturalnumbers,aresultwhoseprocessalgebraicimplicationsarediscussed in [1]. Fokkinkand Nainhaveshownin[19] thatno congruenceoverthelanguage BCCSP, a basic formalism to express finite process behaviour, that is included in possible worlds equivalence, and includes ready trace equivalence, affords a finite ω-completeequationalaxiomatization. Having established that the addition of the interrupt operator to BPA spoils finite axiomatizability modulo bisimulation equivalence, it is natural to ask ourselves whether the same holds true for the disrupt operator from [7]. Intuitively, “p dis- rupted by q” describes a process that normally behaves like p. However, at each point of the computation before p terminates, q can pre-empt it, and begin its exe- cution.Ifthishappens,p neverresumes itscomputation. Weshowthat,perhapssurprisingly,insharpcontrasttothemainresultofthepaper, 3 the use of auxiliary operators isnotnecessary in order to obtain a finite axiomati- zation of bisimulation equivalence over closed terms in the language obtained by enriching BPA with the disrupt operator. The key to this positive result is the dis- tributivity of the disrupt operator with respect to the non-deterministic choice op- erator of BPA in its first argument—aproperty that is not afforded by the interrupt operator. The paper is organized as follows.We begin by presenting the language BPA with the interrupt operator, its operational semantics and preliminaries on equational logic in Section 2. There we also show that the interrupt operator is not definable in BPA modulo bisimilarity. The general structure of the proof of our main result, to the effect that bisimilarity is not finitely based over the language BPA with the interrupt operator, is presented in Section 3. In that section, we also show how to reducetheproofofourmainresulttothatofatechnicalstatementdescribingakey property of closed instantiations of sound equations that is preserved under equa- tionalderivations(Proposition13).WeofferaproofofProposition13inSection4. WeconcludethepaperbypresentinginSection5anaxiomatizationofbisimulation equivalenceoverclosed terms in thelanguageobtainedby enrichingBPA with the disruptoperatorfrom[7].Suchanaxiomatizationisfiniteinthepresenceofafinite set ofactions,anddoes notemployauxiliaryoperators. An extended abstract of this paper appeared as [6]. There we announced without proof our main result (namely, Theorem 9) under the assumption that the set of actions contains two distinct actions. The present version of the paper sharpens Theorem9inthatitnowappliestoanynon-emptysetofactions,andoffersthefull proofofourmainresult(allofthematerialinSection4).Moreover,Proposition20 inthecurrent paperis new. 2 Preliminaries We begin by introducing the basic definitions and results on which the technical developments to follow are based. The interested reader is referred to [7,12] for moreinformation. 2.1 The LanguageBPA int Weassumeanon-emptyalphabet Aofatomicactions,withtypicalelementa. The language for processes we shall consider in the main body of this paper, hence- forth referred to as BPA , is obtained by adding the interrupt operator from [7] to int Bergstra andKlop’sBPA [12]. Thislanguageisgivenbythefollowinggrammar: t ::= x |a| t·t| t+t| t (cid:3) t , 4 where x is a variable drawn from a countably infinite set V and a is an action. In theabovegrammar,weusethesymbol (cid:3) for theinterruptoperator. Intuitively,atermoftheformp (cid:3) q describesaprocessthatnormallybehaveslike p.However,ateachpointofthecomputationbeforepterminates,q caninterruptit, andbeginitsexecution.Ifthishappens,presumesitscomputationupontermination ofq.Analternativecompositionp+q nondeterministicallybehavesaseitherporq. Asequentialcompositionp·q firstbehavesasp,anduponterminationofpbehaves as q. We shall use the meta-variables t,u,v,w to range over process terms, and write var(t) for the collection of variables occurring in the term t. Thesizeof a term is thenumberofsymbolsinit. Formally, • thesizeofvariablesand actionsis1, and • thatoft·u,t+uand t (cid:3) uis oneplusthesumofthesizesoftand u. A process term isclosedif it does not contain any variables. Closed terms will be typically denoted by p,q,r,s. As usual, we shall often writetu in lieu of t·u, and weassumethat ·bindsstrongerthan + and(cid:3). A (closed) substitution is a mapping from process variables to (closed) BPA int terms. For every term t and substitution σ, the term obtained by replacing every occurrence of a variable x in t with the term σ(x) will be written σ(t). Note that σ(t)isclosed,ifsoisσ.Inwhatfollows,weshallusethenotationσ[x 7→ p],where σ isaclosedsubstitutionandpisaclosedBPA term,tostandforthesubstitution int mappingxtop, and actinglikeσ onall oftheothervariablesinV. In the remainder of this paper, we let a1 denote a, and am+1 denote a(am). More- over, we consider terms modulo associativity and commutativity of +. In other words,wedonotdistinguisht+uandu+t,nor(t+u)+v andt+(u+v).This is justified because + is associative and commutative with respect to the notion of equivalence we shall consider over BPA . (See axioms A1, A2 in Table 3 on int page 12.) In what follows,the symbol= will denote equality moduloassociativity and commutativityof+. Wesaythatatermthas+asheadoperatorift = t +t forsometermst andt . 1 2 1 2 Forexample,a+bhas + as head operator, but(a+b)a doesnot. P For k ≥ 1, we use a summation t to denote t + ···+ t . It is easy to i∈{1,...,Pk} i 1 k see that every BPA term t has the form t , for somefinite, non-emptyindex int i∈I i set I, and termst (i ∈ I)that donot have+ as head operator. Thetermst (i ∈ I) i i willbereferred toasthe(syntactic)summandsoft.Forexample,theterm(a+b)a has onlyitselfas (syntactic)summand. TheoperationalsemanticsforthelanguageBPA isgivenbythelabelledtransition int 5 a a →X t →aX u →aX t →a t0 u →a u0 t+u →aX t+u →aX t+u →a t0 t+u →a u0 t →aX t →a t0 t·u →a u t·u →a t0·u t →aX t →a t0 u →aX u →a u0 t (cid:3) u →aX t (cid:3) u →a t0 (cid:3) u t (cid:3) u →a t t (cid:3) u →a u0·t Table1 TransitionRulesforBPA int system (cid:16) n o n o(cid:17) BPA , →a | a ∈ A , →a X | a ∈ A , int wherethetransitionrelations→a andtheunarypredicates→a Xare,respectively,the leastsubsetsofBPA ×BPA andBPA satisfyingtherulesinTable1.Intuitively, int int int atransitiont →a umeansthatthesystemrepresentedbytheterm tcan performthe action a, thereby evolving into u. The special symbol X stands for (successful) termination; therefore the interpretation of the statement t →a X is that the process term t can terminate by performing a. Note that, for every closed term p, there is someactionaforwhicheither p →a p0 holdsforsomep0, orp →a X does. Fortermst,u,and action a, wesaythat uisan a-derivativeoftift →a u. Thetransitionrelations→a naturallycomposetodeterminethepossibleeffectsthat performingasequenceofactionsmay haveon aBPA term. int Definition 1 Forasequenceofactionsa ···a (k ≥ 0),andBPA termst,t0,we 1 k int writet a1→···ak t0 iffthereexists asequenceof transitions t = t →a1 t →a2 ··· →ak t = t0 . 0 1 k Similarly,we say that a ···a (k ≥ 1) is a termination traceof a BPA term t iff 1 k int thereexistsa term t0 suchthat t a1−···→ak−1 t0 →akX . If t a−1·→··ak t0 holds for some BPA term t0, or a ···a is a termination trace of t, int 1 k then a ···a is atraceoft. 1 k Thedepthofa termt, written depth(t), isthelengthofthelongesttraceitaffords. 6 Thenormof a term t, denoted by norm(t), is thelength of its shortest termination trace;thisnotionstemsfrom[9]. Thedepthandthenormofclosedtermscanalsobecharacterized inductivelythus: depth(a) = 1 depth(p+q) = max{depth(p),depth(q)} depth(pq) = depth(p)+depth(q) depth(p (cid:3) q) = depth(p)+depth(q) norm(a) = 1 norm(p+q) = min{norm(p),norm(q)} norm(pq) = norm(p)+norm(q) norm(p (cid:3) q) = norm(p) . NotethatthedepthandthenormofeachclosedBPA termarepositive,andthere- int fore that thenorm of each closed term of theform pq is at least 2. Thissimple,but useful,observationwillbeused repeatedly intheremainderofthisstudy. Inwhatfollows,weshallsometimesneedtoconsiderthepossibleoriginsofatran- sition of the form σ(t) →a p, for some action a, closed substitution σ, BPA term int t and closed term p. Naturally enough, we expect that σ(t) affords that transition if t →a t0, for some t0 such that p = σ(t0). However, the above transition may also derive from the initial behaviour of some closed term σ(x), provided that the col- lectionofinitialmovesofσ(t)depends,insomeformalsense,onthatoftheclosed term substitutedfor the variable x. Similarly,we shall sometimesneed to consider thepossibleorigins ofa transitionof theform σ(t) →a X, for someaction a, closed substitutionσ and BPA term t. int Tofullydescribethesesituations,weintroducetheauxiliarynotionofconfiguration ofaBPA term.To thisend,we assumeasetofsymbols int V = {x | x ∈ V} d d disjointfromV.Intuitively,thesymbolx (read“duringx”)willbeusedtodenote d that the closed term substitutedfor variable x has begun executing,but has not yet terminated. Definition 2 The collectionofBPA configurationsisgiven bythegrammar: int c ::= t|x | c·t|c (cid:3) t , d where tisa BPA term,and x ∈ V . int d d 7 x →xs x x →xX d t →x t0 t →xs c t →xX t+u →x t0 t+u →xs c t+u →xX u→x u0 u →xs c u →xX t+u →x u0 t+u →xs c t+u →xX t →x t0 t →xs c t →xX tu →x t0u tu →xs cu tu →x u t →x t0 t →xs c t →xX t (cid:3) u →x t0 (cid:3) u t (cid:3) u →xs c (cid:3) u t (cid:3) u →xX u →x u0 u →xs c u →xX t (cid:3) u →x u0t t (cid:3) u →xs ct t (cid:3) u →x t Table2 SOSRulesfortheAuxiliaryTransitions →x ,→xs and→xX(x∈ V) For example, the configuration x · (a (cid:3) x) is meant to describe a state of the d computationofsometerminwhichthe(closedtermsubstitutedforthe)occurrence of variable x on the left-hand side of the · operator has begun its execution (and has not terminated), but the one on the right-hand side has not. Note that each configurationcontainsat mostoneoccurrence ofan x ∈ V . d d We shall consider the symbols x as variables, and use the notation σ[x 7→ p], d d where σ is a closed substitution and p is a closed BPA term, to stand for the int substitutionmappingx to p, andacting likeσ on alloftheothervariables. d Thewayinwhichtheinitialbehaviourofatermmaydependonthatofthevariables that occur in it is formally described by three auxiliary transition relations whose elementshavethefollowingforms: • t →xs c (read “t can start executing x and become c in doing so”), where t is a term,xis avariable,andc isaconfiguration, • t →x t0, wheret andt0 areterms andx isavariable,or • t →xX,where tisaterm. The first of these types of transitions will be used to account for those transitions of the form σ(t) →a p that are due to a-labelled transitions of the closed term σ(x) thatdonotleadtoitstermination.Thesecondwilldescribetheoriginoftransitions of the form σ(t) →a σ(t0) that are due to a-labelled transitions of the closed term 8