Dynamic Logic: A Personal Perspective | SpringerLink
Skip to main content
Springer Nature Link
Log in

Dynamic Logic: A Personal Perspective

  • Conference paper
  • First Online:
Dynamic Logic. New Trends and Applications (DALI 2017)

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

Included in the following conference series:

Abstract

We review a few of the developments of dynamic logic from the author’s perspective. As implied by the title the review is not intended as a survey of the field as a whole but rather as how the author’s outlook on imperative programs and their logics evolved during the four decades up to the start of this millennium.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    By way of partial excuse, the Berlin Wall still existed and duplication of effort between East and West was not uncommon, for example Marshall Stone’s discovery [56] that Boolean algebras were rings without being aware that Zhegalkin had pointed it out nine years earlier [58].

  2. 2.

    An R-module is a vector space just when the ring R is a field.

  3. 3.

    I had not used the term “multimodal” explicitly in any of my earlier papers. Rennie’s n-multiply modal calculus based on constants \(M_1,M_2,\ldots ,M_n\) [52] is a much earlier related concept.

References

  1. Barr, M.: \(*\)-Autonomous Categories. Lecture Notes in Mathematics, vol. 752. Springer, Berlin (1979)

    Google Scholar 

  2. Beth, E.W.: The Foundations of Mathematics. North Holland, Amsterdam (1959)

    MATH  Google Scholar 

  3. Brock, J.D., Ackerman, W.B.: An anomaly in the specifications of nondeterministic packet systems. Technical report Computation Structures Group Note CSG-33, MIT Lab. for Computer Science, November 1977

    Google Scholar 

  4. Cannon, J.J.: A general purpose group theory program. In: Proceedings of the Second International Conference Theory of Groups, Canberra, pp. 204–217 (1973)

    Google Scholar 

  5. Cannon, J.J.: A draft description of the group theory language cayley. In: Proceedings of the Third ACM Symposium on Symbolic and Algebraic Computation, SYMSAC 1976, pp. 66–84. ACM, New York (1976)

    Google Scholar 

  6. de Bakker, J.W., de Roever, W.P.: A calculus for recursive program schemes. In: Nivat, M. (ed.) Automata, Languages and Programming, pp. 167–196. North Holland (1972)

    Google Scholar 

  7. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  8. Ehrenfeucht, A., Zeiger, P.: Complexity measures for regular expressions. J. Comput. Syst. Sci. 12(2), 134–146 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  9. Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. In: Proceedings of the 9th ACM Symposium on Theory of Computing, pp. 194–211, Boulder, May 1977. Journal version: Propositional dynamic logic of regular programs, JCSS 18:2 (1979)

    Google Scholar 

  10. Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, pp. 19–32 (1967)

    Google Scholar 

  11. Gentzen, G.: Investigations into logical deductions. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1934)

    Google Scholar 

  12. Gold, E.M.: Language identification in the limit. Inf. Control 10(5), 447–474 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  13. Grabowski, J.: On partial languages. Fundam. Inform. IV(2), 427–498 (1981)

    MathSciNet  MATH  Google Scholar 

  14. Harel, D., Meyer, A.R., Pratt, V.R.: Computability and completeness in logics of programs. In: Proceedings of the 9th Annual ACM Symposium on Theory of Computation, pp. 261–268 (1977)

    Google Scholar 

  15. Henkin, L.: The logic of equality. Amer. Math. Mon. 84(8), 597–612 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hintikka, K.J.J.: Form and content ni quantification theory. Acta Philos. Fenni. 8, 7–55 (1955)

    Google Scholar 

  17. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969)

    Article  MATH  Google Scholar 

  18. Hoare, C.A.R., Lauer, P.E.: Consistent and complementary formal theories of the semantics of programming languages. Acta Inform. 3, 135–153 (1974)

    MathSciNet  MATH  Google Scholar 

  19. Jónsson, B., Tarski, A.: Boolean algebras with operators. Part I. Amer. J. Math. 73, 891–939 (1951)

    Article  MathSciNet  MATH  Google Scholar 

  20. Knuth, D.E., Morris, J., Pratt, V.R.: Fast pattern matching in strings. SIAM J. Comput. 6(2), 323–350 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  21. Kozen, D.: A representation theorem for models of \(*\)-free PDL. Technical report RC7864, IBM, September 1979

    Google Scholar 

  22. Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 23 (1983)

    Google Scholar 

  23. Kripke, S.: A completeness theorem in modal logic. J. Symb. Logic 24(1), 1–14 (1959)

    Article  MathSciNet  MATH  Google Scholar 

  24. Kripke, S.: Semantical considerations on modal logic. Acta Philos. Fenn. 16, 83–94 (1963)

    MathSciNet  MATH  Google Scholar 

  25. Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6(3), 467–480 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  26. Litvintchouk, S.D., Pratt, V.R.: A proof checker for dynamic logic. In: 5th International Joint Conference on A.I., pp. 552–558, August 1977

    Google Scholar 

  27. Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Technical report DAIMI Report PB-78, Aarhus University, Aarhus (1977)

    Google Scholar 

  28. Nelson, G., Oppen, D.C.: Fast decision algorithms based on union and find. In: 18th IEEE Symposium on Foundations of Computer Science, October 1977

    Google Scholar 

  29. Németi, I.: Every free algebra in the variety generated by the representable dynamic algebras is separable and representable. Theoret. Comput. Sci. 17, 343–347 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  30. Parikh, R.: A completeness result for a propositional dynamic logic. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol. 64, pp. 403–415. Springer, Heidelberg (1978)

    Google Scholar 

  31. Petri, C.A.: Fundamentals of a theory of asynchronous information flow. In: Proceedings of the IFIP Congress 62, Munich, pp. 386–390 (1962). North-Holland, Amsterdam

    Google Scholar 

  32. Pnueli, A.: The temporal logic of programs. In: 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57, October 1977

    Google Scholar 

  33. Pratt, V.R.: Translation of lewis carroll’s syllogisms into logic. Masters Thesis, August 1969

    Google Scholar 

  34. Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Proceedings of the 17th Annual IEEE Symposium on Foundations of Computer Science, pp. 109–121, October 1976

    Google Scholar 

  35. Pratt, V.R.: A practical decision method for propositional dynamic logic. In: Proceedings of the 10th Annual ACM Symposium on Theory of Computing, San Diego, pp. 326–337, May 1978

    Google Scholar 

  36. Pratt, V.R.: Axioms or algorithms. In: Proceedings of the 6th Symposium on Mathematical Foundations of Computer Science, Olomouc, Czech. (1979)

    Google Scholar 

  37. Pratt, V.R.: Dynamic algebras: Examples, constructions, applications. Technical report MIT/LCS/TM-138, M.I.T. Laboratory for Computer Science, July 1979

    Google Scholar 

  38. Pratt, V.R.: Dynamic logic. In: Proceedings of the 6th Conference on Logic, Methodology, and Philosophy of Science, Hanover, West Germany, pp. 251–261 (1979)

    Google Scholar 

  39. Pratt, V.R.: Process logic. In: Proceedings of the 6th Annual ACM Symposium on Principles of Programming Languages, San Antonio, pp. 93–100, January 1979

    Google Scholar 

  40. Pratt, V.R.: Dynamic algebras and the nature of induction. In: 12th ACM Symposium on Theory of Computation, Los Angeles, April 1980

    Google Scholar 

  41. Pratt, V.R.: A near optimal method for reasoning about action. J. Comput. Syst. Sci. 2, 231–254 (1980). Also MIT/LCS/TM-113, M.I.T., Sept. 1978

    Article  MathSciNet  MATH  Google Scholar 

  42. Pratt, V.R.: A decidable mu-calculus. In: Proceedings of the 22nd IEEE Conference on Foundations of Computer Science, pp. 421–427, October 1981

    Google Scholar 

  43. Pratt, V.R.: Using graphs to understand PDL. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 387–396. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025792

    Chapter  Google Scholar 

  44. Pratt, V.R.: Position statement. Circulated at the Panel on Mathematics of Parallel Processes, chair A.R.G. Milner, IFIP-83, September 1983

    Google Scholar 

  45. Pratt, V.: The pomset model of parallel processes: unifying the temporal and the spatial. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 180–196. Springer, Heidelberg (1985). https://doi.org/10.1007/3-540-15670-4_9

    Chapter  Google Scholar 

  46. Pratt, V.: Two-way channel with disconnect. In: Denvir, B.T., Harwood, W.T., Jackson, M.I., Wray, M.J. (eds.) The Analysis of Concurrent Systems. LNCS, vol. 207, pp. 110–114. Springer, Heidelberg (1985). https://doi.org/10.1007/3-540-16047-7_39

    Chapter  Google Scholar 

  47. Pratt, V.R.: Modeling concurrency with geometry. In: Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages, pp. 311–322, January 1991

    Google Scholar 

  48. Pratt, V.R.: The duality of time and information. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 237–253. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0084795

    Chapter  Google Scholar 

  49. Pratt, V.R.: Dynamic algebras: examples, constructions, applications. Stud. Logica 50(3/4), 571–605 (1992)

    MathSciNet  MATH  Google Scholar 

  50. Pratt, V.R.: Transition and cancellation in concurrency and branching time. Math. Struct. Comp. Sci. 13(4), 485–529 (2003). Special issue on the difference between sequentiality and concurrency

    Article  MathSciNet  MATH  Google Scholar 

  51. Rasiowa, H., Sikorski, R.: The Mathematics of Metamathematics. Polska Akademia Nauk. Monografie matematyczne, vol. 41. Drukarnia Uniwersytetu, Warsaw (1963)

    Google Scholar 

  52. Rennie, M.K.: Models for multiply modal systems. Zeitschr. j. math. Logik und Grundlagen d. Math. 16, 175–186 (1970)

    Google Scholar 

  53. Salwicki, A.: Formalized algorithmic languages. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. 18(5), 227–232 (1970)

    Google Scholar 

  54. Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 177–192 (1970)

    Article  MathSciNet  MATH  Google Scholar 

  55. Smullyan, R.: First Order Logic. Springer, Berlin (1968)

    Book  MATH  Google Scholar 

  56. Stone, M.: The theory of representations for Boolean algebras. Trans. Amer. Math. Soc. 40, 37–111 (1936)

    MathSciNet  MATH  Google Scholar 

  57. Valiev, M.K.: On axiomatization of deterministic propositional dynamic logic. In: Proceedings of the 6th Symposium on Mathematical Foundations of Computer Science, Olomouc, Czech. (1979)

    Google Scholar 

  58. Zhegalkin, I.I.: On the technique of calculating propositions in symbolic logic. Matematicheskii Sbornik 43, 9–28 (1927)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Stanford University, Stanford, USA

    Vaughan Pratt

Authors
  1. Vaughan Pratt
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vaughan Pratt .

Editor information

Editors and Affiliations

  1. INESC TEC, University of Minho, Braga, Portugal

    Alexandre Madeira

  2. UFRJ, Rio de Janeiro, Brazil

    Mário Benevides

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Pratt, V. (2018). Dynamic Logic: A Personal Perspective. In: Madeira, A., Benevides, M. (eds) Dynamic Logic. New Trends and Applications. DALI 2017. Lecture Notes in Computer Science(), vol 10669. Springer, Cham. https://doi.org/10.1007/978-3-319-73579-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-73579-5_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-73578-8

  • Online ISBN: 978-3-319-73579-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation