JENSEN, Peter G., Kim G. LARSEN and Jiří SRBA. Discrete and Continuous Strategies for Timed-Arc Petri Net Games. International Journal on Software Tools for Technology Transfer (STTT). Springer, 2018, vol. 20, No 5, p. 529-546. ISSN 1433-2779. Available from: https://dx.doi.org/10.1007/s10009-017-0473-2. |
Other formats:
BibTeX
LaTeX
RIS
@article{1412005, author = {Jensen, Peter G. and Larsen, Kim G. and Srba, Jiří}, article_number = {5}, doi = {http://dx.doi.org/10.1007/s10009-017-0473-2}, keywords = {timed-ard Petri nets; games; continuous and discrete time; strategy synthesis}, language = {eng}, issn = {1433-2779}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, title = {Discrete and Continuous Strategies for Timed-Arc Petri Net Games}, volume = {20}, year = {2018} }
TY - JOUR ID - 1412005 AU - Jensen, Peter G. - Larsen, Kim G. - Srba, Jiří PY - 2018 TI - Discrete and Continuous Strategies for Timed-Arc Petri Net Games JF - International Journal on Software Tools for Technology Transfer (STTT) VL - 20 IS - 5 SP - 529-546 EP - 529-546 PB - Springer SN - 14332779 KW - timed-ard Petri nets KW - games KW - continuous and discrete time KW - strategy synthesis N2 - Automatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of real-time reactive systems. The existing symbolic approach for continuous timed game is a computationally hard task and current tools like UPPAAL TiGa often scale poorly with the model complexity. We suggest an explicit approach for strategy synthesis in the discrete-time setting and show that even for systems with closed guards, the existence of a safety discrete-time strategy does not imply the existence of a safety continuous-time strategy and vice versa. Nevertheless, we prove that the answers to the existence of discrete-time and continuous-time safety strategies coincide on a practically motivated subclass of urgent controllers that either react immediately after receiving an environmental input or wait with the decision until a next event is triggered by the environment. We then develop an on-the-fly synthesis algorithm for discrete timed-arc Petri net games. The algorithm is implemented in our tool TAPAAL, and based on the experimental evidence, we discuss the advantages of our approach compared to the symbolic continuous-time techniques. ER -
JENSEN, Peter G., Kim G. LARSEN and Jiří SRBA. Discrete and Continuous Strategies for Timed-Arc Petri Net Games. \textit{International Journal on Software Tools for Technology Transfer (STTT)}. Springer, 2018, vol.~20, No~5, p.~529-546. ISSN~1433-2779. Available from: https://dx.doi.org/10.1007/s10009-017-0473-2.
|