Progressive events in supervisory control and compositional verification

Simon Ware,Robi Malik

1.School of Electronic and Electrical Engineering,Nanyang Technological University,Singapore;

2.Department of Computer Science,University of Waikato,Hamilton,New Zealand

Progressive events in supervisory control and compositional verification

Simon Ware1,Robi Malik2†

1.School of Electronic and Electrical Engineering,Nanyang Technological University,Singapore;

2.Department of Computer Science,University of Waikato,Hamilton,New Zealand

This paper investigates some limitations of the nonblocking property when used for supervisor synthesis in discrete event systems.It is shown that there are cases where synthesis with the nonblocking property gives undesired results.To address such cases,the paper introduces progressive events as a means to specify more precisely how a synthesised supervisor should complete its tasks.The nonblocking property is modified to take progressive events into account,and appropriate methods for verification and synthesis are proposed.Experiments show that progressive events can be used in the analysis of industrial-scale systems,and can expose issues that remain undetected by standard nonblocking verification.

Model validation in design methods;Controller constraints and structure;Computational issues

1 Introduction

In supervisory control theory[1,2],it is common to use the nonblocking property to ensure liveness when automatically synthesising supervisors.A discrete event system is nonblocking if,from every reachable state,all involved components can cooperatively complete their common tasks.It is not required that task completion is guaranteed on every possible execution path,only that there exists an execution path to a terminal state.For finite-state systems,the nonblocking property is equivalent to termination under the fairness assumption that events that are enabled infinitely often will be taken eventually[3].This weak liveness condition ensures the existence of least restrictive synthesis results and has been used successfully in many applications[1,4].

On the other hand,the nonblocking property is weaker than a guarantee of termination,and it is not always expressive enough to give the intended results.Several alternatives and extensions to the standard nonblocking property have been proposed.Multi-tasking supervisory control[5]allowsthespecification ofmultiple nonblocking requirements that must be satisfied simultaneously.The generalised nonblocking property[6]restricts thesituations in which nonblocking is required,which is useful in hierarchical interface-based supervisory control[7].Nonblocking under control[8]changes the fairness assumption of standard nonblocking by makingthe assumption that controllable events can preempt uncontrollable events when completing tasks,facilitating reasoning about supervisor implementations.The authors of[9]replace the nonblocking property by the requirement of true termination and perform synthesis using ω-languages.

A different generalisation of the nonblocking property is proposed in[10].Here,progressive events are introduced as the only events that can be used in traces towards task completion when checking the nonblocking property.Progressive events make it possible to capture nonblocking requirements in some cases where this is difficult with the standard nonblocking property,particularly when synthesis is involved,while verification and synthesis are still possible in the same computational complexity as with the standard nonblocking property.This paper is an extended version of[10].It includes Section 4.3 on compositional verification with some experimental results,which shows that progressive events canbeusedwith industrial-scale discrete eventsystems,and that they can help to reveal issues that remain undetected by a standard nonblocking check.

Next,Section 2 introduces the definitions for discrete event systems and supervisory control theory.Section 3 shows two examples of discrete event systems,for which the standard nonblocking property fails to give a useful synthesis result.Section 4 introduces progressive events to model these examples more appropriately,and shows how nonblocking verification and synthesis are adapted for progressive events.The section also includes a discussion of compositional verification methods,experimental results,and an algorithm for synthesis with progressive events.Afterwards,Section 5 compares nonblocking with progressive events to the other nonblocking properties mentioned above,and Section 6 adds some concluding remarks.

2 Preliminaries

2.1 Events and languages

The behaviour of discrete event systems is modelled using events and languages[1,2].Events represent incidents that cause transitions from one state to another and are taken from a finite alphabet Σ.For the purpose of supervisory control,this alphabet is partitioned into the setof controllable events and the setof uncontrollable events.Controllable events can be disabled by a supervising agent,while uncontrollable events cannot be disabled.Independently of this distinction,the alphabet Σ is also partitioned into the setof observable events and the seof unobservable events.Observable events are visible to the supervising agent,while unobservable events are not.In this paper,it is assumed that all unobservable events are also uncontrollable.

Given an alphabet Σ,the term Σ∗denotes the set of all finite traces of the form σ1σ2...σnof events from Σ,including the empty trace ε.The concatenation of two traces s,t∈ Σ∗is written as st.A subset L⊆ Σ∗is called a language.A trace s∈ Σ∗is a prefix of t∈ Σ∗,writtenif t=su for some u∈ Σ∗.The prefix-closure of a languagefor some t∈L},and L is prefix-closed if L=L.

For Ω ⊆ Σ,the natural projectionis the operation that removes from traces s∈all events not in Ω.Its inverse imageis defined byIf the source alphabet is clear from the context,these functions are also written asand

The synchronous composition of two languages L1⊆and

2.2 Discrete event systems

In this paper,discrete event systems are modelled as pairs of languages or as finite-state automata.

De finition 1Let Σ be a finite set of events.A discrete event system over Σ (Σ-DES)is a pair L=(L,Lω)where L⊆ Σ∗is a prefix-closed language,and Lω⊆ L.These languages are also denoted by L(L)=L and Lω(L)=Lω.

