Design of a Distributed Reachability Algorithm for Analysis of Linear Hybrid Automata

TL;DR

This paper introduces a distributed algorithm, d-IRA, for analyzing the reachability of linear hybrid automata, leveraging iterative relaxation abstraction to distribute computation efficiently and resiliently across multiple nodes.

Contribution

It presents a novel distributed approach, d-IRA, that improves scalability and fault tolerance in reachability analysis of linear hybrid automata.

Findings

Effective distribution of computational tasks among nodes.

Resilience to multiple node failures.

Promising experimental results supporting the approach.

Abstract

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.