Power System Modeling for Inverse Problems
131
Citation
48
Reference
10
Related Paper
Citation Trend
Abstract:
Large disturbances in power systems often initiate complex interactions between continuous dynamics and discrete events. The paper develops a hybrid automaton that describes such behavior. Hybrid systems can be modeled in a systematic way by a set of differential-algebraic equations, modified to incorporate impulse (state reset) action and constraint switching. This differential-algebraic impulsive-switched (DAIS) model is a realization of the hybrid automaton. The paper presents a practical object-oriented approach to implementing the DAIS model. Each component of a system is modeled autonomously. Connections between components are established by simple algebraic equations. The systematic nature of the DAIS model enables efficient computation of trajectory sensitivities, which in turn facilitate algorithms for solving inverse problems. The paper outlines a number of inverse problems, including parameter uncertainty, parameter estimation, grazing bifurcations, boundary value problems, and dynamic embedded optimization.Keywords:
Hybrid automaton
Realization (probability)
A set of states S is said to be inevitable for a hybrid automaton A if every behavior of A ultimately reaches S within bounded time. Inevitability captures various commonly occurring liveness properties. In this paper, we present an algorithm for verifying inevitability of Linear Hybrid Automata (LHA). The algorithm combines (a) Lyapunov function-based relational abstractions for the continuous dynamics with (b) automated construction of well-founded relations for the loops of the hybrid automaton. The algorithm is complete for automata that are symmetric with respect to the chosen Lyapunov functions. The algorithm is implemented in a prototype tool (LySHA) which is integrated with a Simulink/Stateflow frontend for modeling hybrid systems. The experimental results demonstrate the effectiveness of the methodology in verifying inevitability of hybrid automata with up to five continuous dimensions and forty locations.
Hybrid automaton
Stateflow
Liveness
Timed automaton
Büchi automaton
Cite
Citations (22)
Hybrid automaton
Cite
Citations (0)
Hybrid automaton
Cite
Citations (425)
This paper presents a new algorithm for generating finite-state automata models of hybrid systems in which the continuous-state dynamics can be switched when the continuous-state trajectory generates threshold events. The automata state transitions correspond to threshold events and the automata states correspond to portions of the threshold surfaces in the continuous state space. The hybrid system dynamics are approximated by the automata models in the sense that the languages of threshold event sequences generated by the automata contain the threshold event language for the hybrid system. Properties of the algorithm for constructing and refining the approximating automata are demonstrated and the application of approximating automata for system verification is illustrated for a switching controller for an inverted pendulum. Relationships to other approaches to hybrid system synthesis and verification are also discussed.
Hybrid automaton
Continuous spatial automaton
Nested word
Timed automaton
Sequence (biology)
ω-automaton
Cite
Citations (17)
A hybrid automaton is a model of a system with interacting continuous and discrete dynamics. It has been successfully employed in emerging applications on the border between computer science and control theory. In this paper, hybrid automata are formally introduced. Some results on existence and uniqueness of executions for hybrid automata are obtained. Continuous dependence on initial states are shown for a class of hybrid automata. Zeno hybrid automata, i.e., hybrid automata that exhibit infinitely many discrete transitions in finite time, are also discussed.
Hybrid automaton
Continuous spatial automaton
ω-automaton
Timed automaton
Zeno's paradoxes
Cite
Citations (14)
This paper discusses the use of hybrid automata to specify and verify embedded distributed systems, that consist of both discrete and continuous components. The basis of the evaluation is an automotive control system, which controls the height of an automobile by pneumatic suspension. It has been proposed by BMW AG as a case study taken from a current industrial development. Essential parts of the system have been modelled as hybrid automata and for appropiate ions several safety properties have been verified. The verification has been performed using HYTECH, a symbolic model checker for linear hybrid automata. The paper discusses the general appropiateness of hybrid automata to specify hybrid systems as well as advantages and drawbacks of the applied model-checking techniques.
Hybrid automaton
Basis (linear algebra)
Cite
Citations (24)
Physical systems can fail. For this reason the problem of identifying and reacting to faults has received a large attention in the control and computer science communities. In this paper we study the fault diagnosis problem and modeling of Hybrid Dynamical Systems (HDS). Generally speaking, HDS is a system mixing continuous and discrete behaviors that cannot be faithfully modeled neither by using formalism with continuous dynamics only nor by a formalism including only discrete dynamics. We use the well known framework of hybrid automata for modeling hybrid systems, because they combine the continous and discretes parts on the same structure. Hybrid automaton is a states-transitions graph, whose dynamic evolution is represented by discretes and continous steps alternations, also, continous evolution happens in the automaton apexes, while discrete evolution is realized by transitions crossing (arcs) of the graph. Their simulation presents many problems mainly the synchronisation between the two models. Stateflow, used to describe the discrete model, is co-ordinated with Matlab, used to describe the continuous model. This article is a description of a case study, which is a two tanks system.
Stateflow
Hybrid automaton
Formalism (music)
Timed automaton
Cite
Citations (3)
Various methodologies to model and analyze timed and hybrid systems using SAL are reported. We assume that the system is specified as a network of timed/hybrid automata with synchronized transitions and urgency. We show how to translate the system into a SAL model with the time domain being either discrete or dense, and the clocks being either saturated or unsaturated. Depending on these choices, various tools provided by SAL to model check reachability properties over the system are used to establish safety properties of timed systems. We profile the performance of these tools with a comparative study.
Timed automaton
Hybrid automaton
Cite
Citations (0)
Abstraction
Hybrid automaton
Cite
Citations (7)
This paper proposes an approach for the analysis and control of hybrid systems based on the hybrid automaton model. The problem that must be solved can be formulated as follows: given a hybrid automaton how can be restricted the regions associated with the controllable transition, in a systematic way, so that all the remaining behaviors satisfy certain properties. The hybrid nature of the manufacturing system is also investigated as a case study represented by a manufacturing cell. Throughout this paper the proposed methods are illustrated using an example taken from the manufacturing domain.
Hybrid automaton
Cite
Citations (1)