Random Relaxation Abstractions for Bounded Reachability Analysis of Linear Hybrid Automata: Distributed Randomized Abstractions in Model Checking

The state of the art in the validation of linear hybrid automata has been restricted to systems with tens of variables because of the extremely high computational complexity of manipulating polyhedra in high dimensions. In this paper, we present a distributed algorithm that constructs low dimensional randomized over-approximate relaxation abstractions of linear hybrid automata and analyzes these low dimensional hybrid automata to perform bounded model checking of the original high dimensional linear hybrid automata. Our algorithm relies on the feasibility preserving nature of random linear relaxations and the Johnson Lindenstrauss lemma to show that random relaxations preserve the infeasibility of linear constraints with a nonzero probability.