Supervisory Control Synthesis of Timed Automata Using Forcible Events

TL;DR

This paper introduces a direct supervisory control synthesis method for timed automata that avoids state space explosion by not relying on finite automaton abstraction, enabling more efficient control of real-time systems.

Contribution

It presents a novel synthesis algorithm for timed automata that directly incorporates forcible events, ensuring controllability and maximal permissiveness without state space abstraction.

Findings

The algorithm guarantees a controllable and maximally permissive supervisor.

The supervisor is a timed automaton that ensures nonblocking and safe control.

Avoids exponential state space growth typical of abstraction methods.

Abstract

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.