Sökning: id:"swepub:oai:research.chalmers.se:f7df9b6f-0806-4075-91e2-bfd22674c08e" >
Compositional coord...
Compositional coordinator synthesis of extended finite automata
-
- Goorden, Martijn (författare)
- Technische Universiteit Eindhoven,Eindhoven University of Technology
-
- Fabian, Martin, 1960 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- van de Mortel-Fronczak, Joanna M. (författare)
- Technische Universiteit Eindhoven,Eindhoven University of Technology
-
visa fler...
-
- Reniers, Michel A. (författare)
- Technische Universiteit Eindhoven,Eindhoven University of Technology
-
- Fokkink, Wan J. (författare)
- Vrije Universiteit Amsterdam (VU)
-
- Rooda, Jacobus E. (författare)
- Technische Universiteit Eindhoven,Eindhoven University of Technology
-
visa färre...
-
(creator_code:org_t)
- 2021-01-07
- 2021
- Engelska.
-
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
- Relaterad länk:
-
https://research.vu....
-
visa fler...
-
https://doi.org/10.1...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Reglerteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Control Engineering (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Nyckelord
- Compositional synthesis
- Nonblocking
- Extended finite automata
- Supervisory control theory
Publikations- och innehållstyp
- art (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas