Skip to main content
SpringerLink
Log in

From Monadic Logic to PSL

  • Chapter
Pillars of Computer Science

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4800))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Google Scholar 

  2. 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)

    Google Scholar 

  3. Apt, K., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Springer, Heidelberg (2006)

    Google Scholar 

  4. 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)

    Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. 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)

    Google Scholar 

  10. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2002)

    Google Scholar 

  11. Bradfield, J., Stirling, C.: PDL and modal μ-calculus. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, Elsevier, Amsterdam (2006)

    Google Scholar 

  12. 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)

    Google Scholar 

  13. Browne, M.C., et al.: Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computing C-35, 1035–1044 (1986)

    Article  Google Scholar 

  14. Bryant, R.E.: Graph-based algorithms for Boolean-function manipulation. IEEE Transactions on Computing C-35(8), 677–691 (1986)

    Article  Google Scholar 

  15. Büchi, J.R.: Weak second-order arithmetic and finite automata. Zeit. Math. Logik und Grundl. Math. 6, 66–92 (1960)

    MATH  Google Scholar 

  16. 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)

    Google Scholar 

  17. 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)

    Google Scholar 

  18. Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295–311 (1969)

    Article  Google Scholar 

  19. 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)

    Google Scholar 

  20. Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  21. 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)

    Google Scholar 

  22. Bustan, D., et al.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  23. Nowick, S.M., van Berkel, C.H., Josephs, M.B.: Applications of asynchronous circuits. Proceedings of the IEEE 87(2), 223–233 (1999)

    Article  Google Scholar 

  24. 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)

    Google Scholar 

  25. Church, A.: Logic, arithmetics, and automata. In: Proc. Int. Congress of Mathematicians, 1962, Institut Mittag-Leffler, pp. 23–35 (1963)

    Google Scholar 

  26. 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)

    Chapter  Google Scholar 

  27. Clarke, E.M.: The birth of model checking. In: Avron, A., et al. (eds.) Trakhtenbrot/Festschrift. LNCS, vol. 4800 (2007)

    Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. 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)

    Google Scholar 

  30. 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)

    Article  MATH  Google Scholar 

  31. 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)

    Google Scholar 

  32. 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)

    Google Scholar 

  33. Clarke, E.M., Mishra, B.: Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science 38, 269–291 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  34. Constable, R.L.: On the theory of programming logics. In: Proc. 9th ACM Symp. on Theory of Computing, pp. 269–285 (1977)

    Google Scholar 

  35. 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)

    Google Scholar 

  36. 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)

    Chapter  Google Scholar 

  37. Courcoubetis, C., et al.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1, 275–288 (1992)

    Article  Google Scholar 

  38. 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)

    Google Scholar 

  39. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)

    Google Scholar 

  40. 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)

    Google Scholar 

  41. 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)

    Google Scholar 

  42. 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)

    Chapter  Google Scholar 

  43. Elgot, C.: Decision problems of finite-automata design and related arithmetics. Trans. Amer. Math. Soc. 98, 21–51 (1961)

    Article  MathSciNet  Google Scholar 

  44. Elgot, C.C., Wright, J.: Quantifier elimination in a problem of logical design. Michigan Math. J. 6, 65–69 (1959)

    Article  MATH  MathSciNet  Google Scholar 

  45. 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)

    Google Scholar 

  46. 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)

    Google Scholar 

  47. 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)

    Article  MATH  MathSciNet  Google Scholar 

  48. 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)

    Article  MATH  MathSciNet  Google Scholar 

  49. 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)

    Google Scholar 

  50. Engeler, E.: Algorithmic properties of structures. Math. Syst. Theory 1, 183–195 (1967)

    Article  MATH  MathSciNet  Google Scholar 

  51. Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  52. 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)

    Google Scholar 

  53. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and Systems Science 18, 194–211 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  54. Fix, L.: Fifteen years of formal property verification at Intel. In: Proc. 2006 Workshop on 25 Years of Model Checking. LNCS, Springer, Heidelberg (2007)

    Google Scholar 

  55. 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)

    Google Scholar 

  56. Gabbay, D., et al.: On the temporal analysis of fairness. In: Proc. 7th ACM Symp. on Principles of Programming Languages, pp. 163–173 (1980)

    Google Scholar 

  57. 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)

    Google Scholar 

  58. 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)

    Google Scholar 

  59. Goldblatt, R.: Logic of time and computation. Technical report, CSLI Lecture Notes, no.7, Stanford University (1987)

    Google Scholar 

  60. 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)

    Google Scholar 

  61. 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)

    Google Scholar 

  62. Halpern, J.Y., Reif, J.H.: The propositional dynamic logic of deterministic, well-structured programs. Theor. Comput. Sci. 27, 127–165 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  63. 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)

    Google Scholar 

  64. Harel, D., Kozen, D., Parikh, R.: Process logic: Expressiveness, decidability, completeness. J. Comput. Syst. Sci. 25(2), 144–170 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  65. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  66. Harel, D., Peleg, D.: More on looping vs. repeating in dynamic logic. Inf. Process. Lett. 20(2), 87–90 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  67. Harel, D., Peleg, D.: Process logic with regular formulas. Theoreti. Comp. Sci. 38(2–3), 307–322 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  68. Harel, D., Sherman, R.: Looping vs. repeating in dynamic logic. Inf. Comput. 55(1–3), 175–192 (1982)

    MATH  MathSciNet  Google Scholar 

  69. Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)

    Article  MathSciNet  Google Scholar 

  70. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)

    MATH  Google Scholar 

  71. Kamp, J.A.W.: Tense Logic and the Theory of Order. PhD thesis, UCLA (1968)

    Google Scholar 

  72. Keller, R.M.: Formal verification of parallel programs. Communications of the ACM 19, 371–384 (1976)

    Article  MATH  Google Scholar 

  73. 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)

    Chapter  Google Scholar 

  74. Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  75. Kripke, S.: A completeness theorem in modal logic. Journal of Symbolic Logic 24, 1–14 (1959)

    Article  MATH  MathSciNet  Google Scholar 

  76. 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)

    Chapter  Google Scholar 

  77. Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(2), 408–429 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  78. Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp. 531–540 (2005)

    Google Scholar 

  79. 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)

    Google Scholar 

  80. Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)

    Google Scholar 

  81. Kurshan, R.P.: Verification technology transfer. In: Proc. 2006 Workshop on 25 Years of Model Checking. LNCS, Springer, Heidelberg (2007)

    Google Scholar 

  82. 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)

    Google Scholar 

  83. 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)

    Google Scholar 

  84. 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)

    Google Scholar 

  85. Markey, N.: Temporal logic with past is exponentially more succinct. EATCS Bulletin 79, 122–128 (2003)

    MathSciNet  MATH  Google Scholar 

  86. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    MATH  Google Scholar 

  87. McNaughton, R., Papert, S.: Counter-Free Automata. MIT Press, Cambridge (1971)

    MATH  Google Scholar 

  88. 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)

    Chapter  Google Scholar 

  89. Meyer, A.R.: Ten thousand and one logics of programming. Technical report, MIT, MIT-LCS-TM-150 (1980)

    Google Scholar 

  90. 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)

    Google Scholar 

  91. Urquhart, A., Rescher, N.: Temporal Logic. Springer, Heidelberg (1971)

    MATH  Google Scholar 

  92. Ø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)

    Google Scholar 

  93. Park, D.: Finiteness is μ-ineffable. Theoretical Computer Science 3, 173–181 (1976)

    Article  MathSciNet  Google Scholar 

  94. Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundations of Computer Science, pp. 46–57 (1977)

    Google Scholar 

  95. 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)

    Chapter  Google Scholar 

  96. Pnueli, A., Zuck, L.: In and out of temporal logic. In: Proc. 8th IEEE Symp. on Logic in Computer Science, pp. 124–135 (1993)

    Google Scholar 

  97. Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Proc. 17th IEEE Symp. on Foundations of Computer Science, pp. 109–121 (1976)

    Google Scholar 

  98. 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)

    Google Scholar 

  99. Pratt, V.R.: A near-optimal method for reasoning about action. Journal of Computer and Systems Science 20(2), 231–254 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  100. Pratt, V.R.: A decidable μ-calculus: preliminary report. In: Proc. 22nd IEEE Symp. on Foundations of Computer Science, pp. 421–427 (1981)

    Google Scholar 

  101. Prior, A.: Time and Modality. Oxford University Press, Oxford (1957)

    MATH  Google Scholar 

  102. Prior, A.: Past, Present, and Future. Clarendon Press (1967)

    Google Scholar 

  103. Prior, A.N.: Modality de dicto and modality de re. Theoria 18, 174–180 (1952)

    Article  Google Scholar 

  104. Prior, A.N.: Modality and quantification in s5. J. Symbolic Logic 21, 60–62 (1956)

    Article  MATH  MathSciNet  Google Scholar 

  105. 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)

    Google Scholar 

  106. Rabin, M.O.: Automata on infinite objects and Church’s problem. Amer. Mathematical Society (1972)

    Google Scholar 

  107. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)

    Article  MathSciNet  Google Scholar 

  108. Sabnani, K., Wolper, P., Lapone, A.: An algorithmic technique for protocol verification. In: Proc. Globecom (1985)

    Google Scholar 

  109. 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)

    Google Scholar 

  110. 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)

    Google Scholar 

  111. Sistla, A.P.: Theoretical issues in the design of distributed and concurrent systems. PhD thesis, Harvard University (1983)

    Google Scholar 

  112. 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)

    Google Scholar 

  113. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal of the ACM 32, 733–749 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  114. 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)

    Chapter  Google Scholar 

  115. 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)

    Article  MATH  MathSciNet  Google Scholar 

  116. Stockmeyer, L.J.: The complexity of decision procedures in Automata Theory and Logic. PhD thesis, MIT, Project MAC Technical Report TR-133 (1974)

    Google Scholar 

  117. Street, R.S.: Propositional dynamic logic of looping and converse. In: Proc. 13th ACM Symp. on Theory of Computing, pp. 375–383 (1981)

    Google Scholar 

  118. Streett, R.S.: A propositional dynamic logic for reasoning about program divergence. PhD thesis, M.Sc. Thesis, MIT (1980)

    Google Scholar 

  119. Streett, R.S.: Propositional dynamic logic of looping and converse. Information and Control 54, 121–141 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  120. A comparison of reset control methods: Application note 11. Summit Microelectronics, Inc. (1999), http://www.summitmicro.com/tech_support/notes/note11.htm

  121. Thomas, W.: Star-free regular sets of ω-sequences. Information and Control 42(2), 148–156 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  122. 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)

    Google Scholar 

  123. 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)

    MATH  Google Scholar 

  124. Trakhtenbrot, B.: Certain constructions in the logic of one-place predicates. Doklady Akad. Nauk SSSR 138, 320–321 (1961)

    Google Scholar 

  125. 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)

    Google Scholar 

  126. Trakhtenbrot, B.A., Barzdin, Y.M.: Finite Automata. North-Holland, Amsterdam (1973)

    MATH  Google Scholar 

  127. 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)

    Chapter  Google Scholar 

  128. Vardi, M.Y.: The complexity of relational query languages. In: Proc. 14th ACM Symp. on Theory of Computing, pp. 137–146 (1982)

    Google Scholar 

  129. Vardi, M.Y.: A temporal fixpoint calculus. In: Proc. 15th ACM Symp. on Principles of Programming Languages, pp. 250–259 (1988)

    Google Scholar 

  130. 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)

    Google Scholar 

  131. 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)

    Google Scholar 

  132. 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)

    Chapter  Google Scholar 

  133. 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)

    Chapter  Google Scholar 

  134. 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)

    Google Scholar 

  135. 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)

    Google Scholar 

  136. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  137. Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005)

    Google Scholar 

  138. Wolper, P.: Temporal logic can be more expressive. In: Proc. 22nd IEEE Symp. on Foundations of Computer Science, pp. 340–348 (1981)

    Google Scholar 

  139. Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1–2), 72–99 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  140. 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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Rice University, Houston, TX 77251-1892, U.S.A.

    Moshe Y. Vardi

Authors
  1. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Arnon Avron Nachum Dershowitz Alexander Rabinovich

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation