Reachability games for linear hybrid systems
Massimo Benerecetti, Marco Faella, Stefano Minopoli · 2012
We consider the problem of computing the controllable region of a Linear Hybrid Automaton with controllable and uncontrollable transitions, w.r.t. a reachability objective. We provide a semi-algorithm for the problem, by proposing the first algorithm in the literature for computing the set of states that must reach a given polyhedron while avoiding another one, subject to a polyhedral constraint on the slope of the trajectory. Experimental results are presented, based on an implementation of the proposed algorithm on top of the tool PHAVer.