Article

Quantitative analysis of distributed randomized protocols

Authors:

Christel Baier,

Frank Ciesinski,

Marcus GroesserAuthors Info & Claims

FMICS '05: Proceedings of the 10th international workshop on Formal methods for industrial critical systems

Pages 2 - 7

https://doi.org/10.1145/1081180.1081182

Published: 05 September 2005 Publication History

Abstract

A wide range of coordination protocols for distributed systems, internet protocols or systems with unreliable components can formally be modelled by Markov decision processes (MDP). MDPs can be viewed as a variant of state-transition diagrams with discrete probabilities and nondeterminism. While traditional model checking techniques for non-probabilistic systems aim to establish properties stating that all (or some) computations fulfill a certain condition, the verification problem for randomized systems requires reasoning about the quantitative behavior by means of properties that refer to the probabilities for certain computations, for instance, the probability to find a leader within 5 rounds or the probability for not reaching an error state.The paper starts with a brief introduction into modelling randomized systems with MDPs and the modelling language ProbMela which is a guarded command language with features of imperative languages, nondeterminism, parallelism, a probabilistic choice operator and lossy channels. We summarize the main steps for a quantitative analysis of MDPs against linear temporal logical specifications. The last part will report on the main features of the partial order reduction approach for MDPs and its implementation in the model checker LiQuor.

References

[1]

C. Baier, F. Ciesinski, and M. Grösser. Probmela: a modeling language for communicating probabilistic systems. MEMOCODE'04, pages 57--66. IEEE CS Press, 2004.

[2]

C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. ICALP'97, LNCS 1256, pages 430--440, 1997.

Digital Library

[3]

C. Baier, P. D'Argenio, and M. Grösser. Partial order reduction for probabilistic branching time. QAPL'05, To appear in ENTCS.

Digital Library

[4]

C. Baier, M. Grösser, and F. Ciesinski. Partial order reduction for probabilistic systems. QEST'04, IEEE CS Press, pages 230--239, 2004.

Digital Library

[5]

C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, and M. Siegle, editors. Validation of Stochastic Systems, LNCS 2925, 2003.

[6]

C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125--155, 1998.

Digital Library

[7]

A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. FST & TCS'95, LNCS 1026, pages 499--513, 1995.

Digital Library

[8]

H. Bohnenkamp, H. Hermanns, J.-P. Katoen, and R. Klaren. The modest modeling tool and its implementation. Computer Performance Evaluation/TOOLS, pages 116--133, 2003.

[9]

C. Courcoubetis and M. Yannakakis. Markov decision processes and regular events (extended abstract). ICALP'90, LNCS 443, pages 336--349, 1990.

Digital Library

[10]

C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857--907, 1995.

Digital Library

[11]

P.R. D'Argenio and P. Niebert. Partial order reduction on concurrent probabilistic programs. QEST'04, IEEE CS Press, pages 230--239, 2004.

Digital Library

[12]

L. de Alfaro. Temporal logics for the specification of performance and reliability. STACS'97, LNCS 1200, pages 165--179, 1997.

Digital Library

[13]

L. de Alfaro. Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University, 1997.

[14]

E. Dijkstra. Guarded commands, non-determinacy and the formal derivation of programs. Comm. ACM, 18:453--457, 1975

Digital Library

[15]

P. Godefroid. On the costs and benefits of using partial-order methods for the verification of concurrent systems. In POMIV, pages 289--303, 1996.

Digital Library

[16]

P. Godefroid. Partial Order Methods for the Verification of Concurrent Systems: An Approach to the State Explosion Problem, LNCS 1032, 1996.

Digital Library

[17]

G. Holzmann. The SPIN Model Checker, Primer and Reference Manual. Add.Wes., 2003.

Digital Library

[18]

A. Itai and M. Rodeh. Symmetry breaking in distributed networks. Inf. Comput., 88(1):60--87, 1990.

Digital Library

[19]

B.Jeannet, P.d'Argenio and K.G. Larsen. RAPTURE: A tool for verifying Markov Decision Processes. Proc.Tools Day / CONCUR'02. Tech.Rep. FIMU-RS-2002--05,84--98, 2002.

