A Partial Approach To Model Checking

Godefroid, Patrice; Wolper, Pierre

doi:10.1006/inco.1994.1035

Download

Article (Scientific journals)

A Partial Approach To Model Checking

Godefroid, Patrice; Wolper, Pierre

1994 • In Information and Computation, 110 (2), p. 305-326

Peer Reviewed verified by ORBi

Permalink
https://hdl.handle.net/2268/163843

DOI
10.1006/inco.1994.1035

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

GW 94 IC.pdf

Author postprint (331.95 kB)

Download

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

model-checking; partial-order; automata

Abstract :

[en] This paper presents a model-checking method for linear-time temporal logic that can avoid most of the state explosion due to the modelling of concurrency by interleaving. The method relies on the concept of Mazurkiewicz's trace as a semantic basis and uses automata-theoretic techniques, including automata that operate on words of ordinality higher than omega.

Disciplines :

Computer science

Author, co-author :

Godefroid, Patrice

Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique

Language :

English

Title :

A Partial Approach To Model Checking

Publication date :

1994

Journal title :

Information and Computation

ISSN :

0890-5401

eISSN :

1090-2651

Publisher :

Academic Press, Inc., San Diego, United States - California

Volume :

110

Issue :

Pages :

305-326

Peer reviewed :

Peer Reviewed verified by ORBi

Available on ORBi :

since 04 March 2014

Statistics

Number of views

55 (3 by ULiège)

Number of downloads

