TY - GEN

T1 - Verification and Performance Evaluation of Timed Game Strategies

AU - David, Alexandre

AU - Fang, Huixing

AU - Larsen, Kim Guldstrand

AU - Zhang, Zhengkui

PY - 2014

Y1 - 2014

N2 - Control synthesis techniques, based on timed games, derive strategies to ensure a given control objective, e.g., time-bounded reachability. Model checking verifies correctness properties of systems. Statistical model checking can be used to analyse performance aspects of systems, e.g., energy consumption. In this work, we propose to combine these three techniques. In particular, given a strategy synthesized for a timed game and a given control objective, we want to make a deeper examination of the consequences of adopting this strategy. Firstly, we want to apply model checking to the timed game under the synthesized strategy in order to verify additional correctness properties. Secondly, we want to apply statistical model checking to evaluate various performance aspects of the synthesized strategy. For this, the underlying timed game is extended with relevant price and stochastic information. We first explain the principle of translating a strategy produced by Uppaal-tiga into a timed automaton, thus enabling the deeper examination. However, our main contribution is a new extension of Uppaal that automatically synthesizes a strategy of a timed game for a given control objective, then verifies and evaluates this strategy with respect to additional properties. We demonstrate the usefulness of this new branch of Uppaal using two case-studies.

AB - Control synthesis techniques, based on timed games, derive strategies to ensure a given control objective, e.g., time-bounded reachability. Model checking verifies correctness properties of systems. Statistical model checking can be used to analyse performance aspects of systems, e.g., energy consumption. In this work, we propose to combine these three techniques. In particular, given a strategy synthesized for a timed game and a given control objective, we want to make a deeper examination of the consequences of adopting this strategy. Firstly, we want to apply model checking to the timed game under the synthesized strategy in order to verify additional correctness properties. Secondly, we want to apply statistical model checking to evaluate various performance aspects of the synthesized strategy. For this, the underlying timed game is extended with relevant price and stochastic information. We first explain the principle of translating a strategy produced by Uppaal-tiga into a timed automaton, thus enabling the deeper examination. However, our main contribution is a new extension of Uppaal that automatically synthesizes a strategy of a timed game for a given control objective, then verifies and evaluates this strategy with respect to additional properties. We demonstrate the usefulness of this new branch of Uppaal using two case-studies.

U2 - 10.1007/978-3-319-10512-3_8

DO - 10.1007/978-3-319-10512-3_8

M3 - Article in proceeding

SN - 978-3-319-10511-6

VL - 8711

T3 - Lecture Notes in Computer Science

SP - 100

EP - 114

BT - Formal Modeling and Analysis of Timed Systems

A2 - Legay, Axel

A2 - Bozga, Marius

PB - Springer

ER -