| 1. |
- Goorden, Martijn, et al.
(författare)
-
Compositional coordinator synthesis of extended finite automata
- 2021
-
Ingår i: Discrete Event Dynamic Systems: Theory and Applications. - : Springer Science and Business Media LLC. - 0924-6703 .- 1573-7594. ; 31:3, s. 317-348
-
Tidskriftsartikel (refereegranskat)abstract
- To avoid the state-space explosion problem, a set of supervisors may be synthesized using divide and conquer strategies, like modular or multilevel synthesis. Unfortunately, these supervisors may be conflicting, meaning that even though they are individually non-blocking, they are together blocking. Abstraction-based compositional nonblocking verification of extended finite automata provides means to verify whether a set of models is nonblocking. In case of a blocking system, a coordinator can be synthesized to resolve the blocking. This paper presents a framework for compositional coordinator synthesis for discrete-event systems modeled as extended finite automata. The framework allows for synthesis of a coordinator on the abstracted system in case compositional verification identifies the system to be blocking. As the abstracted system may use notions not present in the original model, like renamed events, the synthesized coordinator is refined such that it will be nonblocking, controllable, and maximally permissive for the original system. For each abstraction, it is shown how this refinement can be performed. It turns out that for the presented set of abstractions the coordinator refinement is straightforward.
|
|
| 2. |
- Goorden, Martijn, et al.
(författare)
-
Model properties for efficient synthesis of nonblocking modular supervisors
- 2021
-
Ingår i: Control Engineering Practice. - : Elsevier BV. - 0967-0661. ; 112
-
Tidskriftsartikel (refereegranskat)abstract
- Supervisory control theory provides means to synthesize supervisors for systems with discrete-event behavior from models of the uncontrolled plant and of the control requirements. The applicability of supervisory control theory often fails due to a lack of scalability of the algorithms. This paper proposes a format for the requirements and a method to ensure that the crucial properties of controllability and nonblockingness directly hold, thus avoiding the most computationally expensive parts of synthesis. The method consists of creating a control problem dependency graph and verifying whether it is acyclic. Vertices of the graph are modular plant components, and edges are derived from the requirements. In case of a cyclic graph, potential blocking issues can be localized, so that the original control problem can be reduced to only synthesizing supervisors for smaller partial control problems. The strength of the method is illustrated on two case studies: a production line and a roadway tunnel.
|
|
| 3. |
- Rashidinejad, Aida, et al.
(författare)
-
Non-blocking Supervisory Control of Timed Automata using Forcible Events
- 2020
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 53:4, s. 356-362
-
Konferensbidrag (refereegranskat)abstract
- Real-valued clocks make the state space of timed automata (TA) infinite. Conventional supervisory control synthesis techniques are only applicable to finite automata (FA). Therefore, to synthesize a supervisor for TA using conventional techniques, an abstraction of TA to FA is required. For many applications, the abstraction of real-time values results in an explosion in the finite state space. This paper presents a supervisory control synthesis technique applied directly to TA without any abstraction. The plant is given as a TA with a set of uncontrollable events and a set of forcible events that may preempt the passage of time. To obtain a non-blocking controlled system, a synthesis algorithm is proposed that delivers a supervisor (also as a TA) avoiding the blocking states. The algorithm works by (iteratively) strengthening the guards of edges labeled by controllable events and invariants of locations where time progress can be preempted by forcible events.
|
|
| 4. |
- Rashidinejad, Aida, et al.
(författare)
-
Supervisory Control Synthesis of Timed Automata Using Forcible Events
- 2024
-
Ingår i: IEEE Transactions on Automatic Control. - 0018-9286 .- 1558-2523. ; 69:2, s. 1074-1080
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents an algorithm for synthesizing a supervisor for timed automata (TA) using the conventional supervisory control theory. The algorithm is directly applicable to TA without explicit transformation into finite automata, and iteratively strengthens 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, also a TA, is controllable, maximally permissive, and guarantees a non-blocking and safe supervised plant. The use of real-valued clocks in TA makes it a practical modeling framework, however, the infinite state space brings challenges. The proposed algorithm addresses these by providing a synthesis method that avoids the state-space explosion of finite automata and the loss of information that can result from abstraction of real-time values.
|
|
