Reachability for Multi-Priced Timed Automata with Positive and Negative Rates

TL;DR

The paper tackles reachability for Multi-Priced Timed Automata with observers that can have both positive and negative rates by introducing the Gap Domination Problem and reducing it to a Gap Satisfiability problem for bounded mixed-integer bilinear (MIB) systems. A novel relaxation–rounding and branch‑and‑bound procedure, grounded in Diophantine approximation via the Flatness Theorem, yields a nondeterministic exponential-time decision procedure for the bounded case. This establishes decidability of the Gap Domination Problem in NEXP and enables approximating the Pareto curve of undominated reachable observer values for MPTA, bridging gaps between timed automata, hybrid systems, and multi-objective verification. The results pave the way for practical Pareto analysis and outline future work on infinite runs and multi-ratio specifications.

Abstract

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.

Figures (1)

• Figure 1: An MTPA with three clocks $x,y,z$ and two observer variables $o,e$, respectively standing for odd and even. The observer variables have slope 0 unless otherwise indicated; thus $o$ aggregates the total dwell time in the odd state and $e$ aggregates the total dwell time in the even state. An accepting run is completely determined by a sequence of nonnegative real numbers $d_0,\ldots,d_{2k}$, giving the respective delays between successive transitions. Suppose we wish to reach the accepting state subject to the two objectives $e \geq 2$ and $o \geq 1$. This is achieved, among others, by the run with sequence of time delays $\frac{2}{3}, \frac{1}{3},\frac{2}{3}, \frac{1}{3},\frac{2}{3}, \frac{1}{3},\frac{2}{3}$ and the run with integer sequence of delays $1,0,1,0,1,1,0$ (and any convex combination of the two runs). If the inequalities in the guards on $x$ and $y$ are replaced by equalities then the first run is the unique one realising the two given objectives. In the case of so-called pure reachability objectives, i.e., exclusively upper bound constraints or exclusively lower bound constraints on the observers, there is an explicit upper bound on the granularity of the delays in a run witnessing that the ojbective is realisable ($\frac{1}{3}$ in the present example) FranzleSSW22. This no longer holds in the case of reachability objectives that contain both upper and lower bounds on observers.

Theorems & Definitions (14)

• Proposition 1
• Corollary 2
• Proposition 3
• Proposition 4
• Proposition 5
• Proposition 6
• Theorem 7: Flatness Theorem
• Proposition 8
• Proposition 9
• Proposition 10