A linear time special case for MC games

被引：0

作者：

Poranen, T ^{[1
]}

Nummenmaa, J ^{[1
]}

机构：

[1] Tampere Univ, Dept Comp & Informat Sci, FIN-33014 Tampere, Finland

来源：

FUNDAMENTA INFORMATICAE | 2002年 / 50卷 / 3-4期

关键词：

model checking; MC games; parity games;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

MC games are infinite duration two-player games played on graphs. Deciding the winner in MC games is equivalent to the the modal mu-calculus model checking. In this article we provide a linear time algorithm for a class of MC games. We show that, if all cycles in each strongly connected component of the game graph have at least one common vertex, the winner can be found in linear time. Our results hold also for parity games, which are equivalent to MC games.

引用

页码：315 / 324

页数：10

共 21 条

[1]

Aho A. V., 1983, DATA STRUCTURES ALGO

[2]

Beffara E., 2001, 2001020 UPPS U DEP I

[3]

EMERSON EA, 1991, P 1991 IEEE S FDN CO

[4]

EMERSON EA, 1993, LECT NOTES COMPUT SC, V697, P385, DOI DOI 10.1007/3-540-56922-7_32

[5]

Even S., 1979, Graph Algorithms

[6] Deciding the winner in parity games is in UP∧co-UP [J].

Jurdzinski, M .

INFORMATION PROCESSING LETTERS, 1998, 68 (03) :119-124

[7] RESULTS ON THE PROPOSITIONAL MU-CALCULUS [J].

KOZEN, D .

THEORETICAL COMPUTER SCIENCE, 1983, 27 (03) :333-354

[8] INFINITE GAMES PLAYED ON FINITE GRAPHS [J].

MCNAUGHTON, R .

ANNALS OF PURE AND APPLIED LOGIC, 1993, 65 (02) :149-184

[9]

MOSTOWSKI AW, 1991, GAMES FORBIDDEN POSI

[10]

PETERSSON V, 2001, 2001008 UPPS U DEP I

← 1 2 3 →