e-journal

Symbolic Representation and Computation of Timed Discrete-Event Systems

---

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.
Index Terms—Binary decision diagrams (BDD), extended finite automata (EFA), supervisory control theory (SCT), timed discreteevent systems (TDES).

---

Ketersediaan

Tidak ada salinan data

Informasi Detail

Judul Seri

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING

No. Panggil

-

Penerbit

New York : IEEE., 2014

Deskripsi Fisik

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, VOL. 11, NO. 1, JANUARY 2014

Bahasa

English

ISBN/ISSN

1545-5955

Klasifikasi

-

Tipe Isi

-

Tipe Media

-

Tipe Pembawa

-

Edisi

VOL. 11, NO. 1, JANUARY 2014

Subjek

TEKNIK

Info Detail Spesifik

-

Pernyataan Tanggungjawab

Yuli/Agus

Versi lain/terkait

Lampiran Berkas

Komentar

---

Anda harus masuk sebelum memberikan komentar