[20]

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), to appear, 2004.

Digital Library

[21]

N. Lynch. Distributed Algorithms. Morgan Kaufmann, San Francisco, CS, 1996. MIT.

Digital Library

[22]

C. Morgan and A. McIver. pGCL: formal reasoning for random algorithms. Proc. WOFACS'98, Spec. Iss.of SACJ, 22:14--27, 1999.

[23]

C. Morgan and A. McIver. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005.

Digital Library

[24]

Terence Parr. The ANTLR Reference Manual. 2.6 edition, 1999.

[25]

D. Peled. Partial order reduction: Linear and branching time logics and process algebras. In POMIV, pages 79--88, 1996.

Digital Library

[26]

D. Peled, V. Pratt, and G. Holzmann, editors. Partial Order Methods in Verification, volume 29(10) of DIMACS. American Mathematical Society, 1997.

[27]

A. Valmari. Stubborn set methods for process algebras. In POMIV, pages 79--88, 1996.

Digital Library

[28]

M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. FOCS'85, IEEE CS Press, pages 327--338, 1985.

Digital Library

[29]

M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). LICS'86, pages 332--344, IEEE Computer Society Press, 1986.

Cited By

Größer MNorman GBaier CCiesinski FKwiatkowska MParker D(2006)On reduction criteria for probabilistic reward modelsProceedings of the 26th international conference on Foundations of Software Technology and Theoretical Computer Science10.1007/11944836_29(309-320)Online publication date: 13-Dec-2006
https://dl.acm.org/doi/10.1007/11944836_29
Groesser MBaier C(2005)Partial order reduction for markov decision processesProceedings of the 4th international conference on Formal Methods for Components and Objects10.1007/11804192_19(408-427)Online publication date: 1-Nov-2005
https://dl.acm.org/doi/10.1007/11804192_19

Index Terms

Recommendations

Quantitative Analysis With the Probabilistic Model Checker PRISM

Probabilistic model checking is a formal verification technique for establishing the correctness, performance and reliability of systems which exhibit stochastic behaviour. As in conventional verification, a precise mathematical model of a real-life ...
An Inductive Technique for Parameterised Model Checking of Degenerative Distributed Randomised Protocols

We present a technique to tackle the parameterised probabilistic model checking problem for a particular class of randomised distributed systems, which we model as Markov Decision Processes. These systems, termed degenerative, have the property that a ...
Quantitative verification: models, techniques and tools
ESEC-FSE companion '07: The 6th Joint Meeting on European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering: companion papers

Automated verification is a technique for establishing if certain properties, usually expressed in temporal logic, hold for a system model. The model can be defined using a high-level formalism or extracted directly from software using methods such as ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

FMICS '05: Proceedings of the 10th international workshop on Formal methods for industrial critical systems

September 2005

152 pages

ISBN:1595931481

DOI:10.1145/1081180

General Chairs:
Tiziana Margaria
Universitat Gottingen, Germany
,
Mieke Massink
CNR-ISTI, Italy

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

FMICS05

Sponsor:

FMICS05: Tenth International Workshop on Formal Methods in Industrial Criticial Systems 2005

September 5 - 6, 2005

Lisbon, Portugal

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
161
Total Downloads

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

Reflects downloads up to 26 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Größer MNorman GBaier CCiesinski FKwiatkowska MParker D(2006)On reduction criteria for probabilistic reward modelsProceedings of the 26th international conference on Foundations of Software Technology and Theoretical Computer Science10.1007/11944836_29(309-320)Online publication date: 13-Dec-2006
https://dl.acm.org/doi/10.1007/11944836_29
Groesser MBaier C(2005)Partial order reduction for markov decision processesProceedings of the 4th international conference on Formal Methods for Components and Objects10.1007/11804192_19(408-427)Online publication date: 1-Nov-2005
https://dl.acm.org/doi/10.1007/11804192_19

View Options

Get Access

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.

Media

Figures

Other

Tables

View Table of Contents