Decidability of Model Checking for Infinite-State
`Concurrent Systems *
`
`.J aviPr Esparza
`Institnt fiir Informatik
`TP< ·lmis< ·lw 1._; ni vPrsi tiit :VI iill( ·lwn
`Arcisstr. 21 D-80290 :Vliindwn, GPrmany
`
`Abstract
`
`We study the decidability of the model checking problem for linear and branching
`time logics, <:wd two models of concurrent computation, nanwly Petri nets <:wd lhtsic
`Pa,raJ lei Processes.
`
`1
`
`Introduction
`
`I'vlost techniques for the verification of concurrent systems proceed by <HI exh<uJstive
`traversaJ of the state sp<:u:e. Therefore, they <He inherently incaJ}<:tble of considering
`systems with infinitely many states.
`Recently, some new methods have been developed in order to at least palliate this
`problem. Using them, several verification problems for some restricted infinite-state
`models have been shown to be decidable. These results can be classified into those
`showing the decidability of equivalence relations [8, fl, 2'1, 26]. and those showing the
`decidability of model checking for different modal and temporal logics. In this paper,
`we contribute to this second group.
`The model checking problem has been studied so far for three infinite-state models:
`context-free processes, pushdown processes, <:wd Petri nets. The first two a,re mod(cid:173)
`els of sequential computation, while the latter explicitely models concurrency. The
`modal mu-calculus, the most powerful of the modal and temporal logics commonly
`used for verification, is known to be decidable for context-free processes and push(cid:173)
`down automata. The proof is a complicated reduction to the validity problem for S2S
`(monadic second order logic of two successors) [:32, 1:3]. Simpler algorithms have been
`given for the alternation-free fragment of the mu-calculus [5, 21]. These results have
`been extended to context-free like processes in [22], and to pushdown processes in [6].
`The model checking problem for Petri nets was first studied by Ilowell and Rosier
`[HJ], who observed that a certain linear time temporal logic is undecidable even for
`conflict-free Petri nets, a fairly small class. This logic is interpreted on the infinite
`occurrence sequences of the net, a.nd consists of a.tomic sentences, the usua.l boolea.n
`connectives, and the operator r (eventually). The atomic sentences are of type ge( s, c)
`(with intended me<:uling 'at the current m<:Hking, the number of tokens on place .s is
`
`*This work wa,;; mostly done while the author wa,;; at the l:niversity of Edinhurgh.
`
`1
`
`Blue Coat Systems - Exhibit 1061
`
`

`
`greater than or equal to c') or of type fi(t) (with intended meaning 'I is the next
`transition in the sequence'). A Petri net is said to satisfy a formula if it has an infinite
`run that satisfies it.
`In a subsequent paper [20], !lowell, Rosier and Yen showed that the model checking
`problem for the positive fragment of this logic (in which negations are only applied to
`atomic sentences) can be reduced to the readmbility problem, and is thus decidable .
`.Jani:ar showed in [2:3] that the positive fragment with G/"(infinitely often) as operator,
`instead of/", is decidable as well.
`Although some of these results are very deep, they are also rather fragmentary.
`The logics have been chosen in a, rather <:ul-hoc way, bec<:wse the rn<:tin interest of the
`authors has been to study particular problems (the main goal of [20, 2:3] is to study
`fairness problems), and not the logics themselves. In particular, branching time logics
`have received very little attention. Also, the logics of [Hl, 20, 2:3] contain an ad-hoc set
`of atomic sentences, <:wd the irnp<:u:t on decida,bility of this or other p<Hticula,r choice
`ha,s not been cle<:Hed up.
`The goal of this paper is to offer a more systematic and global picture of the
`decidability issues concerning model checking infinite-state concurrent models for both
`linea,r time <Hid bra,nching time logics. For that, we recaJI some results recently obt<:tined
`by the author [15], and complement them with new ones.
`We consider interleaving semantics and two different models: labelled Petri nets,
`called just Petri nets in the rest of this section, and Basic Parallel Processes (BPI's) [7,
`8]. Petri nets <He a, rather powerful model, which e<Hl be used to represent <:wd a,naJyse
`a, I<Hge V<Hiety of systems. No naturaJ model of concurrent computation lying strictly
`between Petri nets <Hid Turing rmu:hines seems to have been proposed so fa,r (context
`sensitive grammars lie strictly between Petri nets and Turing Machines [:3:3], but they
`are not used as a model for concurrerH:y). Therefore, decidability results for Petri
`nets are very significant, because they cannot be easily generalized, but undecidability
`results <He not very conclusive, because a problem undecidable for arbitrary Petri nets
`could be decidable for relevant net classes. That is why we also study BPI's, which (in
`interleaving semantics) can be seen as a small subclass of Petri nets. BPPs are a rather
`weak process algebra, in which processes are built out of action prefix, nondeterministic
`choice, parallel composition without communication, and recursion. It can be argued
`that any reasonable infinite-state model of concurrency will have more computing power
`than BPI's. Therefore, undecidability results for BPI's should be expected to be very
`significant.
`In the first section, we define Petri nets and
`The paper is organised as follows.
`BPI's. Section 2 recalls the results of [15] on linear time logics. Section :3 deals with
`branching time logics. In these two sections we consider action-based logics without
`atomic sentences. Section :1 investigates how the results change when atomic sentences
`are added.
`
`2 Models: notations and basic definitions
`
`We introduce Petri nets and Basic Parallel Processes, the two models we study. Before
`that, we need a few notions about transition systems.
`
`2
`
`

