CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Symbolic Representation and Computation of Timed Discrete-Event Systems

Sajed Miremadi (Institutionen för signaler och system, Automation) ; Zhennan Fei (Institutionen för signaler och system, Automation) ; Knut Åkesson (Institutionen för signaler och system, Automation) ; Bengt Lennartson (Institutionen för signaler och system, Automation)
Ieee Transactions on Automation Science and Engineering (1545-5955). Vol. 11 (2014), 1, p. 6-19.
[Artikel, refereegranskad vetenskaplig]

In this paper, we symbolically represent timed discrete-event systems (TDES), which can be used to efficiently compute the supervisor in the supervisory control theory context. We model a TDES based on timed extended finite automata (TEFAs): an augmentation of extended finite automata (EFAs) by incorporating discrete time into the model. EFAs are ordinary automata extended with discrete variables, where conditional expressions and update functions can be attached to the transitions. The symbolic computations are based on binary decision diagrams (BDDs). We show how TEFAs can be represented by BDDs. The main feature of this approach is that the BDD-based fixed point computations are not based on tick models that have been commonly used in this area, leading to better performance in many cases. The approach has been implemented and applied to a simple case study and several large-scale benchmarks. Note to Practitioners-In today's industry, the control functions are implemented to a great extent manually by designing a candidate and verifying it towards different properties to ensure that the control function is satisfactory. Designing a control function manually makes it a tedious, error-prone and time consuming process. Another way is to do this process automatically, referred to as the synthesis method. In the synthesis method, the designers model the system's behavior and the desired properties and feed them to an algorithm that can automatically generate the control function. Supervisory Control Theory (SCT) provides a powerful framework for automatically synthesizing safe and flexible control functions, referred to as supervisors, that restrict the system only when it necessary. For large-scale systems, synthesis typically suffers of from the state space explosion problem, that is the required memory to represent the states of the system is more than the available memory. To handle real-time systems, in this paper, we also incorporate time in the theory and show how the supervisor can be efficiently computed for large-scale systems.

Nyckelord: Binary decision diagrams (BDD), extended finite automata (EFA), supervisory control theory (SCT), REAL-TIME, SUPERVISORY CONTROL, AUTOMATA, DESIGN

Denna post skapades 2014-02-06. Senast ändrad 2015-01-16.
CPL Pubid: 193543


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för signaler och system, Automation (2005-2017)


Data- och informationsvetenskap
Datavetenskap (datalogi)
Elektroteknik och elektronik

Chalmers infrastruktur