Propositional dynamic logic for message-passing systems

被引：0

作者：

Bollig, Benedikt ^{[1
]}

Kuske, Dietrich ^{[2
]}

Meinecke, Ingmar ^{[2
]}

机构：

[1] CNRS, ENS Cachan, LSV, 61,Av President Wilson, F-94235 Cachan, France

[2] Univ Leipzig, Inst Informat, D-04009 Leipzig, Germany

来源：

FSTTCS 2007: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS | 2007年 / 4855卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We examine a bidirectional Propositional Dynamic Logic (PDL) for message sequence charts (MSCs) extending LTL and TLC-. Every formula is translated into an equivalent communicating finite-state machine (CFM) of exponential size. This synthesis problem is solved in full generality, i.e., also for MSCs with unbounded channels. The model checking problems for CFMs and for HMSCs against PDL formulas are shown to be in PSPACE for existentially bounded MSCs. It is shown that CFMs are to weak to capture the semantics of PDL with intersection.

引用

页码：303 / +

页数：3

共 20 条

[11] A Kleene theorem and model checking algorithms for existentially bounded communicating automata [J].

Genest, Blaise ;

Kuske, Dietrich ;

Muscholl, Anca .

INFORMATION AND COMPUTATION, 2006, 204 (06) :920-956

[12] Dynamic linear time temporal logic [J].

Henriksen, JG ;

Thiagarajan, PS .

ANNALS OF PURE AND APPLIED LOGIC, 1999, 96 (1-3) :187-207

[13]

Henriksen JG, 1997, LECT NOTES COMPUT SC, V1243, P45

[14]

Madhusudan P, 2001, LNCS, V2245, P256

[15] The monadic quantifier alternation hierarchy over graphs is infinite [J].

Matz, O ;

Thomas, W .

12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1997, :236-244

[16]

Meenakshi B, 2000, LECT NOTES COMPUT SC, V1853, P487

[17]

MEENAKSHI B, 2004, COMPUTER LANG SYSTEM, V30, P529

[18]

Peled D., 2000, Formal Methods for Distributed System Development. FORTE/PSTV 2000. IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX), P139

[19]

VARDI MY, 1994, LECT NOTES COMPUTER, V789, P575

[20]

1996, MESS SEQ CHART 1996

← 1 2 →