Efficient simulation-based verification of probabilistic timed automata

Arnd Hartmanns, Sean Sedwards, Pedro R. d' Argenio

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

  • 1 Citations

Abstract

Probabilistic timed automata are a formal model for real-time systems with discrete probabilistic and nondeterministic choices. To overcome the state space explosion problem of exhaustive verification, a symbolic simulation-based approach that soundly treats nondeterminism to approximate maximum and minimum reachability probabilities has recently become available. Its use of difference-bound matrices to handle continuous real time however leads to poor performance: most operations are cubic or even exponential in the number of clock variables. In this paper, we propose a novel region-based approach and data structure that reduce the complexity of all operations to being linear. It relies on a particular mapping between symbolic regions and concrete representative valuations. Using an implementation within the MODEST TOOLSET, we show that the new approach is not only easier to implement, but indeed significantly outperforms all current alternatives on standard benchmark models.
LanguageEnglish
Title of host publicationProceedings of the 2017 Winter Simulation Conference
Subtitle of host publicationLas Vegas, NV, USA, December 3-6, 2017
EditorsW.K.V. Chan, A. D’Ambrogio, G. Zacharewicz, N. Mustafee, G. Wainer, E. Page
PublisherInstitute of Electrical and Electronics Engineers
Pages1419-1430
Number of pages12
ISBN (Electronic)978-1-5386-3428-8
ISBN (Print)978-1-5386-3430-1
DOIs
StatePublished - 2017
Event2017 Winter Simulation Conference - Las Vegas, United States
Duration: 3 Dec 20176 Dec 2017

Publication series

NameProceedings Winter Simulation Conference (WSC)
PublisherIEEE
ISSN (Print)1558-4305

Conference

Conference2017 Winter Simulation Conference
Abbreviated titleWSC 2017
CountryUnited States
CityLas Vegas
Period3/12/176/12/17

Fingerprint

Real time systems
Explosions
Data structures
Clocks
Concretes

Cite this

Hartmanns, A., Sedwards, S., & d' Argenio, P. R. (2017). Efficient simulation-based verification of probabilistic timed automata. In W. K. V. Chan, A. D’Ambrogio, G. Zacharewicz, N. Mustafee, G. Wainer, & E. Page (Eds.), Proceedings of the 2017 Winter Simulation Conference: Las Vegas, NV, USA, December 3-6, 2017 (pp. 1419-1430). (Proceedings Winter Simulation Conference (WSC)). Institute of Electrical and Electronics Engineers. DOI: 10.1109/WSC.2017.8247885
Hartmanns, Arnd ; Sedwards, Sean ; d' Argenio, Pedro R./ Efficient simulation-based verification of probabilistic timed automata. Proceedings of the 2017 Winter Simulation Conference: Las Vegas, NV, USA, December 3-6, 2017. editor / W.K.V. Chan ; A. D’Ambrogio ; G. Zacharewicz ; N. Mustafee ; G. Wainer ; E. Page. Institute of Electrical and Electronics Engineers, 2017. pp. 1419-1430 (Proceedings Winter Simulation Conference (WSC)).
@inproceedings{1041b5cfe8854922b1f8cfa2d018d1b4,
title = "Efficient simulation-based verification of probabilistic timed automata",
abstract = "Probabilistic timed automata are a formal model for real-time systems with discrete probabilistic and nondeterministic choices. To overcome the state space explosion problem of exhaustive verification, a symbolic simulation-based approach that soundly treats nondeterminism to approximate maximum and minimum reachability probabilities has recently become available. Its use of difference-bound matrices to handle continuous real time however leads to poor performance: most operations are cubic or even exponential in the number of clock variables. In this paper, we propose a novel region-based approach and data structure that reduce the complexity of all operations to being linear. It relies on a particular mapping between symbolic regions and concrete representative valuations. Using an implementation within the MODEST TOOLSET, we show that the new approach is not only easier to implement, but indeed significantly outperforms all current alternatives on standard benchmark models.",
author = "Arnd Hartmanns and Sean Sedwards and {d' Argenio}, {Pedro R.}",
year = "2017",
doi = "10.1109/WSC.2017.8247885",
language = "English",
isbn = "978-1-5386-3430-1",
series = "Proceedings Winter Simulation Conference (WSC)",
publisher = "Institute of Electrical and Electronics Engineers",
pages = "1419--1430",
editor = "W.K.V. Chan and A. D’Ambrogio and G. Zacharewicz and N. Mustafee and G. Wainer and E. Page",
booktitle = "Proceedings of the 2017 Winter Simulation Conference",
address = "United States",

}