`
`2.1 Thansition systems
`
`t
`
`t
`
`t
`
`A (labdledj lmnsilion syslem T over a set of actions Ad consists of a set of states S
`and a relation _"_,t;;; S x S for each action a E Ad. A palh ofT is either an infinite
`f' .
`... ~ ·'n sucn tnat ·'n ll<:ts
`a,
`an-1
`sequence .s1
`·'2 -~ ·'3 ... or a, Hllte sequence .s1
`no successors.
`A transition system is rooted if it has a d.istinguished initial state. A run of a rooted
`transition system Tis a path which starts at the initial state; a state is reachable if
`it <:tppea,rs in some run. The language ofT is the set of sequences of <:u:tions obt<:tined
`by dropping the states in the runs ofT (so the language may contain both finite and
`infinite words).
`In some proofs we have to consider the states of a, tnu1sition system up to strong
`bisimulation. A relation ll t;;; S x Sis a slmng bisimulalion if whenever ·'1 /l.s2 then,
`for every a E A cl,
`'f
`I I' I
`r
`a
`a
`.s1 -~ .s1 tnen .s 2 -~ .s 2 tor some .s 2 w1t11 .s1 L .s 2 ;
`• 1
`'f
`I I' I
`r
`a
`a
`·'2 -~ .s 2 tnen ·'1 -~ .s1 tor some .s1 w1t11 .s 2 L .s1 .
`• 1
`.s 2 <He strongly bisirnilar, denoted by .s1 "'"'
`.s 2 , if there is a, strong
`Two states .s1 <Hid
`bisimulation ll such that .s1 /l.s2. This definition can be extended to states of different
`tnu1sition systems, by putting them 'side by side', <Hid considering them as one single
`transition system.
`
`I
`
`I
`
`t
`
`t
`
`I
`
`I
`
`I
`
`I
`
`•
`
`t
`
`•
`
`t
`
`2.2 Petri Nets
`
`A labelled nfl N is a fourtuple (S,T, W,l), where
`
`• SandT are two disjoint, finite sets,
`• W: (S x T) U (T x S) ~ LV is a weight function, and
`• I is a surjective mapping T ~ Ad, where Act is a set of actions (surjectivity is
`assumed for convenience).
`
`The elements of Sand Tare called places and lmnsilions, respectively. Places and
`transitions are generically called nodes.
`A marking of N is a mapping lvl: S ~ N. A marking lvl enables a transition l
`if lH(.s) :> W(.s,l) for every place .s. If lis enabled at lvl, then it can (X:cur, and its
`occurrence leads to the successor marking iv/ 1 which is defined for every place .s by
`ivt'(.s) = lVI(.s) + L(W(t,.s)- W(.s,t))
`
`tET
`
`A marking lvl is called dead if it enables no transition of N.
`A (labdledj Fflri nfl is a pair L; = ( N, iV/0 ) where N is a labelled net and lV/0 is a
`marking of N. The rooted transition system of~ has all the markings of N as states
`and lV/0 as initial state. For each action a E Acl, we define lv/1 _a_, lv/2 if lv/1 enables
`some transition l labelled by a, and the marking reached by the occurrence of lis lv/ 2 •
`The language of a Petri net is the language of its transition system.
`Unlabelled Petri nets are obtained from labelled ones by dropping the labelling
`function. l';quivalently, one can think of unlabelled Petri nets as labelled Petri nets in
`which the labelling function assigns to a transition its own name. VVith this convention,
`the deli nition of transition system and language of a Petri net carries over to unlabelled
`Petri nets.
`
`3
`
`

`
`2.3 Basic and Very Basic Parallel Processes
`
`The class of Basic Parallel Process (BPP) expressions is defined by the following ab(cid:173)
`stract syntax [7, 8]:
`
`0
`X
`a. 1·.·
`1·.' + 1·.'
`1·: II 1·:
`where a belongs to a, set Act of <:u:tions. The BPP expressions conta,ining no occurrence
`of the choice operator+ are called Very Basic Parallel Process (VBPP) expressions.
`A BPP is a family of recursive equations
`
`(inaction)
`(process variable)
`(action prefix)
`(choice)
`(merge)
`
`where the .:ri a,re distinct <Hid the l·.'i <He BPP expressions at most cont<:urung the
`V<Hi<:tbles {.\" 1 , ••• , .\"11j. VVe further <:tssurne that every V<Hi<:tble occurrence in the ex(cid:173)
`pressions 1·.', is guarded, that is, appears within the scope of an action prefix. The
`variable X 1 is singled out as the leading variable and X 1 ~1 1·.'1 is called the leading
`equal ion.
`The rooted transition system of a BPP {Xi ~1 1·.', 11 <:: i <:: n} has the BPP expres(cid:173)
`Sions over V<Hi<:tbles .\"1, ... ,.\"n <:ts states; the le<:uling V<Hi<:tble is the initiaJ state. For
`every a E Ad, the transition relation _a_, is the least relation satisfying the following
`rules:
`
`a
`1·.' -~ 1·.'
`
`1·.'
`
`a
`
`-~
`
`I·:'
`a
`
`a
`
`-~
`
`I·:'
`
`1·.'
`
`a
`
`(X def 1·.')
`
`-~
`
`-~
`
`-~
`
`-~
`
`a
`
`a
`
`a
`
`1·.'
`X
`
`-~
`
`-~
`
`I·:'
`I·:'
`
`1·.' + "' -~ I·:'
`1·.' II "' -~ I·:' II "'
`a V'
`a V'
`"'
`"'
`a
`1·.' + "' a V'
`1·.' II V'
`1·.' II "'
`I u
`I r·
`I.
`.
`.
`I
`1
`1
`[{
`.
`f
`a
`•or a, su }Set o <:u:t10ns r\, t 1e re at1on ~ IS < e me< <ts
`F
`aEl{ - ............
`A BPP is in normal form if every expression 1·.', on the right hand side of an equation
`is of the form a 1 • n 1 + ... +an · O'n, where for e<:u:h i the expression O'i is a, merge of
`process variables. It is shown in [7] that every BBP is strongly bisimilar to a BPP in
`normal form (i.e., the leading variables are strongly bisimilar).
`)•;very BPP in normal form can be translated into a labelled Petri net. The transla(cid:173)
`tion is graphically illustrated by means of an example in Figure 1. The net has a place
`for each variable .:ri. For each subexpression aJ · O!J in the defining equation of l·.'i, a
`transition is added having the place .:ri in its preset, and the v<u·iables that appear in
`O!J in its post set. If a v<u·iable appears n times in O'J, then the arc leading to it is given
`weight n. Finally, a token is put on the place corresponding to the leading variable.
`It is e<:tsy to see that there exists an isomorphism between the reachable parts of the
`transition systems of a BPP in normal form and its associated Petri net.
`Also, it follows easily from this translation that:
`
`• the transitions of Petri nets correspond.ing to BPPs in normal form have exactly
`one input place,
`
`• the places of VBPPs in normal form have at most one output transition, and
`
`• all the arcs leading from places to transitions have weight 1.
`
`

`
`X~ a (X II Y) + b ( Y II Y)
`y ~ b (X II y)
`
`Fig. 1 A BPP and its corresponding Petri net
`
`3 Linear Time Logics
`
`The contents of this section are taken from [15]. We show that the model checking
`problem for Petri nets and closed formulas of the linear time mu-calculus is decidable.
`The linear time mu-calculus is a powerful linear time logic, in which all the usual linear
`time operators like 'aJways', 'eventuaJiy', <:wd 'until' e<Hl be expressed. VVe describe it
`briefly, and refer the reader to [11] for more information.
`The linear time mu-calculus has the following syntax
`
`4> ::= z I
`I 4> A 4> I (a )4> I v z .</>
`where a r<:tnges over a, set Act of <:u:tions, <:wd Z over a, set of propositionaJ V<Hi<:tbles.
`Free <Hid bound occurrences of v<:Hi<:tbles <He defined <:ts usuaL A formula, is dosed if no
`V<Hi<:tble occurs free in it.
`Forrnula,s <He built out of this gnunrn<H, subject to the rnonotonicity cond.ition that
`aJI free occurrences of a, V<Hi<:tble Z lie in the scope of <HI even number of negations.
`Let Act*, Acl~ be the set of finite and infinite words on Ad, and let Ac(" =
`Act* U Acl~. A valuation V of the logic assigns to each variable Z a set of words V(Z)
`in Ac(". We denote by V[W/Z] the valuation V' which agrees with V except on Z,
`where V'(Z) = W. Given a word a= a1 a2 • •• on Ac(", a(1) denotes the first action
`of a, i.e., a 1 , <Hid a 1 denotes the word a2 a3 .... VVith these notations, the denotation
`II<PIIv of a formula 4> is the set of words of Ac(" inductively defined by the following
`rules:
`
`IIZIIv
`V(Z)
`Ad" - II<PIIv
`IHIIv
`114> A <PIIv
`II<PIIv n II<PIIv
`{a E Ad" I a(1) =a!\ a' E II<PIIv}
`ll(a)4>llv
`U{W t;;; Act" I W t;;; II<PIIv[wjzJ}
`llvZ.</>IIv
`Therefore, llvZ.</>IIv is the greatest fixpoint of the function which assigns to a set
`W of words the set II<PIIv[W/Z]·
`The denotation of a closed formula 4> is independent of the valuation; we then use
`the symbol 114>11-
`A rooted tnu1sition system T satisfies a, closed formula, cP of the linea,r time mu(cid:173)
`Accordingly, a Petri net L; satisfies 4> if f,(L;) t;;;
`calculus if every run ofT satisfies
`114>11, where f,(L;) denotes the language of its transition system. Notice that, with this
`definition of satisfaction, it can be the case that ~ satisfies neither a formula nor its
`negation.
`
`

`
`According to our definition, the denotation of a formula is a set of finite and infinite
`words. This choice is due to the fact that we wish to define satisfaction as {,('!:;) t;;; 114>11,
`<:wd we wish to define f~(L;) as a set of finite and infinite words, in order to account
`for deadlock properties. In particular, with this definition we can express deadlock(cid:173)
`freedom as
`
`vZ. V (a)Z
`
`aEAct
`
`Sometimes the denotation of a formula is defined as a set of only infinite words, as for
`instance in [11].
`We define the model checking problem for the linear time mu-calculus and Petri
`nets as follows: given a Petri net L; and a closed formula
`determine if L; satisfies c/.>
`or not. This problem is proved to be decidable in [15]. llere we just sketch the proof.
`The decision procedure is based on an automata-theoretic characterisation of the logic
`[:35]. It is shown in [11] that, given a closed formula
`there exists a finite automaton
`;1~0 and a Biichi automaton /J~0 that accept the finite and infinite words of II
`respectively. It is then easy to see that L; satisfies ,P if and only if f,(L;) n {,(;1~0 ) = f/J
`and f,(L;) n f,( /J~0) = f/J.
`In order to decide these two properties, two new Petri nets L; x L;k ... ,p and L; x L;R ... ,p
`are constructed, having the properties f~(L; x L;A-.,p) = f~(L;) n f~(L;A-.,?), and f~(L; x
`L;R~.;) = f,(L;) n f,(L;R~.;). Then, the two following results are proved:
`f,(L;) n f,(/J0 ) I f/J holds if and only if the Petri net L; x L;R.; has a run which
`contains infinitely many occurrences of transitions of a set T. The set T can be
`efficiently computed from L; and /J0.
`• f,(L;)nf,(;\ 0 ) I f/J if and only if the Petri net L;xL;·4 ·? has a reachable dead marking
`which marks some place of a setS. The setS can be efficiently computed from
`L; and /J0.
`
`•
`
`The existence of the run was shown to be decidable by Jantzen and Valk [25]. Yen
`shows in [:36] that it is decidable within exponential space.
`The existence of the dead marking can be decided by solving an exponential number
`of instances of the reachability problem. The readmbility problem is decidable [27, :30]
`and known to require exponential space [29], but none of the algorithms known so far
`is primitive recursive.
`
`4 Branching Time Logics
`
`The decidability border changes rather drastically when we move from linear time to
`branching time logics. We have seen that a powerful linear time logic like the linear
`time mu-calculus is decidable for a powerful model like Petri nets. In this section we
`shall see that a weak branching time logic ise undecidable even for VBPPs, a very weak
`model of computation.
`For a smooth approach to the result, we shall first prove that the modal mu(cid:173)
`calculus is undecidable for VBPPs. We introduce the modal mu-calculus very briefly,
`more details can be found in [:}1].
`
`6
`
`

`
`4.1 The modal mu-calculus
`
`The rnodaJ rnu-cakulus ha,s the sanw syntax <:ts the linea,r time rnu-cakulus, just
`substituting (a)¢; for (a)¢;.
`It is interpreted on labelled transition systems. Let
`T = (S, ~aEAct) be a labelled transition system. Given a V<lJuation V that assigns
`to e<:u:h v<:Hia,ble a, subset of states S, the denotation of a, formula, is a, subset of states
`defined by the following rules:
`
`V(Z)
`IIZIIv
`ll,cf;llv
`S- llcf;llv
`II¢;, II cP2IIv
`IIMv n llcP2IIv
`{.s E S I 3/ E S .. s -"'- .s' II .s' E llcf;llv}
`ll(a)cf;llv
`UP t;;; S 111 t;;; llcf;llv[4/ZJ}
`llvZ.cf;llv
`Loosely speaking, a state belongs to ll(a)cf;llv if it has some succesor, reachable by
`means of an a action, which satisfies
`VVe use the following abbreviations:
`true= vZ.Z
`¢;, V cP2 = >(
`II >cP2)
`[a]¢;= >(a),¢;
`11Z.¢; = ,vz.,q,[,Z/Z]
`
`As in the c<:tse of the linea,r time rnu-caJculus, the denotation of a, closed formula, is
`independent of the valuation, and then we drop the index v. Observe that lltruell = S.
`A rooted transition system satisfies a closed formula c/.> if the denotation of c/.> contains
`the initial state.
`The modal mu-calculus has the following property: if two states of a transition
`system are strongly bisimilar, then they satisfy exactly the same closed formulas of the
`logic.
`
`4.2 Undecidability of the modal mu-calculus for VBPPs
`
`We prove the undecidability of the model checking problem by means of a reduction
`from the halting problem of counter machines [:31] (more precisely, to the halting
`problem for counter rmu:hines whose counters <He initiaJised to 0).
`A co1mler machine ;\1 is a tuple
`
`where Ci are the co1mlers, qi are the slales with qo being the inilial slale and qn+J the
`unique hailing slale, and o, is the lmnsilion mle for state qi (0 <:: i <:: n). The states
`are divided into two types. The states of type I have transition rules of the form
`CJ := CJ + 1; goto qk
`for some j, k. The states of type I I have transition rules of the form
`
`if CJ = 0 then goto qk else ( CJ := CJ - 1; go to qk')
`
`for some j, k, k'.
`A configuration of A1 is a, tu pie ( qi, j 1 , ••• , )rn), where qi is a, state, <:wd j 1 , ••• , )m
`are natural numbers indicating the contents of the counters. VVe are interested in
`the behaviour of a machine whose counters are initialised to 0. Therefore, we define
`the inilial con{igumlion as (q0 , 0, ... , 0). The compulalion of ;\1 is the sequence of
`
`7
`
`

`
`configurations which starts with the initial configuration and is inductively defined in
`the expected way, <:u:cording to the tnu1sition rules. Notice that the computation of
`A1 is unique, bec<:wse e<:u:h state ha,s at most one tnu1sition rule. VVe say that A1 halls
`if its computation is finite, or, equhraJently, if its computation conta,ins a, configuration
`with state qn+J· It is undecidable if a given counter machine halts [:31].
`Given a, counter rmu:hine A1, our reduction constructs a, VBPP with le<:uling V<Hi<:tble
`M, and a formula //all of the modal mu-calculus such that ;\1 halts if and only if M
`satisfies //all.
`If instead of VBPPs we were considering a Turing-powerful model like CCS, the
`problem would be trivial: M would just be a faithful model of the counter machine ;\1,
`in which the occurrence of <HI <H:tion halt signaJs termination, <Hid we would t<:tke
`
`//all = 11X. (halt) true V
`
`[a] X
`aEAct\{halt}
`
`which expresses that M eventually performs halt.
`Ilowever, VBPPs are much less powerful than Turing Machines. The idea of the
`reduction is to construct a, VBPP which simulates the counter rmu:hine in a, wea,k sense:
`the VBPP may execute rrnwy runs, some of which -the 'honest' runs- simulate the
`computation of the counter rmu:hine, while the rest a,re 'd.ishonest' runs in which, for
`instance, a counter is decreased by 2 instead of by 1. We replace the formula //all
`<:tbove by a more complicated formula expressing that a certain honest run eventually
`executes halt. Thus, the problem of having a 'weaker' simulation is compensated by
`a 'stronger' formula, and it is still the case that the counter machine halts if and only
`if the BPP satisfies the new formula.
`
`'weak' Inodel of a counter Inachine. A counter CJ containing the number
`A
`n is modeled by n copies in parallel of a process Cj.
`
`Cj ~I deCj · 0
`
`The action decj models decreasing the counter CJ by 1. Notice that VBPPs cannot
`enforce synchronisation between the action decj and a change of state of the counter
`machine. In some sense, the formula //all will be in charge of modelling these synchro(cid:173)
`nisations.
`The states of the counter machine are modelled acconling to their associated in(cid:173)
`struction. A state qi of type I is modelled by the processes
`
`def
`
`der
`
`. (SQi II Qi)
`II
`,
`~
`OUti ·(Qk Cj)
`
`Qi
`
`A state qi of type II is modelled by the processes
`
`def
`
`def
`
`. (SQi II Qi)
`OUti · 0
`
`Qi
`
`and outi model the fact that the counter machine enters and leaves
`The actions
`the state q,, respectively. Notice that VBPPs cannot model the fact that from state
`qi the states qk or q~ can be reached, because in order to model the choice between qk
`and q~ we need the choice operator.
`
`8
`
`

`
`The halting state qn+J is modelled by the processes
`inn+1 · (SQn+1 II Qn+1)
`halt· Qn+1
`
`SQn+1
`
`del
`def
`
`Finally, we define Mas follows
`SM del SQ1 II ... II SQn+1
`M del SM II Qo
`
`It follows easily from the operational semantics of BPI's that every reachable state
`of M is strongly bisirnilar to a unique expression of the form
`
`where pk ~1 P II ... II P for k :> 1, and P0 ~1 0. Hlr instance, the initial state M
`
`~
`k
`is strongly bisimilar to SM
`
`II Qo
`
`II 0 II ... II 0. The expressions in which all the
`
`~
`Tn+n-1
`indkes io, ... ,in+J except one, say iJ, <:He 0, <:wd moreover iJ = 1, correspond to the
`configurations of the counter rmu:hine. The nonzero index indicates which is the state
`of the machine, and the indices j 1 , ••• ,jm indicate the values of the counters. We say
`that the states which are bisirnlar to a expression of this form are rneaningful.
`Let f be the mapping that assigns to each meaningful state the corresponding
`/·.\ ..3~ 1·.'2
`· · · is honest if it
`configuration of the counter machine. A run M
`has a prefix satisfying the following property: the image under f of the subsequence
`of meaningful states of the prefix yields the computation of the counter machine ;\1.
`Loosely spea,king, a, honest run ofM simulates the computation of the counter rmu:hine
`;\1, but if the simulation terminates (with the execution of halt) then it may behave
`arbitrarily. It is clear from the definitions that M has honest runs, but not every run of
`M is honest.
`VVe now construct a, formula, of the rnu-cakulus expressing that a, cert<:tin honest
`run eventuaJiy executes halt. For a, state qi of type I we define the open formula,
`
`For a state qi of type II we define
`
`(outi) Z
`
`(outi) (ink) Z
`
`II
`
`[decj] false
`v
`(decj) (outi) (ink') Z
`
`This formula expresses that either the action decj is not enabled (which models
`that the counter CJ is empty) <:wd then after the execution of the sequence outi ink,
`(which models the transition from the state qi to the state qk) the formula Z holds, or
`after the execution of the sequence decj outi ink' (which models decreasing counter
`CJ by 1 and moving from state qi to qk) the formula Z holds.
`Finally, we deli ne
`
`//all
`
`11Z. (halt) true V V
`
`n
`
`i=O
`
`9
`
`

`
`Loosely speaking, a run of M satisfies this formula if and only if it eventually ex(cid:173)
`ecutes the action halt, and the prefix preceeding the first occurrence of halt is the
`concatenation of srnaJI sequences of <H:tions, e<:u:h of which satisfies one of the forrnul<:ts
`J·~<u:h of these srnaJI sequences simulates one step of the counter rmu:hine.
`
`Theorem 4.1
`The model checking problem for dosed formulas of lite modal mu-calculus and
`V lJ F Fs is undecidabiL
`
`Proof: Let ;\1 be a counter machine with initially empty counters. The VBPP M
`satisfies the formula //all iff it has a honest run that eventually executes the action
`halt. Since honest runs faithfully simulate the computation of ;\1, this is the case iff
`;\1 halts.
`•
`
`Theorem :1.1 rn<w not seem very surprising; the rnodaJ rnu-cakulus is known to be
`<HI extremely powerful logic, <:wd one may expect it to be undecid<:tble even for such
`simple processes as VBPPs. llowever, we will now show that the undecidability result
`still holds for a small subset of the modal mu-calculus.
`
`4.3 Unified System of Branching Time
`
`The Unified System of Branching Time (UB) is a logic introduced by Ben-Ari, Manna
`and Pnueli [2], where it is given a state-oriented semantics in terms of Kripke structures.
`In p<uticui<H, UB includes a, next operator /·.'4>, rne<:wing that cP holds at some successor
`of the current state. Since BPPs <He <HI <:u:tion oriented model, we use a, version of UB
`in which the next operator is relativised: for e<:u:h <:tction a, we have an operator l·.'(a)cf>,
`whose meaning is that 1> holds at some successor reached after performing an a. Also,
`we only allow the atomic sentence true, which holds at every state.
`After these changes, the syntax of UB is
`4> ::=true I
`
`UB is a fragment of Computation Tree Logic [10], which in turn can be easily
`embedded in the modal mu-calculus (see, for instance, ['1]).
`We interpret UB formulas on a rooted labelled transition system. We denote that
`a state .s satisfies a formula 1> by .s f=
`The satisfaction relation is inductively defined
`as follows:
`
`always
`iff not .s f= 4>
`.s I= </>1 and .s I= </>2
`iff
`iff .s ~ .s' and .s' I= 1> for some .s' such that
`for some path (.s1, .s2, ... ) where .s = ·'1, 3i :> 1 ·'i I= 4>
`iff
`for some path (.s1, .s2, ... ) where ·' = ·'1, vJ :> 1 ·':i F= 4>
`iff
`
`We deli ne the following dual operators:
`
`;l(a) = ,f·,'(a)'
`
`;IG = ,f·,'h
`
`A rooted transition system satisfies a formula 1> if the initial state satisfies
`The
`model checking problem for a formula 4> and a BPP or a Petri net consists in deciding
`if the initial state of the associated transition system satisfies the formula.
`
`10
`
`

`
`In the rest of the section we consider two different fragments of UB, which we denote
`by I';F and I';(~. The syntax of I';F is obtained from the syntax of UB by removing the
`operator /·X; (and implicitely its dual ;1 /<'). So I';F can only express properties of the
`form 'always in the future 4> holds' (;1G4>) or 'sometime in the future 4> holds'(/·,'/<'</>),
`but not properties like 'eventually in the future 4> holds' (;IV</>). In [12] this fragment
`is called liB-. The syntax of I•;G is obtained from the syntax of UB by removing the
`operator /·,'/<'(and implicitely its dual ;IG).
`We prove the following three results:
`
`• The model checking problem for I•;G and VB PI's is undecidable.
`
`• The model checking problem for I•;F and Petri nets is undecidable.
`
`• The model checking problem for I•;F and BPI's is decidable and PSPACI•;-hard.
`Moreover, the model checking problem for I•;F is decidable for any class of Petri
`nets whose set of re<:u:ha,ble rn<:Hkings is effectively sernilinea,r (a, concept to be
`deli ned).
`
`4.4 Undecidability of EG for VBPPs
`
`VVe proceed again by a reduction from the halting problem for counter machines. Given
`a, counter rn<:u:hine A1, we construct a, VBPP wea,k model of M <:wd a, formula, cf>h of J·~G
`satisfying the following two properties:
`
`(1) there exists a run ofM such that all the states reached along it satisfy </>n., and
`(2) if all the states reached along a run of M satisfy </>n., then the run is honest.
`
`Let us see that, once M and 4>n. have been given, the undecidability result follows
`easily. We define the formula
`
`//all = ;1 V(
`
`If M satisfies //all, then the runs that satisfy 4>n. at every state must contain a state
`satisfying /·,'(halt) true. Since such runs exist and are honest by (1) and (2), and
`since honest runs fa,ithfully simulate the behaviour of the counter rmu:hine, the counter
`rna,chine terrnina,tes.
`Conversely, <:tssurne that the counter rmu:hine terminates. A run of the model M
`either is honest or visits a state which does not satis(v cf.>h. In the first case, since the
`rmu:hine terminates, the run conta,ins a, state satisfying /·.'(halt)true, <:wd therefore it
`satisfies //all. In the second case, the run directly satisfies //all.
`Unfortunately, it is not possible to find the formula 4>n. for the weak model of the
`counter machine we use for the modal mu-calculus. The essence of the problem is
`eas1er to see in a simpler process P given by
`p ~I Q II R
`
`Q del
`= q·
`
`Q
`
`Assume that P is simulating, in a weak sense, a certain system. Assume further that
`the honest runs ofP are those whose prefixes satisfy l#q- #rl <:: 1, where #q, #r is the
`number of q's and r's in the prefix. It is easy to see that no formula 4>n. of UB satisfies
`1. a1 1. a2
`1· ·
`·1·
`1 ·2·
`r
`t
`t
`•t•t
`·
`t
`tne con< .1t1ons ( ) an< ( ) al}OVe.
`ne reason 1s tnat, tor every run
`·;0 -~ ·;1 -~ •••
`of P, we have P = /·,'0 = /·,'1 = .... Therefore, all intermediate states satisfy exactly the
`same properties, and no formula of I•;G (or UB) can distinguish between honest and
`dishonest runs.
`
`11
`
`

`
`The rest of the section is devoted to finding another weak model of a counter
`machine for which the formula 4>h exists.
`We shall often use formulas of the form /·,'(a) true. To lighten the notation, we
`define
`
`/·,'N(a) is read 'a is enabled'.
`
`The solution. We make use of an idea introduced by Yoram llirshfeld in [18]. If
`we are allowed to split the actions q and r in the definition of the process P above,
`things change. Define
`p ~I Q II R
`
`3 R
`2
`del 1
`= r ·r ·r ·
`
`R
`
`2 3Q
`del1
`= q ·q ·q .
`
`Q
`
`- #r 1
`and define the honest runs as those satis(ving l#q1
`1 <:: 1. The following formula
`4>h holds for all the states of a run only if it performs the sequence (q1 r 1 q2 r 2 q3 r 3 )~,
`which is honest.
`
`(/·,'N(q2)11/·,'N(r 1)) V
`(/·,'N(q3) 11/·,'N(r2 )) V
`(/·,'N(q1) 11/·,'N(r3 ))
`
`(/·,'N(q1) 11/·,'N(r1)) V
`( /·,' N ( q2) II /·,' N ( r 2)) V
`( /·,' N ( q3) II /·,' N ( r 3)) V
`From P, only the <:u:tion q1 e<Hl occur, bec<:wse if r 1 occurs, then a, state is re<:u:hed
`which enables q 1 and r 2 , and such a state does not satisfy 4>h- We can then similarly
`prove that aJter q 1 only r 1
`e<Hl occur, <Hid so on. IncidentaJiy, the re<:uler e<Hl check
`that splitting p and q into two is not enough.
`Once the power of splitting has been identified, the rest is straightforward. We
`refine our VBPP model in the following way.
`
`A second 'weak' Inodel. A counter CJ is now modelled by
`
`def dec} ·dec}· dec}· 0
`
`A state qi of type II is modelled by
`
`def
`
`def
`
`. (Qi II SQi)
`3 0
`1
`2
`out 1 · out 1 · out 1 ·
`
`In the other equations we repl<u:e outi by outf for consistency, but the <:u:tions
`outi are not split.
`For the definition oft he formula, cf>h is convenient to introduce some notations. First
`of aJI, in order to aJiow a, more cornp<:u:t representation of the formula,, we ren<une the
`action halt to out~+1 . Now, define
`;1 = { outL outr, outr I 0 <:: i <:: n + 1} u {dec}, dec} I 1 <:: j <:: rn}
`
`(notice that the actions deci do not belong to ;1), and let a1, ... ,ak be actions of ;1.
`Then,
`
`k
`
`f\ /·,'N(ai) II f\ ,f·,'(a,)I·,'N(ai) II
`
`k
`
`,f·,'N(a)
`
`i=1
`
`i=1
`
`12
`
`

`
`In words, /·,'N(a 1 , ... ,ak) states that the actions a1 , ... ak are enabled, no sequence
`
`a, a, is enabled, and all the other actions of ;1 are disabled.
`The formula 4>h is a disjunction of formulas. For each state qi of type I and for the
`state qn+J, cf>h cont