Reachability analysis of planar multi-linear systems

Abstract

In this paper we study the reachability analysis of a simple class of hybrid systems, namely multi-linear systems. Such systems consist of a partition of the Euclidean space into a finite set of polyhedral sets (regions). Within each region the dynamics is defined by a constant vector field, hence the discrete transitions occur only on the boundaries between the regions where the trajectories change their direction. Such a system can be described by a finite set of guarded commands where the guards are conjunctions of linear inequalities and the commands are differential equations .with constant right hand sides, corresponding to the vector fields. Our goal is to verify, based on the description of the system, various teachability questions between regions of the plane. In particular we show that in planar deterministic systems, the question whether there exists a trajectory connecting a state in a source region to a state in a target region is decidable.