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

D 2016

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

JENSEN, Peter G., Kim G. LARSEN and Jiří SRBA

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

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

DOI

http://dx.doi.org/10.1007/978-3-319-32582-8_9

Keywords in English

strategy synthesis; timed models; Petri nets; discretization

Abstract

V originále

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.

Citovat

JENSEN, Peter G., Kim G. LARSEN and Jiří SRBA. Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization. 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.

@inproceedings{1376938,
   author = {Jensen, Peter G. and Larsen, Kim G. and Srba, Jiří},
   address = {Netherlands},
   booktitle = {Proceedings of the 23rd International SPIN Symposium on Model Checking of Software (SPIN'16)},
   doi = {http://dx.doi.org/10.1007/978-3-319-32582-8_9},
   keywords = {strategy synthesis; timed models; Petri nets; discretization},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Netherlands},
   isbn = {978-3-319-32581-1},
   pages = {129-146},
   publisher = {Springer},
   title = {Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization},
   url = {http://link.springer.com/chapter/10.1007%2F978-3-319-32582-8_9},
   year = {2016}
}

TY  - JOUR
ID  - 1376938
AU  - Jensen, Peter G. - Larsen, Kim G. - Srba, Jiří
PY  - 2016
TI  - Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization
PB  - Springer
CY  - Netherlands
SN  - 9783319325811
KW  - strategy synthesis
KW  - timed models
KW  - Petri nets
KW  - discretization
UR  - http://link.springer.com/chapter/10.1007%2F978-3-319-32582-8_9
L2  - http://link.springer.com/chapter/10.1007%2F978-3-319-32582-8_9
N2  - 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.
ER  -

JENSEN, Peter G., Kim G. LARSEN and Jiří SRBA. Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization. In \textit{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.

Detailed Information on Publication Record