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
Basic information
Original name Discrete and Continuous Strategies for Timed-Arc Petri Net Games
Authors JENSEN, Peter G. (208 Denmark), Kim G. LARSEN (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution).
Edition International Journal on Software Tools for Technology Transfer (STTT), Springer, 2018, 1433-2779.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 10200 1.2 Computer and information sciences
Country of publisher Netherlands
Confidentiality degree is not subject to a state or trade secret
Impact factor Impact factor: 1.270
RIV identification code RIV/00216224:14330/18:00102444
Organization unit Faculty of Informatics
Doi http://dx.doi.org/10.1007/s10009-017-0473-2
UT WoS 000441949300004
Keywords in English timed-ard Petri nets; games; continuous and discrete time; strategy synthesis
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 29/4/2019 15:33.
Abstract
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.
PrintDisplayed: 10/10/2024 18:31