Skip to main content
SpringerLink
Log in

Automatic Verification of Probabilistic Free Choice

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2294))

Abstract

We study automatic methods for establishing P-validity (validity with probability 1) of simple temporal properties over finite-state probabilistic systems. The proposed approach replaces P-validity with validity over a non-probabilistic version of the system, in which probabilistic choices are replaced by non-deterministic choices constrained by compassion (strong fairness) requirements. “Simple” properties are temporal properties whose only temporal operators are ◊ (eventually) and its dual □ (always). In general, the appropriate compassion requirements are “global,” since they involve global states of the system. Yet, in many cases they can be transformed into “local” requirements, which enables their verification by model checkers. We demonstrate our methodology of translating the problem of P-validity into that of verification of a system with local compassion requirement on the “courteous philosophers” algorithm of [LR81], a parameterized probabilistic system that is notoriously difficult to verify, and outline a verification of the algorithm that was obtained by the TLV model checker.

This research was supported in part by the John von Neumann Minerva Center for Verification of Reactive Systems, The European Community IST project “Advance”, and ONR grant N00014-99-1-0131.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.

    Google Scholar 

  2. T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In Proc. 13 rd Intl. Conference on Computer Aided Verification (CAV’01), volume 2102 ofLect. Notes in Comp. Sci., Springer-Verlag, pages 221–234, 2001.

    Google Scholar 

  3. M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. In Proc. 5th ACM Symp. Princ. of Dist. Comp., pages 240–248, 1986.

    Google Scholar 

  4. E.M. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In 6th International Conference on Concurrency Theory (CONCUR’95), pages 395–407, 1995.

    Google Scholar 

  5. S. Cohen, D. Lehmann, and A. Pnueli. Symmetric and economical solutions to the mutual exclusion problem in a distributed system. Theor. Comp. Sci., 34:215–225, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  6. E.A. Emerson and V. Kahlon. Reducing model checking of the many to the few. In 17th International Conference on Automated Deduction (CADE-17), pages 236–255, 2000.

    Google Scholar 

  7. E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In Proc. 22th ACM Conf. on Principles of Programming Languages, POPL’95, San Francisco, 1995.

    Google Scholar 

  8. E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. In R. Alur and T. Henzinger, editors, Proc. 8th Intl. Conference on Computer Aided Verification (CAV’96), volume 1102 of Lect. Notes in Comp. Sci., Springer-Verlag, 1996.

    Google Scholar 

  9. S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent programs. In Proc. 9th ACM Symp. Princ. of Prog. Lang., pages 1–6, 1982.

    Google Scholar 

  10. R.P. Kurshan and K.L. McMillan. A structural induction theorem for processes. Information and Computation, 117:1–11, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  11. Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of practical formal verification. Software Tools for Technology Transfer, 4(2):328–342, 2000.

    Article  Google Scholar 

  12. Zuck L. Interim report to PhD Committee. Technical report, Weizmann Institute of Sciences, 1985.

    Google Scholar 

  13. D. Lehmann and M.O. Rabin. On the advantages of free choice: A symmetric and fully distibuted solution to the dining philosophers problem. In Proc. 8th ACM Symp. Princ. of Prog. Lang., pages 133–138, 1981.

    Google Scholar 

  14. Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E. Chang, M. Colón, L. De Alfaro, H. Devarajan, H. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994.

    Google Scholar 

  15. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.

    Google Scholar 

  16. A. Pnueli, S. Ruah, and L. Zuck. Automatic deductive verification with invisible invariants. In Proc. 7 th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), volume 2031, pages 82–97, 2001.

    Google Scholar 

  17. A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In R. Alur and T. Henzinger, editors, Proc. 8th Intl. Conference on Computer Aided Verification (CAV’96), volume 1102 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 184–195, 1996.

    Google Scholar 

  18. A. Pnueli and L. Zuck. Probablistic verification by tableaux. In Proc. First IEEE Symp. Logic in Comp. Sci., pages 322–331, 1986.

    Google Scholar 

  19. A. Pnueli and L. Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1:53–72, 1986.

    Article  MATH  Google Scholar 

  20. A. Pnueli and L.D. Zuck. Probabilistic verification. Inf. and Cont., 103(1):1–29, 1993.

    MATH  MathSciNet  Google Scholar 

  21. M.O. Rabin. The choice coordination problem. Acta Informatica, 17:121–134, 1982.

    Article  MATH  MathSciNet  Google Scholar 

  22. A.P. Sistla and L.D. Zuck. Reasoning in a restricted temporal logic. Inf. and Cont., 102(2):167–195, 1993.

    MATH  MathSciNet  Google Scholar 

  23. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. First IEEE Symp. Logic in Comp. Sci., pages 332–344, 1986.

    Google Scholar 

  24. P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, volume 407 of Lect. Notes in Comp. Sci., pages 68–80. Springer-Verlag, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. New York University, New York

    Lenore Zuck & Amir Pnueli

  2. Weizmann Institute of Science, Rehovot, Israel

    Amir Pnueli

  3. Ben-Gurion University, Beer-Sheva, Israel

    Yonit Kesten

Authors
  1. Lenore Zuck
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yonit Kesten
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Via Torino 155, 30170, Mestre-Venezia, Italy

    Agostino Cortesi

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zuck, L., Pnueli, A., Kesten, Y. (2002). Automatic Verification of Probabilistic Free Choice. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-47813-2_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43631-7

  • Online ISBN: 978-3-540-47813-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation