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
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.
Author's research is supported in part by NSF grant CCR-9415496 and Semiconductor Research Corporation Contract 94-DP-388.
This author's research is supported in part by NSF grant CCR-9212183.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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.
Bouajjani, A., Fernandez, J, Halbwichs, N., Raymond, P., and Ratel, C., Minimal State Graph Generation, Science of Computer Programming, 1992.
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.
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 1986
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.
Clarke, E. M., Grumberg, O., and Brown, M., Characterizing Kripke Structures in Temporal Logic, Theor. Comp. Sci., 1988
Clarke, E. M., Grumberg, O., and Brown, M., Reasoning about Many Identical Processes, Inform. and Comp., 1989
Cleaveland, R., Analyzing Concurrent Systems using the Concurrency Workbench, Functional Programming, Concurrency, Simulation, and Automated Reasoning Springer LNCS no. 693, pp. 129–144, 1993.
Dams, D., Grumberg, O., and Gerth, R., Generation of Reduced Models for checking fragments of CTL, CAV93, Springer LNCS no. 697, 1993.
Emerson, E. A. and Lei, C.-L., Modalities for Model Checking: branching Time Strikes Back, Science of Computer Programming, v. 8, pp. 275–306, 1987
Emerson, E. A., and Sistla, A. P., Symmetry and Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993
Emerson, E. A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, (J. van Leeuwen, ed.), Elsevier/North-Holland, 1991.
Francez, N., Fairness, Springer-Verlag, New York, 1986
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.
Ip, C-W. N., Dill, D. L., Better Verification through Symmetry, CHDL, April 1993.
Jensen, K., Colored Petri Nets: Basic Concepts, Analysis Methods, and Practical Use, vol. 2: Analysis Methods, EATCS Monographs, Springer-Verlag, 1994.
Jensen,K., and Rozenberg,G. (eds.), High-level Petri Nets: Theory and Application, Springer-Verlag, 1991.
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.
Kurshan, R. P., Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach Princeton University Press, Princeton, New Jersey 1994.
Lee. D., and Yannakakis, M., On-Line Minimization of Transition Systems, STOC92.
Litchtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85
Manna, Z. and Pnueli, A., Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992
Sistla, A. P. and German, S. M., Reasoning with many Processes, Proceedings of the Symposium on Logic in Computer Science, Ithaca, New York, 1987
Streett, R., Propositional Dynamic Logic of Looping and Converse, PhD Thesis, MIT, 1981.
Vardi, M., and Wolper, P., An Automata-Theoretic Framework for Modal Logics of Programs, STOC84
Vardi, M., and Wolper, P., An Automata-Theoretic Framework for Automatic Program Verification, LICS86.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Sistla, A.P. (1995). Utilizing symmetry when model checking under fairness assumptions: An automata-theoretic approach. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_59
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_59
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive