article

Open access

An automata-theoretic approach to modular model checking

Editor: William Pugh Authors:

Orna Kupferman,

Moshe Y. VardiAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 22, Issue 1

Pages 87 - 128

https://doi.org/10.1145/345099.345104

Published: 01 January 2000 Publication History

Abstract

In modular verification the specification of a module consists of two part. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the assume-guarantee paradigm. In this paper we consider assume-guarantee specifications in which the guarantee is specified by branching temporal formulas. We distinguish between two approaches. In the first approach, the assumption is specified by branching temporal formulas too. In the second approach, the assumption is specified by linear temporal logic. We consider guarantees in ∀CTL, and ∀CTL*. We develop two fundamental techniques: building maximal models for ∀CTL and ∀CTL* formulas and using alternating automata to obtain space-efficient algorithms for fair model checking. Using these techniques we classify the complexity of satisfiability, validity, implication, and modular verification for ∀CTL and ∀CTL*. We show that modular verification is PSPACE-complete for ∀CTL and is EXSPACE-complete for ∀CTL*. We prove that when the assumption is linear, these bounds hold also for guarantees in CTL and CTL*. On the other hand, the problem remains EXSPACE-hard even when we restrict the assumptions to LTL and take the guarantees as a fixed ∀CTL formula.

References

[1]

Abadi, M. and Lamport, L. 1993. Composing specifications. ACM Transactions on Programming Languages and Systems 15, 1, 73-132.

[2]

Aziz, A., Shiple, T., Singhal, V., and Sangiovanni-Vincentelli, A. 1994. Formula-dependent equivalence for compositional CTL model checking. In Proc. 6th Conf. on Computer Aided Verification. Lecture Notes in Computer Science, vol. 818. Springer-Verlag, Stanford, CA, 324- 337.

[3]

Beeri, C. 1980. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. on Database Systems 5, 241-259.

[4]

Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. 1990. Symbolic model checking: 10 20 states and beyond. In Proc. 5th Symposium on Logic in Computer Science. Philadelphia, 428-439.

[5]

Clarke, E., Emerson, E., and Sistla, A. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8, 2 (January), 244-263.

[6]

Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press.

[7]

Clarke, E., Long, D., and McMillan, K. 1989. Compositional model checking. In Proc. 4th IEEE Symposium on Logic in Computer Science, R. Parikh, Ed. IEEE Computer Society Press, 353-362.

[8]

Damm, W., Dohmen, G., Gerstner, V., and Josko, B. 1989. Modular verification of Petri nets: the temporal logic approach. In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (Proceedings of REX Workshop). Lecture Notes in Computer Science, vol. 430. Springer-Verlag, Mook, The Netherlands, 180-207.

[9]

Dams, D., Grumberg, O., and Gerth, R. 1993. Generation of reduced models for checking fragments of CTL. In Proc. 5th Conf. on Computer Aided Verification. Lecture Notes in Computer Science, vol. 697. Springer-Verlag, 479-490.

[10]

Emerson, E. and Halpern, J. 1985. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences 30, 1-24.

[11]

Emerson, E. and Halpern, J. 1986. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM 33, 1, 151-178.

[12]

Emerson, E. and Jutla, C. 1988. The complexity of tree automata and logics of programs. In Proc. 29th IEEE Symposium on Foundations of Computer Science. White Plains, 328-337.

[13]

Emerson, E. and Lei, C.-L. 1985. Temporal model checking under generalized fairness constraints. In Proc. 18th Hawaii International Conference on System Sciences. Western Periodicals Company, North Holywood.

[14]

Emerson, E. and Lei, C.-L. 1987. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming 8, 275-306.

[15]

Grumberg, O. and Long, D. 1991. Model checking and modular verification. In Proc. 2nd Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 527. Springer- Verlag, 250-265.

[16]

Grumberg, O. and Long, D. 1994. Model checking and modular verification. ACM Trans. on Programming Languages and Systems 16, 3, 843-871.

[17]

Jones, C. 1983. Specification and design of (parallel) programs. In Information Processing 83: Proc. IFIP 9th World Congress, R. Mason, Ed. IFIP, North-Holland, 321-332.

[18]

Jones, N. 1975. Space-bounded reducibility among combinatorial problems. Journal of Computer and System Sciences 11, 68-75.

[19]

Jonsson, B. and Tsay, Y.-K. 1995. Assumption/guarantee specifications in linear-time temporal logic. In TAPSOFT '95: Theory and Practice of Software Development, P. Mosses, M. Nielsen, and M. Schwartzbach, Eds. Lecture Notes in Computer Science, vol. 915. Springer-Verlag, Aarhus, Denmark, 262-276.

