Model checking meets probability: a gentle introduction

Research output: Chapter in Book/Report/Conference proceedingChapter

  • 5 Citations

Abstract

This paper considers fully probabilistic system models. Each transition is quantified with a probability—its likelihood of occurrence. Properties are expressed as automata that either accept or reject system runs. The central question is to determine the fraction of accepted system runs. We also consider probabilistic timed system models. Their properties are timed automata that accept timed runs iff all timing constraints resent in the automaton are met; otherwise it rejects. The central question is to determine the fraction of accepted timed system runs.
LanguageUndefined
Title of host publicationEngineering Dependable Software Systems
Place of PublicationAmsterdam
PublisherIOS Press
Pages177-205
Number of pages29
ISBN (Print)978-1-61499-206-6
DOIs
StatePublished - 2013

Publication series

NameNATO Science for Peace and Security Series - D: Information and Communication Security
PublisherIOS Press
No.34
Volume34
ISSN (Print)1874-6268

Keywords

  • EWI-23887
  • IR-88331
  • METIS-300115

Cite this

Katoen, J. P. (2013). Model checking meets probability: a gentle introduction. In Engineering Dependable Software Systems (pp. 177-205). (NATO Science for Peace and Security Series - D: Information and Communication Security; Vol. 34, No. 34). Amsterdam: IOS Press. DOI: 10.3233/978-1-61499-207-3-177
Katoen, Joost P./ Model checking meets probability: a gentle introduction. Engineering Dependable Software Systems. Amsterdam : IOS Press, 2013. pp. 177-205 (NATO Science for Peace and Security Series - D: Information and Communication Security; 34).
@inbook{85388e3509c140fc9831b10e473a7ffb,
title = "Model checking meets probability: a gentle introduction",
abstract = "This paper considers fully probabilistic system models. Each transition is quantified with a probability—its likelihood of occurrence. Properties are expressed as automata that either accept or reject system runs. The central question is to determine the fraction of accepted system runs. We also consider probabilistic timed system models. Their properties are timed automata that accept timed runs iff all timing constraints resent in the automaton are met; otherwise it rejects. The central question is to determine the fraction of accepted timed system runs.",
keywords = "EWI-23887, IR-88331, METIS-300115",
author = "Katoen, {Joost P.}",
note = "10.3233/978-1-61499-207-3-177",
year = "2013",
doi = "10.3233/978-1-61499-207-3-177",
language = "Undefined",
isbn = "978-1-61499-206-6",
series = "NATO Science for Peace and Security Series - D: Information and Communication Security",
publisher = "IOS Press",
number = "34",
pages = "177--205",
booktitle = "Engineering Dependable Software Systems",

}

Katoen, JP 2013, Model checking meets probability: a gentle introduction. in Engineering Dependable Software Systems. NATO Science for Peace and Security Series - D: Information and Communication Security, no. 34, vol. 34, IOS Press, Amsterdam, pp. 177-205. DOI: 10.3233/978-1-61499-207-3-177

Model checking meets probability: a gentle introduction. / Katoen, Joost P.

Engineering Dependable Software Systems. Amsterdam : IOS Press, 2013. p. 177-205 (NATO Science for Peace and Security Series - D: Information and Communication Security; Vol. 34, No. 34).

Research output: Chapter in Book/Report/Conference proceedingChapter

TY - CHAP

T1 - Model checking meets probability: a gentle introduction

AU - Katoen,Joost P.

N1 - 10.3233/978-1-61499-207-3-177

PY - 2013

Y1 - 2013

N2 - This paper considers fully probabilistic system models. Each transition is quantified with a probability—its likelihood of occurrence. Properties are expressed as automata that either accept or reject system runs. The central question is to determine the fraction of accepted system runs. We also consider probabilistic timed system models. Their properties are timed automata that accept timed runs iff all timing constraints resent in the automaton are met; otherwise it rejects. The central question is to determine the fraction of accepted timed system runs.

AB - This paper considers fully probabilistic system models. Each transition is quantified with a probability—its likelihood of occurrence. Properties are expressed as automata that either accept or reject system runs. The central question is to determine the fraction of accepted system runs. We also consider probabilistic timed system models. Their properties are timed automata that accept timed runs iff all timing constraints resent in the automaton are met; otherwise it rejects. The central question is to determine the fraction of accepted timed system runs.

KW - EWI-23887

KW - IR-88331

KW - METIS-300115

U2 - 10.3233/978-1-61499-207-3-177

DO - 10.3233/978-1-61499-207-3-177

M3 - Chapter

SN - 978-1-61499-206-6

T3 - NATO Science for Peace and Security Series - D: Information and Communication Security

SP - 177

EP - 205

BT - Engineering Dependable Software Systems

PB - IOS Press

CY - Amsterdam

ER -

Katoen JP. Model checking meets probability: a gentle introduction. In Engineering Dependable Software Systems. Amsterdam: IOS Press. 2013. p. 177-205. (NATO Science for Peace and Security Series - D: Information and Communication Security; 34). Available from, DOI: 10.3233/978-1-61499-207-3-177