TY - GEN
T1 - Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata
AU - Kwiatkowska, Marta
AU - Norman, Gethin
AU - Parker, David
PY - 2017/7/25
Y1 - 2017/7/25
N2 - Probabilistic timed automata are a formalism for modelling systems whose dynamics includes probabilistic, nondeterministic and timed aspects including real-time systems. A variety of techniques have been proposed for the analysis of this formalism and successfully employed to analyse, for example, wireless communication protocols and computer security systems. Augmenting the model with prices (or, equivalently, costs or rewards) provides a means to verify more complex quantitative properties, such as the expected energy usage of a device or the expected number of messages sent during a protocol's execution. However, the analysis of these properties on probabilistic timed automata currently relies on a technique based on integer discretisation of real-valued clocks, which can be expensive in some cases. In this paper, we propose symbolic techniques for verifi cation and optimal strategy synthesis for priced probabilistic timed automata which avoid this discretisation. We build upon recent work for the special case of expected time properties, using value iteration over a zone-based abstraction of the model.
AB - Probabilistic timed automata are a formalism for modelling systems whose dynamics includes probabilistic, nondeterministic and timed aspects including real-time systems. A variety of techniques have been proposed for the analysis of this formalism and successfully employed to analyse, for example, wireless communication protocols and computer security systems. Augmenting the model with prices (or, equivalently, costs or rewards) provides a means to verify more complex quantitative properties, such as the expected energy usage of a device or the expected number of messages sent during a protocol's execution. However, the analysis of these properties on probabilistic timed automata currently relies on a technique based on integer discretisation of real-valued clocks, which can be expensive in some cases. In this paper, we propose symbolic techniques for verifi cation and optimal strategy synthesis for priced probabilistic timed automata which avoid this discretisation. We build upon recent work for the special case of expected time properties, using value iteration over a zone-based abstraction of the model.
UR - http://kimfest.cs.aau.dk/
U2 - 10.1007/978-3-319-63121-9_15
DO - 10.1007/978-3-319-63121-9_15
M3 - Conference contribution
SN - 978-3-319-63120-2
T3 - Lecture Notes in Computer Science
SP - 289
EP - 309
BT - KiMfest
PB - Springer
T2 - KiMfest
Y2 - 19 August 2017 through 20 August 2017
ER -