Advertisement

Utilizing symmetry when model checking under fairness assumptions: An automata-theoretic approach

  • E. A. Emerson
  • A. P. Sistla
Session 10: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

One useful technique for combating the state explosion problem is to exploit symmetry [ID93, CFJ93, ES93] when performing temporal logic model checking [CE81, CES86]. In [CFJ93] [ES93] it is shown how, using some basic notions of group theory, symmetry may be exploited for the full range of correctness properties expressible in the very expressive temporal logic CTL*. Surprisingly, while fairness properties are readily expressible in CTL*, these methods are not powerful enough to admit any amelioration of state explosion, when fairness assumptions are involved. We show that it is nonetheless possible to handle fairness efficiently by trading some group theory for automata theory. Our automata-theoretic approach [VW86] depends on detecting fair paths subtly encoded in a permutation annotated quotient structure, using a threaded structure to “physically” reflect coordinate permutations.

Keywords

Model Check Temporal Logic Basic Modality Fairness Constraint State Explosion Problem 
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

  1. [APS83]
    Aggarwal S., Kurshan R. P., Sabnani K. K., “A Calculus for Protocol Specification and Validation”, in Protocol Specification, Testing and Verification III, H. Ruden, C. West (ed's), North-Holland 1983, 19–34.Google Scholar
  2. [BFHRR92]
    Bouajjani, A., Fernandez, J, Halbwichs, N., Raymond, P., and Ratel, C., Minimal State Graph Generation, Science of Computer Programming, 1992.Google Scholar
  3. [CE81]
    Clarke, E. M., and Emerson, E. A., Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic, Logics of Programs Workshop 1981, Springer LNCS no. 131.Google Scholar
  4. [CES86]
    Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent Programs using Temporal Logic: A Practical Approach, ACM TOPLAS, April 1986Google Scholar
  5. [CFJ93]
    Clarke, E. M., Filkorn, T., Jha, S. Exploiting Symmetry in Temporal Logic Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993.Google Scholar
  6. [CGB88]
    Clarke, E. M., Grumberg, O., and Brown, M., Characterizing Kripke Structures in Temporal Logic, Theor. Comp. Sci., 1988Google Scholar
  7. [CGB89]
    Clarke, E. M., Grumberg, O., and Brown, M., Reasoning about Many Identical Processes, Inform. and Comp., 1989Google Scholar
  8. [C193]
    Cleaveland, R., Analyzing Concurrent Systems using the Concurrency Workbench, Functional Programming, Concurrency, Simulation, and Automated Reasoning Springer LNCS no. 693, pp. 129–144, 1993.Google Scholar
  9. [DGG93]
    Dams, D., Grumberg, O., and Gerth, R., Generation of Reduced Models for checking fragments of CTL, CAV93, Springer LNCS no. 697, 1993.Google Scholar
  10. [EL87]
    Emerson, E. A. and Lei, C.-L., Modalities for Model Checking: branching Time Strikes Back, Science of Computer Programming, v. 8, pp. 275–306, 1987CrossRefGoogle Scholar
  11. [ES93]
    Emerson, E. A., and Sistla, A. P., Symmetry and Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993Google Scholar
  12. [Em90]
    Emerson, E. A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, (J. van Leeuwen, ed.), Elsevier/North-Holland, 1991.Google Scholar
  13. [Fr86]
    Francez, N., Fairness, Springer-Verlag, New York, 1986Google Scholar
  14. [GS92]
    German, S. M. and Sistla, A. P. Reasoning about Systems with many Processes, Journal of the ACM, July 1992, Vol 39, No 3, pp 675–735.Google Scholar
  15. [ID93]
    Ip, C-W. N., Dill, D. L., Better Verification through Symmetry, CHDL, April 1993.Google Scholar
  16. [Je94]
    Jensen, K., Colored Petri Nets: Basic Concepts, Analysis Methods, and Practical Use, vol. 2: Analysis Methods, EATCS Monographs, Springer-Verlag, 1994.Google Scholar
  17. [JR91]
    Jensen,K., and Rozenberg,G. (eds.), High-level Petri Nets: Theory and Application, Springer-Verlag, 1991.Google Scholar
  18. [Ku86]
    Kurshan, R. P., “Testing Containmentof omega-regular Languages”, Bell Labs Tech. Report 1121-861010-33 (1986); conference version in R. P. Kurshan, “Reducibility in Analysis of Coordination”, LNCIS 103 (1987) Springer-Verlag 19–39.Google Scholar
  19. [Ku94]
    Kurshan, R. P., Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach Princeton University Press, Princeton, New Jersey 1994.Google Scholar
  20. [LY92]
    Lee. D., and Yannakakis, M., On-Line Minimization of Transition Systems, STOC92.Google Scholar
  21. [LP85]
    Litchtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85Google Scholar
  22. [MP92]
    Manna, Z. and Pnueli, A., Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992Google Scholar
  23. [SG87]
    Sistla, A. P. and German, S. M., Reasoning with many Processes, Proceedings of the Symposium on Logic in Computer Science, Ithaca, New York, 1987Google Scholar
  24. [St81]
    Streett, R., Propositional Dynamic Logic of Looping and Converse, PhD Thesis, MIT, 1981.Google Scholar
  25. [VW84]
    Vardi, M., and Wolper, P., An Automata-Theoretic Framework for Modal Logics of Programs, STOC84Google Scholar
  26. [VW86]
    Vardi, M., and Wolper, P., An Automata-Theoretic Framework for Automatic Program Verification, LICS86.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • E. A. Emerson
    • 1
  • A. P. Sistla
    • 2
  1. 1.Department of Computer ScienceUniversity of Texas at AustinAustinUSA
  2. 2.Department of Electrical Engineering and Computer ScienceUniversity of Illinois at ChicagoChicagoUSA

Personalised recommendations