On

2003,VOL.76,NO.17,1739–1748

Onasimplifieduntimingprocedureforsupervisorycontroloftimedautomatawhenthetimeincreasesstrictlymonotonically

MICHAELP.SPATHOPOULOS{

GivenatimedautomatonGacceptingthetimedlanguageLTafinitestatemachineG0canbeconstructed,knownastheregionautomaton,whichacceptstheuntimedlanguageUntime(LT).InthispaperweconstructanalternativefinitestatemachinewhichalsoacceptsthelanguageUntime(LT),buthasfewerstatesthanG0.Thisisshownforlanguagesofbothfiniteandinfinitetracesgiventhatthetimevaluesinthetimesequenceincreasestrictlymonotonically.Thesupervisorycontroldesignfortimedautomata,whenthesimplifieduntimingprocedureisusedandthetimeisstrictlypositive,isstudied.

1.Introduction

Timeddiscreteeventsystemsareageneralizationofdiscreteeventsystemsinwhicheacheventisconsideredtohaveoccurredatacertainpointintime.Primarily,researchinthisfieldhasconcentratedonthelogicalsequencingofeventsandabstractedawaytheactualtimingdelaysbetweenevents.However,thecorrectbe-haviourofhardreal-timesystemssuchasmanufactur-ingsystems,transportsystemsandcomputernetworksdependsontheactualdelayvaluesbetweenevents.Variousformalismshavebeendevelopedtomodeltimeddiscreteeventsystems,includingAlurandDill(1994)andBrandinandWonham(1994).WorkinBrandinandWonham(1994)correspondstodiscretetimeusingasinglesystemtimerasoppositetoAlurandDill(1994)wherethedensetimemodelincludesseveralasynchronousclocksandismoreexpressivethanotherformalismsallowingcompositionoftimedprocessesandindependenttimingconditionsforeachsystemcomponent.Here,weareconcernedwithtimedautomataasdefinedinAlurandDill(1994).

Thetimedautomatondefines(oraccepts)alanguageoftimedwords.Atimedwordisdefinedasfollows:givenanordinaryword󰀁1󰀁2...󰀁n,wepaireachletter󰀁iwithanon-negativerealnumberti2R!0,subjecttothecon-ditionthattiReceived1April2003.Revisedandaccepted28September2003.

{SystemDynamicsandControlDepartmentofMechanicalEngineering,UniversityofStrathclyde,JamesWeirBuilding,75MontroseStreet,GlasgowG11XJ,UK.e-mail:mps@mecheng.strath.ac.uk

(timed)!-word,andalanguageof(timed)infinitewordsiscalleda(timed)!-language.

Weinterprettitobethetimeatwhichtheevent󰀁ioccurs;itisaconventioninthetheoryoftimeddiscreteeventsystemsthataneventoccursatasinglepointintime,whereasasystemmaybeinaparticularstateforanon-trivialtimeinterval.

GivenatimedautomatonGacceptingthetimedlan-guageLT,itwasshowninAlurandDill(1994)thatafinitestateautomatonG0canbeconstructed,knownastheregionautomaton,whichacceptsthelanguageUntime(LT).

ThemainresultofthispaperconcernsthedefinitionofafinitestateautomatonGÃthatalsoacceptsthelan-guageUntime(LT),buthassignificantlyfewerstatesthanG0andisthereforeeasiertoconstruct.Werequirethatthetimeincreasesstrictlymonotonically,whileinAlurandDill(1994)timeisfirstassumedtosatisfythesamemonotonicityconstraint(Definition3.1),thiscon-ditionislaterrelaxed.Wefirstconsidertimedautomataasacceptorsoffinitetimedwords,andin}5wegeneral-izeourresultstotimed!-words.Indeed,weneedtodistinguishlanguagesoffiniteandinfinitestringssincethederivedfiniteautomataineachcasearedifferent,whereasinAlurandDill(1994)theresultsarethesameforbothcases.Althoughtheresultaboveisofinterestincomputerscience,weshowthatourresultisusefulforthecontrolofrealtimediscrete-eventsystemsaswell.

ThesecondresultconcernstheapplicationofthesimplifiedconstructionoftheautomatonGÃforthesupervisorycontroloftimeddiscreteeventsystems.SupervisorycontrolfortimeddiscreteeventsystemshasbeenstudiedinHoffmannandWong-Toi(1992),BrandinandWonham(1994),Asarinetal.(1998),LaurenceandSpathopoulos(1998)andSpathopoulos(2003).InHoffmannandWong-Toi(1992)andLaurenceandSpathopoulos(1998)themethodsofRamadgeandWonham(1987)areadaptedtoconstructasupervisorforadensereal-timediscreteeventsystem

InternationalJournalofControlISSN0020–7179print/ISSN1366–5820online#2003Taylor&FrancisLtd

http://www.tandf.co.uk/journalsDOI:10.1080/00207170310001628570

1740M.P.Spathopoulos

modelledbyatimedautomatonusinguntimingpro-cedures.InSpathopoulos(2003)thenon-blockingsupervisorycontrolproblemwithurgencyhasbeenstudiedandinAsarinetal.(1998)thesameproblemisaddressedwithoutusinguntimingprocedures.

Whenthetimeincreasesstrictlymonotonically,asisalwaysthecaseinreality,thesimplifiedautomatonderivedbelow,whichappliesforthefinitestringcase,canbeusedforthesolutionofthesupervisorycontrolproblem.Weshowthatwhenthissimplifiedtechniqueisusedandthetimeisstrictlypositiveitisnecessaryforthecontrolledbehaviourtobecomemoreconservative.Intuitivelythisistobeexpectedsinceallowingthetimetobezerogivesmoreflexibilitytothemodel.

Thepaperisorganizedasfollows.In}}2and3thetimedautomataandtheconstructionoftheregion(untimed)automaton,asgiveninAlurandDill(1994),arebrieflyintroduced.

Themainresultofthepaperisgivenin}4andin}5theresultisextendedforinfinitestrings.Upperboundsfortheclockregionsofthederivedautomataaregivenin}6.Thesecondresultisgivenin}7wherethesimpli-fieduntimingtechniqueisusedforthesupervisorycon-trolproblemofrealtimediscrete-eventsystems.Anillustratedexampleisusedinordertoderivethecon-ditionsunderwhichthesimplifiedconstructionresultsintheleastrestrictivecontrolledbehaviour.Finally,con-clusionsaregivenin}8.2.

Thetimedautomaton

InthissectionwegiveashortoverviewofthetimedautomatonasdefinedinAlurandDill(1994),wherethereaderisreferredformoredetails.Ourpurposehereisnottogiveintuitiveexplanationsofdefinitionsintimedautomataandinterestedreadersshouldbefamiliarwiththem.

