Synthesis of Hybrid Automata with Affine Dynamics from Time-Series Data

TL;DR

This paper introduces an algorithmic method to synthesize hybrid automata with affine dynamics from time-series data, enabling formal modeling of cyber-physical systems with controllable precision.

Contribution

It presents a novel synthesis approach combining reachability and optimization techniques for affine systems, allowing data-driven hybrid automaton construction with iterative refinement.

Findings

Effective synthesis from real data demonstrated

Algorithm can process and refine models incrementally

Experimental validation confirms practical applicability

Abstract

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.