Pushdown processes: Games and model-checking

被引：162

作者：

Walukiewicz, I ^{[1
]}

机构：

[1] Warsaw Univ, Inst Informat, PL-02097 Warsaw, Poland

来源：

INFORMATION AND COMPUTATION | 2001年 / 164卷 / 02期

关键词：

D O I：

10.1006/inco.2000.2894

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

A pushdown game is a two player perfect information infinite game on a transition graph of a pushdown automaton. A winning condition in such a game is defined in terms of states appearing infinitely often in the play. It is shown that if there is a winning strategy in a pushdown game then there is a winning strategy realized by a pushdown automaton. An EXPTIME procedure for finding a winner in a pushdown game is presented. The procedure is then used to solve the model-checking problem for the pushdown processes and the propositional mu -calculus. The problem is shown to be DEXPTIME-complete. (C) 2001 Academic Press.

引用

页码：234 / 263

页数：30

共 26 条

[21] Point characterization of infinite behavior of finite-state systems [J].