Forsimplicityweconsidertimedautomataasaccep-torsoffinitewords.Ourresultsareextendedforlan-guagesofinfinitewordsin}5.Definition1:

AtimedautomatonisatupleG¼ðS;S;C;E;S0;SmÞ

ð1Þ

whereS,asusual,isafinitealphabet,Sisafinitesetofstates,CisafinitesetofclocksandEisafinitesetofedges.ThesetsS0;Sm󰀃Sarecalledtheinitialandfinal(oraccepting)statesetsrespectively.

Anedgeisatupleðs;s0;󰀁;󰀂;C0Þ,alternativelywrittensÀÀÀÀÀÀ󰀁

󰀂

ÀÀCÀ:À¼!0s0

0

ð2Þ

HereC0󰀃Cand󰀂iswhatisknownasaclockcon-straint.Aclockconstraintisapredicate(thatis,acon-dition)builtfromtheatomicpredicatescÃq(where

c2CandÃisoneof ,!or¼andq2Z)using:(not)andtheconnectives^(and)and_(or).Forinstance,ifc;d2Cthenc!1_d¼2isanexampleofapredicate.

Weneedfurtherdefinitionsasfollows.Definition2:A(clock)valuationisafunction

󰀃:C!R!0.

Definition3:Aclockvaluation󰀃:C!R!0issaidtosatisfyaclockconstraint󰀂ifreplacingeachclockcincin󰀂by󰀃ðcÞgivesatruestatement.

Definition4:If󰀃:C!R!0isaclockvaluationandt2R,then󰀃þtistheclockvaluationgivenbyð󰀃þtÞðcÞ¼󰀃ðcþtÞforallclocksc.Also,ift>0then󰀃þtissaidtobeasuccessorof󰀃.

Definition5:If󰀃:C!R!0isaclockvaluationandC0󰀃Cthen½C0¼0󰀆󰀃istheclockvaluationwhichsendsallclocksinC0tozeroandsendsalltheotherstothesamevalueas󰀃.

Essentially,thetimedautomatonisaninfinitestateautomatonwhosestatesareorderedpairsðs;󰀃Þwheres2Sisastateand󰀃:C!R!0isaclockvaluation.Wewillcallsuchpairsgeneralized(orextended)states.WhenthetimedautomatonisGregardedasaninfinitestateautomaton,itsinitial(generalized)statesarethoseorderedpairsðs;󰀃Þwheres2S0andthevaluationsendseveryclocktozero.Thefinalstatesarethoseforwhichs2Sm.Thesetoftransitionsbetweengeneralizedstatesisdefinedasfollows.

Giventheedgein(2)andclockvaluations󰀃;󰀃0,thereisalegaltransitionwithlabel󰀁fromðs;󰀃Þtoðs0;󰀃0Þifthereexistst>0and󰀃0¼½C0¼0󰀆ð󰀃þtÞ.Wecalltthetimejumpofthetransitionatthestates.Wealsodefinetheemptytimedwordð\";0Þ,where\"istheemptyword.Alltransactionsareofthistype,oraretrivial;thatis,thereisatransitionwithlabel\"fromeverygeneralizedstatetoitself.

Itisworthmentioningagainthatitispossibletoallowzerotimejumpsinthedefinitionofatransition.ThiswasconsideredbyAlurandDill(1994)inordertoallowthesametimevaluetobeassociatedwithmanyconsecutiveeventsinthetimesequence.However,inthiscasethemainresultofthispaper,theconstructionofanuntimedautomatonG0withfewerstatesthantheregionautomatonisimpossible,sinceLemma3of}4isfalse.

HavingdefinedGasastatemachine,wenowexplainhowGcanbeusedtodefineatimedlanguage.Letð󰀁1;t1Þ...ð󰀁n;tnÞbeafinitetimedword.ThenwesaythatGacceptsð󰀁1;t1Þ...ð󰀁n;tnÞifGacceptstheuntimedword󰀁1󰀁2...󰀁nasastatemachineandif

Supervisorycontroloftimedautomata

1741

ðs󰀁1

󰀁2

󰀁n

0;󰀃0ÞÀ!ðs1;󰀃1ÞÀ!ðs2;󰀃2ÞÁÁÁðsnÀ1;󰀃nÀ1ÞÀ!ðsn;󰀃nÞisacorrespondingacceptingpathfor󰀁1󰀁2ÁÁÁ󰀁n(recallthatthismeansthats02S0;sn2Smandthevaluation󰀃0sendseveryclocktozero)thentiÀtiÀ1isthetimejumpforthetransition(betweengeneralizedðs󰀁states)

!i

iÀ1;󰀃iÀ1ÞÀðsi;󰀃iÞ.ThetimedlanguageacceptedbyGisthendefinedasthesetoftimedwordsacceptedbyG.IfGacceptsthetimedlanguageLT,thenwealsosaythatGacceptstheuntimedlanguageUntimeðLTÞ.

3.TheAlur–Dilluntimingconstruction

Inthissectionforthesakeofcompletenesswestate

brieflytheregionautomatonasconstructedinAlurandDill(1994).

Thetimedautomatonhasoneimportantdisadvan-tageincomputations;evenifthestatesetSisfinite,therewillnecessarilybeinfinitelymanygeneralizedstates(assumingthereisatleastoneclock)simplybecausethereareinfinitelymanyclockvaluations.Thisproblemisavoidedbypartitioningthesetofclockvaluationsintoequivalenceclassesinsuchawaythattherearefinitelymanysuchclassesandtheessentialstructureofthetimedautomatoniscaptured.

Anequivalencerelation,󰀈,isdefinedonthesetValofclockvaluationsofAhavingthefollowingtwoprop-erties:therearefinitelymanyequivalenceclasses,andifthereexistclockvaluations󰀃1,󰀃2and󰀄1with󰀃1󰀈󰀃2andthereisalegaltransitionfromðs;󰀃1Þtoðs0;󰀄1Þ,thenthereisaclockvaluation󰀄2with󰀄1󰀈󰀄2andalegaltransitionfromðs;󰀃2Þtoðs0;󰀄2Þ.

Definition6:LetGbethetimedautomatonof(1)inDefinition1.

Foreachclockx2C,letcxbethelargestintegerwithwhichxiscomparedinanyclockconstraintinanyedge.

Defineanequivalencerelation󰀈onthesetofclockvaluationsasfollows:giventwovaluations󰀃;󰀄:C!R!0;󰀃󰀈󰀄iff:

