article

Abstraction and refinement in probabilistic systems

Authors:

Annabelle McIver,

Carroll MorganAuthors Info & Claims

ACM SIGMETRICS Performance Evaluation Review, Volume 32, Issue 4

Pages 41 - 47

https://doi.org/10.1145/1059816.1059824

Published: 01 March 2005 Publication History

Abstract

We summarise a verification method for probabilistic systems that is based on abstraction and refinement, and extends traditional assertional styles of verification.The approach makes extensive use of the expectation transformers of pGCL [17, 16, 13], a compact probabilistic programming language with an associated logic of real-valued functions. Analysis of large systems is made tractable by abstraction which, together with algebraic and logical reasoning, results in strong and general guarantees about probabilistic-system properties.Although our examples are specific (to pGCL), our overall goal in this note is to advocate the hierarchical development of probabilistic programs via levels of abstraction, connected by refinement, and to illustrate the proof obligations incurred by such an approach.

References

[1]

O. Celiku and A. McIver. Cost-based analysis of probabilistic programs mechanised in HOL. Nordic Journal of Computing, 11(2):102--128, 2004.

Digital Library

[2]

E. Dijkstra. A Discipline of Programming. Prentice Hall International, Englewood Cliffs, N.J., 1976.

Digital Library

[3]

Y. A. Feldman and D. Harel. A probabilistic dynamic logic. J. Computing and System Sciences, 28:193--215, 1984.

[4]

A. Giacalone, C.-C. Jou, and S. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proc. IFIP WG 2.2/2.3 Working Conf., pages 443--58, Apr. 1990.

[5]

H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512--35, 1994.

Digital Library

[6]

S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent programs. ACM Trans. Prog. Lang. Syst., 5:356--80, 1983.

Digital Library

[7]

J. He, K. Seidel, and A. McIver. Probabilistic models for the guarded command language. Sci. Comput. Programming, 28:171--92, 1997. Available at {14, key HSM95}.

Digital Library

[8]

J. Hurd, A. McIver, and C. Morgan. Probabilistic guarded commands mechanised in HOL. To appear in Proc. QAPL '04 (ETAPS), 2005.

[9]

D. Kozen. A probabilistic PDL. Jnl. Comp. Sys. Sciences, 30(2):162--78, 1985.

[10]

M. Kwiatkowska. Model checking for probability and time: from theory to practice. In P. G. Kolaitis, editor, Proc. Eighteenth Annual IEEE Symp. on Logic in Computer Science, LICS 2003, pages 351--360. IEEE Computer Society Press, June 2003.

Digital Library

[11]

M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2):128--142, 2004.

Digital Library

[12]

A. McIver. Quantitative program logic and expected time bounds in probabilistic distributed algorithms. Theoretical Comput. Sci., 282(1):191--219, 2002.

Digital Library

[13]

A. McIver and C. Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Technical Monographs in Computer Science. Springer Verlag, New York, 2004.

Digital Library

[14]

A. McIver, C. Morgan, J. Sanders, and K. Seidel. Probabilistic Systems Group: Collected reports. web.comlab.ox.ac.uk/oucl/research/areas/probs.

[15]

C. Morgan. Proof rules for probabilistic loops. In H. Jifeng, J. Cooke, and P. Wallis, editors, Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing. Springer Verlag, July 1996. ewic.bcs.org/conferences/1996/. ..refinement/papers/paper10.htm.

Digital Library

[16]

C. Morgan and A. McIver. pGCL: Formal reasoning for random algorithms. South African Computer Journal, 22, Mar. 1999. Available at {14, key pGCL}.

[17]

C. Morgan, A. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Trans. Prog. Lang. Syst., 18(3):325--53, May 1996. doi.acm.org/10.1145/229542.229547.

Digital Library

[18]

P. Whittle. Probability via Expectation. Springer Texts in Statistics. Springer Verlag, third edition, 1992.

Cited By

