×

zbMATH — the first resource for mathematics

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)
PDF BibTeX XML Cite
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, (), 1-12 · Zbl 0147.25103
[3] Büchi, J.R., The monadic theory of ω_1, (), 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 New York · Zbl 0317.94045
[6] Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., The temporal analysis of fairness, 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, (), 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, (), 132-154
[11] Meyer, A.R.; Stockmeyer, L.J., The equivalence problem for regular expressions with squaring requires exponential time, 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, (), 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, Proc. 6th ACM symp. on theory of computing, 161-171, (1974)
[19] Siefkes, D., ()
[20] Sistla, A.P., Theoretical issues in the design and verification of distributed systems, ()
[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, () · Zbl 0444.94037
[23] Trakhtenbrot, B.A.; Barzdin, Y.M., Finite automata behavior and synthesis, (1973), North-Holland Amsterdam · Zbl 0271.94032
[24] Vardi, M.Y.; Stockmeyer, L., Improved upper and lower bounds for modal logics of programs, Providence, Proc. 17th ACM symp. on theory of computing, 240-251, (1985)
[25] Vardi, M.Y.; Wolper, P., Yet another process logic, (), 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. · Zbl 0827.03009
[28] Wolper, P.; Vardi, M.Y.; Sistla, A.P., Reasoning about infinite computation paths, Tucson, Proc. 24th IEEE symp. on foundations of computer science, 185-194, (1983)
[29] Wolper, P., Synthesis of communicating processes from temporal logic specifications, () · 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.