Skip to main content
SpringerLink
Log in

Model theory of propositional logics of programs, some open problems

  • Conference paper
  • First Online:
Computation Theory (SCT 1984)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 208))

Included in the following conference series:

  • 137 Accesses

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. Abrahamson K.R. Decidability and expressiveness of logics of processes Tech. Rep. 80-08-01, Univ. of Washington, 1980.

    Google Scholar 

  2. Barwise J. Axioms for abstract model theory Ann. Math. Logic 7, 1974, pp. 221–265.

    Google Scholar 

  3. Berman F. Models for verifiers Rep. of the Dept. of Comp. Sci., Purdue Univ. CSD-TR 343, 1980

    Google Scholar 

  4. Berman F., Peterson G.L. Expressiveness hierarchy for PDL with rich tests manuscript, Dept. of Comp. Sci., Univ. of Washington, 1978.

    Google Scholar 

  5. Ben-Ari M., Halpern J.Y., Pneuli A. Deterministic Propositional Dynamic Logic: finite models, complexity, completeness rep. of MIT, TM-190, 1981 (see also ICALP '81)

    Google Scholar 

  6. Chandra A., Halpern J., Meyer A., Parikh R. Equations between regular terms and an application to Process Logic STOC '81, pp. 384–390.

    Google Scholar 

  7. Chlebus B.S. On the computational complexity of satisfiability in propositional logics of programs Theoretical Comp. Sci. 21(2), 1982, pp. 179–212.

    Google Scholar 

  8. Clarke E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic LNCS 131, 1981, pp. 52–71.

    Google Scholar 

  9. Clarke E.M., Emerson E.A., Sistla A.P. Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach POPL 83, pp. 117–126.

    Google Scholar 

  10. Danecki R. Propositional Dynamic Logic with strong loop predicate LNCS 176, 1984, pp. 573–581.

    Google Scholar 

  11. — personal communication (see also this volume)

    Google Scholar 

  12. Emerson E.A. Alternative semantics for temporal logics rep. of the Dept. of Comp. Sci., Univ. of Texas, 1981 (also in: TCS 26, 1983, pp. 121–130).

    Google Scholar 

  13. Emerson E.A., Clarke E.M. Using branching time temporal logic to synthesize synchronization skeletons Sci. of Comp. Programming 2, pp. 241–266, NHolland, 1982.

    Google Scholar 

  14. Emerson E.A., Halpern J.Y. Decision procedures and expressiveness in the Temporal Logic of Branching Time STOC 82, pp. 169 180.

    Google Scholar 

  15. — — "Sometimes" and "not never" revisited: on branching versus linear time POPL 83, pp. 127–140.

    Google Scholar 

  16. — Lei Ch. L. Temporal model checking under generalized fairness constraints rep. Dept. Comp. Sci., Univ. of Texas at Austin, 1984. (also in: 18th Hawaii Int. Conf. Systems Sci., 1985)

    Google Scholar 

  17. Emerson E. A., Lei Ch. L. Modalities for model checking: branching time strikes back POPL 85, pp. 84–96.

    Google Scholar 

  18. Emerson E.A., Street R.S. The propositional μ-calculus is elementary ICALP 84

    Google Scholar 

  19. — Sistla A.P. Deciding Branching Time Logic STOC 84, pp. 14–24.

    Google Scholar 

  20. — — Deciding Full Branching Time Logic Inf. and Control 61(3), 1984, pp. 175–201.

    Google Scholar 

  21. Fischer M.J., Ladner R.E. Propositional Modal Logic of Programs STOC 77, pp. 286–294.

    Google Scholar 

  22. — — Propositional Dynamic Logic of regular programs JCSS 18(2), 1979, pp. 194–211.

    Google Scholar 

  23. Habasiński Z. Process logics: two decidability results LNCS 176, pp. 282 290.

    Google Scholar 

  24. Halpern J.Y. Deterministic Process Logic is elementary FOCS 82, pp 204–216.

    Google Scholar 

  25. — Reif J.H. The Propositional Dynamic Logic of deterministic, well-structured programs rep. of MIT, TM-198, 1981.

    Google Scholar 

  26. Harel D. Two results on Process Logic, Inf. Proc. Lett. 8(4), 1979, pp. 195–198.

    Google Scholar 

  27. — Dynamic Logic rep. CS 83-01 of Weizman Inst. of Sci., 1982 (also in: vol. II of Handbook of Philosophical Logic, Reidel Pub. Co. 1984)

    Google Scholar 

  28. — Recurring dominoes: making the highly undecidable highly understandable LNCS 158, pp. 177–194.

    Google Scholar 

  29. Harel D., Kozen D., Parikh R. Process Logic: expressiveness, decidability, completeness JCSS 25, 1982, pp. 144–170.

    Google Scholar 

  30. — Pnueli A., Sherman R. Is the interesting part of Process Logic uninteresting ? A translation from PL to PDL rep. of Weizman Inst. of Sci. CS 81-26, 1981.

    Google Scholar 

  31. Harel D., Sherman R. Propositional Dynamic Logic of Flowcharts LNCS 158, pp. 195–206, 1983.

    Google Scholar 

  32. Kozen D. On the duality of dynamic algebras and Kripke models rep. RC7893 of IBM Res. Lab. Yorktown Heights, 1979.

    Google Scholar 

  33. — On the representation of dynamic algebras rep. RC7898 of IBM Res. Lab., Yorktown Heights, 1979.

    Google Scholar 

  34. — A representation theorem for models of *-free PDL LNCS 85, 1980.

    Google Scholar 

  35. — On the representation of dynamic algebras II rep. RC8290 of IBM Res. Lab., Yorktown Heights, 1980.

    Google Scholar 

  36. — On induction vs. *-continuity rep. RC8468 of IBM Res. Lab., Yorktown Heights, 1980.

    Google Scholar 

  37. — Results on the Propositional μ-calculus LNCS 140, 1982, pp. 348–359.

    Google Scholar 

  38. — Parikh R. An elementary proof of the completeness of PDL TCS 14, 1981, pp. 113–118.

    Google Scholar 

  39. Manna Z., Wolper P. Synthesis of Communicating Processes from Temporal Logic specifications LNCS 131, 1981,pp. 253–281.

    Google Scholar 

  40. Mayer A., Street R., Mirkowska G. The deducibility problem in Propositional Dynamic Logic LNCS 125, 1981, pp. 12–22.

    Google Scholar 

  41. Mirkowska G. On the Propositional Algorithmic Logic LNCS 74, 1979, pp. 381–389.

    Google Scholar 

  42. — Complete axiomatization of algorithmic properties of program schemes with bounded nondeterministic interpretations STOC 80, pp. 14–21.

    Google Scholar 

  43. — PAL — Propositional Algorithmic Logic Fundamenta Informaticae IV.3, 1981, pp. 675–760. (also in: LNCS 125).

    Google Scholar 

  44. Nishimura H. Descriptively complete Process Logic Acta Informatica 14, 1980, pp. 359–369.

    Google Scholar 

  45. Niwiński D. The propositional μ-calculus is more expressive than the Propositional Dynamic Logic of Looping manuscript Math. Inst. Univ. of Warsaw 1984.

    Google Scholar 

  46. Parikh R. A completeness result for PDL LNCS 64, 1978, pp. 403–415.

    Google Scholar 

  47. — Propositional Logics of Programs POPL 80, pp. 186–192.

    Google Scholar 

  48. — Propositional Dynamic Logics of Programs: a survey LNCS 125, pp. 102–144, 1981.

    Google Scholar 

  49. — Propositional Logics of Programs: new directions LNCS 158, pp. 347–359, 1983.

    Google Scholar 

  50. Passy S.I. Combinatory Dynamic Logic Ph.D. Thesis, Sector of Math. Logic, Sofia Univ., 1984.

    Google Scholar 

  51. Passy S.I., Tinchev T. PDL with data constans, Inf. Proc. Lett. 20, pp. 35–41, 1985.

    Google Scholar 

  52. Pratt V.R. A practical decision method for Propositional Dynamic Logic STOC 78, pp. 326–337.

    Google Scholar 

  53. — Process Logic: preliminary report POPL 79, pp. 93–100.

    Google Scholar 

  54. — Models of Program Logics FOCS 79, pp. 115–122.

    Google Scholar 

  55. — Dynamic algebras: examples, constructions, applications rep. TM-138 of MIT Lab. for Comp. Sci. 1979.

    Google Scholar 

  56. — Dynamic algebras and the nature of induction STOC 80, pp. 22–28.

    Google Scholar 

  57. — A decidable mu-calculus: preliminary report FOCS 81, pp. 421–427.

    Google Scholar 

  58. — Using graphs to understand PDL LNCS 131, pp. 378–396, 1981.

    Google Scholar 

  59. — A near optimal method for reasoning about actions JCSS 20, 1980, pp. 231–254.

    Google Scholar 

  60. Salwicki A. On algorithmic theory of stacks Fundamenta Informaticae vol. III(3), 1980

    Google Scholar 

  61. Salwicki A., Muldner T. On the algorithmic properties of concurrent programs LNCS 125, pp. 169–197, 1981

    Google Scholar 

  62. Sistla A.P., Vardi M.Y., Wolper P.L. Reasoning about infinite computation paths (extended abstract) FOCS 83, pp. 185–194.

    Google Scholar 

  63. Street R.S. Propositional Dynamic Logic of looping and converse STOC 81, pp. 375–383.

    Google Scholar 

  64. — Propositional Dynamic Logic of looping and converse is elementarily decidable Infor. and Control 54, 1982, pp. 121–141.

    Google Scholar 

  65. Thiele H. Propositional Computation Tree Dynamic Logic (PCTDL) Akad. der Wissenschaften der DDR, Inst. fur Theorie, Geschichte u. Organisation der Wissenschaft, Heft 32, 1983, pp. 118–137. (in German)

    Google Scholar 

  66. — A classification of Propositional Process Logics on the basis of automata theory (extended abstract) manuscript, 1984.

    Google Scholar 

  67. Tinchev T., Vakarelov D. Propositional Dynamic Logic with least fixed points which are programs manuscript, Sector of Math. Logic, Sofia Univ., 1984.

    Google Scholar 

  68. Valiev B. On axiomatization of Deterministic Propositional Dynamic Logic LNCS 74, pp. 482–491, 1979.

    Google Scholar 

  69. — Decision complexity of variants of Propositional Dynamic Logic LNCS 88, pp. 656–664, 1980.

    Google Scholar 

  70. Vardi M.Y., Wolper P.L. Authomata-theoretic techniques for modal logics of programs manuscript, 1984 (the first version in: STOC 84 pp. 446–456)

    Google Scholar 

  71. Wechler W. Hoare Algebras versus Dynamic Algebras Coll. Algebra Logic and Combinatorics in Comp. Sci., Györ,1983

    Google Scholar 

  72. Wolper P.L. Synthesis of Communicating Processes from Temporal Logic specifications rep. CS-82-925, Dept. of Comp. Sci., Stanford Univ.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Centre, Technical Univ., 60-965, Poznań

    Z. Habasiński

  2. Mathematical Inst., Polish Academy of Sciences, Poland

    Z. Habasiński

Authors
  1. Z. Habasiński
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrzej Skowron

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Habasiński, Z. (1985). Model theory of propositional logics of programs, some open problems. In: Skowron, A. (eds) Computation Theory. SCT 1984. Lecture Notes in Computer Science, vol 208. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16066-3_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-16066-3_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16066-3

  • Online ISBN: 978-3-540-39748-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation