Process logic: Expressiveness, decidability, completeness
作者： David Harel , Dexter Kozen , Rohit Parikh
DOI: 10.1016/0022-0000(82)90003-4
关键词:
摘要: Abstract A process logic (PL) is defined that subsumes Pratt's logic, Parikh's SOAPL, Nishimura's and Pnueli's Temporal Logic in expressiveness. The language of PL an extension the Propositional Dynamic (PDL). deductive system for given which includes Segerberg axioms PDL it proved complete. It also shown decidable.
core.ac.uk
elsevier.com
sci-hub.se 参考文章(22)
Jerzy Tiuryn, Logic of Effective Definitions Fundamenta Informaticae. ,vol. 4, pp. 629- 659 ,(1981) , 10.3233/FI-1981-4308
David Harel, First-Order Dynamic Logic ,(1979)
Albert R. Meyer, Weak monadic second order theory of succesor is not elementary-recursive Lecture Notes in Mathematics. pp. 132- 154 ,(1975) , 10.1007/BFB0064872
Krister Segerberg, A completeness theorem in the modal logic of programs Banach Center Publications. ,vol. 9, pp. 31- 46 ,(1982) , 10.4064/-9-1-31-46
Robert Goldblatt, SEMANTICAL CONSIDERATIONS ON FLOYD-HOARE LOGIC Journal of Symbolic Logic. ,vol. 51, ,(1976) , 10.2307/2273958
Dexter Kozen, A Representation Theorem for Models of *-Free PDL international colloquium on automata, languages and programming. pp. 351- 362 ,(1980) , 10.1007/3-540-10003-2_83
Zohar Manna, Amir Pnueli, The Modal Logic of Programs international colloquium on automata, languages and programming. pp. 385- 409 ,(1979) , 10.1007/3-540-09510-1_31
Dexter Kozen, On the duality of dynamic algebras and kripke models Logic of Programs. pp. 1- 11 ,(1981) , 10.1007/3-540-11160-3_1
Ashok Chandra, Joe Halpern, Albert Meyer, Rohit Parikh, Equations between regular terms and an application to process logic Proceedings of the thirteenth annual ACM symposium on Theory of computing - STOC '81. pp. 384- 390 ,(1981) , 10.1145/800076.802493
Dexter Kozen, Rohit Parikh, An elementary proof of the completeness of PDL Theoretical Computer Science. ,vol. 14, pp. 113- 118 ,(1981) , 10.1016/0304-3975(81)90019-0