Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00094044" target="_blank" >RIV/00216224:14330/16:00094044 - isvavai.cz</a>
Result on the web
<a href="http://link.springer.com/chapter/10.1007%2F978-3-319-32582-8_9" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-319-32582-8_9</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-32582-8_9" target="_blank" >10.1007/978-3-319-32582-8_9</a>
Alternative languages
Result language
angličtina
Original language name
Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the 23rd International SPIN Symposium on Model Checking of Software (SPIN'16)
ISBN
9783319325811
ISSN
0302-9743
e-ISSN
—
Number of pages
18
Pages from-to
129-146
Publisher name
Springer
Place of publication
Netherlands
Event location
Netherlands
Event date
Jan 1, 2016
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—