×

The complementation problem for Büchi automata with applications to temporal logic. (English) Zbl 0613.03015

Cf. the review of the preliminary version [Lect. Notes Comput. Sci. 194, 465-474 (1985)] in Zbl 0577.03019.

MSC:

03D05 Automata and formal grammars in connection with logical questions
03B70 Logic in computer science
03B25 Decidability of theories and sets of sentences
68Q65 Abstract data types; algebraic specification
03D15 Complexity of computation (including implicit computational complexity)
03B45 Modal logic (including the logic of norms)

Citations:

Zbl 0577.03019
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alaiwan, H., Equivalence of infinite behavior of finite automata, Theoret. Comput. Sci., 31, 297-306 (1984) · Zbl 0568.68036
[2] Büchi, J. R., On a decision method in restricted second-order arithmetic, (Proc. Internat. Congr. Logic, Methodology and Philosophy of Science 1960 (1962), Stanford University Press), 1-12 · Zbl 0147.25103
[3] Büchi, J. R., The monadic theory of \(ω_1\), (Decidable Theories II. Decidable Theories II, Lecture Notes in Mathematics, 328 (1973), Springer: Springer Berlin), 1-127
[4] Choueka, Y., Theories of automata on ω-tapes: a simplified approach, J. Comput. System Sci., 8, 117-141 (1974) · Zbl 0292.02033
[5] Eilenberg, S., Automata, Languages and Machines, Vol. A (1974), Academic Press: Academic Press New York · Zbl 0317.94045
[6] Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., The temporal analysis of fairness, Las Vegas. Las Vegas, Proc. 7th ACM Symp. on Principles of Programming Languages, 163-173 (1980)
[7] Harel, D.; Kozen, D.; Parikh, R., Process logic: expressiveness, decidability, completeness, J. Comput. System Sci., 25, 144-170 (1982) · Zbl 0494.03016
[8] Manna, Z.; Pnuelli, A., Verification of concurrent programs: the temporal framework, (Boyer, R. S.; Moore, J. S., The Correctness Problem in Computer Science (1981), Academic Press: Academic Press New York/London), 215-273
[9] McNaughton, R., Testing and generating infinite sequences by a finite automation, Inform. and Control, 9, 521-530 (1966) · Zbl 0212.33902
[10] Meyer, A. R., Weak monadic second-order theory of successor is not elementary recursive, (Proc. Logic Colloquium. Proc. Logic Colloquium, Lecture Notes in Mathematics, 453 (1975), Springer: Springer Berlin), 132-154
[11] Meyer, A. R.; Stockmeyer, L. J., The equivalence problem for regular expressions with squaring requires exponential time, Long Beach. Long Beach, Proc. 13th IEEE Symp. on Switching and Automata Theory, 125-129 (1972)
[12] Nishimura, H., Descriptively complete process logic, Acta Inform., 14, 359-369 (1980) · Zbl 0423.68005
[13] Owicki, S.; Lamport, L., Proving liveness properties of concurrent programs, Trans. ACM, 4, 455-495 (1982) · Zbl 0483.68013
[14] Pnueli, A., The temporal logic of concurrent programs, Theoret. Comput. Sci., 13, 45-60 (1981) · Zbl 0441.68010
[15] Rabin, M. O., Decidability of second-order theories and automata on infinite trees, Trans. AMS, 141, 1-35 (1969) · Zbl 0221.02031
[16] Rabin, M. O., Weakly definable relations and special automata, (Bar-Hillel, Y., Proc. Symp. Mathematical Logic and Foundations of Set Theory (1970), North-Holland: North-Holland Amsterdam), 1-23 · Zbl 0214.02208
[17] Rabin, M. O.; Scott, D., Finite automata and their decision problems, IBM J. Res. & Dev., 3, 114-125 (1959) · Zbl 0158.25404
[18] Robertson, E. L., Structure of complexity in the weak monadic second-order theory of the natural numbers, Seattle. Seattle, Proc. 6th ACM Symp. on Theory of Computing, 161-171 (1974)
[19] Siefkes, D., (Decidable Theories I—Büchi’s Monadic Second-Order Successor Arithmetics. Decidable Theories I—Büchi’s Monadic Second-Order Successor Arithmetics, Lecture Notes in Mathematics, 120 (1970), Springer: Springer Berlin) · Zbl 0213.01901
[20] Sistla, A. P., Theoretical issues in the design and verification of distributed systems, (Ph.D. Thesis (1983), Harvard University)
[21] Sistla, A. P.; Clarke, E. M., The complexity of propositional linear time logics, J. ACM, 32, 733-749 (1985) · Zbl 0632.68034
[22] Stockmeyer, L. J., The complexity of decision problems in automata theory and logic, (Ph.D. Dissertation. Ph.D. Dissertation, Tech. Rep. MAC MIT TR-133 (1974), M.I.T.) · Zbl 0444.94037
[23] Trakhtenbrot, B. A.; Barzdin, Y. M., Finite Automata Behavior and Synthesis (1973), North-Holland: North-Holland Amsterdam · Zbl 0271.94032
[24] Vardi, M. Y.; Stockmeyer, L., Improved upper and lower bounds for modal logics of programs, Providence. Providence, Proc. 17th ACM Symp. on Theory of Computing, 240-251 (1985)
[25] Vardi, M. Y.; Wolper, P., Yet another process logic, (Logics of Programs. Logics of Programs, Lecture Notes in Computer Science, 164 (1983), Springer: Springer Berlin), 501-512 · Zbl 0549.68020
[26] Vardi, M. Y.; Wolper, P., Automata-theoretic techniques for modal logics of programs, J. Comput. System Sci., 32, 183-221 (1986) · Zbl 0622.03017
[27] M.Y. Vardi and P. Wolper, Reasoning about infinite computation paths, to appear.; M.Y. Vardi and P. Wolper, Reasoning about infinite computation paths, to appear. · Zbl 0827.03009
[28] Wolper, P.; Vardi, M. Y.; Sistla, A. P., Reasoning about infinite computation paths, Tucson. Tucson, Proc. 24th IEEE Symp. on Foundations of Computer Science, 185-194 (1983)
[29] Wolper, P., Synthesis of communicating processes from temporal logic specifications, (Ph.D. Thesis (1982), Stanford University) · Zbl 0487.68027
[30] Wolper, P., Temporal logic can be more expressive, Inform. and Control, 56, 72-99 (1983) · Zbl 0534.03009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.