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].
Bouyer, Patricia ;
Brihaye, Thomas ;
Bruyere, Veronique ;
Raskin, Jean-Francois .
FORMAL METHODS IN SYSTEM DESIGN, 2007, 31 (02) :135-175
[9]  
Bouyer P, 2010, HSSC 10: PROCEEDINGS OF THE 13TH ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, P61
[10]   Discount-Optimal Infinite Runs in Priced Timed Automata [J].
Fahrenberg, Uli ;
Larsen, Kim G. .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 239 (0C) :179-191