Hartmanns, A, Sedwards, S & d' Argenio, PR 2017, Efficient simulation-based verification of probabilistic timed automata. in WKV Chan, A D’Ambrogio, G Zacharewicz, N Mustafee, G Wainer & E Page (eds), Proceedings of the 2017 Winter Simulation Conference: Las Vegas, NV, USA, December 3-6, 2017. Proceedings Winter Simulation Conference (WSC), Institute of Electrical and Electronics Engineers, pp. 1419-1430, 2017 Winter Simulation Conference, Las Vegas, United States, 3/12/17. DOI: 10.1109/WSC.2017.8247885

Efficient simulation-based verification of probabilistic timed automata. / Hartmanns, Arnd ; Sedwards, Sean; d' Argenio, Pedro R.

Proceedings of the 2017 Winter Simulation Conference: Las Vegas, NV, USA, December 3-6, 2017. ed. / W.K.V. Chan; A. D’Ambrogio; G. Zacharewicz; N. Mustafee; G. Wainer; E. Page. Institute of Electrical and Electronics Engineers, 2017. p. 1419-1430 (Proceedings Winter Simulation Conference (WSC)).

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

TY - GEN

T1 - Efficient simulation-based verification of probabilistic timed automata

AU - Hartmanns,Arnd

AU - Sedwards,Sean

AU - d' Argenio,Pedro R.

PY - 2017

Y1 - 2017

N2 - Probabilistic timed automata are a formal model for real-time systems with discrete probabilistic and nondeterministic choices. To overcome the state space explosion problem of exhaustive verification, a symbolic simulation-based approach that soundly treats nondeterminism to approximate maximum and minimum reachability probabilities has recently become available. Its use of difference-bound matrices to handle continuous real time however leads to poor performance: most operations are cubic or even exponential in the number of clock variables. In this paper, we propose a novel region-based approach and data structure that reduce the complexity of all operations to being linear. It relies on a particular mapping between symbolic regions and concrete representative valuations. Using an implementation within the MODEST TOOLSET, we show that the new approach is not only easier to implement, but indeed significantly outperforms all current alternatives on standard benchmark models.

AB - Probabilistic timed automata are a formal model for real-time systems with discrete probabilistic and nondeterministic choices. To overcome the state space explosion problem of exhaustive verification, a symbolic simulation-based approach that soundly treats nondeterminism to approximate maximum and minimum reachability probabilities has recently become available. Its use of difference-bound matrices to handle continuous real time however leads to poor performance: most operations are cubic or even exponential in the number of clock variables. In this paper, we propose a novel region-based approach and data structure that reduce the complexity of all operations to being linear. It relies on a particular mapping between symbolic regions and concrete representative valuations. Using an implementation within the MODEST TOOLSET, we show that the new approach is not only easier to implement, but indeed significantly outperforms all current alternatives on standard benchmark models.

U2 - 10.1109/WSC.2017.8247885

DO - 10.1109/WSC.2017.8247885

M3 - Conference contribution

SN - 978-1-5386-3430-1

T3 - Proceedings Winter Simulation Conference (WSC)

SP - 1419

EP - 1430

BT - Proceedings of the 2017 Winter Simulation Conference

PB - Institute of Electrical and Electronics Engineers

ER -

Hartmanns A, Sedwards S, d' Argenio PR. Efficient simulation-based verification of probabilistic timed automata. In Chan WKV, D’Ambrogio A, Zacharewicz G, Mustafee N, Wainer G, Page E, editors, Proceedings of the 2017 Winter Simulation Conference: Las Vegas, NV, USA, December 3-6, 2017. Institute of Electrical and Electronics Engineers. 2017. p. 1419-1430. (Proceedings Winter Simulation Conference (WSC)). Available from, DOI: 10.1109/WSC.2017.8247885