Feng SYang TChen MZhan N(2024)A Unified Framework for Quantitative Analysis of Probabilistic ProgramsPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_10(230-254)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_10
Matheja C(2024)A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVLBridging the Gap Between AI and Reality10.1007/978-3-031-75434-0_17(242-258)Online publication date: 30-Dec-2024
https://doi.org/10.1007/978-3-031-75434-0_17
Avanzini MMoser GPéchoux RPerdrix S(2024)On the Hardness of Analyzing Quantum Programs QuantitativelyProgramming Languages and Systems10.1007/978-3-031-57267-8_2(31-58)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_2
Show More Cited By

Index Terms

Abstraction and refinement in probabilistic systems

Recommendations

Abstraction refinement for termination
SAS'05: Proceedings of the 12th international conference on Static Analysis

Abstraction can often lead to spurious counterexamples. Counterexample-guided abstraction refinement is a method of strengthening abstractions based on the analysis of these spurious counterexamples. For invariance properties, a counterexample is a ...
SAT-based Abstraction Refinement for Real-time Systems

In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. We present a faithful embedding of bounded model checking for systems of timed automata into propositional logic ...
Compositional Abstraction Refinement for Timed Systems
TASE '10: Proceedings of the 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering

Model checking suffers from the state explosion problem. Compositional abstraction and abstraction refinement have been investigated in many areas to address this problem. This paper considers the compositional model checking for timed systems. We ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGMETRICS Performance Evaluation Review

ACM SIGMETRICS Performance Evaluation Review Volume 32, Issue 4

March 2005

45 pages

ISSN:0163-5999

DOI:10.1145/1059816

Issue’s Table of Contents

Copyright © 2005 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 2005

Published in SIGMETRICS Volume 32, Issue 4

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

50
Total Citations
View Citations
262
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Feng SYang TChen MZhan N(2024)A Unified Framework for Quantitative Analysis of Probabilistic ProgramsPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_10(230-254)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_10
Matheja C(2024)A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVLBridging the Gap Between AI and Reality10.1007/978-3-031-75434-0_17(242-258)Online publication date: 30-Dec-2024
https://doi.org/10.1007/978-3-031-75434-0_17
Avanzini MMoser GPéchoux RPerdrix S(2024)On the Hardness of Analyzing Quantum Programs QuantitativelyProgramming Languages and Systems10.1007/978-3-031-57267-8_2(31-58)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_2
Avanzini MMoser GSchaper M(2023)Automated Expected Value Analysis of Recursive ProgramsProceedings of the ACM on Programming Languages10.1145/35912637:PLDI(1050-1072)Online publication date: 6-Jun-2023
https://doi.org/10.1145/3591263
Batz KChen MJunges SKaminski BKatoen JMatheja C(2023)Probabilistic Program Verification via Inductive Synthesis of Inductive InvariantsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30820-8_25(410-429)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30820-8_25
Deng YFeng Y(2022)Formal semantics of a classical-quantum languageTheoretical Computer Science10.1016/j.tcs.2022.02.017913(73-93)Online publication date: Apr-2022
https://doi.org/10.1016/j.tcs.2022.02.017
Pardo RJohnsen ESchaefer IWąsowski A(2022)A Specification Logic for Programs in the Probabilistic Guarded Command LanguageTheoretical Aspects of Computing – ICTAC 202210.1007/978-3-031-17715-6_24(369-387)Online publication date: 3-Oct-2022
https://doi.org/10.1007/978-3-031-17715-6_24
Batz KFesefeldt IJansen MKatoen JKeßler FMatheja CNoll T(2022)Foundations for Entailment Checking in Quantitative Separation LogicProgramming Languages and Systems10.1007/978-3-030-99336-8_3(57-84)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_3
AFFELDT RGARRIGUE JNOWAK DSAIKAWA T(2021)A trustful monad for axiomatic reasoning with probability and nondeterminismJournal of Functional Programming10.1017/S095679682100013731Online publication date: 15-Jul-2021
https://doi.org/10.1017/S0956796821000137
Batz KChen MKaminski BKatoen JMatheja CSchröer P(2021)Latticed k-Induction with an Application to Probabilistic ProgramsComputer Aided Verification10.1007/978-3-030-81688-9_25(524-549)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_25
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents