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

Tags

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

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.
Displayed: 9/11/2024 01:29