The prefix-closed behaviour L(L)contains possibly incomplete system executions.The(not necessarily prefix-closed)sub-language Lω(L)⊆ L(L)is the socalled marked behaviour and contains traces representing completed tasks.

Language operations are applied to discrete events systems by applying them to both components.For example,iffor i=1,2,then L1‖L2=,and the same notation is used for ∪.Discrete event systems form a lattice with inclusion,L1⊆L2,defined to hold if and only if L1⊆L2and

Alternatively,it is common to model discrete event systems as finite-state machines or automata.

De finition 2A(nondeterministic)automaton is a tuple,where Σ is a finite set of events,Q is a set of states,→⊆Q×Σ×Q is the state transition relation,Q°⊆Q is the set of initial states,and Qω⊆Q is the set of marked states.

G is finite-state if the state set Q is finite,and G is deterministic ifandandalways implies y1=y2.Here,the transition relation is written in infix notation,,and extended to traces in Σ∗in the standard way.Also,meansfor some x°∈ Q°.The prefix-closed and marked languages of an automaton G are

Using these definitions,an automaton G is also considered as the Σ-DES G=(L(G),Lω(G)).Conversely,a discrete event system given by two languages is considered as an automaton by taking the canonical recogniser[11]of its languages.

2.3 Supervisory control

Given a plant L and a specification K,supervisory control theory[1,2]is concerned about the question whether and how the plant can be controlled in such a way that the specification is satisfied.This is dependent on the conditions of controllability,normality,and nonblocking.

De finition 3Let K be a ΣK-DES,L a ΣL-DES,and letThen,K is controllable with respect to L if

De finition 4Let K be a ΣK-DES,L a ΣL-DES,and letThen,K is normal with respect to L if

Controllability expresses that a supervisor cannot disable uncontrollable events,and normality expressesthat a supervisor cannot detect the occurrence of unobservable events.Every controllable and normal behaviour can be implemented by a supervisor that only uses observable events as input and only disables controllable events.

In addition to the safety properties of controllability and normality,it is common to require the nonblocking property to ensure some form of liveness.

De finition5AΣ-DESLiscalledstandard nonblocking(or simply nonblocking)if,for every trace s∈L(L),there exists a trace t∈Σ∗such that st∈Lω(L).

If a given system behaviour K is not controllable,normal,or nonblocking,then this behaviour cannot be implemented through control or is undesirable due to livelock or deadlock.The question then arises whether K cansomehow bemodified to satisfy the requirements.A keyresult fromsupervisory controltheorystates thatevery DES K has a largest possible sub-behaviour K′⊆ K that exhibits the desired properties of controllability,normality,and nonblocking.

Theorem1[1]LetK and L be two DES.There exists a unique supremal sub-behaviour supCN(K)⊆K that is controllable,normal,and nonblocking:

Furthermore,if K andLarerepresented byfinite-state automata,a finite-state representation of the supremal controllable,normal,and nonblocking sub-behaviour supCNL(K)can be computed using a fixpoint iteration.This computation is called supervisor synthesis,and its result can be used to implement an appropriate supervisor[1].

3 Applications

This paper is concerned about the nonblocking property and its use in synthesis.In the following,two examples are discussed where the synthesis of a least restrictive supervisor using the standard nonblocking property from Definition 5 gives unexpected and probably undesirable results.

3.1 Computer-controlled board game

A board game is to be controlled,where a computer player and an opponent are taking moves in turn[6].The control objective it to prevent the computer player from losing,while it is always possible for the game to end,either by the computer player winning or by a draw being declared.This is achieved by marking all states where the computer player has won,or the game is over without a winner.A least restrictive nonblocking supervisor can be synthesised to ensure that the game can always end in the desired way.

To complicate the example slightly,a reset feature is added:an additional event reset is introduced,which can always be executed by the environment and resets the game to its initial state.With this addition,the standard nonblocking property is much less expressive.Now,a least restrictive supervisor may allow the game to enter states where defeat for the computer player is inevitable,however due the omnipresent possibility of reset,the system is still nonblocking as long as there is some way of ending the game from its initial state.A synthesised supervisor may exploit this and make bad moves,knowing it is always possible to restart.In this modified model,it is much more interesting to synthesise a supervisor to ensure that“the game can always end,even if reset is not used.”

3.2 Manufacturing cell

Fig.1 shows a modified version of a manufacturing cell proposed in[12],which consists of a robot,a machine,two conveyors,two buffers,and a switch.The machine(plant machine)can manufacture two types of products.Event start[k]initiates the manufacturing of a type k product(k=1or k=2)from a workpiecein input buffer inbuf,which upon completion is placed in output buffer outbuf,indicated by the uncontrollable event! finish[k].Therobot(plantrobot)takesworkpiecesfrom the input conveyor(plant incon)on event load_i and puts them in inbuf on event unload_i,and it takes type k products from outbuf on event load_o[k]and puts them on the output conveyor(plant outcon)on event unload_o[k].The conveyors can be advanced to bring in new workpieces(!advance_i),or to remove completed products(!advance_o[k]).Specifications inbuf_spec and outbuf_spec request a supervisor that prevents overflow and underflow of two one-place buffers.

