Parallel First-Order Dynamic Logic and Its Expressiveness and Axiomatization
For modeling the parallel actions, the quantified dynamic logic (QDL) is extended to Parallel First- order Dynamic Logic (PaFDL) with parallel action compositions. The composition is introduced as an operator ∩ on actions in the same syntax as in Pelegs CQDL but its semantics is defined differently from those of CQDL. The expressive power of PaFDL is proved to be the same as that of QDL. An axiomatic system is given and its first-order soundness and completeness are proved. Compared with other parallel or concurrent Dynamic Logics, PaFDL has a very easy and intuitive understanding for parallel actions as they are in the sequential models.
Dynamic logic First-order logic Parallel actions Expressiveness Axiomatization
Zhiguo Zhang Yunfei Jiang
Faculty of Information Science and Technology Sun Yatsen University Guangzhou City, 510275 China
国际会议
7th International Symposium,APPT 2007(第7届高级并行处理技术大会)
广州
英文
600-607
2007-11-22（万方平台首次上网日期，不代表论文的发表时间）