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

MaRDI QIDQ866004zbMATH OpenFDO

Authors Rui Xue, Huimin Lin

Publication date 20 February 2007

Published in Science in China. Series F (Search for Journal in Brave)

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

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.

Recommendations

• scientific article; zbMATH DE number 1231562
• scientific article; zbMATH DE number 1088043
• On logics with two variables
• A modal logic for message passing processes
• Decidability of modular logics for concurrency

Cited in

(3)

• scientific article; zbMATH DE number 1670836 (Why is no real title available?)
• Model Checking Value-Passing Modal Specifications
• scientific article; zbMATH DE number 1231561 (Why is no real title available?)

This page was built for publication: On decidability and model checking for a first order modal logic for value-passing process

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q866004)