On decidability and model checking for a first order modal logic for value-passing processes

摘要

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(FO~2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO~2) is obtained.