270 (1 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

235

Bibliography

Alur, R., Courcoubetis, C, and Dill, D. (1990), Model-checking for realtime systems, in "Proceedings of the 5th Symposium on Logic in Computer Science, Philadelphia, June 1990," pp. 414-425.
Aggarwal, S., Courcoubetis, C., and Wolper, P. (1990), Adding liveness properties to coupled finite-state machines, ACM Trans. Programming Languages Systems 12, No. 2, 303-339.
Alur, R., and Henzinger, T., Real-time logics; complexity and expressiveness, in "Proceedings of the 5th Symposium on Logic in Computer Science, Philadelphia, June 1990," pp. 390-401.
Aho, A. V., Hopcrokt, J. E., and Ullman, J. D. (1974), "The Design and Analysis of Computer Algorithms," Addison-Wesley, Reading, MA.
Browne, M., Clarke, E. M., and Dill, D. L. (1985), Automatic circuit verification using temporal logic: Two new examples, in "IEEE International Conference on Computer Design: VLSI and Computers, Port Chester, October 1985."
Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. (1990), Symbolic model checking: 1020 states and beyond, in "Proceedings of the 5th Symposium on Logic in Computer Science, Philadelphia, June 1990," pp. 428-439.
Bouajjani, A., Fernandez, J. C., and Halbwachs, N. (1990), "On the Verification of Safety Properties," Technical Report SPECTRE L12, IMAG, Grenoble.
Browne, M. C. (1986), An improved algorithm for the automatic verification of finite state systems using temporal logic, in "Proceedings of the First Symposium on Logic in Computer Science, Cambridge, June 1986," pp. 260-266.
Buchi, J. R. (1962), On a decision method in restricted second order arithmetic, in "Proceedings, International Congress, Logic, Method and Philosophy of Science, 1960, Stanford, 1962," pp. 112, Stanford Univ. Press, Stanford, CA.
Buchi, J. R. (1965), Decision methods in the theory of ordinals, Bull. Amer. Math. Soc. 71, 767-770.
Buchi, J. R. (1965), Transfinite automata recursions and weak second order theory of ordinals, in "Proceedings, International Congress, Logic, Method and Philosophy of Science, 1964," pp. 2-23, North-Holland, Amsterdam.
Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986), Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages Systems 8, No. 2, 244-263.
Clarke, E. M., and Grumberg, O. (1987), Avoiding the state explosion problem in temporal logic model-checking algorithms, in "Proceedings, 6th ACM Symposium on Principles of Distributed Computing, Vancouver, British Columbia, August 1987," pp. 294-303.
Clarke, E. M., Grumberg, O., and Browne, M. C. (1986), Reasoning about networks with many identical finite-state processes, in "Proceedings, 5th ACM Symposium on Principles of Distributed Computing, Calgary, Alberta, August 1986," pp. 240-248.
Cleaveland, R. (1990), Tableau-based model checking in the propositional mu-calculus, Acta Informal. 27, 725-747.
Coudert, O., Madre, J. C., and Berthet, C. (1990), Verifying temporal properties of sequential machines without building their state diagram, in "Proceedings, 2nd Workshop on Computer Aided Verification, Rutgers, June 1990," Lecture Notes in Computer Science, Vol. 531, pages 23-32, Springer- Verlag, Berlin/New York.
Col'rcoubetis, C., Vardi, M., Wolper, P., and Yannakakis, M. (1990), Memory efficient algorithms for the verification of temporal properties, in "Proceedings, 2nd Workshop on Computer Aided Verification, Rutgers, June 1990," Lecture Notes in Computer Science, Vol. 531, pp. 233-242.
Courcoubetis, C., and Yannakakis, M. (1990), Markov decision processes and regular events, in "Proceedings, 17th International Colloquium on Automata Languages and Programming, Coventry, July 1990," pp. 336-349, Lecture Notes in Computer Science, Vol. 443, Springer-Verlag, Berlin/New York.
Emerson, E. A., and Lei, C.-L. (1985), Modalities for model checking: Branching time logic strikes back, in "Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, New Orleans, January 1985," pp. 84-96.
Emerson, E. A., and Lei, C.-L., Temporal model checking under generalized fairness constraints, in "Proceedings, 18th Hawaii International Conference on System Sciences, Hawaii, 1985."
Emerson, E. A., and Lei, C.-L., Modalities for model checking: Branching time logic strikes back, in "Proceedings of the First Symposium on Logic in Computer Science, Cambridge, June 1986," pp. 267-278.
Godefroid, P., Holzmann, G. J., and Pirottin, D. (1992), State space caching revisited, in "Proceedings, 4th Workshop on Computer Aided Verification, Montreal, June 1992," pp. 178-191, Lecture Notes in Computer Science, Vol. 663, Springer-Verlag, Berlin/New York.
Godefroid, P. (1990), Using partial orders to improve automatic verification methods, in "Proceedings, 2nd Workshop on Computer Aided Verification, Rutgers, June 1990," pp. 176-185, Lecture Notes in Computer Science, Vol. 531, Berlin/New York.
Godefroid, P., and Pirottin, D. (1993), Refining dependencies improves partial-order verification methods, in "Proceedings, 5th Conference on Computer Aided Verification, Elounda. June 1993," pp. 438-149, Notes in Computer Science, Vol. 697, Springer-Verlag, Berlin/New York.
German, S., and Sistla, A. P. (1987), Reasoning with many processes, in "Proceedings of the First Symposium on Logic in Computer Science, Ithaca, June 1987," pp. 138-152.
Graf, S., and Stkffen, B. (1990), Using interface specifications for compositional reduction, in "Proceedings, 2nd Workshop on Computer Aided Verification, Rutgers, June 1990," pp. 186-196, Lecture Notes in Computer Science, Vol. 531, Springer-Verlag, Berlin/New York.
Godefroid, P., and Wolper, P. (1991), A partial approach to model checking, in "Proceedings of the 6th IEEE Symposium on Logic in Computer Science, Amsterdam, July 1991," pp. 406-451.
Godefroid, P., and Wolper, P. (1991), Using partial orders for the efficient verification of deadlock freedom and safety properties, in "Proceedings, 3rd Workshop on Computer Aided Verification, Aalborg, July 1991," pp. 332-342, Lecture Notes in Computer Science, Vol. 575.
Holzmann, G. J., Godefroid, P., and Pirottin, D. (1992), Coverage preserving reduction strategies for reachability analysis, in "Proceedings, 12th IFIP WG 6.1 International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida, June 1992," pp. 349-363, North-Holland.
Harel, E., Lichtenstein, O., and Pnleli, A. (1990), Explicit-clock temporal logic, in "Proceedings of the 5th Symposium on Logic in Computer Science, Philadelphia, June 1990," pp. 402-413.
Halbwachs, N., Pilaud, D., Olabdessflam, F., and Glory, A. C. (1989), Specifying, programming and verifying real-time systems, using a synchronous declarative language, in "Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, June 1989," pp. 213-231. Lecture Notes in Computer Science, Vol. 407, Springer-Verlag, Berlin/New York.
Jard, C., and Jeron, T. (1989), On-line model-checking for finite linear temporal logic specifications, in "Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, June 1989," pp. 189-196, Lecture Notes in Computer Science, Vol. 407, Springer-Verlag, Berlin/New York.
Kurshan, R. P., and McMillan, K. (1989), A structural induction theorem for processes, in "Proceedings of the Eighth ACM Symposium on Principles of Distributed Computing, Edmonton, Alberta, August 1989."
Kornatzky, Y., and Pinter, S. S. (1986), "A Model Checker for Partial Order Temporal Logic," EE PUB 597, Department of Electrical Engineering, Technion-Israel Institute of Technology.
Lichtenstein, O., and Pnueli, A. (1985), Checking that finite state concurrent programs satisfy their linear specification, in "Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, New Orleans, January 1985," pp. 97-107.
Mazurkiewicz, A. (1986), Trace theory, in "Petri Nets: Applications and Relationships to Other Models of Concurrency. Advances in Petri Nets 1986, Part II: Proceedings of an Advanced Course," pp. 279-324, Lecture Notes in Computer Science, Vol. 255.
Penczek, W. (1990), Proving partial order properties using cctl, in "Proceedings, Concurrency and Compositionality Workshop, San Miniato, Italy, 1990."
Probst, D. K., and Li, H. F. (1990), Using partial-order semantics to avoid the state explosion problem in asynchronous systems, in "Proceedings, 2nd Workshop on Computer Aided Verification, Rutgers, June 1990," pp. 146-155. Lecture Notes in Computer Science, Vol. 531, Springer-Verlag, Berlin/New York.
Pinter, S. S., and Wolper, P. (1984), A temporal logic for reasoning about partially ordered computations, in "Proceedings, 3rd ACM Symposium on Principles of Distributed Computing, Vancouver, 1984," pp. 28-37.
Pnueli, A., and Zuck, L. (1986), Probabilistic verification by tableaux, in "Proceedings of the First Symposium on Logic in Computer Science, Cambridge, June 1986," pp. 322-331.
Quielle, J. P., and Sifakis, J. (1981), Specification and verification of concurrent systems in cesar, in "Proceedings. 5th International Symposium on Programming," pp. 337-351, Lecture Notes in Computer Science, Vol. 137, Springer-Verlag, Berlin/New York.
Richier, J. L., Rodriguez, C., Sifakis, J., and Voiron, J. (1987), Verification in xesar of the sliding window protocol, in "Proceedings. IFIP WG 6.1 7th International Conference on Protocol Specification, Testing and Verification, Zurich, 1987," pp. 235-250. North-Holland, Amsterdam.
Stirling, C., and Walker, D. (1989), Local model checking in the modal mu-calculus, in "Proceedings, 15th Colloquium on Trees in Algebra and Programming," Lecture Notes in Computer Science. Springer-Verlag, Berlin/New York.
Thayse, A., et al. (1989), "From Modal Logic to Deductive Databases: Introducing a Logic Based Approach to Artificial Intelligence," Wiley. New York.
Valmari, A. (1990), A stubborn attack on state explosion, in "Proceedings, 2nd Workshop on Computer Aided Verification, Rutgers, June 1990," pp. 156-165, Lecture Notes in Computer Science, Vol. 531, Springer-Verlag, Berlin, New York.
Valmari, A. (1991), Stubborn sets for reduced state space generation, in "Advances in Petri Nets 1990," pp. 491-515, Lecture Notes in Computer Science, Vol. 483, Springer-Verlag, Berlin/New York.
Vardi, M. (1985), Automatic verification of probabilistic concurrent finite-state programs, in "Proceedings, 26th IEEE Symposium on Foundations of Computer Science, Portland, October 1985," pp. 327-338.
Vardi, M. (1988), A temporal fixpoint calculus, in "Proceedings, 15th ACM Symposium on Principles of Programming Languages, San Diego, January 1988," pp. 250-259.
Vardi, M. (1989), Unified verification theory, in "Proceedings, Temporal Logic in Specification" (B. Banieqbal, H. Barringer, and A. Pnueli, Eds.), pp. 202-212. itors, Lecture Notes in Computer Science, Vol. 398, Springer-Verlag, Berlin, New York.
Vardi, M. Y., and Wolper, P. (1986). An automata-theoretic approach to automatic program verification, in "Proceedings of the First Symposium on Logic in Computer Science, Cambridge, June 1986," pp. 322-331.
Wolper, P., and Godefroid, P. (1993), Partial-order methods for temporal verification, in "Proceedings, CONCUR "93," pp. 233-246, Lecture Notes in Computer Science, Vol. 715, Springer-Verlag, Berlin/New York.
Wolper, P., and Lovinfosse, V. (1989), Verifying properties of large sets of processes with network invariants, in "Automatic Verification Methods for Finite State Systems, Proceedings, International Workshop, Grenoble, June 1989," pp. 68-80, Lecture Notes in Computer Science, Vol. 407, Springer-Verlag, Berlin/New York.
Wolper, P. (1983), Temporal logic can be more expressive, Inform. and Control 56, 72-99.
Wolper, P. (1989), On the relation of programs and computations to models of temporal logic, in "Proceedings, Temporal Logic in Specification" (B. Banieqbal, FL Barringer, and A. Pnueli, Eds.), pp. 75-123, Lecture Notes in Computer Science, Vol. 398, Springer-Verlag, Berlin/New York.
Wolper, P., Vardi, M. Y., and Sistla, A. P. (1983), Reasoningb about infinite computation paths, in "Proceedings, 24th IEEE Symposium on Foundations of Computer Science, Tucson, 1983," pp. 185-194.