Article

Liveness with (0, 1, infty)-Counter Abstraction

Authors:

Lenore D. ZuckAuthors Info & Claims

CAV '02: Proceedings of the 14th International Conference on Computer Aided Verification

Pages 107 - 122

Published: 27 July 2002 Publication History

Abstract

We introduce the (0, 1, )-counter abstraction method by which a parameterized system of unbounded size is abstracted into a finite-state system. Assuming that each process in the parameterized system is finite-state, the abstract variables are limited counters which count, for each local state s of a process, the number of processes which currently are in local state s. The counters are saturated at 2, which means that ( s )= 2 whenever 2 or more processes are at state s . The emphasis of the paper is on the derivation of an adequate and sound set of fairness requirements (both weak and strong) that enable proofs of liveness properties of the abstract system, from which we can safely conclude a corresponding liveness property of the original parameterized system. We illustrate the method on few parameterized systems, including Szymanski's Algorithm for mutual exclusion. The method is also extended to deal with parameterized systems whose processes may have infinitely many local states, such as the Bakery Algorithm, by choosing few "interesting" state assertions and (0, 1, )-counting the number of processes satisfying them.

References

[1]

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

[2]

T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV'01 , pages 221-234, 2001.

[3]

K. Baukus, Y. Lakhnesche, and K. Stahl. Verification of parameterized protocols. Journal of Universal Computer Science , 7(2):141-158, 2001.

[4]

N. Bjørner, I. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In 1st Intl. Conf. on Principles and Practice of Constraint Programming , volume 976 of LNCS , pages 589-623. Springer-Verlag, 1995.

[5]

E. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In CONCUR'95 , pages 395-407, 1995.

[6]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'77 . ACM Press, 1977.

[7]

E. 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.

[8]

E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In POPL'95 , 1995.

[9]

E. Gribomont and G. Zenner. Automated verification of szymanski's algorithm. In B. Steffen, editor, TACAS'98 , pages 424-438, 1998.

[10]

V. Gyuris and A. P. Sistla. On-the-fly model checking under fairness that exploits symmetry. In CAV'97 , 1997.

[11]

J. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In TACAS'95 , 1995.

[12]

B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In TACAS'00 , 2000.

[13]

Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In CAV'97 , pages 424-435, 1997.

[14]

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.

[15]

D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL'97 , Paris, 1997.

[16]

O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specification. In POPL'85 , pages 97-107, 1985.

[17]

B. D. Lubachevsky. An approach to automating the verification of compact parallel coordination programs. Acta Infromatica , 21, 1984.

[18]

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

[19]

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

[20]

K. McMillan. Verification of an implementation of Tomasulo's algorithm by compositional model checking. In CAV'98 , pages 110-121, 1998.

[21]

A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In CAV'96 , pages 184-195, 1996.

[22]

F. Pong and M. Dubois. A new approach for the verification of cache coherence protocols. IEEE Transactions on Parallel and Distributed Systems , 6(8):773-787, Aug. 1995.

[23]

B. K. Szymanski. A simple solution to Lamport's concurrent programming problem with linear wait. In Proc. 1988 International Conference on Supercomputing Systems , pages 621-626, St. Malo, France, 1988.

Cited By

Lomuscio APirovano EEl Fallah Seghrouchni ASukthankar GAn BYorke-Smith N(2020)Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent SystemsProceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3398761.3398852(762-770)Online publication date: 5-May-2020
https://dl.acm.org/doi/10.5555/3398761.3398852
Lomuscio APirovano EElkind EVeloso MAgmon NTaylor M(2019)A Counter Abstraction Technique for the Verification of Probabilistic Swarm SystemsProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3331689(161-169)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3331689
Klinkhamer AEbnenasir A(2019)On the Verification of Livelock-Freedom and Self-Stabilization on Parameterized RingsACM Transactions on Computational Logic10.1145/332645620:3(1-36)Online publication date: 5-Jun-2019
https://dl.acm.org/doi/10.1145/3326456
Show More Cited By

Liveness with (0, 1, infty)-Counter Abstraction
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation

Recommendations

Abstraction for liveness
VMCAI'05: Proceedings of the 6th international conference on Verification, Model Checking, and Abstract Interpretation

Unlike model checking which is restricted to finite-state systems, there are two methods which can be applied for the verification of arbitrary infinite-state systems. These are the methods of deductive verification and finitary abstraction (FA). ...
Counter Abstraction in the CSP/FDR setting

In this paper we consider an adaptation of counter abstraction for the CSP/FDR setting. The technique allows us to transform a concurrent system with an unbounded number of agents into a finite-state abstraction. The systems to which the method can be ...
Fair Model Checking with Process Counter Abstraction
FM '09: Proceedings of the 2nd World Congress on Formal Methods

Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed/concurrent systems. A common state space abstraction for checking parameterized systems ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '02: Proceedings of the 14th International Conference on Computer Aided Verification

July 2002

629 pages

ISBN:3540439978

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 July 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

67
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lomuscio APirovano EEl Fallah Seghrouchni ASukthankar GAn BYorke-Smith N(2020)Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent SystemsProceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3398761.3398852(762-770)Online publication date: 5-May-2020
https://dl.acm.org/doi/10.5555/3398761.3398852
Lomuscio APirovano EElkind EVeloso MAgmon NTaylor M(2019)A Counter Abstraction Technique for the Verification of Probabilistic Swarm SystemsProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3331689(161-169)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3331689
Klinkhamer AEbnenasir A(2019)On the Verification of Livelock-Freedom and Self-Stabilization on Parameterized RingsACM Transactions on Computational Logic10.1145/332645620:3(1-36)Online publication date: 5-Jun-2019
https://dl.acm.org/doi/10.1145/3326456
v. Gleissenthall KKıcı RBakst AStefan DJhala R(2019)Pretend synchrony: synchronous verification of asynchronous distributed programsProceedings of the ACM on Programming Languages10.1145/32903723:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290372
Konnov ILazić MVeith HWidder J(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/3093333.300986052:1(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009860
Konnov ILazić MVeith HWidder JCastagna GGordon A(2017)A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009860(719-734)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009860
Konnov IVeith HWidder J(2017)On the completeness of bounded model checking for threshold-based distributed algorithmsInformation and Computation10.1016/j.ic.2016.03.006252:C(95-109)Online publication date: 1-Feb-2017
https://dl.acm.org/doi/10.1016/j.ic.2016.03.006
Konnov ILazić MVeith HWidder J(2017)Para$$^2$$2Formal Methods in System Design10.1007/s10703-017-0297-451:2(270-307)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1007/s10703-017-0297-4
Durand-Gasselin AEsparza JGanty PMajumdar R(2017)Model checking parameterized asynchronous shared-memory systemsFormal Methods in System Design10.1007/s10703-016-0258-350:2-3(140-167)Online publication date: 1-Jun-2017
https://dl.acm.org/doi/10.1007/s10703-016-0258-3
Sankur OTalpin J(2017)An Abstraction Technique for Parameterized Model Checking of Leader Election ProtocolsProceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020510.1007/978-3-662-54577-5_2(23-40)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54577-5_2
Show More Cited By

View Options

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

Media

Figures

Other

Tables

View Table of Contents