Quantitative refinement and model checking for the analysis of probabilistic systems

A. K. McIver*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

6 Citations (Scopus)

Abstract

For standard (ie non-probabilistic) systems of reasonable size, correctness is analysed by simulation and/or model checking, possibly with standard program-logical arguments beforehand to reduce the problem size by abstraction. For probabilistic systems there are model checkers and simulators too; but probabilistic program logics are rarer. Thus e.g. model checkers face more severe exposure to state explosion because "front-end" probabilistic abstraction techniques are not so widely known [18]. We formalise probabilistic refinement of action systems [3] in order to provide just such a front end, and we illustrate with the probabilistic model checker PRISM [21] how it can be used to reduce state explosion. The case study is based on a performance analysis of randomised backoff in wireless communication [1].

Original languageEnglish
Title of host publicationFM 2006: Formal Methods - 14th International Symposium on Formal Methods, Proceedings
EditorsJayadev Misra, Tobias Nipkow, Emil Sekerinski
Place of PublicationBerlin; New York
PublisherSpringer, Springer Nature
Pages131-146
Number of pages16
Volume4085 LNCS
ISBN (Electronic)9783540372165
ISBN (Print)3540372156, 9783540372158
DOIs
Publication statusPublished - 2006
EventFM 2006: 14th International Symposium on Formal Methods - Hamilton, Canada
Duration: 21 Aug 200627 Aug 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4085 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

OtherFM 2006: 14th International Symposium on Formal Methods
Country/TerritoryCanada
CityHamilton
Period21/08/0627/08/06

Fingerprint

Dive into the research topics of 'Quantitative refinement and model checking for the analysis of probabilistic systems'. Together they form a unique fingerprint.

Cite this