[20]

Josko, B. 1987a. MCTL - an extension of CTL for modular verification of concurrent systems. In Temporal Logic in Specification, Proceedings. Lecture Notes in Computer Science, vol. 398. Springer-Verlag, Altrincham,UK, 165-187.

[21]

Josko, B. 1987b. Model checking of CTL formulae under liveness assumptions. In Proc. 14th Colloq. on Automata, Programming, and Languages (ICALP). Lecture Notes in Computer Science, vol. 267. Springer-Verlag, 280-289.

[22]

Josko, B. 1989. Verifying the correctness of AADL modules using model chekcing. In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (Proceedings of REX Workshop). Lecture Notes in Computer Science, vol. 430. Springer-Verlag, Mook, The Netherlands, 386-400.

[23]

Kupferman, O. and Grumberg, O. 1996. Buy one, get one free Journal of Logic and Computation 6, 4, 523-539.

[24]

Kupferman, O. and Vardi, M. 1995. On the complexity of branching modular model checking. In Proc. 6th Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 962. Springer-Verlag, Philadelphia, 408-422.

[25]

Kupferman, O. and Vardi, M. 1998. Verifcation of fair transition systems. Chicago Journal of Theoretical Computer Science 1998, 2 (March).

[26]

Kupferman, O., Vardi, M., and Wolper, P. 2000. An automata-theoretic approach to branching-time model checking. Journal of the ACM 47, 2 (March).

[27]

Kurshan, R. 1987. Reducibility in analysis of coordination. Lecture Notes in Computer Science, vol. 103. Springer-Verlag, 19-39.

[28]

Lamport, L. 1980. Sometimes is sometimes not never" - on the temporal logic of programs. In Proc. 7th ACM Symposium on Principles of Programming Languages. 174-185.

[29]

Lamport, L. 1983. Specifying concurrent program modules. ACM Trans. on Programming Languages and Systenms 5, 190-222.

[30]

Lichtenstein, O. and Pnueli, A. 1985. Checking that iinite state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symposium on Principles of Programming Languages. New Orleans, 97-107.

[31]

Lynch, N. 1977. Log space recognition and translation of parenthesis languages. Journal ACM 24, 583-590.

[32]

Milner, R. 1971. An algebraic definition of simulation between programs. In Proc. 2nd International Joint Conference on Artificial Intelligence. British Computer Society, 481-489.

[33]

Misra, B. and Chandy, K. 1981. Proofs of networks of processes. IEEE Trans. on Software Engineering 7, 417-426.

[34]

Muller, D. and Schupp, P. 1987. Alternating automata on infinite trees. Theoretical Computer Science 54, 267-276.

[35]

Muller, D., Saoudi, A., and Schupp, P. 1986. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Colloquium on Automata, Languages and Programming. Springer-Verlag.

[36]

Pnueli, A. 1977. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science. 46-57.

[37]

Pnueli, A. 1981. The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45-60.

[38]

Pnueli, A. 1985a. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Proc. Advanced School on Current Trends in Concurrency. Volume 224, LNCS, Springer-Verlag, Berlin, 510-584.

[39]

Pnueli, A. 1985b. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, K. Apt, Ed. NATO Advanced Summer Institutes, vol. F-13. Springer-Verlag, 123-144.

[40]

Queille, J. and Sifakis, J. 1981. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming. Vol. 137. Springer-Verlag, Lecture Notes in Computer Science, 337-351.

[41]

Safra, S. 1988. On the complexity of !-automata. In Proc. 29th IEEE Symposium on Foundations of Computer Science. White Plains, 319-327.

[42]

Safra, S. 1989. Complexity of automata on infinite objects. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel.

[43]

Savitch, W. 1970. Relationship between nondeterministic and deterministic tape complexities. Journal on Computer and System Sciences 4, 177-192.

[44]

Sistla, A. and Clarke, E. 1985. The complexity of propositional linear temporal logic. Journal ACM 32, 733-749.

[45]

Sistla, A. and Zuck, L. 1993. Reasoning in a restricted temporal logic. Information and Computation 102, 2, 167-195.

[46]

Stark, E. 1984. Foundations of theory of specifications for distributed systems. Ph.D. thesis, M.I.T.

[47]

Vardi, M. 1995. On the complexity of modular model checking. In Proc. 10th IEEE Symposium on Logic in Computer Science. 101-111.

[48]

Vardi, M. and Stockmeyer, L. 1985. Improved upper and lower bounds for modal logics of programs. In Proc 17th ACM Symp. on Theory of Computing. 240-251.

