Deciding Reachability for 3-Dimensional Multi-Linear Systems

TL;DR

This paper investigates the reachability problem in 3D multi-linear systems, providing a decidability result under certain conditions and demonstrating practical efficiency over simulation methods.

Contribution

It proves that reachability in 3D multi-linear systems is decidable under specific conditions, extending known results from 2D and offering an efficient analysis approach.

Findings

Reachability is decidable in 3D multi-linear systems under certain conditions.

The proposed method outperforms simulation in efficiency by orders of magnitude.

Experimental results validate the practical applicability of the approach.

Abstract

This paper deals with the problem of point-to-point reachability in multi-linear systems. These systems consist of a partition of the Euclidean space into a finite number of regions and a constant derivative assigned to each region in the partition, which governs the dynamical behavior of the system within it. The reachability problem for multi-linear systems has been proven to be decidable for the two-dimensional case and undecidable for the dimension three and higher. Multi-linear systems however exhibit certain properties that make them very suitable for topological analysis. We prove that reachability can be decided exactly in the 3-dimensional case when systems satisfy certain conditions. We show with experiments that our approach can be orders of magnitude more efficient than simulation.