Article

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 stateof-the-art theorem prover Z3 and present some preliminary results.

Creator

• Trivedi, Ashutosh
• Krishna, Shankara Narayanan
• Bhave, Devendra

Date Issued

• 2016-12-01

Academic Affiliation

• Computer Science

Journal Title

• Electronic Proceedings in Theoretical Computer Science

Journal Volume

• 232

File Extent

• 65-78

Subject

• QA1-939
• Mathematics
• Electronic computers. Computer science
• B.2.2
• Computer Science
• Systems and Control
• QA75.5-76.95
• Logic in Computer Science
• Formal Languages and Automata Theory

Last Modified

• 2019-12-06

Resource Type

• Article

Rights Statement

• In Copyright

DOI

•  http://dx.doi.org/10.4204/EPTCS.232.9

ISSN

• 2075-2180

Language

• English [eng]

Relationships

Items

Thumbnail	Title	Date Uploaded	Visibility	Actions
	onNonlinearPricesInTimedAutomata.pdf	2019-12-06	Public	Download