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.
Parameter Synthesis Problems for Parametric Timed Automata
RISE & School of Computer and Information Science, Southwest University（重庆西南大学计算机与信息科学学院）；Department of Computer Science and Information Systems Birkbeck, University of London（伦敦大学伯贝克学院计算机科学与信息系统系）
Parameter Synthesis Problems for one parametric clock Timed Automata
RISE, Southwest University（西南大学 RISE）；Department of Computer Science and Informatioin Systems, Birkbeck, University of London（伦敦大学伯贝克学院计算机科学与信息系统系）；LMAM & School of Mathematical Sciences, Peking University（北京大学数学科学学院 LMAM）；State Key Laboratory of Computer Science, Institute of Software, CAS（中国科学院软件研究所 计算机科学国家重点实验室）；CISS, CS, Aalborg University（奥尔堡大学计算机科学与工程系 CISS）
