2007/10/19 by Sumit Kumar Jha, Jha, Sumit Kumar
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Testing and Debugging Techniques #cs.LO
paper · pdf · doi:10.48550/arxiv.0710.3764
8 pages
arxiv created 2007/10/19 · openalex publication_date 2007/10/19 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This paper presents the design of a novel distributed algorithm d-IRA for the reachability analysis of linear hybrid automata. Recent work on iterative relaxation abstraction (IRA) is leveraged to distribute the computational problem among multiple computational nodes in a non-redundant manner by performing careful infeasibility analysis of linear programs corresponding to spurious counterexamples. The d-IRA algorithm is resistant to failure of multiple computational nodes. The experimental results provide promising evidence for the possible successful application of this technique.