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 :
The complementation problem for Buchi automata with applications to temporal logic
Alaiwan, Equivalence of infinite behavior of finite automata (1984) Theoret. Comput. Sci., 31, pp. 297-306
Büchi, On a decision method in restricted second-order arithmetic (1962) Proc. Internat. Congr. Logic, Methodology and Philosophy of Science 1960, pp. 1-12. , Stanford University Press
Büchi, The monadic theory of ω1 (1973) Decidable Theories II, 328, pp. 1-127. , Lecture Notes in Mathematics, Springer, Berlin
Choueka, Theories of automata on ω-tapes: a simplified approach (1974) J. Comput. System Sci., 8, pp. 117-141
Eilenberg, (1974) Automata, Languages and Machines, Vol. A, , Academic Press, New York
Gabbay, Pnueli, Shelah, Stavi, The temporal analysis of fairness (1980) Proc. 7th ACM Symp. on Principles of Programming Languages, pp. 163-173. , Las Vegas
Harel, Kozen, Parikh, Process logic: expressiveness, decidability, completeness (1982) J. Comput. System Sci., 25, pp. 144-170
Manna, Pnuelli, Verification of concurrent programs: the temporal framework (1981) The Correctness Problem in Computer Science, pp. 215-273. , R.S. Boyer, J.S. Moore, Academic Press, New York/London
McNaughton, Testing and generating infinite sequences by a finite automation (1966) Inform. and Control, 9, pp. 521-530
Meyer, Weak monadic second-order theory of successor is not elementary recursive (1975) Proc. Logic Colloquium, 453, pp. 132-154. , Lecture Notes in Mathematics, Springer, Berlin
Meyer, Stockmeyer, The equivalence problem for regular expressions with squaring requires exponential time (1972) Proc. 13th IEEE Symp. on Switching and Automata Theory, pp. 125-129. , Long Beach
Nishimura, Descriptively complete process logic (1980) Acta Inform., 14, pp. 359-369
Owicki, Lamport, Proving liveness properties of concurrent programs (1982) Trans. ACM, 4, pp. 455-495
Pnueli, The temporal logic of concurrent programs (1981) Theoret. Comput. Sci., 13, pp. 45-60
Rabin, Decidability of second-order theories and automata on infinite trees (1969) Trans. AMS, 141, pp. 1-35
Rabin, Weakly definable relations and special automata (1970) Proc. Symp. Mathematical Logic and Foundations of Set Theory, pp. 1-23. , Y. Bar-Hillel, North-Holland, Amsterdam
Rabin, Scott, Finite automata and their decision problems (1959) IBM J. Res. & Dev., 3, pp. 114-125
Robertson, Structure of complexity in the weak monadic second-order theory of the natural numbers (1974) Proc. 6th ACM Symp. on Theory of Computing, pp. 161-171. , Seattle
Siefkes, Decidable Theories I—Büchi's Monadic Second-Order Successor Arithmetics (1970) Lecture Notes in Mathematics, 120. , Springer, Berlin
Sistla, Theoretical issues in the design and verification of distributed systems (1983) Ph.D. Thesis, , Harvard University
Sistla, Clarke, The complexity of propositional linear time logics (1985) J. ACM, 32, pp. 733-749
Stockmeyer, The complexity of decision problems in automata theory and logic (1974) Ph.D. Dissertation, , Tech. Rep. MAC MIT TR-133, M.I.T
Vardi, Stockmeyer, Improved upper and lower bounds for modal logics of programs (1985) Proc. 17th ACM Symp. on Theory of Computing, pp. 240-251. , Providence
Vardi, Wolper, Yet another process logic (1983) Logics of Programs, 164, pp. 501-512. , Lecture Notes in Computer Science, Springer, Berlin
Vardi, Wolper, Automata-theoretic techniques for modal logics of programs (1986) J. Comput. System Sci., 32, pp. 183-221
M.Y. Vardi and P. Wolper, Reasoning about infinite computation paths, to appear
Wolper, Vardi, Sistla, Reasoning about infinite computation paths (1983) Proc. 24th IEEE Symp. on Foundations of Computer Science, pp. 185-194. , Tucson
Wolper, Synthesis of communicating processes from temporal logic specifications (1982) Ph.D. Thesis, , Stanford University
Wolper, Temporal logic can be more expressive (1983) Inform. and Control, 56, pp. 72-99
