Deciding Reachability for 3-Dimensional Multi-Linear Systems

Olga Tveretina
(Karlsruhe Institute of Technology)
Daniel Funke
(Karlsruhe Institute of Technology)

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.

In Giovanna D'Agostino and Salvatore La Torre: Proceedings Second International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2011), Minori, Italy, 15-17th June 2011, Electronic Proceedings in Theoretical Computer Science 54, pp. 250–262.
Published: 4th June 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: