Supervisory Control Synthesis of Timed Automata Using Forcible Events

Aida Rashidinejad (Corresponding author), Michel A. Reniers, Martin Fabian

Research output: Contribution to journalArticleAcademic

35 Downloads (Pure)


Considering real-valued clocks in timed automata (TA) makes it a practical modeling framework for discrete-event systems. However, the infinite state space brings challenges to the control of TA. To synthesize a supervisor for TA using the conventional supervisory control theory, existing methods abstract TA to finite automata (FA). For many applications, the abstraction of real-time values results in an explosion in the state space of FA. This paper presents a supervisory control synthesis algorithm directly applicable to the TA without any abstraction. The plant is given as a TA with a set of uncontrollable events and a set of forcible events. Forcible events can preempt the passage of time when needed. The synthesis algorithm works by iteratively strengthening the guards of edges labeled by controllable events and invariants of locations where the progression of time can be preempted by forcible events. The synthesized supervisor, which is also a TA, is guaranteed to be controllable, maximally permissive, and results in a nonblocking and safe supervised plant.
Original languageEnglish
Article number2102.09338
Number of pages16
Publication statusPublished - 18 Feb 2021


Dive into the research topics of 'Supervisory Control Synthesis of Timed Automata Using Forcible Events'. Together they form a unique fingerprint.

Cite this