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 条

[1]

ALUR R, 1995, IEEE S LOG, P90, DOI 10.1109/LICS.1995.523247

[2]

BOLLIG B, 2007, LSV0722

[3]

BOLLIG B, 2006, LSV0611

[4] Message-passing automata are expressively equivalent to EMSO logic [J].

Bollig, Benedikt ;

Leucker, Martin .

THEORETICAL COMPUTER SCIENCE, 2006, 358 (2-3) :150-172

[5]

BRANDT D, 1983, J ACM, V30

[6]

Clarke E, 2001, Model checking

[7]

Emerson E.A., 1990, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, P995, DOI [DOI 10.1016/B978-0-444-88074-1.50021-4, 10.1016/B978-0-444-88074-1.50021-4.]

[8] PROPOSITIONAL DYNAMIC LOGIC OF REGULAR PROGRAMS [J].

FISCHER, MJ ;

LADNER, RE .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1979, 18 (02) :194-211

[9]

Gastin P, 2003, LECT NOTES COMPUT SC, V2761, P222

[10]

Genest B, 2002, LECT NOTES COMPUT SC, V2380, P657

← 1 2 →