Abstract
Systems with an arbitrary number of homogeneous processes occur in many applications. The Parameterized Model Checking Problem (PMCP) is to determine whether a temporal property is true of every size instance of the system. We consider systems formed by a synchronous parallel composition of a single control process with an arbitrary number of homogeneous user processes, and show that the PMCP is decidable for properties expressed in an indexed propositional temporal logic. While the problem is in general PSPACE-complete, our initial experimental results indicate that the method is usable in practice.
This work was supported in part by NSF grant CCR 9415496 and SRC Contract 95-DP-388.
Chapter PDF
Similar content being viewed by others
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.
References
Apt, K., Kozen, D. Limits for automatic verification of finite-state concurrent systems. IPL 15, pp. 307–309.
Browne, M. C., Clarke, E. M., Grumberg, O. Reasoning about Networks with Many Identical Finite State Processes, Information and Computation, vol. 81, no. 1, pp. 13–31, April 1989.
Clarke, E.M., Emerson, E.A. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. Workshop on Logics of Programs, Springer-Verlag LNCS 131.
Clarke, E.M., Emerson, E.A., and Sistla, A.P., Automatic Verification of Finite-State Concurrent Systems using Temporal Logic, ACM Trans. Prog. Lang. and Sys., vol. 8, no. 2, pp. 244–263, April 1986.
Clarke, E.M., Filkorn, T., Jha, S. Exploiting Symmetry in Temporal Logic Model Checking, 5th CAV, Springer-Verlag LNCS 697.
Clarke, E.M., Grumberg, O. Avoiding the State Explosion Problem in Temporal Logic Model Checking Algorithms, PODC 1987.
Clarke, E.M., Grumberg, O., Jha, S. Verifying Parameterized Networks using Abstraction and Regular Languages. CONCUR 95.
Emerson, E.A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, vol. B, (J. van Leeuwen, ed.), Elsevier/North-Holland, 1991.
Emerson, E.A., Namjoshi, K.S. Reasoning about Rings. Proc. ACM Symposium on Principles of Programming Languages, 1995.
Emerson, E.A., Sistla, A.P. Symmetry and Model Checking, 5th CAV, Springer-Verlag LNCS 697.
Emerson, E.A., Sistla, A.P. Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic approach. CAV 1995.
Emerson, E.A., Srinivasan, J. A decidable temporal logic to reason about many processes. PODC 1990.
German, S.M., Sistla, A.P. Reasoning about Systems with Many Processes. J.ACM, Vol. 39, Number 3, July 1992.
Hojati, R., Brayton, R. Automatic Datapath Abstraction in Hardware Systems, CAV 1995.
Ip, C., Dill, D. Better verification through symmetry. Proc. 11th Intl. Symp. on Computer Hardware Description Languages and their Applications.
Kurshan, R.P., McMillan, K. A Structural Induction Theorem for Processes, PODC 1989.
Li, J., Suzuki, I., Yamashita, M. Fair Petri Nets and structural induction for rings of processes. Theoretical Computer Science, vol. 135(2), 1994. pp. 337–404.
Litchtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL 85, pp. 97–107.
Long, D. Model Checking, Abstraction, and Compositional Verification. Ph.D. Thesis, Carnegie-Mellon University, 1993.
Lubachevsky, B. An Approach to Automating the Verification of Compact Parallel Coordination Programs I. Acta Informatica 21, 1984.
Manna, Z., Pnueli, A. Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992.
McMillan, K., Symbolic Model Checking: An Approach to the State Explosion Problem, Ph.D. Thesis, Carnegie-Mellon University, 1992.
Pnueli, A. The Temporal Logic of Programs. FOCS 1977.
Pong, F., Dubois, M. A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems, August 1995.
Reif, J., Sistla, A. P. A multiprocess network logic with temporal and spatial modalities. JCSS 30(1), 1985.
Rho, J. K., Somenzi, F. Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems. CAV 1993, LNCS 697.
SAE J1850 Class B data communication network interface. Society of Automotive Engineers, Inc., 1992.
Shtadler, Z., Grumberg, O. Network Grammars, Communication Behaviours and Automatic Verification. Springer-Verlag, LNCS 407.
Suzuki, I. Proving properties of a ring of finite state machines. IPL 28, pp. 213–214.
Vardi, M. An Automata-theoretic Approach to Linear Temporal Logic, Proceedings of Banff Higher Order Workshop on Logics for Concurrency, F. Moller, ed., Springer-Verlag LNCS, to appear.
Vardi, M., Wolper, P. An Automata-theoretic Approach to Automatic Program Verification, Proc. IEEE LICS, pp. 332–344, 1986.
Vernier, I. Specification and Verification of Parameterized Parallel Programs. Proc. 8th Intl. Symp. on Computer and Information Sciences, Istanbul, Turkey, pp. 622–625.
Wolper, P., Lovinfosse, V. Verifying Properties of Large Sets of Processes with Network Invariants. Springer-Verlag, LNCS 407.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Namjoshi, K.S. (1996). Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_60
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_60
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive