Abstract
The Parameterized Model Checking Problem (PMCP) is to determine whether a temporal property is true for every size instance of a system comprised of many homogenous processes. Unfortunately, it is undecidable in general. We are able to establish, nonetheless, decidability of the PMCP in quite a broad framework. We consider asynchronous systems comprised of an arbitrary number of homogeneous copies of a generic process template. The process template is represented as a synchronization skeleton while correctness properties are expressed using Indexed CTL*∖ X. We reduce model checking for systems of arbitrary size n to model checking for systems of size up to (of) a small cutoff size c. This establishes decidability of PMCP as it is only necessary to model check a finite number of relatively small systems. Efficient decidability can be obtained in some cases. The results generalize to systems comprised of multiple heterogeneous classes of processes, where each class is instantiated by many homogenous copies of the class template (e.g., m readers and n writers).
This work was supported in part by NSF grant CCR-980-4737, SRC contract 99-TJ-685 and TARP project 003658-0650-1999.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters 15, 307–309 (1986)
Attie, P.C., Emerson, E.A.: Synthesis of Concurrent Systems with Many Similar Processes. ACM Transactions on Programming Languages and Systems 20(1), 51–115 (1998)
Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about Networks with Many Identical Finite State Processes. Information and Control 81(1), 13–31 (1989)
Clarke, E.M., Grumberg, O.: Avoiding the State Explosion Problem in Temporal Logic Model Checking Algorithms. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pp. 294–303 (1987)
Clarke, E.M., Grumberg, O., Jha, S.: Verifying Parameterized Networks using Abstracion and Regular Languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 395–407. Springer, Heidelberg (1995)
Emerson, E.A., Namjoshi, K.S.: Reasoning about Rings. In: Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 85–94 (1995)
Emerson, E.A., Namjoshi, K.S.: Automatic Verification of Parameterized Synchronous Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Emerson, E., Trefler, R.: Parametric Quantitative Temporal Reasoning.In: LICS(1999),pp. 336–343 (1999)
German, S.M., Sistla, A.P.: Reasoning about Systems with Many Processes.J. ACM 39(3) (July 1992)
Ip, C., Dill, D.: Better verification through symmetry. In: Proceedings of the 11th International Symposium on Computer Hardware Description Languages and their Applications (1993)
Ip, C., Dill, D.: Verifying Systems with Replicated Components in Murphi. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 147–158. Springer, Heidelberg (1996)
Kurshan, R.P., McMillan, L.: A Structural Induction Theorem for Processes. In: Proceedings of the Eight Annual ACM Symposium on Principles of Distributed Computing, pp. 239–247 (1989)
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specifications. In: Conference Record of POPL 1985: 12nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97–107 (1985)
Lubachevsky, B.: An Approach to Automating the Verification of Compact Parallel Coordination Programs I. Acta Informatica 21 (1984)
McMillan, K.: Verification of Infinite State Systems by Compositional Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219–237. Springer, Heidelberg (1999)
Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of the eighteenth Symposium on Foundations of Computer Science (1977)
Pong, F., Dubois, M.: A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems (August 1995)
Sistla, A.P.: Parameterized Verification of Linear Networks Using Automata as Invariants. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 412–423. Springer, Heidelberg (1997)
Vardi, M., Wolper, P.: An Automata-theoretic Approach to Automatic Program Verification. In: Proceedings, Symposium on Logic in Computer Science, pp. 332–344 (1986)
Vernier, I.: Specification and Verification of Parameterized Parallel Programs. In: Proceedings of the 8th International Symposium on Computer and Information Sciences, Istanbul, Turkey, pp. 622–625 (1993)
Wolper, P., Lovinfosse, V.: Verifying Properties of Large Sets of Processes with Network Invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Kahlon, V. (2000). Reducing Model Checking of the Many to the Few. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_19
Download citation
DOI: https://doi.org/10.1007/10721959_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive