Olga Tveretina, University of Karlsruhe

 

 

Point-to-point reachability  for 3-dimensional PCDs

 

 

One of the most central problems in the analysis of hybrid
systems is the reachability  problem.  This problem has been shown to be
decidable for special kinds of hybrid automata including timed automata,
certain special classes of rectangular hybrid automata and o-minimal
hybrid automata.

Piecewise Constant Derivative Systems (PCDs), on the one hand, belong to
the class of linear hybrid systems for which the  problem of
region-to-region reachability has been shown to be decidable. Proof of
decidability is based on the existence of a finite, computable partition
of the state space that is bisimilar to the original system.  On the
other hand, the results due to E. Asarin, O. Maler and A. Pnueli  state
that the problem of point-to-point reachability is undecidable for PCDs
for dimensions 3 and higher.

In my talk I will revise the problem of point-to-point reachability  for
3-dimensional PCDs and present a proof of decidability of it based on
spatial properties of trajectories.