Zohar Manna
Amir Pnueli
- AS85.B. Alpern and F.B. Schneider, Defining liveness, In}o. Prac. I, ett. 21, 1985, pp. 181- 185.Google Scholar
- AS87.B. Alpern and F.B. Schneider, Recognizing safety and liveness, Dist. Comp. 2, 1987, pp. 117-126.Google ScholarDigital Library
- AS89.B. Alpern and F.B. Schneider, Verifying temporal properties without temporal logic, A CM Trans. Prog. Lang. Sys. 11, 1989, pp. 147-167. Google ScholarDigital Library
- Kam85.M. Kaminski, A classification of w-regular languages, Theor. Comp. Sci. 36, 1985, pp. 217-229. Google ScholarDigital Library
- Lam77.L. Lamport, Proving the correctness of multiproeess programs, IEEE Trans. Software Engin. 3, 1977, pp. 125-143.Google ScholarDigital Library
- Lam83.L. Lamport, What good is temporal logic, Proc. IFIP 9th World Congress (R.E.A. Mason, ed.), North-Holland, 1983, pp. 657- 668.Google Scholar
- Lan69.L.H. Landweber, Decision problems for w-automata, Math. Sys. Theory 4, 1969, pp. 376-384.Google ScholarCross Ref
- LPZ85.O. Lichtenstein, A. Pnueli, and L. Zuck, The glory of the past, Proc. Conf. Logics of Programs, Lee. Notes in Comp. Set. 193, Springer, 1985, pp. 196-218. Google ScholarDigital Library
- Man74.Z. Manna, Mathematical Theory of Computation, McGraw-Hill, 1974. Google ScholarDigital Library
- MP71.R. McNaughton and S. Papert, Counter Free Automata, MIT Press, 1971. Google ScholarDigital Library
- MP83.Z. Manna and A. Pnueli, How to cook a temporal proof system for your pet language, Proc. lOih A CM Syrup. Princ. of Prog. Lang., 1983, pp. 141-154. Google ScholarDigital Library
- MP84.Z. Manna and A. Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs, Sci. Comp. Prog. 32, 1984, pp. 257-289. Google ScholarDigital Library
- MP87.Z. Manna and A. Pnueli, Specification and verification of concurrent programs by k/- automata, Proc. 14~h A CM Symp. Princ. of Prog. Lang., 1987, pp. 1-12. Google ScholarDigital Library
- MP89a.Z. Manna and A. Pnueli, The anchored version of the temporal framework, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency (J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, eds.), Lee. Notes in Comp. Set. 354, Springer, 1989, pp. 201-284. Google ScholarDigital Library
- MP89b.Z. Manna and A. Pnueli, Completing the temporal picture, Proc. 16th Int. Colloq. Ant. Lang. Prog., Lec. Notes in Comp. Sci. 372, Springer, 1989, pp. 534-558. Google ScholarDigital Library
- OL82.S. Owicki and L. Lamport, Proving liveness properties of concurrent programs, A CM Trans. Prog. Lang. Sys. 4, 1982, pp. 455- 495. Google ScholarDigital Library
- Pnu77.A. Pnueli, The temporal logic of programs, Proc. 18th IEEE Symp. Found. of Comp. Sci., 1977, pp. 46-57.Google ScholarDigital Library
- Rab72.M.O. Rabin, Automata on lnfinite Objects and Chute's Problem, Volume 13 of Regional Conference Series in Mathematics, Amer. Math. Soe., 1972. Google ScholarDigital Library
- Sis85.A.P. Sistla, On caracterization of safety and liveness properties in temporal logic, Proc. 4~h A CM Syrup. Princ. of Dist. Comp., 1985, pp. 39-48. Google ScholarDigital Library
- Str82.R.S. Streett, Propositional dynamic logic of looping and converse is elementarily decidable, Inf. and Cont. 54, 1982, pp. 121-141.Google ScholarCross Ref
- Wag79.K. Wagner, On w-regular sets, Inf. and Cont. 43, 1979, pp. 123-177.Google ScholarCross Ref
- Wol83.P. Wolper, Temporal logic can be more expressive, Inf. and Cont. 56, 1983, pp. 72-99.Google ScholarCross Ref
- Zuc86.L. Zuek, Past Temporal Logic, Ph.D. thesis, Weizmann Institute, 1986.Google Scholar
- Zuc87.L. Zuck, Manuscript, 1987.Google Scholar
Index Terms
- A hierarchy of temporal properties (invited paper, 1989)
Recommendations
Dynamically inferring temporal properties
PASTE '04: Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineeringModel checking requires a specification of the target system's desirable properties, some of which are temporal. Formulating a temporal property of the system based on either its abstract model or implementation requires a deep understanding of its ...
Comments