Process logic: Expressiveness, decidability, completeness
- 1 October 1980
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 24 (02725428) , 129-142
- https://doi.org/10.1109/sfcs.1980.35
Abstract
We define a process logic PL that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL is an extension of the language of Propositional Dynamic Logic (PDL). We give a deductive system for PL which includes the Segerberg axioms for PDL and prove that it is complete. We also show that PL is decidable.Keywords
This publication has 14 references indexed in Scilit:
- Dynamic algebras and the nature of inductionPublished by Association for Computing Machinery (ACM) ,1980
- Definability in Dynamic LogicPublished by Association for Computing Machinery (ACM) ,1980
- On the temporal analysis of fairnessPublished by Association for Computing Machinery (ACM) ,1980
- Models of program logicsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1979
- Two results on process logicInformation Processing Letters, 1979
- First-Order Dynamic LogicLecture Notes in Computer Science, 1979
- A decidability result for a second order process logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1978
- Propositional modal logic of programsPublished by Association for Computing Machinery (ACM) ,1977
- Weak monadic second order theory of succesor is not elementary-recursiveLecture Notes in Mathematics, 1975
- Decidability of Second-Order Theories and Automata on Infinite TreesTransactions of the American Mathematical Society, 1969