Fig.1 Manufacturing cell example.Uncontrollable events are prefixed with!,and all events are observable.

In addition,there is aswitch(plant switch)that allows the user to choose the type of products to be delivered.Specification switch_spec requires that,when the user changesthedesired outputtypeto k(!select[k]),atmost one product of the other type may be released from the cell;after that only type k products may be released(unload_o[k])until the switch is operated again.

The model in Fig.1 is not controllable and blocking.Standard synthesis[1]with supervisor reduction[13]gives the least restrictive supervisor in Fig.2.This supervisor correctly prevents buffer overflow by not allowing the machine to start before the output buffer is empty,and prevents deadlock by restricting the number of workpieces in the cell to two.

The supervisor does not distinguish start[1]and start[2],always allowing both types of products to be manufactured.This works because specification switch_spec can be satisfied by disabling the controllable event unload_o[k]when the robot holds a workpiece of an undesired type k,delaying delivery until the user changes the switch with another!select[k]event.While this is the least restrictive controllable and nonblocking behaviour,it seems unreasonable to delay delivery and override the user’s choice in this way.A more reasonable supervisor would respect the user’s choice whenstarting themachine,instead of elyingontheuser to request delivery of what has already been produced.

Fig.2 Synthesised manufacturing cell supervisor.

4 Nonblocking with progressive events

4.1 Progressive events

To provide a better way of modelling examples such as those in Section 3,this section proposes to distinguish events that can be used to establish the nonblocking property from other events.Independently of controllability and observability,the event set Σ is partitioned into the sets Σpof progressive events and Σnpof nonprogressive events.

De finition 6Let L be a Σ-DES,and let Σp⊆ Σ.Then,L is Σp-nonblocking if,for every trace s ∈ L(L),there exists a tracesuch that st∈ Lω(L).

Nonblocking with progressive events requires that,from all reachable states,it is possible to reacha marked state using only progressive events.Non-progressive events are assumed to occur only occasionally or as external input,and a supervisor should not rely on them for task completion.

De finition 7Let K and L be two DES,and let Σpbe a set of progressive events.The least restrictive controllable,normal,and Σp-nonblocking sub-behaviour of K with respect to L is

Definition 7 redefines the objective of synthesis to use the modified nonblocking property.It follows from Proposition 1 below that the definition is sound in that it indeed defines a controllable,normal,and Σpnonblocking behaviour.

In Section 3,events reset and!select[k]would be non-progressive.Then,a Σp-nonblocking supervisor ensures task completion even if the game is not reset,or the manufacturing cell user never changes the requested workpiece type.Fig.3 shows a least restrictive reduced supervisor for the manufacturing cell subject to the!select[k]events being non-progressive.In addition to preventing buffer overflow and deadlock,this supervisor prevents the machine from producing a second workpiece while another is being delivered.

Fig.3 Synthesised manufacturing cell supervisor with progressive events.

4.2 Relationship to standard nonblocking

This section relates the nonblocking property with progressive events to the standard nonblocking property.As Definitions 5 and 6 coincide when Σp= Σ,it is clear that standard nonblocking is a special case of nonblocking with progressive events.If there are nonprogressive events,then nonblocking with progressive events is a stronger condition.

Yet,nonblocking with progressive events can be expressed using standard nonblocking by means of an additional DES P(Σnp,τ)as shown in Fig.4,which uses a new event τ that disables all nonprogressive events.Initially,non-progressive events are possible,but τ may be executed at any time,taking P(Σnp,τ)to state p1where only progressive events can occur.When P(Σnp,τ)is composed with a system to be analysed,all states remain reachable,yet standard nonblocking can only hold if marked states can be reached using progressive events only.

Fig.4 The DES P(Σnp,τ)to express Σp-nonblocking as standard nonblocking.The self loop marked Σnpstands for transitions with all events in Σnp,and τ ∉ Σ is a new event that does not appear elsewhere in the system.

Proposition 1Let L be a Σ-DES withand τ ∉ Σ.Then,L is Σp-nonblocking if and only if L‖P(Σnp,τ)is standard nonblocking.

ProofLet P=P(Σnp,τ).

First assume that L is Σp-nonblocking,and let s ∈L(L‖P).Then,first note thatLett=τif the event τ does not appear ins,and lett=ε if τ appears ins.It follows thatand thusFurthermore,note that PΣ(st)=PΣ(s) ∈ L(L),and as L is Σp-nonblocking,there existssuch that PΣ(st)u ∈ Lω(L).This impliesAlso sinceit holds thatand thusTherefore,stu ∈ Lω(L‖P),i.e.,L‖P is standard nonblocking.

Conversely assume L‖Pis standard nonblocking,and let s∈ L(L).Then,sτ ∈ L(L‖P).As L‖P is nonblocking,there exists u ∈ Σ∗such that sτu ∈ Lω(L‖P).Then,which by construction of P impliesSince furthermore su=PΣ(sτu) ∈ Lω(L),it follows that L is Σpnonblocking.

