LIPIcs.CSL.2025.18.pdf
- Filesize: 0.71 MB
- 13 pages
Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are read-once variables: they do not affect the control flow of the automaton and their value is output only at the end of a run. Thus MPTA lie between timed and hybrid automata in expressiveness. Previous work considered observers with non-negative slope in every location. In this paper we treat observers that have both positive and negative rates. Our main result is an algorithm to decide a gap version of the reachability problem for this variant of MPTA. We translate the gap reachability problem into a gap satisfiability problem for mixed integer-real systems of nonlinear constraints. Our main technical contribution - a result of independent interest - is a procedure to solve such contraints via a combination of branch-and-bound and relaxation-and-rounding.
Feedback for Dagstuhl Publishing