.forallclocksx2C,eitherintð󰀃ðxÞÞ¼intð󰀄ðxÞÞor󰀃ðxÞ;󰀄ðxÞ>cx;

.forallclocksx2C,󰀃ðxÞisaninteger cxifandonlyif󰀄ðxÞalsosatisfiesthiscondition;.forallclocksx;y2C,if󰀃ðxÞ;󰀄ðxÞ cxand󰀃ðyÞ;󰀄ðyÞ cythenfracð󰀃ðxÞÞ fracððyÞÞimpliesfracð󰀄ðxÞÞ fracð󰀄ðyÞÞ.Thentheequivalenceclassesdefinedby󰀈areknownasclockregions.If󰀃isavaluation,thenregð󰀃Þistheclockregioncontaining󰀃.ItshouldbenotedthatC0󰀃Cifisasetofclocksthen󰀃󰀈󰀄implies½C0¼0󰀆󰀃󰀈½C0¼0󰀆󰀄:

Thefollowinglemmaisfundamentaltothemotiva-tionofthedefinitionoftheregionautomatonG0andofDefinition8of}4.

Lemma1:Letr1;r2beclockregionsandlet󰀃;󰀄2r1.If󰀃þt2r2,forsomet!0,thenthereexistst0!0suchthat󰀄þt02r2.

Proof:Wewillprovethelemmabyinductiononjfregð󰀃þa0Þja02½0;t󰀆gj.Ifthissetisemptythenr1¼r2andthelemmaisobvious.Hencewemayas-sumethatr1¼r2.Thusnecessarily󰀃ðxÞ cxforatleastonex2C.WedefineK¼fx2Cj󰀃ðxÞ cxand󰀃ðxÞ2Zgweconsidertwocases.1.K¼1.Define

t1¼minfint󰀃ðxÞþ1À󰀃ðxÞjx2Cand󰀃ðxÞ cxgandlet

t10Àminfint󰀄ðxÞþ1À󰀄ðxÞjx2Cand󰀄ðxÞ cxg

Then󰀃þt1󰀈󰀄þt10

.

2.K¼1.Chooseanypositive

t1and󰀃ðxÞ cxgÞ

andpositive

t1

0

0.Inbothcaseswehaveregð󰀃Þ¼regð󰀃þtregð󰀃þt10

1Þ¼

Þ.Theresultnowfollowsfromtheinductivehypothesisappliedto󰀃þt10;󰀄þt10

thevaluations

andtÀt1inplaceoftsincejfregð󰀃þt1þa0Þja02½0;tÀt1󰀆gjðs;󰀃!󰀁

1ÞÀ

ðs0;󰀄1Þthenthereexistsaclockvaluation󰀄2with󰀄2󰀈󰀄1andalegaltransition

ðs;󰀃!󰀁2ÞÀ

ðs0;󰀄2ÞProof:ThisfollowsimmediatelyfromLemma1and

thedefinitionofatransitionbetweengeneralizedstatesinatimedautomaton.&

1742M.P.Spathopoulos

Fromthisresultitfollowsthatwecanreplacethesetofclockvaluationsbythesetofclockregions,thusmotivatingthefollowingdefinition.

Definition7:LetGbethetimedautomatondefinedin(1)inDefinition1.WedefineG0tobethefinitestatemachine

G0ðS;ðSÂRÞ;T;S0Â0;SmÂRÞ

whereRisthesetofclockregionsofGand0istheclockregionwhoseuniquevaluationsendsallclockstozero.

WedefinethesetofTtransitionsasfollows.Thereisatransition

ðs;r󰀁

1ÞÀ!ðs0;r2Þ

fortwoclockregionsr1;r2iffthereexistclockvalua-tions󰀃1;󰀃2with󰀃i2riandthereisatransitioninG

betweengeneralizedstates

ðs;󰀃󰀁1ÞÀ!ðs0;󰀃2Þ

G0iscalledtheregionautomaton.

Thefollowingisthemainresultofthissection.The

proof,whichmaybeinferredfromLemma2,isomitted.Theorem1:LetLTbethetimedlanguageacceptedbyG.ThenUntimeðLTÞisthelanguageacceptedbythefi-nitestateautomatonG0.

TheimportanceofG0isthattherearefinitelymanyclockregions(thisfollowsfromDefinition6andthefactthattheclocksetCisfinite),andsoG0alwayshasfinitelymanystates.4.

Anewfiniteautomatonforlanguagesoffinitestrings

ThispartitionofthesetofclockvaluationsValdefinedabovehasthefollowingproperties:

.Therearefinitelymanyclockregions.

.Let󰀃2Valand!2regð󰀃Þ.Then!and󰀃satisfythesamesetoflockconstraints.Ift!0thenthereexistst0!0suchthatregð󰀃þtÞ¼regð!þt0Þ..if0 t1 t2 t3and󰀃2Valandregð󰀃þt1Þ¼regð󰀃þt3Þthen󰀃þt22regð󰀃þt3Þ..if!2regð󰀃ÞandC0󰀃Cisasetofclocksthen½C0¼0󰀆!2reg½C0¼0󰀆󰀃Þ.Givenapartitionsatisfyingtheseproperties,andaclockregionr2R,wedefinesuccðrÞ2R,thesucces-sorregiontor2R,asfollows.Ift!0impliesregð󰀃þtÞ¼regð󰀃ÞthensuccðrÞisundefined.OtherwiseletsuccðrÞ¼regð󰀃þtÞfor󰀃2randt!0chosensuchthat󰀃2=regð󰀃þtÞand0 t0 timplies

thatregð󰀃þt0Þ¼regð󰀃þtÞorregð󰀃þt0Þ¼regð󰀃Þ.Owingtothethirdpropertylistedaboveandthefactthattherearefinitelymanyclockregions,suchavalueoft!0canbefound;andowingtothesecondpropertylisted,thechoiceof󰀃2risirrelevant.WewillwritesuccnðrÞ¼succðsuccnÀ1ðrÞÞforn!1.

Thefollowingdefinitionintroducesthenotionofclosedandnon-closedregionsandwillbeusedinthissectionforthesimplificationoftheuntimingprocedure.Definition8:Letrandr0beclockregions.Wesaythatr0isasuccessorofrifr0containsavaluationwhichisasuccessorofavaluationlyinginr.ByLem-ma1,thisimpliesthateveryelementofrhasasucces-sorinr0.WedefinenextðrÞtobetheminimalsuccessorofr;thatis,theuniquesuccessorofrsuchthatallothersuccessorsofrarealsosuccessorsofnext(r).

Ifany(andhenceevery)valuationinrmapsanyclockx2Ctoaninteger cxand󰀃2r,thennextðrÞisdefinedastheclockregioncontainingthevaluationsf󰀃þ\"j0<\"<1Àfracð󰀃ðyÞÞ:8y2Csuchthat󰀃ðyÞOntheotherhand,ifthevaluationsinrdonotmapanyclockx2Ctoaninteger cx,thenwedefinenextðrÞ¼r.Inotherwords,inthiscase,theclockregionrhasitselfaminimaltimesuccessorregion.Wecallsuchclockregionsnon-closed.Intuitivelyaregionisnon-closedoropenwhentimecanpasswithoutleavingtheregion.

ObservethatnextðnextðrÞÞ¼nextðrÞforallclockregionsr.

Example1:Consideratimedautomatonwithtwostatess1;s2,oneclocksaxandpossibletransition

1À!s1,1Supervisorycontroloftimedautomata

1743

BelowwegiveadifferentprocedurefordefiningtheuntimedlanguageofG.WeprovethattheclockregionsofGwhichareclosedmaybedeletedfromG0,providedcertainmodificationsaremadetothetransitionsofG0.Thus,wedefineanewfiniteautomatonGÃthathasconsiderablefewerstatesthanG0.

Themainresultofthispaperisbasedonthefollow-inglemma.

Lemma3:

1.SupposethatthereisatransitionofthefollowingformbetweenthestatesofG0

ðs;r󰀁

1ÞÀ!ðs0;r2Þ

ð3Þ

Thenthereisalsoatransition

ðs;nextðr1ÞÞÀ

!󰀁

ðs0

;r2Þð4Þ

2.Conversely,theexistenceofthetransitionin(4)

impliestheexistenceofthatin(3).Proof:Wefirstassumethatthetransition(3)existsandprovethat(4)does.Following(3)therearevalua-tions󰀅ifori¼1;2suchthat󰀅12r1,󰀅2¼󰀅1þt;t>0andavaluation󰀄¼½C0¼0󰀆󰀅2whichmeansthat󰀄2r2.Clearlyregð󰀅2Þisasuccessorofr1andsincethetimejumptisstrictlypositiveitisalsoasuccessorofnext(r1).Thisimpliesthatthereisatransitionfromnextðr1Þtor2.Morespecificallylet0<\"r1¼regð󰀅1Þ!nextðregð󰀅1ÞÞ!regð󰀅1þ\"Þ

!regð󰀅2Þ!r2andthisshowsthatthereexistsatransitionfromnextðr1Þtor2.Notethatitmightbethatnextðr1Þ¼regð󰀅1þ\"Þ.Theconversestatementfollowsfromthefactthatanysuccessorofnextðr1Þisalsoasuccessorofr1.

Definition9:DefinethefinitestateautomatonGÃasfollows.GÃisobtainedfromG0bydeletingallstatesðs;rÞsuchthattheregionrisclosed,deletingalltransi-tionsincidenttothesestatesandaddingintransitionsoftheform

ðs;nextðr󰀁

1ÞÞÀ!ðs0;nextðr2ÞÞ

foreverytransitioninG0oftheform

ðs;r󰀁1ÞÀ

!ðs0;r2ÞThefollowingisthemainresultofthissection.Theorem2:

GÃandG0acceptthesamelanguage.

Proof:Letw¼󰀁1ÁÁÁ󰀁nbeacceptedbyG0.This

meansthatthereisasequenceoftransitionsinG0

ðs0ÞÀ󰀁!1

ðs;r󰀁n

0;1;r1ÞÁÁÁðsnÀ1nÀ1ÞÀ!ðsn;rnÞ

forclockregionsriofGandwiths02S0;sn2Sm.

BythedefinitionoftheautomatonGÃ,thereisasequenceoftransitionsinGÃ

ðs󰀁1

0;nextð0ÞÀ!ðs1;nextðr1ÞÞÁÁÁðsnÀ1;nextðrnÀ1ÞÞ

À󰀁!n

ðsn;nextðrnÞÞ

andthuswisacceptedbyGÃ.

Toshowtheconverse,againletw¼󰀁1ÁÁÁ󰀁nandassumethatwisacceptedbyGÃ.BythedefinitionoftheautomatonGÃ,thismeansthatthereisasequenceoftransitionsinGÃ

ðs󰀁1

0;nextð0ÞÀ!ðs1;nextðr1ÞÞÁÁÁðsnÀ1;nextðrnÀ1ÞÞ

À󰀁!n

ðsn;nextðrnÞÞ

ð5Þ

forclockregionsriofGandwiths02S0,sn2Sm.We

nowshowbyinductiononithatforalli nthereisthefollowingsequenceoftransitionsinG0,forclockregionsrj0satisfyingnextðrj0Þ¼nextðrjÞ

ðs󰀁1

0;0ÞÀ!ðs1;r10

ÞÁÁÁðsiÀ1;r󰀁i

i0À1ÞÀ!ðsi;ri0Þ

ð6Þ

Fori¼0thisistrivial.Assume(6)holdsforsomei.

,thereisatransitionðsi;ri00ÞÀ󰀁!ðsiþ1;ri0þ1ÞinG0G

iþ1withnextðri00Þ¼nextðriÞ¼nextðri0Þandnextðri0þ1Þ¼nextðthereisatransitionðsi;nextðri00

riþ1ÞÞÀ󰀁Þi!þ.1

ByLemma3.1ðsiþ1;ri0þ1ÞinG0;henceÀ󰀁byLemma3.2thereisatransition

ðsi!þ1

i;ri0Þðsiþ1;ri0þ1ÞinG0.Thuswehaveprovedtheinductivestep,andhenceprovedthatwisacceptedbyG0.&Remark:Ourresultcanbesummarizedasfollows.Foranyclosedregion,sincetimemusttakeplace(leadingtonext(r))beforeanyfurthertransition,wecanconsiderrandnext(r)tobebisimilar.

Transitionsthatareenabledatexactlytheclosedregionrarecoveredbyregions‘after’r,i.e.forrbeingfx¼1g,theregionf1sab1À!s1,1GÃwillinvolvethetransitionsðsa

1;f0 x<1gÞÀ!ðs1;

f1 x<2gÞ,ðsa

1;f1 x<2gÞÀ!ðs1;f1 x<2gÞ

ðsf0 x<0gÞÀb

1;!ðs2;f1 x<2gÞ

1744M.P.Spathopoulos

5.

Extensionofresultstoacceptorsofinfinitewords

Inthissectionweconstructanotherautomaton,similartoGÃ,inordertosimplifytheuntimingpro-cedureinthecasewherethetimedautomataareregardedasacceptorsof!-words.