Proposition 1 shows that any nonblocking verification task with progressive events can be reduced to a standard nonblocking verification task.However,composition with the progressive automaton P(Σnp,τ)doubles the state space and verification time.

The extra effort is not necessary.Standard nonblocking can be checked by searching backwards from marked states to see whether all states are reached.By changing the backward search to use progressive events only,nonblocking with progressive events can be checked on the original system state space,exploring less transitions than a standard nonblocking check.

Proposition 1 is of theoretical interest,because it shows that progressive events do not add to the expressive power of standard nonblocking,and it can be of practical use,because it shows that a wide variety of nonblocking verification algorithms,particularly compositional verification,can also be used with progressive events.This is explained in detail in Section 4.3 below.

It is not immediately clear whether the progressive DES P(Σnp,τ)can also be used to express synthesis with progressive events as standard synthesis.Indeed,if there are uncontrollable nonprogressive events,then P(Σnp,τ)used as an additional plant will disable some uncontrollable events,and a supervisor could wait for the auxiliary event τ to occur in order to avoid controllability problems.

This is avoided if τ is unobservable.Then,the supervisor cannot distinguish the states of P(Σnp,τ),so it has to enable uncontrollable events enabled in p0and at the same time ensure task completion from p1.Lemma 1 shows for unobservable τ that controllability and normality are preserved by the addition of P(Σnp,τ),which together with Proposition 1 implies the preservation of synthesis results as shown in Proposition 2.

Lemma 1Let K and L be Σ-DES withand let τ ∉ Σ be an uncontrollable and unobservable event.

i)K is controllable with respect to L if and only if K is controllable with respect to L‖P(Σnp,τ).

ii)K is normal with respect to L if and only if K is normal with respect to L‖P(Σnp,τ).

ProofLet P=P(Σnp,τ).

i)First assume that K is controllable with respect to L‖P,and letThen,sυ ∈ Σ∗,andby construction of P,and thusas K is controllable with respect to L‖P.It follows that sυ∈L(K),which means that K is controllable with respect to L.The converse inclusion holds by Proposition 3 in[14].

ii)First assume that K is normal with respect to L,and letThen,clearlyas K is normal with respect to L.Thus,K is normal with respect to L‖P.

Conversely assume K is normal with respect to L‖P,and letThen,s∈ Σ∗and thereforewhich impliesas K is normal with respect to L‖P.This shows that K is normal with respect to L.

Proposition 2Let K and L be Σ-DES with Σ =,and let τ∉Σ be an uncontrollable and unobservable event.Then,

ProofConsider an arbitrary sub-behaviour K′⊆ K.In Lemma 1 it has been shown that K′is controllable and normal with respect to L if and only if K′is controllable and normal with respect to L‖P(Σnp,τ),and in Proposition 1 it has been shown that K′‖L is Σp-nonblocking if and only if K′‖L‖P(Σnp,τ)is nonblocking.As this holds for all sub-behaviours K′of K,the least restrictive sub-behaviours must also be equal.

Thus,synthesis with progressive events can be achieved using standard synthesis methods.However,the introduced automaton P(Σnp,τ)includes the unobservable event τ,making it necessary to use the more complex synthesis algorithm with unobservable events[2],even if the original model only has observable events.Section 4.4 below presents a direct algorithm for synthesis with progressive events that does not have these performance issues.

4.3 Compositional veri fication

This section investigates compositional verification and shows how the nonblocking property with progressive events can be verified efficiently for large systems.

The standard method to check whether a system is nonblocking[2]involves the explicit composition of all the automata involved,and is limited by the well-known state-space explosion problem.Compositional verification[15,16]is an effective alternative that works by simplifying individual automata of a large synchronous composition,gradually reducing the state space of the system and allowing much larger systems to be verified in the end.Compositional verification requires the use of abstraction methods that preserve the property being verified.

While no abstraction methods have been developed for nonblocking with progressive events,Proposition 1 shows that a nonblocking checkwith progressive events can be replaced by a standard nonblocking check after the addition of a single automaton P(Σnp,τ).This makes it possible to apply all the techniques that exist for compositional verification of the standard nonblocking property[17–20].These techniques arebased onthe preservation of conflict equivalence,which is the most general process equivalence for use in compositional nonblocking verification[21].If a component of a system is replaced by a conflict equivalent component,the nonblocking property is guaranteed to be preserved.

Compositional algorithms verify whether a set G of automata is nonblocking by taking a subset H⊆G of the automata and composing them to create an automaton H=‖H.Then,the set of local events of H is identified:these are events that appear only in H and not in the rest of the system GH.The local events are hidden from H,i.e.,they are replaced by a new event τH∉ Σ,resulting in a new automaton H′.Then,abstraction techniques[17–20]are used to simplify H′and obtain a conflictequivalent abstraction H′′.Because H′′is conflict equivalent to H′,and H′is obtained by hiding local events from H,it can be shown[21]that H synchronised with the automata in GH is nonblocking if and only if H′′composed with the same automata is nonblocking.Therefore,the problem to verify whether the set of automata G is nonblocking is replaced by the equivalent problem to verify whether the simpler set of automata(GH)∪ {H′}is nonblocking.This procedure is repeated until the set of automata is simple enough to be composed together in a standard nonblocking check.

