An automata-theoretic approach to linear temporal logic. (English) Zbl 1543.68236
Moller, Faron (ed.) et al., Logics for concurrency: structure versus automata. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1043, 238-266 (1996).
Summary: The automata-theoretic approach to linear temporal logic uses the theory of automata as a unifying paradigm for program specification, verification, and synthesis. Both programs and specifications are in essence descriptions of computations. These computations can be viewed as words over some alphabet. Thus, programs and specifications can be viewed as descriptions of languages over some alphabet. The automata-theoretic perspective considers the relationships between programs and their specifications as relationships between languages. By translating programs and specifications to automata, questions about programs and their specifications can be reduced to questions about automata. More specifically, questions such as satisfiability of specifications and correctness of programs with respect to their specifications can be reduced to questions such as nonemptiness and containment of automata.
Unlike classical automata theory, which focused on automata on finite words, the applications to program specification, verification, and synthesis, use automata on infinite words, since the computations in which we are interested are typically infinite. This paper provides an introduction to the theory of automata on infinite words and demonstrates its applications to program specification, verification, and synthesis.
For the entire collection see [Zbl 1540.68015].
Unlike classical automata theory, which focused on automata on finite words, the applications to program specification, verification, and synthesis, use automata on infinite words, since the computations in which we are interested are typically infinite. This paper provides an introduction to the theory of automata on infinite words and demonstrates its applications to program specification, verification, and synthesis.
For the entire collection see [Zbl 1540.68015].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 03B70 | Logic in computer science |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q45 | Formal languages and automata |
References:
| [1] | M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable concurrent program specifications. In Proc. 16th Int. Colloquium on Automata, Languages and Programming, volume 372, pages 1-17. Lecture Notes in Computer Science, Springer-Verlag, July 1989. |
| [2] | J.R. Büchi and L.H.G. Landweber. Solving sequential conditions by finite-state strategies. Trans. AMS, 138:295-311, 1969. · Zbl 0182.02302 |
| [3] | J.A. Brzozowski and E. Leiss. Finite automata, and sequential networks. Theoretical Computer Science, 10:19-35, 1980. · Zbl 0415.68023 |
| [4] | J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, pages 1-12, Stanford, 1962. Stanford University Press. · Zbl 0147.25103 |
| [5] | Y. Choueka. Theories of automata on \(ω\)-tapes: A simplified approach. J. Computer and System Sciences, 8:117-141, 1974. · Zbl 0292.02033 |
| [6] | A. Church. Logic, arithmetics, and automata. In Proc. International Congress of Mathematicians, 1962, pages 23-35. institut Mittag-Leffler, 1963. · Zbl 0116.33604 |
| [7] | A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114-133, January 1981. · Zbl 0473.68043 |
| [8] | T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. MIT Press, 1990. · Zbl 1158.68538 |
| [9] | 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. |
| [10] | D.L. Dill. Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, 1989. |
| [11] | E.A. Emerson and E.M. Clarke. Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241-266, 1982. · Zbl 0514.68032 |
| [12] | E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151-178, 1986. · Zbl 0629.68020 |
| [13] | 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, October 1988. |
| [14] | E.A. Emerson and C. Jutla. On simultaneously determinizing and complementing \(ω\)-automata. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pages 333-342, 1989. · Zbl 0716.03035 |
| [15] | E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 84-96, New Orleans, January 1985. |
| [16] | E.A. Emerson and C.-L. Lei. Temporal model checking under generalized fairness constraints. In Proc. 18th Hawaii International Conference on System Sciences, Hawaii, 1985. |
| [17] | 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. · Zbl 0603.03005 |
| [18] | M. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-completeness. W. Freeman and Co., San Francisco, 1979. · Zbl 0411.68039 |
| [19] | D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pages 163-173, January 1980. |
| [20] | D. Gale and F. M. Stewart. Infinite games of perfect information. Ann. Math. Studies, 28:245-266, 1953. · Zbl 0050.14305 |
| [21] | D. Harel and A. Pnueli. On the development of reactive systems. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 477-498. Springer-Verlag, 1985. · Zbl 0581.68046 |
| [22] | R. Hossley and C.W. Rackoff. The emptiness problem for automata on infinite trees. In Proc. 13th IEEE Symp. on Switching and Automata Theory, pages 121-124, 1972. |
| [23] | J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, New York, 1979. · Zbl 0426.68001 |
| [24] | N.D. Jones. Space-bounded reducibility among combinatorial problems. Journal of Computer and System Sciences, 11:68-75, 1975. · Zbl 0317.02039 |
| [25] | L. Lamport. Sometimes is sometimes “not never” — on the temporallogic of programs. In Proceedings of the 7th ACM Symposiumon Principles of Programming Languages, pages 174-185, January 1980. |
| [26] | Leiss. Succinctrepresentation of regular languages by boolean automata. Theoretical Computer Science, 13:323-330, 1981. · Zbl 0458.68017 |
| [27] | M.T. Liu. Protocol engineering. Advances in Computing, 29:79-195, 1989. |
| [28] | O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97-107, New Orleans, January 1985. |
| [29] | O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logics of Programs, volume 193, pages 196-218, Brooklyn, June 1985. Lecture Notes in Computer Science, Springer-Verlag. · Zbl 0586.68028 |
| [30] | R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521-530, 1966. · Zbl 0212.33902 |
| [31] | A.R. Meyer and M.J. Fischer. Economy of description by automata, grammars, and formal systems. In Proc. 12th IEEE Symp. on Switching and Automata Theory, pages 188-191, 1971. |
| [32] | S. Miyano and T. Hayashi. Alternating finite automata on \(ω\)-words. Theoretical Computer Science, 32:321-330, 1984. · Zbl 0544.68042 |
| [33] | M. Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 1988. |
| [34] | Y.N. Moschovakis. Descriptive Set Theory. North Holland, 1980. · Zbl 0433.03025 |
| [35] | Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, January 1992. |
| [36] | A.R. Meyer and L.J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential time. In Proc. 13th IEEE Symp. on Switching and Automata Theory, pages 125-129, 1972. |
| [37] | D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54,:267-276, 1987. · Zbl 0636.68108 |
| [38] | 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 tune. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, pages 422-427, Edinburgh, July 1988. |
| [39] | Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6(1):68-93, January 1984. · Zbl 0522.68030 |
| [40] | S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455-495, July 1982. · Zbl 0483.68013 |
| [41] | R. Peikert. \(ω\)-regular languages and propositional temporal logic. Technical Report 85-01, ETH, 1985. |
| [42] | A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46-57, 1977. |
| [43] | A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the Sixteenth ACM Symposium on Principles of Programming Languages, Austin, Januery 1989. |
| [44] | M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1-35, 1969. · Zbl 0221.02031 |
| [45] | M.O. Rabin. Automata on infinite objects and Church’s problem. In Regional Conf. Ser. Math., 13, Providence, Rhode Island, 1972. AMS. · Zbl 0315.02037 |
| [46] | M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM J. of Research and Development, 3:115-125, 1959. · Zbl 1461.68105 |
| [47] | H. Rudin. Network protocols and tools to help produce them. Annual Review of Computer Science, 2:291-316, 1987. |
| [48] | S. Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988. |
| [49] | W.J. Savitch. Relationship between nondeterministic and deterministic tape complexities. J. on Computer and System Sciences, 4:177-192, 1970. · Zbl 0188.33502 |
| [50] | A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. J. ACM, 32:733-749, 1985. · Zbl 0632.68034 |
| [51] | A.P. Sistla. Theoretical issues in the design and analysis of distributed systems. PhD thesis, Harvard University, 1983. |
| [52] | R. Sherman, A. Pnueli, and D. Harel. Is the interesting part of process logic uninteresting: a translation from PL to PDL. SIAM J. on Computing, 13(4):825-839, 1984. · Zbl 0551.68031 |
| [53] | A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217-237, 1987. · Zbl 0613.03015 |
| [54] | W. Thomas. Automata on infinite objects. Handbook of theoretical computer science, pages 165-191, 1990. |
| [55] | M.Y. Vardi. Nontraditional applications of automata theory. In Proc. Int’l Symp. on Theoretical Aspects of Computer Software, volume 789, pages 575-597. Lecture Notes in Computer Science, Springer-Verlag, 1994. · Zbl 0942.68600 |
| [56] | 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. |
| [57] | 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. |
| [58] | M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, November 1994. · Zbl 0827.03009 |
| [59] | P. Wolper. Synthesis of Communicating Processes from Temporal Logic Specifications. PhD thesis, Stanford University, 1982. |
| [60] | P. Wolper, M.Y. Vardi, and A.P. Sistla. Reasoning about infinite computation paths. In Proc. 24th IEEE Symposium on Foundations of Computer Science, pages 185-194, Tucson, 1983. |
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.
