| 1. |
- Fabian, Martin, 1960, et al.
(author)
-
Lupremica - Lua Scripting for Supremica
- 2023
-
In: IFAC-PapersOnLine. - 2405-8963. ; 56:2, s. 6099-6104
-
Conference paper (peer-reviewed)abstract
- Supremica is a software tool that implements several state-of-the-art algorithms to manipulate discrete-event systems, such as different types of compositions and compositional supervisor synthesis. Lua is a light-weight programming language suitable as a scripting language embedded into other applications. This paper describes the use of Lua as a scripting language for Supremica. To this end, the LuaJ interpreter is added to Supremica as a bridge between the Java-based implementation of Supremica and the Lua scripts. In this way, Supremica's entire Java API is made available to Lua scripts. Thus, scripts can automatically create automata, and manipulate them with all the algorithms available in Supremica and further manipulate the result with new algorithms implemented by Lua scripts. This opens up a new world of possibilities to try out new ideas and to extend the power of Supremica.
|
|
| 2. |
- Flordal, Hugo, 1977, et al.
(author)
-
Compositional Synthesis of Maximally Permissive Supervisors Using Supervision Equivalence
- 2007
-
In: Discrete Event Dynamic Systems: Theory and Applications. - : Springer Science and Business Media LLC. - 0924-6703 .- 1573-7594. ; 17:4, s. 475-504
-
Journal article (peer-reviewed)abstract
- This paper presents a general framework for efficient synthesis of supervisors for discrete event systems. The approach is based on compositional minimisation, using concepts of process equivalence. In this context, a large number of ways are suggested how a finite-state automaton can be simplified such that the results of supervisor synthesis are preserved. The proposed approach yields a compact representation of a least restrictive supervisor that ensures controllability and nonblocking. The method is demonstrated on a simple manufacturing example to significantly reduce the number of states constructed for supervisor synthesis. © 2007 Springer Science+Business Media, LLC.
|
|
| 3. |
- Flordal, Hugo, 1977, et al.
(author)
-
Supervision Equivalence
- 2006
-
In: 8th International Workshop on Discrete Event Systems (WODES'06). ; , s. 155--160-
-
Conference paper (peer-reviewed)
|
|
| 4. |
- Krook, Jonas, 1986, et al.
(author)
-
Robust stutter bisimulation for abstraction and controller synthesis with disturbance
- 2024
-
In: Automatica. - 0005-1098. ; 160
-
Journal article (peer-reviewed)abstract
- This paper proposes a method to synthesise controllers for cyber-physical systems subjected to disturbances, such that the controlled system satisfies specifications given as linear temporal logic formulas. To solve this problem, a finite-state abstraction of the original system is first constructed, and then a controller is synthesised for the abstraction. Due to the disturbances and uncertainty in the environment, future states cannot be predicted exactly, and the abstraction must take this into account. For this purpose, the robust stutter bisimulation relation is introduced, which preserves the existence of controllers for any given linear temporal logic formula that excludes the next operator. States are related by the robust stutter bisimulation relation if the same target sets can be guaranteed to be reached or avoided under control of some controller, thus ensuring that disturbances have similar effect on paths that start in related states. It is shown that there exists a controller enforcing a linear temporal logic formula for the original system if and only if a controller exists for the abstracted system. The approach is illustrated by a robot navigation example.
|
|
| 5. |
- Krook, Jonas, 1986, et al.
(author)
-
Robust Stutter Bisimulation for Abstraction and Controller Synthesis with Disturbance: Proofs
- 2022
-
Journal article (other academic/artistic)abstract
- This paper proposes a method to synthesise controllers for cyber-physical systems such that the controlled systems satisfy specifications given as linear temporal logic formulas. The focus is on systems with disturbance, where future states cannot be predicted exactly due to uncertainty in the environment. The approach used to solve this problem is to first construct a finite-state abstraction of the original system and then synthesise a controller for the abstract system. For this approach, the robust stutter bisimulation relation is introduced, which preserves the existence of controllers for any given linear temporal logic formula. States are related by the robust stutter bisimulation relation if the same target sets can be guaranteed to be reached or avoided under control of some controllers, thereby ensuring that disturbances have similar effect on paths that start in related states. This paper presents an algorithm to construct the corresponding robust stutter bisimulation quotient to solve the abstraction problem, and it is shown, by explicit construction, that there exists a controller enforcing a linear temporal logic formula for the original system if and only if a corresponding controller exists for the quotient system. Lastly, the result of the algorithm and the controller construction are demonstrated by application to an example of robot navigation.
|
|
| 6. |
- Malik, Robi, et al.
(author)
-
A survey on compositional algorithms for verification and synthesis in supervisory control
- 2023
-
In: Discrete Event Dynamic Systems: Theory and Applications. - 0924-6703 .- 1573-7594. ; 33:3, s. 279-340
-
Journal article (peer-reviewed)abstract
- This survey gives an overview of the current research on compositional algorithms for verification and synthesis of modular systems modelled as interacting finite-state machines. Compositional algorithms operate by repeatedly simplifying individual components of a large system, replacing them by smaller so-called abstractions, while preserving critical properties. In this way, the exponential growth of the state space can be limited, making it possible to analyse much bigger state spaces than possible by standard state space exploration. This paper gives an introduction to the principles underlying compositional methods, followed by a survey of algorithmic solutions from the recent literature that use compositional methods to analyse systems automatically. The focus is on applications in supervisory control of discrete event systems, particularly on methods that verify critical properties or synthesise controllable and nonblocking supervisors.
|
|
| 7. |
- Malik, Robi, et al.
(author)
-
Supremica–An Efficient Tool for Large-Scale Discrete Event Systems
- 2017
-
In: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 50:1, s. 5794-5799
-
Conference paper (peer-reviewed)abstract
- Supremica is a tool for the modelling and analysis of discrete-event control functions based on state machine models of the uncontrolled plant and specification of the desired closed-loop behaviour. The modelling framework in Supremica is based on finite-state machines extended with variables, guard conditions, and action functions. In order to handle large-scale problems of industrially interesting size, Supremica uses advanced model checking techniques such as symbolic representations and compositional abstraction. Supremica has been used in several industrial research projects to verify and synthesise control functions for embedded controllers, industrial robots, and flexible manufacturing systems, and to verify program code for autonomous vehicles. This paper gives an overview of the modelling features of Supremica, shows the verification and synthesis facilities and their performance for large problems, and presents some of the industrial applications where Supremica has been used.
|
|
| 8. |
- Malik, Robi, et al.
(author)
-
Yet another approach to compositional synthesis of discrete event systems
- 2008
-
In: 9th International Workshop on Discrete Event Systems, WODES' 08; Goteborg; Sweden; 28 May 2008 through 30 May 2008. - 9781424425921 ; , s. 16-21
-
Conference paper (peer-reviewed)abstract
- A two-pass algorithm for compositional synthesis of modular supervisors for large-scale systems of composed finite-state automata is proposed. The first pass provides an efficient method to determine whether a supervisory control problem has a solution, without explicitly constructing the synchronous composition of all components. If a solution exists, the second pass yields an over-approximation of the least restrictive solution which, if nonblocking, is a modular representation of the least restrictive supervisor. Using a new type of equivalence of nondeterministic processes, called synthesis equivalence, a wide range of abstractions can be employed to mitigate state-space explosion throughout the algorithm.
|
|
| 9. |
- Mohajerani, Sahar, 1982, et al.
(author)
-
A framework for compositional nonblocking verification of extended finite-state machines
- 2016
-
In: Discrete Event Dynamic Systems: Theory and Applications. - : Springer Science and Business Media LLC. - 0924-6703 .- 1573-7594. ; 26:1, s. 1-52
-
Journal article (peer-reviewed)abstract
- This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results are improved to consider general conflict-equivalence based abstractions of EFSMs communicating both via shared variables and events. Performance issues resulting from the conversion of EFSM systems to finite-state machine systems are avoided by operating directly on EFSMs, deferring the unfolding of variables into state machines as long as possible. Several additional methods to abstract EFSMs and remove events are also presented. The proposed algorithm has been implemented in the discrete event systems tool Supremica, and the paper presents experimental results for several large EFSM models that can be verified faster than by previously used methods.
|
|
| 10. |
- Mohajerani, Sahar, 1982, et al.
(author)
-
A Framework for Compositional Synthesis of Modular Nonblocking Supervisors
- 2014
-
In: IEEE Transactions on Automatic Control. - 0018-9286 .- 1558-2523. ; 59:1, s. 150-162
-
Journal article (peer-reviewed)abstract
- This paper describes a framework for compositional supervisor synthesis, which is applicable to all discrete event systems modeled as a set of deterministic automata. Compositional synthesis exploits the modular structure of the input model, and therefore works best for models consisting of a large number of small automata. The state-space explosion is mitigated by the use of abstraction to simplify individual components, and the property of synthesis equivalence guarantees that the final synthesis result is the same as it would have been for the non-abstracted model. The paper describes synthesis equivalent abstractions and shows their use in an algorithm to efficiently compute supervisors. The algorithm has been implemented in the DES software tool Supremica and successfully computes nonblocking modular supervisors, even for systems with more than 10(14) reachable states, in less than 30 seconds.
|
|