Definition10:AtimedBuechiautomaton(Aluranddill1994,Definition3.10)isatuple

H¼ðÆ;S;C;E;S0;SmÞB

wherethesymbolshavethesamemeaningsasin(1)ofDefinition1.ButHisregardedasanacceptoroftimed!-wordsasfollows:letw¼ð󰀁1;t1ÞÁÁÁð󰀁i;tiÞÁÁÁbeatimed!-word.ThenHacceptswprovidedthefollowingtwoconditionshold:

1.Thereðs󰀁isaninfinitesequenceoftransitions

1󰀁i0;0ÞÀ!ðs1;t1ÞÁÁÁðsiÀ1;tiÀ1ÞÀ!ðsi;tiÞÁÁÁthroughHwiths02S0andsi2Smforinfinitelymanyvaluesofi.2.limi!1ti¼1.Thisiscalledtheprogresscondi-tion.Thetimed!-languageacceptedbyHisthendefinedtobethesetoftimed!-wordsacceptedbyH.IfHdefinesthetimed!-languageLTthenwesaythatHacceptstheuntimed!-languageUntime(LT),byanalogywithordinarytimedautomata.

Lemma4:LetÁÁÁð󰀁i;tiÞÁÁÁbeaninfinitetimedwordwhichdefinesapaththroughthesequenceofgeneralizedstatesÁÁÁðsi;󰀃iÞÁÁÁofH.ThenthereisawordÁÁÁð󰀁i;ti0ÞÁÁÁpassingthroughthesamesequenceofstatesofHandsatisfyingtheprogressconditionifandonlyifforeveryclockx2C,wehave󰀃iðxÞ¼0or󰀃iðxÞ>cxforinfinitelymanyvaluesofi.ThisisshowninAlurandDill(1994,Lemma4.13).

Definition11:AtimedMullerautomatonisatupleM¼ðS;S;C;E;S0;FÞautomatonexceptMwhichisidenticaltoaBuechitimedthattheacceptingsetSmisre-placedbyacollectionFofsubsetsofthestatesetS,andinsteadofthecondition(1),tobeacceptedbyMatimedwordmusthaveapaththroughMwhichpassesinfinitelymanytimesthroughthesetsinP󰀃SandfinitelymanytimesthroughthesetsinSÀP,forsomesetP2F.

NextwedefinetheMullerautomatonM0

¼ðÆ;SÂR;T;S0Â0;FÞfollowingsubsetsofthestateMwhereFcontainsthesetSÂR;FcontainsallthosesubsetsofSÂRwhichintersectnon-triviallywithSmÂRandwithallsetsSÂRxforx2C,whereRxisthesetofallclockregionswhosevaluationsmaptheclockxtozeroortoanumbergreaterthancx.

Theorem3:

M0acceptsthesame!-languageasH.

Proof:Let󰀁1ÁÁÁbeanuntimed!-word.ThenbothconditionsofDefinition10aresatisfiedforsometimesequenceÁÁÁtiÁÁÁifandonlyifthereisapathwithlabel󰀁1ÁÁÁthroughM0startingatS0Â0andalsosa-tisfyingthefollowingconditions:thepathpassesinfi-nitelyoftenthroughthestatesetSmÂRanditpassesinfinitelyoftenthroughthesetsSÂRxforallx2C,byLemma4.ThustheresultfollowsimmediatelyfromthedefinitionofM0.

WemimictheconstructionofM0usingamodifiedversionofthedefinitionofnext(r).

WedefineaMullerautomatonMÃobtainedfromM0inasimilarwayinwhichGÃwasobtainedfromG0.&Definition12:TheMullerautomatonMÃisdefined

asMüðÆ;SÃ;TÃ;SÃ0;SÃ

mÞMwhere.thestatesetSÃcontainsallelementsofSÂRof

theform(s,next(r)),whererisanyclockregion,oroftheformðs;rÞ,whererisaclockregionwhosevaluationssendanyclocktozero.

.ThetransitionsetTÃisasfollows:foreverytran-sitionintheregionautomatonG0ðs;r󰀁

oftheform

1ÞÀ!ðs0;r2ÞthereisatransitioninTÃofthe

formðs;secðrÞÀ󰀁

1!ðs0;secðr2ÞÞwheretheclockregionsec(r)isdefinedtobenext(r)unlessrmapsanyclocktozero,inwhichcasesecðrÞ¼r..SÃ0¼S0Â0isthesetofinitialstates..Theacceptingstatesetsarethosewhichintersectnon-triviallywithSmÂsecðRÞandwithallsetsSÂsecðRxÞforallx2C.ThusMÑliesbetween’G0andGÃinthesensethatitisobtainedfromG0byeliminatingsomeofthenon-closedclockregions.Theorem4:

HandMÃacceptthesamelanguage.

Proof:SincetheclockregionsecðrÞisalwayseithernext(r)orr,Lemma3stillholdswithnext(r)replacedbysecðrÞ.Theresultthereforefollowsfromanargu-mentsimilartothatinTheorem2.&6.Upperboundsfornumbersofclockregions

InAlurandDill(1994,Lemma4.5)anupperboundof

jCj!2jCjÀ1

Y

ð2cxþ2Þ

x2C

isgivenforthenumberofclockregionsofthetimedautomatonG.Thenumberofnon-closedclockregions

Supervisorycontroloftimedautomata

1745

forthefinitestringcasecansimilarlybeshowntobeboundedby

jCj!2jCjÀ1Y

ðcxþ1Þ

x2C

Toprovethis,observethattheclockregionofGis

uniquelyspecifiedbythefollowing:

(a)foreachclockx,oneclockconstraintfromthe

