Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata

TL;DR

This paper studies the verification of safety properties in large, spatially distributed systems of linear hybrid automata, providing conditions for decidability and tractability, with applications to vehicle coordination.

Contribution

It introduces a class of spatial hybrid automata systems and safety properties where verification reduces to bounded cases, establishing decidability and fixed parameter tractability.

Findings

Verification reduces to small neighboring systems

Decidability and tractability conditions identified

Implementation enables automatic safety verification

Abstract

We consider systems composed of an unbounded number of uniformly designed linear hybrid automata, whose dynamic behavior is determined by their relation to neighboring systems. We present a class of such systems and a class of safety properties whose verification can be reduced to the verification of (small) families of neighbouring systems of bounded size, and identify situations in which such verification problems are decidable, resp. fixed parameter tractable. We illustrate the approach with an example from coordinated vehicle guidance, and describe an implementation which allows us to perform such verification tasks automatically.