Random Relazation 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.
Sumit Kumar Jha Susmit Jha
School of Computer Science Carnegie Mellon University Electrical Engineering Computer Science Department University of California Berkeley
国际会议
11th IEEE High Assurance Systems Engineering Symposium(HASE 2008)(第十一届IEEE高可信系统工程国际研讨会)
南京
英文
147-153
2008-12-03（万方平台首次上网日期，不代表论文的发表时间）