The above algorithm relies on local events.Thus,the addition of a single progressive automaton P(Σnp,τ)can be problematic,because it increases the coupling between these events in the model.If there are a lot of non-progressive events that are used by a lot of automata,then many automata may have to be composed with P(Σnp,τ)before events can be removed.The following Proposition 3 suggests a way to avoid this problem by splitting the progressive automaton P(Σnp,τ)into smaller automata.It is possible to create separate automatafor different subsetsof the set of non-progressive events.The proposition shows that,no matter what the system T to be verified is,T ‖P(Σnp,τ)is nonblocking if and only if■is nonblocking.

Proposition 3Let Σ1,Σ2⊆ Σ be sets of events,and let τ,τ1,τ2∉ Σ be three distinct events.For every Σ-DES T,it holds that T ‖P(Σ1∪ Σ2,τ)is nonblocking if and only if T ‖P(Σ1,τ1)‖P(Σ2,τ2)is nonblocking.

ProofLetand P2=P(Σ2,τ2).Then,it is to be shown that T ‖P12is nonblocking if and only if T ‖P1‖P2is nonblocking.

First assume that T‖P12is nonblocking,and let s∈ L(T ‖P1‖P2).For i=1,2,let ti= τiif the event τidoes not appear in s,and ti= ε if τiappears in s.Then,for i=1,2 by Definition 8,andFurthermore,PΣ(s)∈ L(T‖P12)asby Definition 8.As τ ∉ Σ,it followsthat PΣ(s)τ ∈ L(T ‖P12).As T ‖P12is nonblocking,there exists a trace u ∈ (Σ ∪{τ})∗such that PΣ(s)τu ∈ Lω(T‖P12).By Definition 8,it follows thatand thusand as τ,τ1,τ2∉Σ it holds that PΣ(st1t2u)=PΣ(su)=PΣ(PΣ(s)τu) ∈Lω(T).As u ∈ (ΣΣ12)∗,it holds that Pand thusfor i=1,2.Hence,st1t2u ∈ Lω(T‖P1‖P2),i.e.,T‖P1‖P2is nonblocking.

Now assume that T ‖P1‖P2is nonblocking,and let s∈ L(T ‖P12).Let t= τ if the event τ does not appear in s,and t= ε if τ appears in s.Then,PΣ∪{τ}(st)∈ Lω(P12)by Definition 8,and st∈ L(T‖P12).Furthermore,PΣ(s)∈ L(T ‖P1‖P2),asfor i=1,2 by Definition 8.As τ1,τ2∉ Σfor i=1,2 and thus u ∈ (Σ Σ12)∗,and as τ,τ1,τ2∉ Σ it holds that PΣ(stu)=PΣ(su)=As u ∈ (ΣΣ12)∗,it holds thatand thusHence,i.e.,T‖P12is nonblocking.

The compositional nonblocking checker implemented in the DES software tool Supremica[22]has been used to check the nonblocking property of five discrete event systems.One of these is the example given in Section 3.2 above,while the other four are industrial-scale models also used as benchmarks for compositional verification in[23],where a reasonable set of non-progressive events was identified.The following list gives some more information about these models.

aip0aipModel of the automated manufacturing system of the Atelier Inter-´etablissement de Productique[24].Considered here is an early version based on[25].

big_bmwBMW window lift controller model from Petra Malik’s dissertation[26].

cell_switchManufacturing cell model described in Section 3.2.The model considered for the experiments consists of the automata in Fig.1 and the supervisor in Fig.2,and is Σp-blocking.

tip3Model of the interaction between a mobile client and event-based servers of a tourist information system[27].

verriegel4Car central locking system,originally from the KORSYS project[28].

Table 1 shows the results of compositional verification of the nonblocking property with progressive events for the above models.The “Size”column refers to the total number of states in the full synchronous composition of each model,without the additional progressive events automata,and the “Result”column indicates whether or not the model is nonblocking with progressive events.The columns“Single P”and “Multiple P”refer to two ways of performing the compositional nonblocking check.In the case of“Single P”,only one proit holds that.As T ‖P1‖P2is nonblocking,there exists a tracesuch that PΣ(s)τ1τ2u ∈ Lω(T ‖P1‖P2).By Definition 8,it follows thatiiiiiigressive automaton is created for all non-progressive events,whereas in the case of“Multiple P”,separate progressive automata are used,each containing the non progressive events of a single system component.For each experiment,the “Peak states”column shows the number of states of the largest automaton constructed during the check,and “Time”is the number of seconds taken to complete the check.The entries for the tip3 model with the“Multiple P”method are blank,because the algorithm ran out of memory in this case.

