On Nonlinear Prices in Timed Automata

Devendra Bhave
(IIT Bombay, India)
Shankara Narayanan Krishna
(IIT Bombay, India)
Ashutosh Trivedi
(University of Colorado Boulder, USA)

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.

In Mehdi Kargahi and Ashutosh Trivedi: Proceedings of the The First Workshop on Verification and Validation of Cyber-Physical Systems (V2CPS-16), Reykjavík, Iceland, June 4-5, 2016, Electronic Proceedings in Theoretical Computer Science 232, pp. 65–78.
Published: 13th December 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.232.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org