Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata

Marta Kwiatkowska, Gethin Norman, David Parker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

182 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationKiMfest
Subtitle of host publicationA conference in honour of Kim G. Larsen on the occasion of his 60th birthday
PublisherSpringer
Pages289-309
Number of pages21
ISBN (Electronic)978-3-319-63121-9
ISBN (Print)978-3-319-63120-2
DOIs
Publication statusPublished - 25 Jul 2017
EventKiMfest: A conference in honour of Kim G. Larsen on the occasion of his 60th birthday - Aalborg, Denmark
Duration: 19 Aug 201720 Aug 2017

Publication series

NameLecture Notes in Computer Science
Volume10460
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceKiMfest
Country/TerritoryDenmark
CityAalborg
Period19/08/1720/08/17

Fingerprint

Dive into the research topics of 'Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata'. Together they form a unique fingerprint.

Cite this