The results show that compositional nonblocking verification works well to check the nonblocking property with progressive events of large models.In most cases,using only one progressive events automaton works better than splitting it,with the exception of the aip0aip model.This may be because a larger number of automata means more work,also for compositional algorithms,or because the compositional algorithms has no knowledge about the progressive events automata and may compose them with other automata than the ones they were created for.It is possible that performance can be improved using a more specific composition strategy.

Verification of the central locking system model verriege l4 shows that it is blocking with progressive events,although it is standard nonblocking.This is an unexpected result,and investigation of the counterexamples suggests an issue with the controller in that it exhibits a deadlock-like situation after two simultaneous requests to unlock the car,which can only be resolved after the arrival of another request.This suspected controller bug was not found by the standard nonblocking checks performed on the model before.

Table 1 Experimental results.

4.4 Direct synthesis algorithm

This section proposes a direct synthesis algorithm with progressive events for the case of total observation,i.e.,when all events are observable.In this case,the unobservable event τ can be avoided,which gives rise to a more efficient solution.The following synthesis objective is considered.

De finition 9Let K and L be Σ-DES,and let Σp⊆ Σ.The least restrictive controllable and Σp-nonblocking sub-behaviour of K with respect to L is

Definition 10 defines a synthesis operator on the subbehaviours of L,which afterwards is shown to have the above supCL,Σp(K)as its greatest fixpoint[29].

De finition10LetL be a Σ-DES,and let Σp⊆ Σ.The operator ΘL,Σpon the lattice of Σ-DES is defined by

It is first shown that the post-fixpoints of ΘL,Σpare exactly the controllable and Σp-nonblocking subbehaviours of L.

Proposition 4Let L and K be a Σ-DES such that K ⊆ L,and let Σp⊆ Σ.Then,K ⊆ ΘL,Σp(K),if and only if K is controllable with respect to L and L‖K is Σp-nonblocking.

ProofFirst assumeTo see that K is controllable with respect to L,let s∈ L(K)and υ ∈ Σucsuch that sυ ∈ L(L).As s ∈ L(K)andit holds thatwhich implies sυ ∈ L(K).As s and υ were chosen arbitrarily,it follows by Definition 3 that K is controllable with respect to L.To see that K‖L is Σp-nonblocking,let s∈ L(K‖L).Then,i.e.,there existssuch that st∈ Lω(L‖K).Thus,K‖L is Σp-nonblocking.

Conversely,assume that K is controllable with respect to L and L‖K is Σp-nonblocking,and let s ∈ L(K).Let r■ s and υ ∈ Σucsuch that rυ ∈ L(L).Then,r∈ L(K),and as K is controllable with respect to L,it follows that rυ ∈ L(K)and thusFurther,as L ‖K is Σp-nonblocking,for r ∈ L(K)⊆ L(L),there existssuch that rt∈ Lω(L‖K),i.e.,Thus,s∈ θL,Σp(K),and it follows from(6)that K ⊆ ΘL,Σp(K).

Furthermore, ΘL,Σpis a monotonic operator on the lattice of Σ-DES.

Proposition 5Let L,K1,and K2be Σ-DES andIf K1⊆ K2,then

ProofAssume K1⊆K2.Considering Definition 10,it is enough to show thatandFirst,forit holds that s∈L(K1)⊆ L(K2)and for all r■ s and all υ ∈ Σucsuch that rυ ∈ L(L)it holds that rυ ∈ L(K1)⊆ L(K2),and thusSecond,forit holds that s∈L(K1)⊆L(K2)and for allthere existssuch thatand thus

Proposition 5 shows that ΘL,Σpis a monotonic operator on the lattice of Σ-DES,so it follows by the Knaster-Tarski theorem[29]that ΘL,Σphas a greatest fixpoint,which by Proposition 4 is the least restrictive controllable and Σp-nonblocking sub-behaviour of L.

To compute the fixpoint in a finite number of steps,it is next shown that the least restrictive controllable and Σp-nonblocking sub-behaviour for finite-state deterministic specification K and plant L can be computed using the states of the synchronous composition L‖K.Therefore,Definition 12 introduces an iteration on the state set of L‖K,which in Proposition 6 is shown to be equivalent to the above ΘL,Σp.

De finition 11The restriction of G= 〈Σ,Q,→,Q°,Qω〉to X ⊆ Q is G|X= 〈Σ,X,→|X,Q°∩ X,Qω∩ X〉where→|X={(x,σ,y)∈→|x,y∈X}.

De finition 12Letandbe two deterministic finitestate automata,and let Σp⊆ Σ.The synthesis step operatorfor L and K with respect to Σpis defined by

Proposition 6Let〉and K=be two deterministic finite-state automata,let S=L‖K,and let Σp⊆ Σ.For every state set X⊆QL×QK,it holds that

ProofBased on Definition 11 and(2)and(6),it is enough to show

By Proposition 6,a language-based stepgives the sameresult asa state-based step ofwhenapplied to a subset of the states of L‖K.To synthesise the least restrictive controllable and Σp-nonblocking subbehaviour of specification K with respect to plant L,one first constructs the composition S=L‖K.Then,the iteration

