Abstract
The paper studies automatic verification of liveness properties with probability 1 over parameterized programs that include probabilistic transitions, and proposes two novel approaches to the problem. The first approach is based on a Planner that occasionally determines the outcome of a finite sequence of “random”choices, while the other random choices are performed non-deterministically.Using a Planner, a probabilistic protocol can be treated just like a non-probabilistic one and verified as such. The second approach is based on γ-fairness, a notion of fairness that is sound and complete for verifying simple temporal properties (whose only temporal operators are ⋄and □) over finite-state systems.The paper presents a symbolic model checker based on γ-fairness.We then show how the network invariant approach can be adapted to accommodate probabilistic protocols. The utility of the Planner approach is demonstrated on a probabilistic mutual exclusion protocol. The utility of the approach of γ-fairness with network invariants is demonstrated on Lehman and Rabin's Courteous Philosophers algorithm.
This research was supported in part by ONR grant N00014-99-1-0131, and the John von Neumann Minerva Center for Verification of Reactive Systems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.
T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In Proc. 13 thIntl. Conference on Computer Aided Verification (CAV’01), volume 2102 ofLect. Notes in Comp. Sci., Springer-Verlag, pages 221–234, 2001.
T. Arons, A. Pnueli, and L. Zuck. Verification by probabilistic abstraction. Weizmann Institute of Science Technical Report, 2003.
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.
K. Baukus, Y. Lakhnesche, and K. Stahl. Verification of parameterized protocols. Journal of Universal Computer Science, 7(2):141–158, 2001.
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.
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.
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.
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.
W. Feller. An Introduction to Probability Theory and its Applicaitons, volume 1. John Wiley & Sons, 3 edition, 1968.
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.
R.P. Kurshan and K.L. McMillan. A structural induction theorem for processes. Information and Computation, 117:1–11, 1995.
M. Kwiatkowska, G. Norman, and D. Parker. Verifying randomized distributed algorithms with prism. In Proc. of the Workshop on Advances in Verification (WAVe) 2000. 2000.
M. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic symbolic model checker. In TOOLS 2002, volume 2324 of LNCS, 2002.
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.
Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proc. 25th Int. Colloq. Aut. Lang. Prog., volume 1443 of LNCS, pages 1–16. Springer-Verlag, 1998.
Y. Kesten, A. Pnueli, E. Shahar, and L. Zuck. Network invariants in action. In Proceedings of Concur’02, volume 2421 of LNCS. Springer-Verlag, 2002.
D. Lehmann and M.O. Rabin. On the advantages of free choice: A symmetric and fully distibuted solution to the dining philosophers problem (exended abstract). In Proc. 8th ACM Symp. Princ. of Prog. Lang., pages 133–138, 1981.
B.D. Lubachevsky. An approach to automating the verification of compact parallel coordination programs. Acta Infromatica, 21, 1984.
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.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
A. Pnueli. On the extremely fair treatment of probabilistic algorithms. In Proc. 15th ACM Symp. Theory of Comp., pages 278–290, 1983.
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.
A. Pnueli, J. Xu, and L. Zuck. The (0, 1,∈) counter abstraction. In Proc. 14 thIntl. Conference on Computer Aided Verification (CAV’02), volume 2404 ofLect. Notes in Comp. Sci., Springer-Verlag, 2002. http://www.cs.nyu.edu/~zuck/pubs/cav02.ps.
A. Pnueli and L. Zuck. Probablistic verification by tableaux. In Proc. First IEEE Symp. Logic in Comp. Sci., pages 322–331, 1986.
A. Pnueli and L. Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1:53–72, 1986.
A. Pnueli and L.D. Zuck. Probabilistic verification. Information and Computation, 103(1):1–29, 1993.
M.O. Rabin. The choice coordination problem. Acta Informatica, 17:121–134, 1982.
Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 151–165. Springer-Verlag, 1989.
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.
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 LNCS, pages 68–80. Springer-Verlag, 1989.
L. Zuck, A. Pnueli, and Y. Kesten. Automatic verification of probabilistic free choice. In Proc. of the 3 rdworkshop on Verification, Model Checking, and Abstract Interpretation, volume 2294 of LNCS, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pnueli, A., Zuck, L. (2003). Parameterized Verification by Probabilistic Abstraction. In: Gordon, A.D. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2003. Lecture Notes in Computer Science, vol 2620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36576-1_6
Download citation
DOI: https://doi.org/10.1007/3-540-36576-1_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00897-2
Online ISBN: 978-3-540-36576-1
eBook Packages: Springer Book Archive