| 1. |
- Vahidi Mazinani, Arash, 1974, et al.
(author)
-
Efficient Application of Symbolic Tools for Resource Booking Problems
- 2001
-
In: American Control Conference, Arlington, VA, USA; 25 June through 27 June 2001. ; 6, s. 4937-4942
-
Conference paper (peer-reviewed)abstract
- This paper describes how symbolic model checking tools, like binary decision diagrams, may be used to analyze and synthesize supervisors for discrete event systems. As an application a general routing resource booking problem is considered. A specification language is presented which makes it easy to handle both multiple and alternative resource booking problems. The language is directly translated to a relational model, which is immediately implemented as a BDD. Two optimization concepts, namely smoothing and variable reduction in the BDD representation, are shown to be extremely valuable to handle huge state space problems in short time.
|
|
| 2. |
- Byröd, Martin, 1980, et al.
(author)
-
Efficient Reachability Analysis on Modular Discrete-Event Systems using Binary Decision Diagrams
- 2006
-
In: 8th International Workshop on Discrete Event Systems, WODES 2006; Ann Arbor, MI; United States; 10 July 2006 through 12 July 2006. - 1424400538 ; , s. 288-293
-
Conference paper (peer-reviewed)abstract
- A well known strategy for handling the exponential complexity of modular discrete event systems is to represent the state space symbolically, using binary decision diagrams (BBDs). In this paper, key success factors in the design of efficient BDD-based reachability algorithms for synthesis and verification are discussed. It is also shown how the modular structure of a discrete event system (DES) can be utilized by taking advantage of the process communication graph and partitioning techniques. A reachability algorithm based on these principles is discussed and a proof of correctness for the algorithm is given.
|
|
| 3. |
- Falkman, Petter, 1972, et al.
(author)
-
Modeling and Controller Synthesis for Resource Booking Problems using BDDs
- 2002
-
In: Proceedings of the 15th IFAC World Congress, Barcelona, Spain, 8 July through 12 July 2001. ; 2, s. 1011-1016
-
Conference paper (peer-reviewed)abstract
- A modeling framework for general routing and resource booking problems is presented. The task is to specify desired routes for individual objects (products, data packets, vehicles), which are to be served by a number of shared resources (machines, computers, communication links). Based on simple booking models for the resources and routing specifications for the objects, a controller that synchronizes the objects utilization of the available resources is automatically generated. A high level language is presented in order to simplify the specification of desired routes. This modeling language combines Petri nets and process algebra. Process operators are introduced for specification of alternative and synchronization, which are applied in order to model join and split operations. Multiple as well as alternative resources are easily specified utilizing sets of resources. These sets and operators imply a very compact and efficient representation of complex routing specifications. In fact, the representatio n is suitable for verification and synthesis based on symbolic tools such as BDDs.
|
|
| 4. |
- Miremadi, Sajed, 1983, et al.
(author)
-
Solving Two Supervisory Control Benchmark Problems Using Supremica
- 2008
-
In: 9th International Workshop on Discrete Event Systems, 2008. - 9781424425921 ; , s. 131-136
-
Conference paper (peer-reviewed)abstract
- Two supervisory control benchmark problems for WODES'08 are solved using the tool Supremica. Supremica is a tool for formal synthesis of discrete-event control functions based on discrete event models of the uncontrolled plant and specifications of the desired closed-loop behavior. By using formal synthesis of control functions the need for formal verification is reduced since the control functions are computed to automatically fulfill the given specifications, that is, they are "correct by construction". The modeling framework in Supremica is based on finite automata. Supremica implements several techniques for being able to solve large scale problems. In this paper it is evaluated how the algorithms implemented in Supremica that are based on binary decision diagrams performs on the two benchmark problems. The two benchmark problems are generalization of two classical problems; cat and mouse, and the dining philosophers' problem. The benchmark problems are parametrized such that it is possible to create problem instances with huge state-spaces. The benchmark shows that Supremica can efficiently solve rather large problem instances.
|
|
| 5. |
|
|
| 6. |
|
|
| 7. |
- Vahidi Mazinani, Arash, 1974
(author)
-
Efficient Analysis of Discrete Event Systems: Supervisor Synthesis with Binary Decision Diagrams
- 2004
-
Doctoral thesis (other academic/artistic)abstract
- Due to the ever-increasing complexity of software and hardware, it is becoming more and more important to develop methods and tools for automatic analysis and synthesis of systems. One obstacle in achieving this goal has been the unmanageable size and complexity of the involved mathematical operations. For example, real-world systems such as manufacturing cells or embedded systems represented as composite discrete-event systems tend to have huge numbers of states. The enormity of these models will make most types of analysis very hard if not impossible. Taking advantage of Binary Decision Diagrams, this work presents a set of algorithms and heuristics for searching the enormous state-space of large discrete event systems in a efficient manner. Furthermore, the author demonstrates how important problems within the field of supervisor control theory can be solved using the presented search methods. It is also shown how the conjunction of such methods and algorithmic optimization is used to gain performance even more.
|
|
| 8. |
- Vahidi Mazinani, Arash, 1974, et al.
(author)
-
Efficient Analysis of Large Discrete-Event Systems with Binary Decision Diagrams
- 2005
-
In: Decision and Control, 2005 and 2005 European Control Conference. CDC-ECC '05. 44th IEEE Conference on. ; , s. 2751 - 2756
-
Conference paper (peer-reviewed)abstract
- Efficient analysis and controller synthesis in the context of Discrete-Event Systems (DES) is discussed in this paper. We consider efficient reachability search for solving common problems in the Supervisory Control Theory (SCT). The search is based on symbolic computations including crucial partitioning techniques. Finally, the efficiency of the presented algorithms is demonstrated on a set of hand-made and real-world industrial systems.
|
|
| 9. |
|
|
| 10. |
- Vahidi Mazinani, Arash, 1974, et al.
(author)
-
Efficient Supervisory Synthesis of Large Systems
- 2006
-
In: Control Engineering Practice. - : Elsevier BV. - 0967-0661. ; 14:10, s. 1157-1167
-
Journal article (peer-reviewed)abstract
- Due to the state-space explosion, many synthesis and verification problems for discrete event systems cannot be solved using traditional state-space traversal algorithms. This work presents efficient methods for reachability search based on symbolic computations using Binary Decision Diagrams. In addition, simple guidelines and quantities for separating hard and easy reachability problems are presented. Furthermore, the performance of the presented algorithms and heuristics is demonstrated on a set of industrial benchmark examples. It is also shown that such examples are much more challenging than some well-known handmade benchmark models. This is also indicated by the presented hardness quantities.
|
|
