Reachability Problems on Extended O-Minimal Hybrid Automata

Within hybrid systems theory, o-minimal automata are often considered on the border between decidability and undecidability. In such classes of hybrid automata, the constraint of having only constant reset upon discrete jumps is a strong limitation for their applicability: hence, an important issue for both theoreticians and practitioners, is that of relaxing the above constraint, while not fall into undecidability. In this paper we start considering the problem of timed-bounded reachability on o-minimal automata. This can be seen either as a reachability problem paired with time-constraints or as a classical reachability problem for a class of hybrid automata which properly extends the o-minimal one, with an extra variable representing time. Then, we directly face the problem of extending o-minimal automata by allowing some variables to retain their values upon a discrete jump, without crossing the undecidability border.