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

TL;DR

This paper introduces an algorithm to decide reachability in multi-priced timed automata with both positive and negative observer rates, extending previous work limited to non-negative rates, by translating the problem into nonlinear constraints and solving them with a novel approach.

Contribution

It presents the first decision procedure for gap reachability in MPTA with mixed observer rates, using a new method combining branch-and-bound and relaxation-rounding techniques.

Findings

Algorithm successfully decides gap reachability for the new class of MPTA.

The approach handles nonlinear mixed integer-real constraints effectively.

Extends the theoretical understanding of timed automata with complex observer dynamics.

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.