converges against a greatest fixpoint Xnin a finite number of n steps,which by Proposition 6 satisfies

5 Related work

This section relates nonblocking with progressive events to other nonblocking conditions studied in the literature.

Multi-tasking supervisory control[5]requires a synthesised supervisor to be nonblocking with respect to several sets of marked states at the same time.Generalised nonblocking[6]uses a second set of marked states to specify a subset of the states,from which marked states must be reachable.Both conditions are amenable to synthesis and can be combined with progressive events to further increase modelling capabilities.

The condition of nonblocking under control[8]is more similar to that of nonblocking with progressive events.When modelling a supervisor implementation,it is assumed that an implemented supervisor or controller sends controllable events as commands to the plant.Typically,the controller can generate several controllable events in quick sequence,and it is considered unlikely that uncontrollable events occur during such a sequence.Then,it makes sense to require the system to complete its tasks using Σc-complete traces.

De finition 13[8] Let G= 〈Σ,Q,→,Q°,Qω〉and Σc⊆ Σ.The pathis Σc-complete,if for each i=1,...,n it holds that either σi∈ Σcor there do not exist σ ∈ Σcand y ∈ Q such that

De finition 14[8] Let G= 〈Σ,Q,→,Q°,Qω〉and Σc⊆ Σ.Then,G is nonblocking under Σc-control if for all paths,there exists a Σc-complete pathsuch that yω∈Qω.

Nonblocking under control is similar to nonblocking with progressive events,in that it considers uncontrollable events as non-progressive in states where a controllable event is enabled.However,it depends on the state whether an event is progressive or not,and this dependency means that in general there do not exist least restrictive supervisors that are nonblocking under control.

Fig.5 A DES G that has no least restrictive supervisor that is nonblocking under control.Events c and d are controllable,while!u is uncontrollable.

For example,Fig.5 shows a DES G which is not nonblocking under control.As the uncontrollable!utransitions are only enabled in states where controllable eventsarealso enabled,these transitions areconsidered as non-progressive and cannot be used to prove that the marked state is reachable.The two sub-behaviours S1and S2are nonblocking under control,however neither of them is least restrictive,and their least upper bound,G,is not nonblocking under control.

It is shown in[26]how the property of nonblocking under control canbe verified.Synthesis for this and similar properties can be achieved using ω-languages[9],however these methods do not in general produce a state-based supervisor that can be readily implemented.

6 Conclusions

The condition of nonblocking with progressive events is introduced as an extension of standard nonblocking.It is shown that there are situations where synthesis using the standard nonblocking property results in an unexpected result,because the synthesised supervisor can complete its tasks only if certain rare or undesirable events occur.Using progressive events,it can be specified more precisely how a synthesised supervisor must complete its tasks.The nonblocking property with progressive events of some industrial-scale discrete eventsystems has been checkedusing the compositional verification algorithm in Supremica[22],in one case exposing an issue that remains undetected when only the standard nonblocking property is considered.While progressive events increase the modelling capabilities,verification and synthesis can still be achieved without increase in complexity over the standard nonblocking property.

[1]P.J.G.Ramadge,W.M.Wonham.The control of discrete event systems.Proceedings of the IEEE,1989,77(1):81–98.

[2]C.G.Cassandras,S.Lafortune.Introduction to Discrete Event Systems.2nd ed.New York:Springer Science&Business Media,2008.

[3]A.Arnold.Finite Transition Systems:Semantics of Communicating Systems.Hertfordshire,UK:Prentice-Hall,1994.

[4]Y.Chen,S.Lafortune,F.Lin.Design of nonblocking modular supervisors using event priority functions.IEEE Transactions on Automatic Control,2000,45(3):432–452.

[5]M.H.de Queiroz,J.E.R.Cury,W.M.Wonham.Multitasking supervisory control of discrete-event systems.Proceedings of the 7th International Workshop on Discrete Event Systems.Reims,France:IFAC,2004:175–180.

[6]R.Malik,R.Leduc.Generalised nonblocking.Proceedings of the 9th InternationalWorkshop on Discrete Event Systems.Göteborg,Sweden:IEEE,2008:340–345.

[7]R.J.Leduc,B.A.Brandin,M.Lawford,etal.Hierarchical interfacebased supervisory control–Part I:Serial case.IEEE Transactions on Automatic Control,2005,50(9):1322–1335.

[8]P.Dietrich,R.Malik,W.M.Wonham,et al.Implementation considerations in supervisory control.B.Caillaud,P.Darondeau,L.Lavagno,X.Xie,editors.Synthesis and Control of Discrete Event Systems.Dordrecht,the Netherlands:Kluwer Academic Publishers,2002:185–201.

[9]C.Baier,T.Moor.A hierarchical control architecture for sequential behaviours.Proceedings of the 11th International Workshop on Discrete Event Systems.Guadalajara,Mexico:IFAC,2012:259–264.

[10]S.Ware,R.Malik.Supervisory control with progressive events.Proceedings of the 11th IEEE International Conference on Control and Automation(ICCA 2014).Taiwan:IEEE,2014:1461–1466.

