Reasoning about rings

ABSTRACT

The ring is a useful means of structuring concurrent processes. Processes communicate by passing a token in a fixed direction; the process that possesses the token is allowed to make certain moves. Usually, correctness properties are expected to hold irrespective of the size of the ring. We show that the problem of checking many useful correctness properties for rings of all sizes can be reduced to checking them on a ring of small size. The results do not depend on the processes being finite state. We illustrate our results on examples.

REFERENCES

• AK 86: K R Apt , D C Kozen, Limits for automatic verification of finite-state concurrent systems, Information Processing Letters, v.22 n.6, p.307-309, May 30,1986 [doi>10.1016/0020-0190(86)90071-2]
• BCG 88: M. C. Browne , E. M. Clarke , O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science, v.59 n.1-2, p.115-131, July 1988 [doi>10.1016/0304-3975(88)90098-9]
• BCG 89: M. C. Browne , E. M. Clarke , O. Grumberg, Reasoning about networks with many identical finite state processes, Information and Computation, v.81 n.1, p.13-31, April 1989 [doi>10.1016/0890-5401(89)90026-6]
• Br 89: M. C Browne, Automatic verification of finite state machines using temporal logic, Carnegie Mellon University, Pittsburgh, PA, 1989
• C 93: Rance Cleaveland, Analysing Concurrent Systems Using the Concurrency Workbench, Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992, McMaster University, Hamilton, Ontario, Canada, p.129-144, January 1993
• CC 77: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• CE 81: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• CES 86: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• CFJ 93: Edmund M. Clarke , Thomas Filkorn , Somesh Jha, Exploiting Symmetry In Temporal Logic Model Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.450-462, June 28-July 01, 1993
• CG 87: E. M. Clarke , O. Grumberg, Avoiding the state explosion problem in temporal logic model checking, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.294-303, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41865]
• CH 93: Cleaveland, R., Hennessy, M. Testing Equivalence as a Bisimulation Equivalence. Formal Aspects of Computing, vol. 5, 1993.
• CPS 89: R. Cleaveland , J. Parrow , B. Steffen, The concurrency workbench, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.24-37, February 1990, Grenoble, France
• D 85: E. W. Dijkstra, Invariance and non-determinacy, Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, p.157-165, June 1985, London, United Kingdom
• DV 90: De Nicola, R., Vaandrager, F. Three logics for Branching Bisimulation, 5th Annual IEEE Symp. on Logic in Computer Science, pp. i18-129, 1990.
• Em 90: Emerson, E. A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, (J. van Leeuwen, ed.), Elsevier/North-Holland, 1991.
• ES 93: E. Allen Emerson , A. Prasad Sistla, Symmetry and Model Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.463-478, June 28-July 01, 1993
• GS 92: Steven M. German , A. Prasad Sistla, Reasoning about systems with many processes, Journal of the ACM (JACM), v.39 n.3, p.675-735, July 1992 [doi>10.1145/146637.146681]
• KM 89: R. P. Kurshan , K. McMillan, A structural induction theorem for processes, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.239-247, June 1989, Edmonton, Alberta, Canada [doi>10.1145/72981.72998]
• LSY 94: Jianan Li , I. Suzuki , M. Yamashita, A New Structural Induction Theorem for Rings of Temporal Petri Nets, IEEE Transactions on Software Engineering, v.20 n.2, p.115-126, February 1994 [doi>10.1109/32.265633]
• LSY 92: Jianan Li , Ichiro Suzuki , Masafumi Yamashita, Fair Petri nets and structural induction for rings of processes, Theoretical Computer Science, v.135 n.2, p.377-404, Dec. 12, 1994 [doi>10.1016/0304-3975(94)90113-9]
• Mil 90: Robin Milner, Communication and concurrency, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1995
• ShG 89: Z. Shtadler , O. Grumberg, Network grammars, communication behaviors and automatic verification, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.151-165, February 1990, Grenoble, France
• Su 88: Ichiro Suzuki, Proving properties of a ring of finite-state machines, Information Processing Letters, v.28 n.4, p.213-214, July 29, 1988 [doi>10.1016/0020-0190(88)90211-6]
• WL 89: P. Wolper , V. Lovinfosse, Verifying properties of large sets of processes with network invariants, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.68-80, February 1990, Grenoble, France

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory

General Terms:
Algorithms, Theory, Verification