ABSTRACT
Two distinct extensions of temporal logic has been recently advocated in the literature. The first extension is the addition of fixpoint operators that enable the logic to make assertions about arbitrary regular events. The second extension is the addition of past temporal connectives that enables the logic to refer directly to the history of the computation. Both extensions are motivated by the desire to adapt temporal logic to modular, i.e., compositional, verification (as opposed to global verification). We introduce and study here the logic μTL, which is the extension of temporal logic by fixpoint operators and past temporal connectives. We extend the automata-theoretic paradigm to μTL. That is, we show how, given an μTL formula @@@@, we can produce a finite-state Büchi automaton A@@@@, whose size is at most exponentially bigger than the size of @@@@, such that A@@@@ accepts precisely the computations that satisfy @@@@. The result has immediate applications, e.g., an optimal decision procedure and a model-checking algorithm for μTL.
- AS85.Alpern, B., Schneider, F.B.: Verifying temporal properties without using temporal logic. Technical Report TP~-85-723, Cornell University, Dec. 1985. Google ScholarDigital Library
- AS87.Alpern, B., Schneider, F.B.: Proving Boolean combinations of deterministic properties. Proc. 2nd IEEE Syrup. on Logic in Computer Science, Ithaca, june 1987.Google Scholar
- Ba86.Barringer, H.: Using tempora.1 logic in the compositional specification of concurrent systems. Dept. of Computer Science, University of Manchester, Technica.1 Report UMCS-86-10-1.Google Scholar
- BB86.Banieqbal, B. Barringer: A study of an extended temporal language and a temporal fixed point calculus. Dept. of Computer Science, University of Manchester, Technical Report UMCS-86-10-2.Google Scholar
- BK85.B. Barringer, Kuiper, R.: Hierarchical development of concurrent systems in a temporal logic framework. Seminar in Concurrency, eds. S.D. Brookes et al., Springer- Verlag, Lecture Notes in Computer Science 197, 1985, pp. 35-61. Google ScholarDigital Library
- BKP85.Barringer, H., Kuiper, R., Pnueli, A.: A compositional temporal approach to a csplike language. Formal Models of Programming, eds. E.J. Neuhold and G. Chroust, North Holland, 1985, pp. 207-227.Google Scholar
- BKP86.Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. Proc. 13th ACM Syrup. on Principles of Programming Languages, St. Petersburg, 1986. Google ScholarDigital Library
- Bu62.Biichi, J.R.: On a decision method in restricted second-order arithmetics. Proc. Int'l Congr. on Logic, Method. and Phil. of Sci. 1960, Stanford University Press, 1962, pp. 1-12.Google Scholar
- Ch74.Choueka, Y.: Theories of automata on co-tapes- a simplified approach. J. Computer and System Science 8(1974), pp. 117- 141.Google ScholarDigital Library
- EC80.Emerson, E.A., Clarke, E.C.: Characterizing correctness properties of parallel programs using fixpoints. Proc. 7th Int'l Colloq. on Automata, Languages and Programming, 1980, pp. 169-18I. Google ScholarDigital Library
- EP87.Emerson, E.A., Pnueli, A.: Temporal and Modal Logic. Handbook of Theoretical Computer Science, eds. J. van Leeuwen et. al., North-Holland Pub., in press, 1987.Google Scholar
- FL79.Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Y. Computer and Systems Science, 18(1979), pp. 194-211.Google ScholarCross Ref
- GPSS80.Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. Proc. 7th A CM Syrup. on Principles of Programming Languages, 1980, pp. 163- 173. Google ScholarDigital Library
- Ko82.Kozen, D.: t~esults on the propositional mu-calculus. Proc. 9th Int'l Colloq. on Automata, Languages and Programming, 1982, pp. 348-359. Google ScholarDigital Library
- KVR83.Koymans, R., Vytopil, J., DetLoever, W.P.: Real-time programming and asynchronous message passing. Proc. 2nd A CM Syrup. on Principles o/Distributed Computing, Montreal, 1983, pp. 187-197. Google ScholarDigital Library
- LP85.Lichtenstein, O., Pnueli, A.: Checking that finite-state concurrent programs satisfy their linear specification. Proc. 12th A CM Symp. on Principles of programming Languages, 1985, pp. 97-107. Google ScholarDigital Library
- LPZ85.Lichtenstein, O., Pnueli, A., Zuck L.: The glory of the past. Proc. Workshop on Logics of Programs, Brooklyn, Springer- Verlag, Lecture Notes in Computer Science 193, 1985, pp. 97-107. Google ScholarDigital Library
- MP83.Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. Proc. l Oth Symposium on Principles of Programming Languages, Austin, Texas, 1983, pp. 141-154. Google ScholarDigital Library
- MP87.Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by V-automata. Proc. i4 A CM Symp. on Principles of Programming Languages, Munich, :lan. 1987, pp. 1-12. Google ScholarDigital Library
- MW84.Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. A CM Trans. on Pro- 9ramming Languages, 1984, pp. 68-93. Google ScholarDigital Library
- Pn77.Pnueli, A.: The temporal logic of programs. Proc. 18th Syrup. on Foundations of Computer Science, 1977, pp. 46-5'7.Google ScholarDigital Library
- Pn85.Pnueli, A: In transition from global to modular reasoning about programs. Logics and Models of Concurrent Systems:, ed. K.R. Apt, Springer-Verlag, 1985, pp. 123-144. Google ScholarDigital Library
- Pn86.Pnueli, A: Applications of temporal logic to the specification and verification of reactive systems- a survey of current trends. Current Trends in Concurrency, eds. J.W. de Ba.kker et al., Springer-Verlag, Lecture Notes in Computer Science 224, 1986, pp. 510-584. Google ScholarDigital Library
- Pr51.Prior, A.: Past, Present, and Future, Oxford Press, 1951.Google Scholar
- Pr81.Pratt, V.I~.: Program Logic Without Binding is Decidable, Proc. 8th A CM Syrup. on Principles of Programming Languages, 1981. Google ScholarDigital Library
- Pr82.Pratt, V.R.: A decidable mu-calculus. Proc. 23rd IEEE Syrup. ou Foundations of Computer Science, 1982, pp. 421-427.Google Scholar
- RS59.Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Research and Development, 3(1959), PP-i 114- 125.Google Scholar
- RU71.Rescher, N, Urquhart, A.: Temporal Logic. Springer-Verlag, 1971.Google ScholarCross Ref
- SC85.Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(1985), pp. 733-749. Google ScholarDigital Library
- SE84.Streett, R.S., Emerson, E.A.: The propositional mu-calculus is elementary. Proc. 11~h Iu~'l Colloq. on Automata, Languages and Programming, 1984, Springer- Verlag, Lecture Notes in Computer Science 172, pp. 465-472. Google ScholarDigital Library
- Sh59.Shepherdson, 3.C.: The reduction of two-way automata to one-way automata. IBM J. Research and Development, 3(1959), pp. 199-201.Google ScholarDigital Library
- St82.Streett~ R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control, 54(1982), pp. 121-141.Google ScholarCross Ref
- SVW85.Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Bfichi automata with applications to temporal logic. Theoretical Computer Science,49(1987), pp. 217-237. Google ScholarDigital Library
- To81.Thomas, W.: A combinatorial approach to the theory of w-automata. Information and Control 48(1981), pp. 261-283.Google ScholarCross Ref
- Va85.Vardi, M.Y.: Automatic verification of probabilistie concurrent finite-state programs. Proc. 26th IEEE Symp. on 2"oundalions of Computer Science, Portland, 1985, pp. 327-338.Google Scholar
- VW86.Vardi, M.Y:, Wolp~,. P.: An automata-theoretic approach to automatic program verification. Proc. IEEE Syrup. on Logic in Computer Science, Cambridge, 1986, pp. 332-344.Google Scholar
- VW86.Vardi, M.Y., Wolper, P.: Applications of temporal logic- an automata-theoretic prespective. Stanford University, CSLI, 1985.Google Scholar
- Wo83.Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1983), pp. 72-99.Google ScholarCross Ref
- WVS83.Wolper, P.L., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. Proc. 24th IEEE Syrup. on Foundation of Computer Science, Tuscon, 1983, pp. 185-194.Google ScholarDigital Library
Index Terms
- A temporal fixpoint calculus
Recommendations
A Fixpoint Semantics and an SLD-Resolution Calculus for Modal Logic Programs
We propose a modal logic programming language called MProlog, which is as expressive as the general modal Horn fragment. We give a fixpoint semantics and an SLD-resolution calculus for MProlog in all of the basic serial modal logics KD, T, KDB, B, KD4, ...
Alternating automata and a temporal fixpoint calculus for visibly pushdown languages
CONCUR'07: Proceedings of the 18th international conference on Concurrency TheoryWe investigate various classes of alternating automata for visibly pushdown languages (VPL) over infinite words. First, we show that alternating visibly pushdown automata (AVPA) are exactly as expressive as their nondeterministic counterpart (NVPA) but ...
A fixpoint semantics and an SLD-resolution calculus for modal logic programs
We propose a modal logic programming language called MProlog, which is as expressive as the general modal Horn fragment. We give a fixpoint semantics and an SLD-resolution calculus for MProlog in all of the basic serial modal logics KD, T, KDB, B, KD4, ...
Comments