PRICED TIMED PETRINETS

被引:11
作者
Abdulla, Parosh Aziz [1 ]
Mayr, Richard [2 ]
机构
[1] Uppsala Univ, Dept Informat Technol, SE-75105 Uppsala, Sweden
[2] Univ Edinburgh, Sch Informat, Edinburgh EH89AB, Midlothian, Scotland
关键词
Formal verification; Petrinets; Timed Automata; REACHABILITY; AUTOMATA; PROGRAMS; PERFECT;
D O I
10.2168/LMCS-9(4:10)2013
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We consider priced timed Petrinets, i.e., unbounded Petrinets where each token carries areal-valued clock. Transition arcs are labeled with time intervals, which specify constraints on the ages of tokens. Furthermore, our cost model assigns token storage costs per time unit to places, and firing costs to transitions. This general model strictly subsumes both priced timed automata and unbounded priced Petri nets. We study the cost of computations that reach a given control-state. In general, a computation with minimal cost may not exist, due to strict inequalities in the time constraints. However, we show that the infimum of the costs to reach a given control-state is computable in the case where all place and transition costs are non-negative. On the other hand, if negative costs are allowed, then the question whether a given control-state is reachable with zero overall cost becomes undecidable. Infact, this negative result holds even in the simpler case of discretet ime(i.e., integer-valuedclocks).
引用
收藏
页数:51
相关论文
共 36 条
[1]  
Abdulla P., 2009, LNCS, V5504
[2]  
Abdulla P. A., 2001, Applications and Theory of Petri Nets 2001. 22nd International Conference, ICATPN 2001. Proceedings (Lecture Notes in Computer Science Vol.2075), P53
[3]  
Abdulla P.A., 2002, INFINITY 2002
[4]  
Abdulla P.A., 2011, 26 ANN IEEE S LOG CO
[5]  
Abdulla P. A., 2007, LOGICAL METHODS COMP, V3
[6]  
Abdulla PA, 2004, LECT NOTES COMPUT SC, V3253, P343
[7]   Verifying programs with unreliable channels [J].
Abdulla, PA ;
Jonsson, B .
INFORMATION AND COMPUTATION, 1996, 127 (02) :91-101
[8]   Algorithmic analysis of programs with well quasi-ordered domains [J].
Abdulla, PA ;
Cerans, K ;
Jonsson, B ;
Tsay, YK .
INFORMATION AND COMPUTATION, 2000, 160 (1-2) :109-127
[9]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[10]   Optimal paths in weighted timed automata [J].
Alur, R ;
La Torre, S ;
Pappas, GJ .
THEORETICAL COMPUTER SCIENCE, 2004, 318 (03) :297-322