[49]

Vardi, M. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proc. First Symposium on Logic in Computer Science. Cambridge, 332-344.

[50]

Vardi, M. and Wolper, P. 1994. Reasoning about infinite computations. Information and Computation 115, 1 (November), 1-37.

Cited By

Aminof BCooper LRubin SVardi MZuleger FMarquis POrtiz MPagnucco M(2024)Probabilistic synthesis and verification for LTL on finite tracesProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning10.24963/kr.2024/3(27-37)Online publication date: 2-Nov-2024
https://dl.acm.org/doi/10.24963/kr.2024/3
Rajasekaran SBansal SVardi MElkind E(2023)Multi-agent systems with quantitative satisficing goalsProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/32(280-288)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/32
MARTÍN ÓVERDEJO AMARTÍ-OLIET N(2023)Compositional Verification in Rewriting LogicTheory and Practice of Logic Programming10.1017/S1471068423000340(1-53)Online publication date: 31-Aug-2023
https://doi.org/10.1017/S1471068423000340
Show More Cited By

Index Terms

An automata-theoretic approach to modular model checking

Recommendations

On the complexity of modular model checking
LICS '95: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science

In modular verification the specification of a module consists of two parts. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the environment with which the module is interacting. This is called ...
Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement

Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an ...
Modular Model Checking
COMPOS'97: Revised Lectures from the International Symposium on Compositionality: The Significant Difference

In modular verification the specification of a module consists of two parts. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 22, Issue 1

Jan. 2000

186 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/345099

Editor:
William Pugh
Univ. of Maryland, College Park

Issue’s Table of Contents

Copyright © 2000 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2000

Published in TOPLAS Volume 22, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

43
Total Citations
View Citations
1,060
Total Downloads

Downloads (Last 12 months)73
Downloads (Last 6 weeks)4

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Aminof BCooper LRubin SVardi MZuleger FMarquis POrtiz MPagnucco M(2024)Probabilistic synthesis and verification for LTL on finite tracesProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning10.24963/kr.2024/3(27-37)Online publication date: 2-Nov-2024
https://dl.acm.org/doi/10.24963/kr.2024/3
Rajasekaran SBansal SVardi MElkind E(2023)Multi-agent systems with quantitative satisficing goalsProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/32(280-288)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/32
MARTÍN ÓVERDEJO AMARTÍ-OLIET N(2023)Compositional Verification in Rewriting LogicTheory and Practice of Logic Programming10.1017/S1471068423000340(1-53)Online publication date: 31-Aug-2023
https://doi.org/10.1017/S1471068423000340
Chodil MKučera AKřetínský J(2022)Satisfiability of Quantitative Probabilistic CTL: Rise to the ChallengePrinciples of Systems Design10.1007/978-3-031-22337-2_18(364-387)Online publication date: 29-Dec-2022
https://doi.org/10.1007/978-3-031-22337-2_18
Westman JNyberg M(2018)Conditions of contracts for separating responsibilities in heterogeneous systemsFormal Methods in System Design10.1007/s10703-017-0294-752:2(147-192)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10703-017-0294-7
Martín ÓVerdejo AMartí-Oliet N(2018)Parameterized Programming for Compositional System SpecificationRewriting Logic and Its Applications10.1007/978-3-319-99840-4_4(59-75)Online publication date: 8-Sep-2018
https://doi.org/10.1007/978-3-319-99840-4_4
Soleimanifard SGurov D(2016)Algorithmic verification of procedural programs in the presence of code variabilityScience of Computer Programming10.1016/j.scico.2015.08.010127:C(76-102)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1016/j.scico.2015.08.010
Martín ÓVerdejo AMartí-Oliet N(2016)Synchronous Products of Rewrite SystemsAutomated Technology for Verification and Analysis10.1007/978-3-319-46520-3_10(141-156)Online publication date: 22-Sep-2016
https://doi.org/10.1007/978-3-319-46520-3_10
Westman JNyberg M(2015)Contracts for Specifying and Structuring Requirements on Cyber-Physical SystemsCyber-Physical Systems10.1201/b19290-19(307-341)Online publication date: 13-Oct-2015
https://doi.org/10.1201/b19290-19
Soleimanifard SGurov D(2015)Algorithmic Verification of Procedural Programs in the Presence of Code VariabilityFormal Aspects of Component Software10.1007/978-3-319-15317-9_20(327-345)Online publication date: 30-Jan-2015
https://doi.org/10.1007/978-3-319-15317-9_20
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents