| 241. |
- 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.
|
|
| 242. |
- 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.
|
|
| 243. |
- 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.
|
|
| 244. |
|
|
| 245. |
- Pellicciari, M., et al.
(författare)
-
AREUS — Innovative hardware and software for sustainable industrial robotics
- 2015
-
Ingår i: IEEE International Conference on Automation Science and Engineering. - 2161-8070 .- 2161-8089. - 9781467381833 ; 2015-October, s. 1325-1332
-
Konferensbidrag (refereegranskat)abstract
- Industrial Robotics (IR) may be envisaged as the key technology to keep the manufacturing industry at the leading edge. Unfortunately, at the current state-of-the-art, IR is intrinsically energy intensive, thus compromising factories sustainability in terms of ecological footprint and economic costs. Within this scenario, this paper presents a new framework called AREUS, focusing on eco-design, eco-programming and Life Cycle Assessment (LCA) of robotized factories. The objective is to overcome current IR energetic limitations by providing a set of integrated technologies and engineering platforms. In particular, novel energy-saving hardware is firstly introduced, which aim at exchanging/storing/recovering energy at factory level. In parallel, innovative engineering methods and software tools for energy-focused simulation are developed, as well as energy-optimal scheduling of multi-robot stations. At last, LCA methods are briefly described, which are capable to assess both environmental and economic costs, linked to the flows of Material, Energy and Waste (MEW). A selected list of industrially-driven demonstration case studies is finally presented, along with future directions of improvement.
|
|
| 246. |
- Pellicciari, M., et al.
(författare)
-
Object-oriented modeling of industrial manipulators with application to energy optimal trajectory scaling
- 2011
-
Ingår i: ASME 2011 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference, IDETC/CIE 2011; Washington, DC; United States; 28 August 2011 through 31 August 2011. - 9780791854822 ; 5:A and B, s. 997-1006
-
Konferensbidrag (refereegranskat)abstract
- The development of safe, energy efficient mechatronic systems is currently changing standard paradigms in the design and control of industrial manipulators. In particular, most optimization strategies require the improvement or the substitution of different system components. On the other hand, from an industry point of view, it would be desirable to develop energy saving methods applicable also to established manufacturing systems being liable of small possibilities for adjustments. Within this scenario, an engineering method is reported for optimizing the energy consumption of serial manipulators for a given operation. An object-oriented modeling technique, based on bond graph, is used to derive the robot electromechanical dynamics. The system power flow is then highlighted and parameterized as a function of the total execution times. Finally, a case study is reported show- ing the possibility to reduce the operation energy consumption when allowed by scheduling or manufacturing constraints.
|
|
| 247. |
|
|
| 248. |
|
|
| 249. |
- Pettersson, Stefan, 1969, et al.
(författare)
-
Exponential Stability Analysis of Nonlinear Systems using LMIs
- 1997
-
Ingår i: Proc. of 36th IEEE Conference on Decision and Control, San Diego, DEC 10-12. ; , s. 199-204
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a constructive method for showing exponential stability of autonomous nonlinear systems consisting of state-dependent weighted linear systems. This kind of system representation is common in for instance fuzzy systems or is the result of an exact or approximative description of an arbitrary nonlinear vector field. Stability is shown by joining multiple local Lyapunov functions properly in the state-space. The overall Lyapunov function, consisting of the local ones, are allowed to be discontinuous at the states where the trajectory passes from one local region to another. By using local quadratic Lyapunov functions the stability conditions are formulated as linear matrix inequalities (LMIs), which can be solved efficiently by computerized methods.
|
|
| 250. |
|
|
