State feedback control of real-time discrete event systems with infinite states

Abstract

In this paper, we study a state feedback supervisory control of timed discrete event systems (TDESs) with infinite number of states modelled as timed automata. To this end, we represent a timed automaton with infinite number of untimed states (called locations) by a finite set of conditional assignment statements. Predicates and predicate transformers are employed to finitely represent the behaviour and specification of a TDES with infinite number of locations. In addition, the notion of clock regions in timed automata is used to identify the reachable states of a TDES with an infinite time space. For a real-time specification described as a predicate, we present the controllability condition for the existence of a state feedback supervisor that restricts the behaviour of the controlled TDES within the specification.

Keywords:

• real-time discrete event systems
• timed automata
• infinite states
• state feedback control
• predicates

Additional information

Funding

This research was supported by Basic Science Research Program through the National Research Foundation of Korea (NRF) funded by the Ministry of Education, Science and Technology [grant number 2011-0007830]; the National Research Foundation of Korea (NRF) grants funded by the Korea Government, the Ministry of Science, ICT & Future Planning [grant number 2014R1A2A1A10052404], [grant number 2013M3A9A7046303]; the KUSTAR-KAIST Institute, Korea, under the R&D program supervised by the KAIST.