Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization

JENSEN, Peter G., Kim G. LARSEN and Jiří SRBA. Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization. Online. In Proceedings of the 23rd International SPIN Symposium on Model Checking of Software (SPIN'16). Netherlands: Springer, 2016. p. 129-146. ISBN 978-3-319-32581-1. Available from: https://dx.doi.org/10.1007/978-3-319-32582-8_9. [citováno 2024-04-23]

Basic information

• Original name: Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization
• Authors: JENSEN, Peter G. (208 Denmark), Kim G. LARSEN (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution)
• Edition: Netherlands, Proceedings of the 23rd International SPIN Symposium on Model Checking of Software (SPIN'16), p. 129-146, 18 pp. 2016.
• Publisher: Springer

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Netherlands
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: printed version "print"
• WWW: URL
• Impact factor: Impact factor: 0.402 in 2005
• RIV identification code: RIV/00216224:14330/16:00094044
• Organization unit: Faculty of Informatics
• ISBN: 978-3-319-32581-1
• ISSN: 0302-9743
• Doi: http://dx.doi.org/10.1007/978-3-319-32582-8_9
• Keywords in English: strategy synthesis; timed models; Petri nets; discretization
• Tags: firank_B

Abstract

Automatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of reactive systems. The existing symbolic approach for continuous timed games 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.