On Nonlinear Prices in Timed Automata

被引：4

作者：

Bhave, Devendra ^{[1
]}

Krishna, Shankara Narayanan ^{[1
]}

Trivedi, Ashutosh ^{[2
]}

机构：

[1] Indian Inst Technol, Bombay, Maharashtra, India

[2] CU Boulder, Boulder, CO USA

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2016年 / 232期

基金：

美国国家科学基金会;

关键词：

MODEL CHECKING;

D O I：

10.4204/EPTCS.232.9

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：65 / 78

页数：14

共 17 条

[1] A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[2] Optimal paths in weighted timed automata [J].

Alur, R ;

La Torre, S ;

Pappas, GJ .

THEORETICAL COMPUTER SCIENCE, 2004, 318 (03) :297-322

[3]

[Anonymous], 1967, Computation

[4]

Audemard G, 2002, LECT NOTES COMPUT SC, V2529, P243

[5]

Behrmann G., 2001, Hybrid Systems: Computation and Control. 4th International Workshop, HSCC 2001. Proceedings (Lecture Notes in Computer Science Vol.2034), P147

[6]

Behrmann G., 2005, Performance Evaluation Review, V32, P34, DOI 10.1145/1059816.1059823

[7]

Bouyer P, 2004, LECT NOTES COMPUT SC, V2993, P203

[8] On the optimal reachability problem of weighted timed automata [J].