|
|||||
|
|
On decidability and model checking for a first order modal logic for value-passing processes |
|
| Authors: | |
| Affiliation: | Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China |
| Abstract: | A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained. |
| Keywords: | first order modal logic decidability model checking value-passing processes |
| 本文献已被 CNKI 万方数据 SpringerLink 等数据库收录！ | |