×

Propositional dynamic logic of regular programs. (English) Zbl 0408.03014


MSC:

03B45 Modal logic (including the logic of norms)
68Q65 Abstract data types; algebraic specification
68N01 General topics in the theory of software
03B60 Other nonclassical logic
68W99 Algorithms in computer science
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
03D10 Turing machines and related notions
Full Text: DOI

References:

[1] Abrahamson, K.; Fischer, M. J., Applications of Boolean Variables to Automata Theory and Dynamic Logic, (Tech. Report 78-08-02 (1978), University of Washington)
[2] Berman, F.; Paterson, M. S., Test-Free Propositional Dynamic Logic is Weaker than PDL, Tech. Report TR 77-10-02 (1977)
[3] Chandra, A. K.; Stockmeyer, L. J., Alternation, (17th IEEE Symposium on Foundations of Computer Science (1976)), 98-108
[4] Constable, R. L., On the theory of programming logics, (Ninth ACM Symposium on Theory of Computing (1977)), 269-285
[5] Dijkstra, E. W., Guarded commands, nondeterminacy and formal derivation of programs, Comm. ACM 18, 8, 453-457 (1975) · Zbl 0308.68017
[6] Greibach, S. A., Theory of Program Structures: Schemes, Semantics, Verification, (Lecture Notes in Computer Science No. 36 (1975), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0345.68002
[7] Harel, D., (Tech. Report MIT/LCS/TR200 (1978)), Available as · Zbl 0589.68030
[8] Harel, D.; Meyer, A. R.; Pratt, V. R., Computatibility and completeness in logics of programs: preliminary report, (Ninth ACM Symposium on Theory of Computing (1977)), 261-268
[9] Harel, D.; Pratt, V. R., Nondeterminism in logics of programs, (Fifth ACM Symposium on Principles of Programming Languages (1978))
[10] Hoare, C. A.R., An axiomatic basis for computer programming, Comm. ACM 12, 10, 583 (1969) · Zbl 0179.23105
[11] Hoare, C. A.R.; Lauer, P., Consistent and complementary formal theories of the semantics of programming languages, Acta Inform. 3, 2, 135-153 (1974) · Zbl 0264.68006
[12] Kozen, D., On parallelism in Turing machines, (17th IEEE Symposium on Foundations of Computer Science (1976)), 89-97
[13] Kreczmar, A., Effectivity problems of algorithmic logic, (Loeckx, J., Automata, Languages and Programming, 2nd Colloquium, University of Saarbrücken. Automata, Languages and Programming, 2nd Colloquium, University of Saarbrücken, Lecture Notes in Computer Science No. 14 (July 29-Aug. 2, 1974), Springer-Verlag: Springer-Verlag Berlin/New York) · Zbl 0294.68017
[14] Kripke, S. A., Sementical analysis of modal logic I: Normal modal propositional calculi, Z. Math. Logik Grundlagen Math., 9, 67-96 (1963) · Zbl 0118.01305
[15] Kröger, F., Logical rules of natural reasoning about programs, (Michaelson, S.; Milner, R., Automata, Languages and Programming (1976), Edinburgh Univ. Press: Edinburgh Univ. Press Edinburgh), 87-98 · Zbl 0362.68038
[16] Ladner, R. E., The computational complexity of provability in systems of modal propositional logic, SIAM J. Comput. 6, 3, 467-480 (1977) · Zbl 0373.02025
[17] Meyer, A. R.; Stockmeyer, L. J., Word problems requiring exponential time, (Fifth ACM Symposium on Theory of Computing (1973)), 1-9 · Zbl 0359.68050
[18] Parikh, R., A completeness result for PDL, (Symposium on Mathematical Foundations of Computer Science. Symposium on Mathematical Foundations of Computer Science, Zakopane, Warsaw (Sept. 1978)) · Zbl 0188.02102
[19] Pratt, V. R., Semantical considerations on Floyd-Hoare logic, (17th IEEE Symposium on Foundations of Computer Science (1976)), 109-121
[20] Pratt, V. R., A practical decision method for propositional dynamic logic, (10th ACM Symposium on Theory of Computing (1978)), 326-337 · Zbl 1283.03066
[21] Saltvicki, A., Formalized algorithmic languages, Bull. Acad. Polon. Sci. Sir. Sci. Math. Astronom. Phys., 18, 227-232 (1970) · Zbl 0198.02801
[22] Segerberg, K., A completeness theorem in the modal logic of programs, Notices Amer. Math. Soc. 24, 6, A-552 (1977)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.