2026-08-20T07:03:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22775 2025-10-02T11:31:39Z ddc:004 open_access

Reachability for Multi-Priced Timed Automata with Positive and Negative Rates Scoones, Andrew Shirmohammadi, Mahsa Worrell, James Bilinear constraints Existential theory of real closed fields Diophantine approximation Pareto curve 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrew Scoones and Mahsa Shirmohammadi and James Worrell 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.18 urn:nbn:de:0030-drops-227758 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.18 eng https://creativecommons.org/licenses/by/4.0/legalcode