| 231. |
- Miremadi, Sajed, 1983, et al.
(författare)
-
Symbolic Representation and Computation of Timed Discrete-Event Systems
- 2014
-
Ingår i: IEEE Transactions on Automation Science and Engineering. - : Institute of Electrical and Electronics Engineers (IEEE). - 1558-3783 .- 1545-5955. ; 11:1, s. 6-19
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 232. |
- Miremadi, Sajed, 1983, et al.
(författare)
-
Symbolic Supervisory Control of Timed Discrete Event Systems
- 2015
-
Ingår i: IEEE Transactions on Control Systems Technology. - 1063-6536 .- 1558-0865. ; 23:2, s. 584-597
-
Tidskriftsartikel (refereegranskat)abstract
- We symbolically compute a nonblocking, controllable, and minimally restrictive supervisor for timed discrete event systems (TDESs), in the supervisory control theory context. We model 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 controllability is defined based on the corresponding tick models of the TEFAs. A tick can be considered as an event that is generated by a global digital clock. The tick models suffer from a major problem: the state size is very sensitive to the clock frequency. We show how a controllable supervisor, equivalent to the one computed based on the tick models, can be obtained by eliminating the tick events. To tackle large problems, all computations are conducted symbolically using binary decision diagrams (BDDs). We show that, based on the proposed approach, a fixed point is reached earlier in the reachability analysis and that the size of the intermediate BDDs usually becomes smaller. The framework has been applied to a real industrial application and several benchmarks.
|
|
| 233. |
- Nia, Nima, 1975, et al.
(författare)
-
Efficient geometrical simulation and virtual commissioning performed in stamping
- 2012
-
Ingår i: Proceedings of 2012 IEEE 17th International Conference on Emerging Technologies & Factory Automation (ETFA 2012). - Polen : IEEE. - 9781467347372 - 9781467347365 - 9781467347358 ; , s. 1-8
-
Konferensbidrag (refereegranskat)abstract
- In order to perform efficient geometrical simulation and virtual commissioning in stamping, three fields are investigated namely: simulation building time, collision detection time and optimization time. Hence, reducing time is the main theme of this paper. To reduce simulation building time and optimization time, an efficient stamping simulation model is built and tested. Collision detection time is examined by a relative motion method based on 3D to 2D geometrical collision detection. The presented results mean that simulation and virtual commissioning can be performed at least ten times faster compared to standard approaches.
|
|
| 234. |
- Nia, Nima K., et al.
(författare)
-
A faster collision detection method applied on a sheet metal press line
- 2011
-
Ingår i: The 4th International Swedish Production Symposium. - Lund : Swedish Production Academy. ; , s. 467-472, s. 833-840, s. 833-840
-
Konferensbidrag (refereegranskat)abstract
- Geometrical collision detection is a time and resource consuming simulation task. In order to decrease time and resources, a general method applicable for 2D motions has been developed. The method is useful in simulation cases where 3D CAD data is part of an iterative method, e.g. optimization. The method is based on a transformation of a general 3D problem to a 2D problem, eliminating the need of 3D CAD models. Press Line simulations during the last decade have been accepted as a quality improvement method. Today simulations of automated press lines are done for internal collision checks in dies and external collision checks against dies and material handling equipment. If these collisions are not detected in simulations, they result in delays, in introduction of a new product in the line, so called line tryout or later when the line is ramped up to decide rate. The results of these collisions are used for pre-die design, design of grippers, maintenance and production planning. In this paper a new method, based on 2D simplifications, is developed and tested successfully in a virtual model of a press line at Volvo Car Manufacturing. Die Uppers 2 917 708 triangles and Die Lowers 602 686 triangles where reduced to 58 and 90 points. The result of the method shows substantial reduction of geometry data and considerable improvement in collision detection evaluation time over general 3D algorithms in the tested case.
|
|
| 235. |
|
|
| 236. |
- Noori-Hosseini, Mona, 1982, et al.
(författare)
-
A survey on efficient diagnosability tests for automata and bounded Petri nets
- 2013
-
Ingår i: IEEE International Conference on Emerging Technologies and Factory Automation, ETFA. - 1946-0759 .- 1946-0740. - 9781479908622 ; , s. 1-6
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a survey and evaluation of the efficiency of polynomial diagnosability algorithms for systems modeled by Petri nets and automata. A modified verification algorithm that reduces the state space by exploiting symmetry and abstracting unobservable transitions is also proposed. We show the importance of minimal explanations on the performance of diagnosability verifiers.Different verifiers are compared in terms of state spaceand elapsed time. It is shown that the minimal explanationnotion involved in the modified basis reachabilitygraph, a graph presented by Cabasino et al. [3] for diagnosability analysis of Petri nets, has great impact alsoon automata-based diagnosability methods. The evaluationoften shows improved computation times of a factor1000 or more when the concept of minimal explanation isincluded in the computation.
|
|
| 237. |
- Noori-Hosseini, Mona, 1982, et al.
(författare)
-
Compositional Visible Bisimulation Abstraction Applied to Opacity Verification
- 2018
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 51:7, s. 434-441
-
Konferensbidrag (refereegranskat)abstract
- In this paper, an alternative equivalence based definition of bisimulation is proposed, called visible bisimulation equivalence. It includes both state and transition labels and therefore unifies stuttering and branching bisimulation. Furthermore, it is equivalent to a temporal logic called ECTL*, where CTL* is extended with events. The presented bisimulation abstraction is applied to a set of synchronized submodels, where local events are identified incrementally and abstracted after each synchronization. Since the bisimulation reduction is applied after each synchronization, a significant part of the state space explosion in ordinary synchronization is avoided. This compositional abstraction is used for opacity verification, where it is shown that local observers can be generated before they are synchronized, a key factor to be able to apply compositional opacity verification. The efficiency of this method is illustrated on a modular opacity problem with mutual exclusion of moving agents.
|
|
| 238. |
- Noori-Hosseini, Mona, 1982, et al.
(författare)
-
Diagnosability Verification Using Compositional Branching Bisimulation
- 2016
-
Ingår i: 13th International Workshop on Discrete Event Systems, Xi'an, China, May 30 - June 1. - 1550-5227. - 9781509041909 ; , s. 245-250
-
Konferensbidrag (refereegranskat)abstract
- This paper presents an efficient diagnosabilityverification technique, based on a general abstraction approach.More specifically, branching bisimulation including state labelswith explicit divergence (BBSD) is defined. This bisimulationpreserves the temporal logic property that verifies diagnosability.Based on a proposed BBSD algorithm, compositionalabstraction for modular diagnosability verification is shownto offer a significant state space reduction in comparison tostate-of-the-art techniques. This is illustrated by verifying nondiagnosabilityanalytically for a set of synchronized components,where the abstracted solution is independent of thenumber of components and the number of observable events.
|
|
| 239. |
- Noori-Hosseini, Mona, 1982, et al.
(författare)
-
Incremental Abstraction for Diagnosability Verification of Modular Systems
- 2019
-
Ingår i: IEEE International Conference on Emerging Technologies and Factory Automation, ETFA. - 1946-0759 .- 1946-0740. - 9781728103037 ; 2019-September, s. 393-399
-
Konferensbidrag (refereegranskat)abstract
- In a diagnosability verifier with polynomial complexity, a non-diagnosable system generates uncertain loops. Such forbidden loops are in this paper transformed to forbidden states by simple detector automata. The forbidden state problem is trivially transformed to a nonblocking problem by considering all states except the forbidden ones as marked states. This transformation is combined with one of the most efficient abstractions for modular systems called conflict equivalence, where nonblocking properties are preserved. In the resulting abstraction, local events are hidden and more local events are achieved when subsystems are synchronized. This incremental abstraction is applied to a scalable production system, including parallel lines where buffers and machines in each line include some typical failures and feedback flows. For this modular system, the proposed diagnosability algorithm shows great results, where diagnosability of systems including millions of states is analyzed in less than a second.
|
|
| 240. |
|
|
