Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.14/29233
23 Visitors
25 Hits
0 Downloads
- Title
- Quantitative refinement and model checking for the analysis of probabilistic systems
- Related
- FM 2006 : International Symposium on Formal Methods (14th : 2006) (21 - 27 August 2006 : Hamilton, Canada)
- Related
- Misra, Jayadev; Nipkow, Tobias and Sekerinski, Emil. FM 2006 : Formal methods. Proceedings of 14th international symposium on formal methods, p.131-146
- DOI
- 10.1007/11813040_10
- Related
- Lecture notes in computer science Vol. 4085
- Publisher
- Berlin, Germany : Springer-Verlag
- Date
- 2006
- Author/Creator
- McIver, A. K
- Description
- 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].
- Description
- 16 page(s)
- Subject Keyword
- probabilistic abstraction and refinement
- Subject Keyword
- structured specification and analysis of performance
- Subject Keyword
- probabilistic model checking
- Resource Type
- conference paper
- Organisation
- Macquarie University. Dept. of Computing
- Identifier
- http://hdl.handle.net/1959.14/29233
- Identifier
- ISBN:9783540372158
- Identifier
- ISSN:1611-3349
- Identifier
- mq-rm-2006003301
- Language
- eng
- Reviewed
List Of Titles
