On Nonlinear Prices in Timed Automata

TL;DR

This paper explores the complexity of priced timed automata with nonlinear prices, showing that the optimal reachability problem becomes undecidable in the most general case, and presents an implementation using Z3.

Contribution

It extends the analysis of priced timed automata to nonlinear pricing models and demonstrates the undecidability of the optimal reachability problem in this setting.

Findings

Optimal reachability is undecidable for general nonlinear priced timed automata.

Implemented a Z3-based framework for analyzing nonlinear priced timed automata.

Provided preliminary results indicating the complexity of nonlinear pricing models.

Abstract

Priced timed automata provide a natural model for quantitative analysis of real-time systems and have been successfully applied in various scheduling and planning problems. The optimal reachability problem for linearly-priced timed automata is known to be PSPACE-complete. In this paper we investigate priced timed automata with more general prices and show that in the most general setting the optimal reachability problem is undecidable. We adapt and implement the construction of Audemard, Cimatti, Kornilowicz, and Sebastiani for non-linear priced timed automata using state-of-the-art theorem prover Z3 and present some preliminary results.