Abstract
One of the surprising developments in the area of program verification is how ideas introduced originally by logicians in the 1950s ended up yielding by 2003 an industrial-standard property-specification language called PSL. This development was enabled by the equally unlikely transformation of the mathematical machinery of automata on infinite words, introduced in the early 1960s for second-order arithmetics, into effective algorithms for model-checking tools. This paper attempts to trace the tangled threads of this development.
A shorter version of this paper, under the title “From Church and Prior to PSL”, appeared in the Proc. 2006 Workshop on 25 Years of Model Checking, Lecture Notes in Computer Science, Springer.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aggarwal, S., Kurshan, R.P.: Automated implementation from formal specification. In: Proc. 4th Int’l Workshop on Protocol Specification, Testing and Verification, pp. 127–136. North-Holland, Amsterdam (1984)
Aggarwal, S., Kurshan, R.P., Sharma, D.: A language for the specification and analysis of protocols. In: Proc. 3rd Int’l Workshop on Protocol Specification, Testing, and Verification, pp. 35–50. North-Holland, Amsterdam (1983)
Apt, K., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Springer, Heidelberg (2006)
Armoni, R., et al.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 65–80. Springer, Heidelberg (2003)
Armoni, R., et al.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 211–296. Springer, Heidelberg (2002)
Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62–74. Springer, Heidelberg (1989)
Beer, I., et al.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)
Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 184–194. Springer, Heidelberg (1998)
Ben-Ari, M., Manna, Z., Pnueli, A.: The logic of nexttime. In: Proc. 8th ACM Symp. on Principles of Programming Languages, pp. 164–176 (1981)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2002)
Bradfield, J., Stirling, C.: PDL and modal μ-calculus. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, Elsevier, Amsterdam (2006)
Brayton, R.K., et al.: VIS: a system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)
Browne, M.C., et al.: Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computing C-35, 1035–1044 (1986)
Bryant, R.E.: Graph-based algorithms for Boolean-function manipulation. IEEE Transactions on Computing C-35(8), 677–691 (1986)
Büchi, J.R.: Weak second-order arithmetic and finite automata. Zeit. Math. Logik und Grundl. Math. 6, 66–92 (1960)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pp. 1–12. Stanford University Press (1962)
Büchi, J.R., Elgot, C.C., Wright, J.B.: The non-existence of certain algorithms for finite automata theory (abstract). Notices Amer. Math. Soc. 5, 98 (1958)
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295–311 (1969)
Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. In: Proc. 5th IEEE Symp. on Logic in Computer Science, pp. 428–439 (1990)
Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)
Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing 1974, Stockholm, Sweden, pp. 308–312. North-Holland, Amsterdam (1974)
Bustan, D., et al.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)
Nowick, S.M., van Berkel, C.H., Josephs, M.B.: Applications of asynchronous circuits. Proceedings of the IEEE 87(2), 223–233 (1999)
Church, A.: Applicaton of recursive arithmetics to the problem of circuit synthesis. In: Summaries of Talks Presented at The Summer Institute for Symbolic Logic, pp. 3–50. Communications Research Division, Institute for Defense Analysis (1957)
Church, A.: Logic, arithmetics, and automata. In: Proc. Int. Congress of Mathematicians, 1962, Institut Mittag-Leffler, pp. 23–35 (1963)
Cimatti, A., et al.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E.M.: The birth of model checking. In: Avron, A., et al. (eds.) Trakhtenbrot/Festschrift. LNCS, vol. 4800 (2007)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In: Proc. 10th ACM Symp. on Principles of Programming Languages, pp. 117–126 (1983)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languagues and Systems 8(2), 244–263 (1986)
Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model-checking algorithms. In: Proc. 16th ACM Symp. on Principles of Distributed Computing, pp. 294–303 (1987)
Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)
Clarke, E.M., Mishra, B.: Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science 38, 269–291 (1985)
Constable, R.L.: On the theory of programming logics. In: Proc. 9th ACM Symp. on Theory of Computing, pp. 269–285 (1977)
Copty, F., et al.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436–453. Springer, Heidelberg (2001)
Courcoubetis, C., et al.: Memory efficient algorithms for the verification of temporal properties. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 233–242. Springer, Heidelberg (1991)
Courcoubetis, C., et al.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1, 275–288 (1992)
Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using transition-based generalized büchi automata. In: Proc. 12th Int’l Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, pp. 76–83. IEEE Computer Society, Los Alamitos (2004)
Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)
Eisner, C., Fisman, D., Havlicek, J.: A topological characterization of weakness. In: Proc. 24th ACM Symp. on Principles of Distributed Computing, pp. 1–8 (2005)
Eisner, C., et al.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)
Eisner, C., et al.: The definition of a temporal clock operator. In: Baeten, J.C.M., et al. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 857–870. Springer, Heidelberg (2003)
Elgot, C.: Decision problems of finite-automata design and related arithmetics. Trans. Amer. Math. Soc. 98, 21–51 (1961)
Elgot, C.C., Wright, J.: Quantifier elimination in a problem of logical design. Michigan Math. J. 6, 65–69 (1959)
Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Proc. 7th Int. Colloq. on Automata, Languages, and Programming, pp. 169–181 (1980)
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: On branching versus linear time. In: Proc. 10th ACM Symp. on Principles of Programming Languages, pp. 127–140 (1983)
Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and Systems Science 30, 1–24 (1985)
Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: On branching versus linear time. Journal of the ACM 33(1), 151–178 (1986)
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus. In: Proc. 1st IEEE Symp. on Logic in Computer Science, pp. 267–278 (1986)
Engeler, E.: Algorithmic properties of structures. Math. Syst. Theory 1, 183–195 (1967)
Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)
Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs (extended abstract). In: Proc. 9th ACM Symp. on Theory of Computing, pp. 286–294 (1977)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and Systems Science 18, 194–211 (1979)
Fix, L.: Fifteen years of formal property verification at Intel. In: Proc. 2006 Workshop on 25 Years of Model Checking. LNCS, Springer, Heidelberg (2007)
Fix, L., Kamhi, G.: Adaptive variable reordering for symbolic model checking. In: Proc. ACM/IEEE Int’l Conf. on Computer Aided Design, pp. 359–365 (1998)
Gabbay, D., et al.: On the temporal analysis of fairness. In: Proc. 7th ACM Symp. on Principles of Programming Languages, pp. 163–173 (1980)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Gerth, R., et al.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3–18. Chapman and Hall, Boca Raton (1995)
Goldblatt, R.: Logic of time and computation. Technical report, CSLI Lecture Notes, no.7, Stanford University (1987)
Hafer, T., Thomas, W.: Computation tree logic CTL ⋆ and path quantifiers in the monadic theory of the binary tree. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 269–279. Springer, Heidelberg (1987)
Halpern, J., Reif, J.H.: The propositional dynamic logic of deterministic, well-structured programs (extended abstract). In: Proc. 22nd IEEE Symp. on Foundations of Computer Science, pp. 322–334 (1981)
Halpern, J.Y., Reif, J.H.: The propositional dynamic logic of deterministic, well-structured programs. Theor. Comput. Sci. 27, 127–165 (1983)
Hardin, R.H., Har’el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 423–427. Springer, Heidelberg (1996)
Harel, D., Kozen, D., Parikh, R.: Process logic: Expressiveness, decidability, completeness. J. Comput. Syst. Sci. 25(2), 144–170 (1982)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Harel, D., Peleg, D.: More on looping vs. repeating in dynamic logic. Inf. Process. Lett. 20(2), 87–90 (1985)
Harel, D., Peleg, D.: Process logic with regular formulas. Theoreti. Comp. Sci. 38(2–3), 307–322 (1985)
Harel, D., Sherman, R.: Looping vs. repeating in dynamic logic. Inf. Comput. 55(1–3), 175–192 (1982)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Kamp, J.A.W.: Tense Logic and the Theory of Order. PhD thesis, UCLA (1968)
Keller, R.M.: Formal verification of parallel programs. Communications of the ACM 19, 371–384 (1976)
Kozen, D.: Results on the propositional μ-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Kripke, S.: A completeness theorem in modal logic. Journal of Symbolic Logic 24, 1–14 (1959)
Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(2), 408–429 (2001)
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp. 531–540 (2005)
Kurshan, R.P.: Analysis of discrete event coordination. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 414–453. Springer, Heidelberg (1990)
Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)
Kurshan, R.P.: Verification technology transfer. In: Proc. 2006 Workshop on 25 Years of Model Checking. LNCS, Springer, Heidelberg (2007)
Lamport, L.: “Sometimes” is sometimes “not never” - on the temporal logic of programs. In: Proc. 7th ACM Symp. on Principles of Programming Languages, pp. 174–185 (1980)
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 97–107 (1985)
Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)
Markey, N.: Temporal logic with past is exponentially more succinct. EATCS Bulletin 79, 122–128 (2003)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
McNaughton, R., Papert, S.: Counter-Free Automata. MIT Press, Cambridge (1971)
Meyer, A.R.: Weak monadic second order theory of successor is not elementary recursive. In: Proc. Logic Colloquium. Lecture Notes in Mathematics, vol. 453, pp. 132–154. Springer, Heidelberg (1975)
Meyer, A.R.: Ten thousand and one logics of programming. Technical report, MIT, MIT-LCS-TM-150 (1980)
Morley, M.J.: Semantics of temporal e. In: Melham, T.F., Moller, F.G. (eds.) Banff 1999 Higher Order Workshop (Formal Methods in Computation), University of Glasgow, Department of Computing Science Technical Report (1999)
Urquhart, A., Rescher, N.: Temporal Logic. Springer, Heidelberg (1971)
Øhrstrøm, P., Hasle, P.F.V.: Temporal Logic: from Ancient Times to Artificial Intelligence. Studies in Linguistics and Philosophy, vol. 57. Kluwer Academic Publishers, Dordrecht (1995)
Park, D.: Finiteness is μ-ineffable. Theoretical Computer Science 3, 173–181 (1976)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundations of Computer Science, pp. 46–57 (1977)
Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15–32. Springer, Heidelberg (1985)
Pnueli, A., Zuck, L.: In and out of temporal logic. In: Proc. 8th IEEE Symp. on Logic in Computer Science, pp. 124–135 (1993)
Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Proc. 17th IEEE Symp. on Foundations of Computer Science, pp. 109–121 (1976)
Pratt, V.R.: A practical decision method for propositional dynamic logic: Preliminary report. In: Proc. 10th Annual ACM Symposium on Theory of Computing, pp. 326–337 (1978)
Pratt, V.R.: A near-optimal method for reasoning about action. Journal of Computer and Systems Science 20(2), 231–254 (1980)
Pratt, V.R.: A decidable μ-calculus: preliminary report. In: Proc. 22nd IEEE Symp. on Foundations of Computer Science, pp. 421–427 (1981)
Prior, A.: Time and Modality. Oxford University Press, Oxford (1957)
Prior, A.: Past, Present, and Future. Clarendon Press (1967)
Prior, A.N.: Modality de dicto and modality de re. Theoria 18, 174–180 (1952)
Prior, A.N.: Modality and quantification in s5. J. Symbolic Logic 21, 60–62 (1956)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Rabin, M.O.: Automata on infinite objects and Church’s problem. Amer. Mathematical Society (1972)
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)
Sabnani, K., Wolper, P., Lapone, A.: An algorithmic technique for protocol verification. In: Proc. Globecom (1985)
Sakoda, W., Sipser, M.: Non-determinism and the size of two-way automata. In: Proc. 10th ACM Symp. on Theory of Computing, pp. 275–286 (1978)
Salwicki, A.: Algorithmic logic: a tool for investigations of programs. In: Butts, R.E., Hintikka, J. (eds.) Logic Foundations of Mathematics and Computability Theory, pp. 281–295. Reidel (1977)
Sistla, A.P.: Theoretical issues in the design of distributed and concurrent systems. PhD thesis, Harvard University (1983)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. In: Proc. 14th Annual ACM Symposium on Theory of Computing, pp. 159–168 (1982)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal of the ACM 32, 733–749 (1985)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 465–474. Springer, Heidelberg (1985)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)
Stockmeyer, L.J.: The complexity of decision procedures in Automata Theory and Logic. PhD thesis, MIT, Project MAC Technical Report TR-133 (1974)
Street, R.S.: Propositional dynamic logic of looping and converse. In: Proc. 13th ACM Symp. on Theory of Computing, pp. 375–383 (1981)
Streett, R.S.: A propositional dynamic logic for reasoning about program divergence. PhD thesis, M.Sc. Thesis, MIT (1980)
Streett, R.S.: Propositional dynamic logic of looping and converse. Information and Control 54, 121–141 (1982)
A comparison of reset control methods: Application note 11. Summit Microelectronics, Inc. (1999), http://www.summitmicro.com/tech_support/notes/note11.htm
Thomas, W.: Star-free regular sets of ω-sequences. Information and Control 42(2), 148–156 (1979)
Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Trakhtenbrot, B.: The synthesis of logical nets whose operators are described in terms of one-place predicate calculus. Doklady Akad. Nauk SSSR 118(4), 646–649 (1958)
Trakhtenbrot, B.: Certain constructions in the logic of one-place predicates. Doklady Akad. Nauk SSSR 138, 320–321 (1961)
Trakhtenbrot, B.A.: Finite automata and monadic second order logic. Siberian Math. J. 3, 101–131 (1962) Russian; English translation in: AMS Transl. 59, 23–55 (1966)
Trakhtenbrot, B.A., Barzdin, Y.M.: Finite Automata. North-Holland, Amsterdam (1973)
Vardi, M.Y.: The büchi complementation saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 12–22. Springer, Heidelberg (2007)
Vardi, M.Y.: The complexity of relational query languages. In: Proc. 14th ACM Symp. on Theory of Computing, pp. 137–146 (1982)
Vardi, M.Y.: A temporal fixpoint calculus. In: Proc. 15th ACM Symp. on Principles of Programming Languages, pp. 250–259 (1988)
Vardi, M.Y.: Unified verification theory. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 202–212. Springer, Heidelberg (1989)
Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575–597. Springer, Heidelberg (1994)
Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)
Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 137–150. Springer, Heidelberg (2007)
Vardi, M.Y., Wolper, P.: Yet another process logic. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 501–512. Springer, Heidelberg (1984)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st IEEE Symp. on Logic in Computer Science, pp. 332–344 (1986)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005)
Wolper, P.: Temporal logic can be more expressive. In: Proc. 22nd IEEE Symp. on Foundations of Computer Science, pp. 340–348 (1981)
Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1–2), 72–99 (1983)
Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th IEEE Symp. on Foundations of Computer Science, pp. 185–194 (1983)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Vardi, M.Y. (2008). From Monadic Logic to PSL. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds) Pillars of Computer Science. Lecture Notes in Computer Science, vol 4800. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78127-1_36
Download citation
DOI: https://doi.org/10.1007/978-3-540-78127-1_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78126-4
Online ISBN: 978-3-540-78127-1
eBook Packages: Computer ScienceComputer Science (R0)