On decidability and model checking for a first order modal logic for value-passing process (Q866004)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: On decidability and model checking for a first order modal logic for value-passing process |
scientific article; zbMATH DE number 5128548
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | On decidability and model checking for a first order modal logic for value-passing process |
scientific article; zbMATH DE number 5128548 |
Statements
On decidability and model checking for a first order modal logic for value-passing process (English)
0 references
20 February 2007
0 references
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.
0 references
