Predicates and predicate transformers for supervis

PredicatesandPredicateTransformersforSupervisoryControlofDiscreteEventDynamicalSystems1RatneshKumarDepartmentofElectricalEngineeringUniversityofKentuckyLexington,KY40506-0046VijayGargDepartmentofElectricalandComputerEngineeringUniversityofTexasatAustinAustin,TX78712-1084StevenI.MarcusDepartmentofEEandSystemResearchCenterUniversityofMarylandCollegePark,MD20742February2,19951ThisresearchwassupportedinpartbytheCenterforRoboticsandManufacturing,UniversityofKentucky,inpartbytheNationalScienceFoundationunderGrantNSFD-CDR-8803012andNSF-CCR-9110605,inpartbytheAirForceOceofScienticResearch(AFOSR)underContractF49620-92-J-0045,inpartbyaUniversityResearchInstituteGrantandinpartbyaBureauofEngineeringResearchGrant.AbstractMostdiscreteeventsystemmodelsarebasedondeningthealphabetsetorthesetofeventsasafundamentalconcept.Inthispaper,wetakeanalternativeviewoftreatingthestatespaceasthefundamentalconcept.Weapproachtheproblemofcontrollingdiscreteeventsystemsbyusingpredicatesandpredicatetransformers.Predicateshavetheadvantagethattheycanconciselycharacterizeaninnitestatespace.Thenotionofcontrollabilityofapredicateisdened,andthesupervisorypredicatecontrolproblemintroducedinthispaperissolved.Aclosedformexpressionfortheweakestcontrollablepredicateisobtained.Theproblemofcontrollingdiscreteeventsystemsunderincompletestateobservationisalsoconsideredandobservabilityofpredicatesisdened.Techniquesforndingextremalsolutionsofbooleanequationsisusedtoderiveminimallyrestrictivesupervisors.1IntroductionManydiscreteeventsystemmodels[24,23,25,9,11,12]arebasedondeningthealphabetsetorthesetofeventsasafundamentalconcept.Thelanguageofadeterministicsystemcharacterizesitsbehavior,andtwosystemsareconsideredequivalentiftheyhavethesamealphabetandlanguage[9].Inthispaper,wetakeanalternativeviewoftreatingthestatespaceasthefundamentalconcept.Problemstreatedin[22,19,3,1,18,14,7]arealsoformalizedwithasimilarpointofview.Weapproachtheproblemofcontrollingthebehaviorofadiscreteeventsystemdescribedintermsofitsstatetrajectoriesbyusingpredicatesandpredicatetransformers.Predicateshavetheadvantagethattheycanconciselycharacterizeaninnitestatespace.Petrinetbasedmodelshavealsobeenusedfordescribinginnitestatediscreteeventdynamicalsystems[26,17].Thenotionsoftwotypesofpredicatetransformers,namelystrongestpost-condition(sp)andweakestliberalprecondition(wlp)[5,6,8]areveryusefulincharacterizingthedynamicsofdiscreteeventdynamicalsystems.Inthispaper,westudythesystemdy-namicsintheframeworkofthesepredicatetransformers.Weusethenotionofdualityofpredicatetransformersandshowthatspandwlparedualsofeachother.Thusoneofthepredicatetransformers-eithersporwlp-canbetreatedasfundamentalandtheotherasaderivednotion.Inthispaperwetreatsptobethefundamentalpredicatetransformer,asitdescribestheforwardevolutionofthesystembehavior,anddevelopthesupervisorycontroltheoryusingit.Wedescribeafewbasicproperties-strictness,monotonicity,disjunctivity,conjunctivityetc.-ofpredicatetransformers.spisastrict,monotoneanddisjunctivepredicatetrans-former,whileitsdualwlpisastrict,monotoneandconjunctive.Oneormoreofthesepropertiesofspandwlpareusedtoobtainalltheresultsinthispaper.Itisknown[6]thatapredicateequationinthevariablepredicateQofthetypeQ:f(Q)g(Q)hasuniqueextremalsolutions,providedthepredicatetransformersf;gsatisfycertainbasicproperties.Weusetheextremalsolutionsofsuchpredicateequationstodemonstratetheexistenceanduniquenessofminimallyrestrictive[23,2]supervisors.Weintroducethesupervisorypredicatecontrolproblemastheproblemofsynthesizingasupervisorforagivensystemsothatthestatetrajectoriesofthesystemremainconnedtoasetof\legalstates,andalsovisitallthestatesinthesetoflegalstates.Thusthesetoflegalpredicatecorrespondstotheweakestpredicatethatremainsinvariantundercontrol.Aspecialcaseofthisproblemwherethelatterconstraintisrelaxedwasconsideredin[22].Thenotionofcontrollabilityisdenedanditisshownthatitservesasanecessaryandsucientconditionfortheexistenceofasupervisorthatsolvesthesupervisorypredicatecontrolproblem.Adierentdenitionofcontrollabilityispresentedin[19],whichcanbeshowntobeequivalenttoourdenition.Ourdenitionofcontrollabilityispurelyintermsofthepredicatetransformersp,whichresultsinamorecompactdenition,simplicityoftheproofs(asdemonstratedbytheproofofTheorem4.5)aswellasthesynthesistechniquesofthesupervisors.Inthispaper,wealsoaddresstheproblemofsynthesizingsupervisorsforthecasewhentherequiredpredicateisnotcontrollable.Thisproblemisquiteimportantandisnotad-dressedin[19,22].Weshowthatifthegiven\legalpredicateisnotcontrollable,thentheminimallyrestrictivesupervisorcanbeconstructedsothatthestatetrajectoriesofthe1controlledsystemremainconnedtoandalsovisitallthestatesinthesetofstateswheretheweakestcontrollablelegalpredicateholds.Weprovethattheweakestcontrollablepred-icatestrongerthantherequiredpredicateexistsandpresentanalgorithmforcomputingit.Thisalgorithmisthenusedforconstructingtheminimallyrestrictivesupervisor.Thusourworkextendstheearlierworksonsupervisorypredicatecontrol[22,19].In[22]amethodispresentedforcomp