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 a Jiří SRBA

Základní údaje

Originální název

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

Autoři

JENSEN, Peter G. (208 Dánsko), Kim G. LARSEN (208 Dánsko) a Jiří SRBA (203 Česká republika, garant, domácí)

Vydání

Netherlands, Proceedings of the 23rd International SPIN Symposium on Model Checking of Software (SPIN'16), od s. 129-146, 18 s. 2016

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00094044

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-32581-1

ISSN

DOI

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

Klíčová slova anglicky

strategy synthesis; timed models; Petri nets; discretization

Štítky

firank_B

Změněno: 30. 3. 2017 22:30, Prof. Jiří Srba, Ph.D.

Anotace

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 a 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, s. 129-146. ISBN 978-3-319-32581-1. Dostupné z: 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 a 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, s.~129-146. ISBN~978-3-319-32581-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-32582-8\_{}9.

Podrobný výpis o publikaci