setfx¼cjc¼0;...cxg[fx2ðcÀ1;cÞjc¼1;...cxg

[fx>cxg(b)anorderingoftheintegersf1;2;...;jCjgtoindi-cateanorderingofthenumbersfrac(x)forx2C,

(c)foreachintegern2f2;3;...jCjg,whether

fracðxÞ>fracðyÞorfracðxÞ¼fracðyÞ,wherexandyarethenthandnÀ1thclocksintheorder-inggivenin(b).

ThereQarejCj!choicesin(b)and2

jCjÀ1

in(c).Case(a)givesclosedregionsx2Cð2cxþ2Þchoicesforallregions,butifonlyneedtobelisted,thenQthefirstsetgivenin(a)isirrelevant,givingx2Cðcxþ1Þ

choices.Multiplyingtheresultsgivestheupperboundsclaimedabove.ThusreplacingG0byGÃreducestheupperboundonthenumberofstatesbyafactorof2jCj.

WeconsiderthetimedautomatonexamplewithtwoclocksgiveninAlurandDill(1994,Example4.4).Theregionautomatoninvolves28clockregions,ofwhichonly10areclosed.Thereforeinthenewautomatonwemaydeletetheclosedregionsorconsiderthemtogetherwiththeassociatednon-closedregions.Infigure1,theassociatednon-closedregionsjust‘after’theclosedregionsareshownusingarrows.The10(non-closed)regionsneededforthenewfiniteautomatonareillu-stratedinfigure1usingboldnumbers.Notethatonly2and5arelinesegments.Thederivedupperboundsareratherconservative.Thus,inpracticeandforspecificproblemsthenon-closedregionsaremuchfewerthan

theclosedones.Thisresultsinderivingsignificantlyfewerextendedstatesforthenewfiniteautomaton.Itisnotdifficulttoconcludethatthenumberofnon-closedclockregionsintheinfinitestringcaseisbounded

byjCj!2jCjÀ1Qx2Cðcxþ2Þ.ThusreplacingG0byMÃ

reducesagaintheupperboundonthenumberofstatesbyafactorofalmost2jCj.Fortheaboveexampleswemustnowincludeallclosedregionsassociatedwiththeclockaxisxandyandillustratedinfigure1as1i–9i.ThisallowsthevaluationstoberesetinfinitelymanytimestozerorequiredbyLemma4.Now19clockregionsareneeded.

7.Onsupervisorycontrolfordensereal-timediscrete-eventsystemsInthissectiontheapplicationofthederivedsimpli-fiedtechniquetothesupervisorycontroldesignanditseffectinobtainingtheleastrestrictivecontrolledbehav-iouraregiven.

ForsimplicityweconsiderthetimedautomatonA¼ðS;s0;Æ;E;CÞsimilartotheonedefinedin(1)butwithoutaccepting(marked)states.Inthissection,weareonlyinterestedintimedautomataasacceptorsoflanguagesoffinitetimedwords.WeassumethatAistimedeterministic;thatis,itsatisfiesthefollowingcon-dition;besideshavingonlyoneinitialstate,foranysodefinedextendedstatedðs;󰀃Þ,where󰀃:C!R!0aretheclockvaluations,andforanyevent󰀁2Æthereisamaxi-mumofoneedgeðs;s0;󰀁;󰀂;C0ÞinAsuchthat󰀃satisfiestheclockconstraint󰀂.Thisimpliesthatforanytimedwordð󰀁1;t1ÞÁÁÁð󰀁n;tnÞthereisamaximumofonepathstartingattheinitialstates0overthetimedwordð󰀁1;t1ÞÁÁÁð󰀁n;tnÞthroughA.

WedenoteOthesetofextendedstatesofAandasinthecaseofafinitestateautomaton,wepartitiontheeventalphabetintocontrollableanduncontrollableevents:ƼÆc[Æu.ThecontrolfunctionforAisdefinedas󰀆:OÂÆ!f0;1gsatisfying󰀆ðe;󰀁Þ¼1if󰀁2Æuandeisanyextendedstate.WecallthepairðA;󰀆Þacontrolledtimedautomaton.WedefinethetimedlanguageLtimedðA;󰀆Þtobethesetofalltimedwordsð󰀁1;t1ÞÁÁÁð󰀁n;tnÞsuchthatthereisapath

ðsð󰀁1;t1Þ

ð󰀁n;tnÞ

0;0ÞÀ!ðs1;󰀃1ÞÁÁÁÀ!ðsn;󰀃nÞ

wheretheclockvaluation0sendsallclockstozero,

satisfyingthecondition󰀆ðsiÀ1;󰀃iÀ1þti;󰀁iÞ¼1foralli.Ifsuchapathexistswesaythattheextendedstatesðsi;󰀃iÞareaccessibleunder󰀆.

LetF(forforbidden)beasetofextendedstates(possiblyinfinite,sincethenumberofvaluationsareinfinite)ofA.Thesupervisorycontrolproblemthatwearedealingisthefollowing(forbiddencontrolproblem):

1746M.P.Spathopoulos

Findthecontrolfunctionmsuchthateveryelementof

FisinaccessibleundermandsuchthatLtimedðA;󰀆Þismaximalforallsuchcontrolfunctionsm.

Forsimplicitythenon-blockingconditionisnotincludedassumingthatthelanguagesareclosed.TheinterestedreaderisreferredtoSpathopoulos(2003)forthenon-blockingforbiddencontrolproblem.

Ithasbeenshown(HoffmanandWong-Toi1992,LaurenceandSpathopoulos1988)thatthiscanbesolvedconsideringthecontrolproblemforthefinitestateautomatonUntime(A)(asdefinedinthefollowingdefinition)providedthattheforbiddenstatesetFsatis-fiesacertainconditionstatedinTheorem5.

Definition13:LetRbethesetofclockregionsofA.ThenthefinitestateautomatonUntime(A)hasstatesetSÂR,initialstateðs0;0Þ,eventalphabetS[f󰀅gandtransitionsðs;rÞÀ󰀅

oftwokinds.Therearetransitions

!ðs;succðrÞÞfromeverystateðs;rÞwheresucc(r)isthesuccessorregiontorandtherearetran-sitionsðs;rÞÀ󰀁

!ðs0;½C0¼0󰀆ðr0ÞÞforeveryedgeðs;s0;󰀁;󰀂;C0ÞinAsuchthattheelementsoftheclockregionrsatisfytheclockconstraint󰀂.

Remark:TheautomatonUntime(A)issimilartoG0wheretheevent󰀅thatmodelsthe‘timepassage’hasbeenaddedinthealphabet.Basicallyweusethetime-abstracttransitionsystemforwhichthesetofeventsisÆ[f󰀅g.Thetimepassageistreatedinthispaperasanuncontrollableevent.ThereaderisreferredtoSpathopoulous(2003)wherethenotionofurgencyisintroducedandthetimepassagemaybedefinedasacontrollableeventaswell.

ItcanbeshownthatAtimedeterministicimpliesUntime(A)deterministic.Thiswasthereasonforrequir-ingAtobetimedeterministic.

Itisusefultomakethefollowingdefinition:ifðs;󰀃Þisanextendedstatethenlet󰀇ðs;󰀃Þ¼ðs;regð󰀃ÞÞ.Lemma5:

(1)Ifthereisalegaltransitionðs;󰀃ÞÀ󰀁

!ðs0;󰀃0ÞinA

withtimejumptthenthereisapath

ðs;regð󰀃ÞÞÀ!󰀅

ðs;succðregð󰀃ÞÞÞÀ!󰀅ÁÁÁÀ!

󰀅

ðs;succnðregð󰀃ÞÞÞÀ!󰀁

ðs0;regð󰀃0ÞÞ

throughUntime(A)forsuccnðregð󰀃ÞÞ¼regð󰀃þtÞ:

(2)Ifthereisatransitionðs;rÞÀ󰀁

!ðs0;r0Þin

Untime(A)with󰀁2Æand󰀃2rÃforsome󰀃2Val;rÃ2RandsuccnðrÃÞ¼rthenthereistransitionðs;󰀃ÞÀ󰀁

a

!ðs0;󰀃0Þforsome󰀃02r0.Proof:

FollowsfromDefinition13andLemma2.&

Givenatimedwordð󰀁1;t1ÞÁÁÁð󰀁n;tnÞpathÁÁÁðs󰀁defininga

i

i;󰀃iÞÀ!ðsi0þ1;󰀃i0þ1ÞÁÁÁthroughA,theprojec-tionofthiswordisdefinedtobethelabelofthecorre-spondingpathinUntime(A)givenbycombiningthepath-segmentsoftheformgiveninLemma5(1).ThefollowingtheoremstatesthatthesupervisorycontrolproblemfortimedautomatacanbesolvedusingtheautomatonUntime(A).

Theorem5:Let󰀆beacontrolfunctionforthetimedautomatonA,andletFbeasetofextendedstatesofAsuchthatifðs;󰀃Þ2Fand󰀃02regð󰀃Þthenðs;󰀃0Þ2F(orequivalently,󰀇À1ð󰀇ðFÞÞ¼FÞandlet󰀈:SÂRÂðÆ[f󰀅gÞ!f0;1gbeacontrolfunctionforthefinitestateautomatonUntime(A),withthe‘timepas-sage’event󰀅classedasuncontrollable.Definethecon-trolfunction󰀆:OÂÆ!f0;1gas󰀆ðs;󰀃;󰀁Þ¼󰀈ðs;regð󰀃Þ;󰀁Þ.Assumethatthestates󰀇ðFÞareinacces-siblein(Untime(A),󰀈);thentheextendedstatesinFareinaccessibleinðA;󰀈Þ;furthermore,ifL(Un-time)(A),󰀈)ismaximalwiththisproperty,thensoisLtimed(A,󰀆).

Proof:Supposethatanextendedstateðsn;󰀃nÞisac-cessibleinðA;󰀆Þ;thenthereisapath

ðsð󰀁1;t1Þ

ð󰀁n;tnÞ

0;0ÞÀ!ðs1;󰀃1ÞÁÁÁÀ!ðsn;󰀃nÞ

throughAsatisfying󰀆ðsiÀ1;󰀃iÀ1þti;󰀁iÞ¼1foralli.

ThusfrommultipleapplicationsofLemma5(1)thereisapath

ðs󰀅󰀅0;0ÞÁÁÁðsiÀ1;regð󰀃iÀ1ÞÞÀ!ðsiÀ1;succðregð󰀃iÀ1ÞÞÞÀ!ÁÁÁÀ!󰀅ðsiÀ1;succniÀ1ðregð󰀃󰀁iiÀ1ÞÞÞÀ!ðsi;regð󰀃iÞÞÁÁÁðsn;regð󰀃nÞÞthroughUntime(A)forsuccniðregð󰀃iÞÞ¼regð󰀃iþtiþ1Þwith󰀈ðsiÀ1;regð󰀃iÀ1þtiÞ;󰀁iÞ¼1foralli.Thusðsn;regð󰀃nÞÞ¼󰀇ðsn;󰀃nÞisaccessiblein(Untime(A),󰀈)andthisprovesthefirstpartofthetheorem.

NowassumethatthetimedlanguageLtimed(A,󰀆)isnotmaximalwiththisproperty:thatis,thatthereisacontrolfunction󰀆ÃsuchthatLtimedðA;󰀆ÃÞ󰀊LtimedðA;󰀆Þ,thereisatimedwordð󰀁1;t1ÞÁÁÁð󰀁n;tnÞlyinginLtimedðA;󰀆ÃÞÀLtimedðA;󰀆ÞandtheextendedstatesinFarealsoinaccessibleinðA;󰀆ÃÞ.Let

ðsð󰀁1;t1Þ

ð󰀁n;tnÞ

0;0ÞÀ!ðs1;󰀃1ÞÁÁÁÀ!ðsn;󰀃nÞ

bethepathinAdefinedbythetimedword

ð󰀁1;t1ÞÁÁÁð󰀁n;tnÞstartingatðs0;0Þ.Foralli n,theredoesnotexistapathoveranywordinÆÃustartingatðsi;󰀃iÞandendingatanelementofF.Furthermore,foratleastonevalueofi󰀈ðsi;regð󰀃iþtiþ1Þ;󰀁iþ1Þ¼󰀆ðsi;󰀃iþtiþ1;󰀁iþ1Þ¼0(sinceð󰀁1;t1ÞÁÁÁð󰀁n;tnÞ2=LtimedðA;󰀆Þ)andsothepro-jectionofthetimedwordð󰀁1;t1ÞÁÁÁð󰀁n;tnÞonto

Supervisorycontroloftimedautomata

1747

Untime(A)startingatðsÃ0;0ÞdoesnotlieinL(UntimeðAÞ;󰀈).Let󰀈:SÂRÂÆ[f󰀅g!f0;1gbethecontrolfunctionforUntime(A)definedasfollows.Ifastateðs;rÞisaccessibleinUntime(A),󰀈)then󰀈Ãðs;r0;󰀁Þ¼󰀈ðs;r0;󰀁Þforanytimesuccessorr0ofr,unlessðs;r0;󰀁Þ¼ðsi;reg;ð󰀃iþtiþ1Þ;󰀁iþ1ÞforsomeiItfollowsbyinductiononwordlengththatL(Untime(A),󰀈Þ󰀃LðUntimeAÞ;󰀈ÃÞ;furthermore,theprojectionofthetimedwordð󰀁Ã1;t1ÞÁÁÁð󰀁n;tnÞliesinL(Untime(A),󰀈),butnotinL(Untime(A),󰀈),sotheinclusionisstrict.

OwingtothemaximalityconditiononL(Untime(A),󰀈),anelementof󰀇ðFÞisaccessiblein(Untime(A),󰀈Ã).ThereforethereisapathpinUntime(A)fromðs0;0Þtoanelementof󰀇ðFÞwhichispermittedby󰀈Ã,butnot,ofcourse,by󰀈.Thuspmustpassthroughatransition

ðs󰀁iþ1

i;regð󰀃iþtiþ1ÞÞÀ!ðsiþ1;regð󰀃iþ1ÞÞ

forsomeionesarepermittedby󰀈.Letp0beafinalsegmentofp,startingatthestateðsiþ1;regð󰀃iþ1ÞÞforsomei󰀈ðs;r;󰀁Þ¼󰀈Ãðs;r;󰀁Þ¼1foralledgesðs;rÞÀ󰀁

!ðs0;r0Þthroughwhichp0passes.Wewillshowthat󰀁2Æu[f󰀅gforallsuchedges.Assumethatnotthecaseandletðs;rÞÀ󰀁

thisis

!ðs0;r00Þbethelastedgeinpforwhich󰀁2Æc.Thedefinitionof󰀈Ãimpliesthatðs;rÞisaccessiblein(Untime(A),󰀈),whichleadstoacontradictionsincetheendpointofp,whichliesin󰀇ðFÞ,wouldbeaccessiblein(Untime(A),󰀈).Wecanliftp0toapathq,usingLemma5(2)repeatedly,startingatðsiþ1;󰀃iþ1Þandendingatanextendedstatef2󰀇À1󰀇ðFÞ¼F.ThepathqislegalinðA;󰀆ÃÞ,sinceallitseventslieinSu.However,theextendedstateðsiþ1;󰀃iþ1ÞisaccessibleinðA;󰀆ÃÞ;thustheforbiddenstatefisaccessibleinðA;󰀆ÃÞ,contrarytohypotheses.&Remark:FollowingTheorem5,whenthetimein-creasesstrictlymonotonically,theautomatonUntime(A)canbereplacedbythesimplifiedautoma-tonUntime(AÃ)thatissimilartoGÃwheretheevent󰀅hasbeenaddedtoitsalphabet.

Example3:Considerasimpletimedautomatongiveninfigure2ainvolvingonlytwostates,onecontrollabletransitionandinitialstates.Assumethattheforbid-denstateisthestateðs0;x¼1Þ.Inordertosolvethecontrolproblem,theUntime(A)giveninfigure2b(󰀅-transitionsareshownaswell)isderivedandclearlyall

transitionsleadingtothisstateshouldbedisabled.IftimeisstrictlypositivethesimplifiedautomatonUntimeðAÃÞ,giveninfigure2b,isderived.Thenclearlybothextendedstatesðs0;x¼1Þandðs0;11748M.P.Spathopoulos

isstrictlypositiveanditisnaturaltoexpectthatthecontrolledbehaviourshouldbecomemoreconserva-tive.Inotherwords,whenthetimeisnotallowedtobezero,theautomatonwouldnotbepermittedtovisitnon-closedstatesassociatedwithforbiddenclosedstates.Thisisduetothefactthat,whenthesimplifiedautomatonisused,ifnextðxÞ¼nextðyÞthen,whenðs;xÞisforbidden,ðs;yÞalsobecomesforbiddensincetherecanbenodifferencebetweenextendedstateswiththesamenext-value.

Fromtheaboveitfollowsthatwhenthetimejumpisstrictlypositivethecontrolledbehaviourismoreconser-vative.Thefollowingcorollarygivesaconditionunderwhichthecontrolledbehaviouristheleastrestrictiveonederivedusingtheorem5.

Corollary1:TheforbiddenstatecontrolproblemusingthesimplifieduntimingproceduregivestheleastrestrictivecontrolledbehaviourasstatedbyTheorem5undertheconditionthattheforbiddenstatesarenotclosedregions.InotherwordstheatomicpredicatesspecifyingtheforbiddenextendedstatesshouldbeoftheformxÃcforaclockx2CwhereÃisoneof ,<,!or>(butnot¼).

8.

Conclusions

GivenatimedautomatonG,wehavedefinedanewfinitestateautomatonGÃthatacceptsthesameuntimedlanguageasGandhassignificantlyfewerstatesthantheregionautomatonG0.GivenatimedBuechiautomaton,wehaveprovedasimilarresult.

Next,thisresultisusedinconnectionwiththefor-biddenstatecontrolproblemfortimeddiscreteeventsystems.Westudythisproblemandshowthatthesim-plifieduntimingconstructionleadstoasimplifiedsuper-visorycontroldesignforrealtimediscrete-eventsystemsmodelledbytimedautomata.Conditionsunderwhichtheleastrestrictivesolutionisobtainedaregiven.

Duetoitscomplexity,theuntimingprocedurefordensetimeautomataresultsinalargenumberofregionsfortheuntimedautomaton.Theefficiencyoftheinvolvedsupervisorydesigndependsonthenumberofregionsoftheuntimedautomaton.Therefore,simplifi-cationsandcomputationalapproximationsfortimedautomataareofimportance.Forthesimplifieduntimingprocedureaddressedhere,thenumberofregionsinthegraphstilldependexponentiallyonthenumberofclocks.Inpractice,asexplainedin}6,thereductionofregionsissignificant.InLaurenceandSpathopoulos(1998),thesimplifiedprocedurereducestheexponentialnumberofregions.However,itworksonlyforaspecialcasethatessentiallycorrespondstothecasewherethetimeisdiscretized.FurtherworkwithreferencetothenotionofurgencyintroducedinSpathopoulos(2003)willbereportedelsewhere.

References

Alur,R.,andDill,D.,1994,Atheoryoftimedautomata.TheoreticalComputerScience,126,183–235.

Asarin,E.,Maler,O.,Pneuli,A.,andSifakis,J.,1998,Controllersynthesisfortimedautomata.ProceedingsoftheIFACSymposiumonSystemStructureandControl(Elsevier),pp.469–474.

Brandin,B.A.,Wonham,W.M.,1994,Supervisorycontroloftimeddiscrete-eventsystems.IEEETransactionsonAutomaticControl,39,329–342.

Hoffmann,G.,andWong-Toi,H.,1992,TheControlofDenseReal-timeDiscreteEventSystems,StanfordUniversityCSReport,No.STAN-CS-92-1411.

Laurence,M.R.,andSpathopoulos,M.P.,1998,Forbiddenstateproblemsintimedautomata.Proceedingsofthe4thInternationalWorkshoponDiscrete-EventSystems(WODES98),Cagliari,Italy,August,pp.15–23.

Ramadge,P.J.,andWonham,W.M.,1987,Supervisorycontrolofaclassofdiscreteeventprocesses,SIAMJournalofControlandOptimization,25,206–230.

Spathopoulos,M.P.,2003,Onsupervisorycontrolfortimedautomatausingurgency.Proceedingsofthe9thIEEEInter-nationalConferenceonMethodsandMethodsinAutomationandRobotics,Miedzyzdroje,Poland,August,pp.863–869.