×
Harel, David; Kozen, Dexter; Parikh, Rohit

Process logic: Expressiveness, decidability, completeness. (English) Zbl 0494.03016

J. Comput. Syst. Sci. 25, 144-170 (1982).
Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page
scan of Zbl 0494.03016

Cited in 8 Reviews
Cited in 31 Documents

MSC:

03B45 Modal logic (including the logic of norms)
68Q65 Abstract data types; algebraic specification
68N01 General topics in the theory of software

Keywords:

process logic; extending propositional dynamic logic; temporal logic; axiomatization

Citations:

Zbl 0423.68005; Zbl 0431.68041; Zbl 0221.02031
Cite Review PDF
Full Text: DOI

References:

[1] K. Abrahamson, correspondence.; K. Abrahamson, correspondence.
[2] Banachowski, L.; Kreczmar, A.; Mirkowska, G.; Rasiowa, H.; Salwicki, A., An introduction to Algorithmic Logic, (Mazurkiewicz; Pawlak, Mathematical Foundation of Computer Science (1977), Banach Center Publications: Banach Center Publications Warsaw) · Zbl 0358.68035
[3] Ben-Ari, M.; Halpern, J.; Pnueli, A., Finite models of deterministic propositional dynamic logic, (Proc. 8th Colloq. on Automata, Languages, and Programming. Proc. 8th Colloq. on Automata, Languages, and Programming, Springer Lecture Notes in Comp. Sci. (1981)) · Zbl 0465.68011
[4] Chandra, A. K.; Halpern, J.; Meyer, A.; Parikh, R., Equations between regular terms and an application to Process Logic, (Proc. 13th ACM Symp. on Theory of Computing (May 1981)) · Zbl 0587.68031
[5] Fischer, M. J.; Ladner, R. E., Propositional dynamic logic of regular programs, J. Comput. System Sci., 18, 2, 194-211 (1979) · Zbl 0408.03014
[6] Gabbay, D., Axiomatizations of Logics of Programs (November 1977), manuscript
[7] Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal analysis of fairness, (Proc. 7th ACM Symp. on Principles of Programming Languages (January 1980)), 163-173
[8] Harel, D., First-Order Dynamic logic, (Goos; Hartlmanis, Lecture Notes in Computer Science 68 (1979), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0403.03024
[9] Harel, D., Two results on process logic, Inform. Process. Lett., 8, 4, 195-198 (1979) · Zbl 0417.68017
[10] Kamp, H. W., Tense logics and the theory of linear order, (PhD. Thesis (1968), UCLA: UCLA California)
[11] Kozen, D., A representation theorem for models of \(^∗\)-free PDL, (Proc. 7th Int. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science, Vol. 85 (1980), Springer-Verlag: Springer-Verlag New York/Berlin), 351-362 · Zbl 0451.03005
[12] Kozen, D., On the Duality of Dynamic Algebras and Kripke Models (October 1979), IBM Research, Yorktown Heights: IBM Research, Yorktown Heights New York, Report RC7893
[13] Kozen, D., On the Representation of Dynamic Algebras (October 1979), IBM Research: IBM Research Yorktown Heights, New York, Report RC7898
[14] Kozen, D., On the Representation of Dynamic Algebras II (May 1980), IBM Research: IBM Research Yorktown Heights, New York, Report RC8290
[15] Kozen, D.; Parikh, R., An elementary proof of the completeness of PDL, Theoret. Comput. Sci., 14, 1, 113-118 (1981) · Zbl 0451.03006
[16] Manna, Z.; Pnueli, A., The modal logic of programs, (Proc. 6th ICALP. Proc. 6th ICALP, Lecture Notes in Computer Sci., Vol. 74 (1979), Springer-Verlag: Springer-Verlag New York/Berlin), 385-409 · Zbl 0404.68011
[17] Meyer, A. R., Weak monadic second order theory of successor is not elementary recursive, (Proc. Logic Colloquium. Proc. Logic Colloquium, Lecture Notes in Mathematics, Vol. 453 (1975), Springer-Verlag: Springer-Verlag New York/Berlin), 132-151 · Zbl 0326.02036
[18] Meyer, A. R., Ten thousand and one logics of programming, Bull. European Assoc. Theoret. Comput. Sci., 10, 11-29 (1980)
[19] Meyer, A. R.; Parikh, R., Definability in dynamic logic, (Proc. 12th ACM Symp. on Theory of Computing (April 1980)), 1-7 · Zbl 0472.03013
[20] Nishimura, H., Descriptively complete process logic, Acta Inform., 14, 4, 359-369 (1980) · Zbl 0423.68005
[21] Parikh, R., A completeness result for PDL, (Symp. on Math. Found. of Comp. Sci.. Symp. on Math. Found. of Comp. Sci., Zakopane, Warsaw (May 1978), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0188.02102
[22] Parikh, R., A decidability result for second order process logic, (Proc. 19th FOCS (October 1978)), 177-183
[23] Pnueli, A., The temporal logic of programs, (Proc. 18th FOCS (October 1977)), 46-57
[24] Pnueli, A., The temporal semantics of concurrent programs, (Proc. Int. Symp. on Semantics of Concurrrent Programs. Proc. Int. Symp. on Semantics of Concurrrent Programs, Evian, France (July 1979)) · Zbl 0402.68009
[25] Pratt, V. R., Semantical considerations on Floyd-Hoare logic, (Proc. 17th IEEE Symp. on Foundations of Comp. Sci. (Oct. 1976)), 109-121
[26] Pratt, V. R., A practical decision method for Propositional Dynamic Logic, (Proc. 10th ACM Symp. on Theory of Computing (May 1978)), 326-337 · Zbl 1283.03066
[27] Pratt, V. R., Process logic, (Proc. 6th ACM Symp. on Principles of Programming Languages (January 1979)), 93-100
[28] Pratt, V. R., A near optimal method for reasoning about action, J. Comput. System Sci., 20, 2, 231-254 (1980) · Zbl 0424.03010
[29] Pratt, V. R., Models of program logics, (Proc. 20th IEEE Symp. on Foundations of Comp. Sci. (October 1979)), 115-122
[30] Pratt, V. R., Dynamic algebras and the nature of induction, (Proc. 12th ACM Symp. on Theory of Computing (May 1980)), 22-28
[31] Rabin, M. O., Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc., 141, 1-35 (1969) · Zbl 0221.02031
[32] Salwicki, A., Formalized algorithmic languages, Bull. Acad. Polon. Sci. Ser. Math. Astronom. Phys., 18, 5 (1970) · Zbl 0198.02801
[33] Segerberg, K., A completeness theorem in the modal logic of programs, Notices Amer. Math. Soc., 24, 6, A-552 (1977)
[34] Tiuryn, J., Logic of Effective Definitions (July 1979), Inst. of Math., Warsaw Univ, manuscript
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.