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

被引：0

作者：

Xue, R ^{[1
]}

Lin, HM ^{[1
]}

机构：

[1] Chinese Acad Sci, Inst Software, Comp Sci Lab, Beijing 100080, Peoples R China

来源：

SCIENCE IN CHINA SERIES F-INFORMATION SCIENCES | 2003年 / 46卷 / 01期

关键词：

first order modal logic; decidability; model checking; value-passing processes;

D O I：

10.1360/03yf9004

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：45 / 59

页数：15

共 18 条

[1] A LOGICAL CHARACTERIZATION OF OBSERVATION EQUIVALENCE
BLOOM, SL
TROEGER, DR
[J]. THEORETICAL COMPUTER SCIENCE, 1985, 35 (01) : 43 - 53
[2] Borger Egon, 1997, CLASSICAL DECISION P
[3] PROPOSITIONAL DYNAMIC LOGIC OF REGULAR PROGRAMS
FISCHER, MJ
LADNER, RE
[J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1979, 18 (02) : 194 - 211
[4] GABBAY D, 1971, ASPECTS PHILOS LOGIC, P91
[5] On the decision problem for two-variable first-order logic
Gradel, E
Kolaitis, PG
Vardi, MY
[J]. BULLETIN OF SYMBOLIC LOGIC, 1997, 3 (01) : 53 - 69
[6] On logics with two variables
Grädel, E
Otto, M
[J]. THEORETICAL COMPUTER SCIENCE, 1999, 224 (1-2) : 73 - 113
[7] A MODAL CHARACTERIZATION OF OBSERVATIONAL CONGRUENCE ON FINITE TERMS OF CCS
GRAF, S
SIFAKIS, J
[J]. INFORMATION AND CONTROL, 1986, 68 (1-3): : 125 - 145
[8] ALGEBRAIC LAWS FOR NONDETERMINISM AND CONCURRENCY
HENNESSY, M
MILNER, R
[J]. JOURNAL OF THE ACM, 1985, 32 (01) : 137 - 161
[9] A MODAL LOGIC FOR MESSAGE-PASSING PROCESSES
HENNESSY, M
LIU, X
[J]. ACTA INFORMATICA, 1995, 32 (04) : 375 - 393
[10] PROOF SYSTEMS FOR SATISFIABILITY IN HENNESSY-MILNER LOGIC WITH RECURSION
LARSEN, KG
[J]. THEORETICAL COMPUTER SCIENCE, 1990, 72 (2-3) : 265 - 288

← 1 2 →