Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)
Language :
English
Title :
An Automata-Theoretic Approach to Branching-Time Model Checking
Publication date :
1994
Event name :
6th International workshop on computer-aided verification
Event place :
Stanford, United States - California
Event date :
June 21–23, 1994
Audience :
International
Main work title :
Computer Aided Verification, Proc. 6th Int. Workshop
[Bee80] C. Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. on Database Systems, 5:241-259, 1980.
[BG93] O. Bernboltz and O. Grumberg. Branching time temporal logic and amorphous tree automata. In Proc. 4th Conferance on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 262-277, Hildesheim, August 1993. Springer- Verlag.
[CES86] E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, January 1986.
[Cle93] R. Cleaveland. A linear-time model-checking algorithm for the alternation-free modal #-calculus. Formal Methods in System Design, 2:121-147, 1993.
[CVWY92] C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275-288, 1992.
[EJ88] E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, oct 1988.
[EJ91] E.A. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science, pages 368-377, San Juan, Oct 1991.
[EJS93] E.A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of µ- calculus. In Computer Aided Verification, Proc. 5th Int. Workshop, volume 697, pages 385-396, Elounda, Crete, June 1993. Lecture Notes in Computer Science, Springer- Verlag.
[Eme85] E.A. Emerson. Automata, tableaux, and temporal logics. In Proc. Workshop on Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79-87. Springer-Verlag, 1985.
[Eme90] E.A. Emerson. Temporal and modal logic. Handbook of theoretical computer science, pages 997-1072, 1990.
[Eme94] E.A. Emerson. Automated temporal reasoning about reactive systems. In VIII-th BANFF Higher Order Workshop, 1994. unpublished abstract of forthcoming talk.
[ES84] A.E. Emerson and A.P. Sistla. Deciding full branching time logics. Information and Control, 61(3):175-201, 1984.
[JJ89] C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, volume 407, pages 189-196, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag.
[Koz83] D. Kozen. Results on the propositional µ-calculus. Theoretical Computer Science, 27:333-354, 1983.
[Lam80] L. Lamport. Sometimes is sometimes”not never” - on the temporal logic of programs. In Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pages 174-185, January 1980.
[LP85] O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposiumon Principles of Programming Languages, pages 97-107, New Orleans, January 1985.
[MS87] D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267-276, 1987.
[MSS86] D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Colloquium on Automata, Languages and Programming. Springer-Verlag, 1986.
[MSS88] D. E. Muller, A. Saoudi, and P. E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, pages 422-427, Edinburgh, July 1988.
[Pnu81] A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45-60, 1981.
[QS81] J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th Int’l Symp. on Programming, volume 137, pages 337-351. Springer-Verlag, Lecture Notes in Computer Science, 1981.
[SE84] R. S. Street and E. A. Emerson. An elementary decision procedure for the mucalculus. In Proc. 11th Int. Colloquium on Automata, Languages and Programming, volume 172. Lecture Notes in Computer Science, Springer-Verlag, July 1984.
[SW91] C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1):161-177, 1991.
[Tho90] W. Thomas. Automata on infinite objects. Handbook of theoretical computer science, pages 165-191, 1990.
[Var88] M.Y. Vardi. A temporal fixpoint calculus. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 250-259, San Diego, January 1988.
[VL93] B. Vergauwen and J. Lewi. A linear local model checking algorithm for ctl. In Proc. CONCUR '93, volume 715 of Lecture Notes in Computer Science, pages 447-461, Hildesheim, August 1993. Springer-Verlag.
[VS85] M.Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th ACM Symp. on Theory of Computing, pages 240-251, 1985.
[VW84] M.Y. Vardi and P. Wolper. Yet another process logic. In Logics of Programs, volume 398, pages 501-512. Lecture Notes in Computer Science, Springer-Verlag, 1984.
[VW86a] M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322-331, Cambridge, June 1986.
[VW86b] M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2): 182-21, April 1986.
[VW94] M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 110(2), May 1994. (To appear).
[Wo183] P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1- 2):72-99, 1983.
[Wo189] P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specijication, volume 398, pages 75-123. Lecture Notes in Computer Science, Springer-Verlag, 1989.
