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.

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.

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.

In this paper, we explain the architecture and implementation of the tool Averist that performs stability verification for linear hybrid systems. This tool implements a hybridization method for approximating linear hybrid systems by hybrid systems with polyhedral inclusion dynamics. It also implements a new counterexample guided abstraction refinement framework for analyzing the hybrid systems with polyhedral inclusion dynamics that are generated as a result of the hybridization. Some of the main features of our tool are as follows: (1) our tool is based on algorithmic techniques that do not rely on the computation of Lyapunov functions, (2) it returns a counterexample when it fails to establish stability, (3) it is less prone to numerical instability issues as compared to Lyapunov function based tools.

In this paper, we describe an abstraction-based method for synthesizing a state-based switching control for stabilizing a family of dynamical systems. Given a set of dynamical systems and a set of polyhedral switching surfaces, the algorithm synthesizes a strategy that assigns to every surface the linear dynamics to switch to at the surface. Our algorithm constructs a finite game graph that consists of the switching surfaces as the existential nodes and the choices of the dynamics as the universal nodes. In addition, the edges capture quantitative information about the evolution of the distance of the state from the equilibrium point along the executions. A switching strategy for the family of dynamical systems is extracted by finding a strategy on the game graph which results in plays having a bounded weight. Such a strategy is obtained by reducing the problem to the strategy synthesis for an energy game, which is a well-studied problem in the literature. We have implemented our algorithm for polyhedral inclusion dynamics and linear dynamics. We illustrate our algorithm on examples from these two classes of systems.

In this paper, we present an algorithmic approach to global asymptotic stability (GAS) verification of hybrid systems. Our broad approach consists of reducing the GAS verification to the verification of a region stability (RS) analysis problem and an asymptotic stability (AS) analysis problem. We use a recently developed quantitative predicate abstraction technique for AS analysis and extract from it a stability zone with respect to which we perform RS analysis. We present a new algorithm for RS analysis based on abstractions. While we develop the theory for polyhedral hybrid systems, our broad approach of decomposing GAS analysis to RS and AS analysis can be applied to more general class of systems including linear hybrid systems. As a proof of concept, we apply the GAS verification algorithm to a linear hybrid system model of a cruise control for an automatic gearbox, and provide a semi-automated proof of GAS.

In this paper, we present a hybridization method for stability analysis of switched linear hybrid system (LHS), that constructs a switched system with polyhedral inclusion dynamics (PHS) using a state-space partition that is specific to stability analysis. We use a previous result based on quantitative predicate abstraction to analyse the stability of PHS. We show completeness of the hybridization based verification technique for the class of asymptotically stable linear system and a subclass of switched linear systems whose dynamics are pairwise Lipschitz continuous on the state-space and uniformly converging in time. For this class of systems, we show that by increasing the granularity of the region partition, we eventually reach an abstract switched system with polyhedral inclusion dynamics that is asymptotically stable. On the practical side, we implemented our approach in the tool averist, and experimentally compared our approach with a state-of-the-art tool for stability analysis of hybrid systems based on Lyapunov functions. Our experimental results illustrate that our method is less prone to numerical errors and scales better than the traditional approaches. In addition, our tool returns a counterexample in the event that it fails to prove stability, providing feedback regarding the potential reason for instability. We also examined heuristics for the choice of state-space partition during refinement.