[11]J.E.Hopcroft,R.Motwani,J.D.Ullman.Introduction to Automata Theory,Languages,and Computation.Boston:Addison-Wesley,2001.

[12]W.M.Wonham.Supervisory Control of Discrete-Event Systems.Ontario,Canada:University ofToronto,2009:http://www.control.utoronto.edu/.

[13]R.Su,W.Murray Wonham.Supervisor reduction for discrete event systems.Discrete Event Dynamic Systems:Theory and Applications,2004,14(1):31–53.

[14]B.A.Brandin,R.Malik,P.Malik.Incremental verification and synthesis of discrete-event systems guided by counterexamples.IEEE Transactions on Control Systems Technology,2004,12(3):387–401.

[15]S.Graf,B.Steffen.Compositional minimization of finite state systems.Proceedings of the Workshop on Computer-Aided Verification.New Brunswick:Springer,1990:186–196.

[16]A.Valmari.Compositionality in state space verification methods.Proceedings of the 18th International Conference on Application and Theory of Petri Nets.Osaka,Japan:Springer,1996:29–56.

[17]H.Flordal,R.Malik.Compositional verification in supervisory control.SIAM Journal of Control and Optimization,2009,48(3):1914–1938.

[18]P.N.Pena,J.E.R.Cury,S.Lafortune.Verification of nonconflict of supervisors using abstractions.IEEE Transactionson Automatic Control,2009,54(12):2803–2815.

[19]R.Su,J.H.van Schuppen,J.E.Rooda,et al.Nonconflict check by using sequential automaton abstractions based on weak observation equivalence.Automatica,2010,46(6):968–978.

[20]S.Ware,R.Malik.Conflict-preserving abstraction of discrete event systems using annotated automata.Discrete Event Dynamic Systems:Theory and Applications,2012,22(4):451–477.

[21]R.Malik,D.Streader,S.Reeves.Conflicts and fair testing.International Journal of Foundations of Computer Science,2006,17(4):797–813.

[22]K.˚Akesson,M.Fabian,H.Flordal,et al.Supremicaan integrated environment for verification,synthesis and simulation of discrete event systems.Proceedings of the 8th InternationalWorkshop on Discrete Event Systems.Ann Arbor,MI:IEEE,2006:384–385.

[23]R.Malik,R.Leduc.Compositional nonblocking verification using generalised nonblocking abstractions.IEEE Transactions on Automatic Control,2013,58(8):1–13.

[24]B.Brandin,F.Charbonnier.The supervisory control of the automated manufacturing system of the AIP.Proceedings of Rensselaer’s4 thInternational Conference on Computer Integrated Manufacturing and Automation Technology.Troy,NY:IEEE Computer Society Press,1994:319–324.

[25]R.J.Leduc.Hierarchical Interface-based Supervisory Control.Ontario,Canada:University of Toronto,2002.

[26]P.Malik.From Supervisory Control to Nonblocking Controllers for Discrete Event Systems.Kaiserslautern,Germany:University of Kaiserslautern,2003.

[27]A.Hinze,P.Malik,R.Malik.Interaction design fora mobile context-aware system using discrete event modelling.Proceedingsofthe 29th Australasian ComputerScience Conference,ACSC’06.Hobart,Australia:Australian Computer Society,2006:257–266.

[28]Project KorSys:http://www4.in.tum.de/proj/korsys/.

[29]A.Tarski.A lattice-theoretical fixpoint theorem and its applications.Pacific Journal of Mathematics,1955,5(2):285–309.

4 July 2014;revised 13 July 2014;accepted 13 July 2014

DOI10.1007/s11768-014-4097-8

†Corresponding author.

E-mail:robi@waikato.ac.nz.Tel.:+64(0)7 838 4796;fax:+64(0)7 858 5095.

©2014 South China University of Technology,Academy of Mathematics and Systems Science,CAS,and Springer-Verlag Berlin Heidelberg

Simon WAREreceived his Bachelor of Computing and Mathematical Sciences degree with Honours from the University of Waikato in Hamilton,New Zealand in 2007.Also in 2007,he was involved in a project for discrete event simulation of port biosecurity procedures at AgResearch in Hamilton.He received his Ph.D.in Computer Science from the University of Waikato in 2014.He is currently a research fellow at Nanyang Technological University in Singapore.His main research interests are liveness and fairness properties of discrete event systems.E-mail:siw4@waikato.ac.nz.

Robi MALIKreceived the M.S.and Ph.D.degree in Computer Science from the University of Kaiserslautern,Germany,in 1993 and 1997,respectively.From 1998 to 2002,he worked in a research and development group at Siemens Corporate Research in Munich,Germany,where he was involved in the development and application of modelling and analysis software for discrete event systems.Since 2003,he is lecturing at the Department of Computer Science at the University of Waikato in Hamilton,New Zealand.He is participating in the development of the Supremica software for modelling and analysis of discrete event systems.His current research interests are in the area of model checking and synthesis of large discrete event systems and other finite-state machine models.E-mail:robi@waikato.ac.nz.