Symbolic model checking for probabilistic timed automata

Research output: Contribution to journalArticle

Standard

Symbolic model checking for probabilistic timed automata. / Kwiatkowska, Marta; Norman, Gethin; Sproston, Jeremy; Wang, F.

In: Information and Computation, Vol. 205, No. 7, 01.07.2007, p. 1027-1077.

Research output: Contribution to journalArticle

Harvard

APA

Vancouver

Author

Bibtex

@article{7388333e79b64dc78da6b72299e60487,
title = "Symbolic model checking for probabilistic timed automata",
abstract = "Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton's clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies. (c) 2007 Elsevier Inc. All rights reserved.",
author = "Marta Kwiatkowska and Gethin Norman and Jeremy Sproston and F Wang",
year = "2007",
month = jul,
day = "1",
doi = "10.1016/j.ic.2007.01.004",
language = "English",
volume = "205",
pages = "1027--1077",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier",
number = "7",

}

RIS

TY - JOUR

T1 - Symbolic model checking for probabilistic timed automata

AU - Kwiatkowska, Marta

AU - Norman, Gethin

AU - Sproston, Jeremy

AU - Wang, F

PY - 2007/7/1

Y1 - 2007/7/1

N2 - Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton's clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies. (c) 2007 Elsevier Inc. All rights reserved.

AB - Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton's clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies. (c) 2007 Elsevier Inc. All rights reserved.

U2 - 10.1016/j.ic.2007.01.004

DO - 10.1016/j.ic.2007.01.004

M3 - Article

VL - 205

SP - 1027

EP - 1077

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 7

ER -