Reachability for Multi-Priced Timed Automata with Positive and Negative Rates
<|reference_start|>Reachability for Multi-Priced Timed Automata with Positive and Negative Rates: Multi-priced timed automata (MPTA) are timed automata with observer   variables whose derivatives can change from one location to another.   Observers are write-only variables, that is, they do not affect the control   flow of the automaton; 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.<|reference_end|>
@article{scoones2024reachability,
    title={Reachability for Multi-Priced Timed Automata with Positive and Negative
  Rates},
    author={Andrew Scoones, Mahsa Shirmohammadi, James Worrell},
    journal={arXiv preprint arXiv:2407.18131},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.18131},
    primaryClass={cs.FL}
}