TY - CONF
AB - Formal design of embedded and cyber-physical systems relies on mathematical modeling. In this paper, we consider the model class of hybrid automata whose dynamics are defined by affine differential equations. Given a set of time-series data, we present an algorithmic approach to synthesize a hybrid automaton exhibiting behavior that is close to the data, up to a specified precision, and changes in synchrony with the data. A fundamental problem in our synthesis algorithm is to check membership of a time series in a hybrid automaton. Our solution integrates reachability and optimization techniques for affine dynamical systems to obtain both a sufficient and a necessary condition for membership, combined in a refinement framework. The algorithm processes one time series at a time and hence can be interrupted, provide an intermediate result, and be resumed. We report experimental results demonstrating the applicability of our synthesis approach.
AU - Garcia Soto, Miriam
AU - Henzinger, Thomas A
AU - Schilling, Christian
ID - 9200
KW - hybrid automaton
KW - membership
KW - system identification
SN - 9781450383394
T2 - HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control
TI - Synthesis of hybrid automata with affine dynamics from time-series data
ER -
TY - CONF
AB - We propose a novel hybridization method for stability analysis that over-approximates nonlinear dynamical systems by switched systems with linear inclusion dynamics. We observe that existing hybridization techniques for safety analysis that over-approximate nonlinear dynamical systems by switched affine inclusion dynamics and provide fixed approximation error, do not suffice for stability analysis. Hence, we propose a hybridization method that provides a state-dependent error which converges to zero as the state tends to the equilibrium point. The crux of our hybridization computation is an elegant recursive algorithm that uses partial derivatives of a given function to obtain upper and lower bound matrices for the over-approximating linear inclusion. We illustrate our method on some examples to demonstrate the application of the theory for stability analysis. In particular, our method is able to establish stability of a nonlinear system which does not admit a polynomial Lyapunov function.
AU - Garcia Soto, Miriam
AU - Prabhakar, Pavithra
ID - 9202
T2 - 2020 IEEE Real-Time Systems Symposium
TI - Hybridization for stability verification of nonlinear switched systems
ER -
TY - JOUR
AB - This paper presents a novel abstraction technique for analyzing Lyapunov and asymptotic stability of polyhedral switched systems. A polyhedral switched system is a hybrid system in which the continuous dynamics is specified by polyhedral differential inclusions, the invariants and guards are specified by polyhedral sets and the switching between the modes do not involve reset of variables. A finite state weighted graph abstracting the polyhedral switched system is constructed from a finite partition of the state–space, such that the satisfaction of certain graph conditions, such as the absence of cycles with product of weights on the edges greater than (or equal) to 1, implies the stability of the system. However, the graph is in general conservative and hence, the violation of the graph conditions does not imply instability. If the analysis fails to establish stability due to the conservativeness in the approximation, a counterexample (cycle with product of edge weights greater than or equal to 1) indicating a potential reason for the failure is returned. Further, a more precise approximation of the switched system can be constructed by considering a finer partition of the state–space in the construction of the finite weighted graph. We present experimental results on analyzing stability of switched systems using the above method.
AU - Garcia Soto, Miriam
AU - Prabhakar, Pavithra
ID - 7426
IS - 5
JF - Nonlinear Analysis: Hybrid Systems
SN - 1751570X
TI - Abstraction based verification of stability of polyhedral switched systems
VL - 36
ER -
TY - CONF
AB - We present two algorithmic approaches for synthesizing linear hybrid automata from experimental data. Unlike previous approaches, our algorithms work without a template and generate an automaton with nondeterministic guards and invariants, and with an arbitrary number and topology of modes. They thus construct a succinct model from the data and provide formal guarantees. In particular, (1) the generated automaton can reproduce the data up to a specified tolerance and (2) the automaton is tight, given the first guarantee. Our first approach encodes the synthesis problem as a logical formula in the theory of linear arithmetic, which can then be solved by an SMT solver. This approach minimizes the number of modes in the resulting model but is only feasible for limited data sets. To address scalability, we propose a second approach that does not enforce to find a minimal model. The algorithm constructs an initial automaton and then iteratively extends the automaton based on processing new data. Therefore the algorithm is well-suited for online and synthesis-in-the-loop applications. The core of the algorithm is a membership query that checks whether, within the specified tolerance, a given data set can result from the execution of a given automaton. We solve this membership problem for linear hybrid automata by repeated reachability computations. We demonstrate the effectiveness of the algorithm on synthetic data sets and on cardiac-cell measurements.
AU - Garcia Soto, Miriam
AU - Henzinger, Thomas A
AU - Schilling, Christian
AU - Zeleznik, Luka
ID - 6493
KW - Synthesis
KW - Linear hybrid automaton
KW - Membership
SN - 0302-9743
T2 - 31st International Conference on Computer-Aided Verification
TI - Membership-based synthesis of linear hybrid automata
VL - 11561
ER -
TY - CONF
AB - In this paper, we address the problem of synthesizing periodic switching controllers for stabilizing a family of linear systems. Our broad approach consists of constructing a finite game graph based on the family of linear systems such that every winning strategy on the game graph corresponds to a stabilizing switching controller for the family of linear systems. The construction of a (finite) game graph, the synthesis of a winning strategy and the extraction of a stabilizing controller are all computationally feasible. We illustrate our method on an example.
AU - Kundu, Atreyee
AU - Garcia Soto, Miriam
AU - Prabhakar, Pavithra
ID - 6565
SN - 978-153866246-5
T2 - 5th Indian Control Conference Proceedings
TI - Formal synthesis of stabilizing controllers for periodically controlled linear switched systems
ER -