Model checking the full modal mu-calculus for infinite sequential processes

被引：0
|
作者：
Burkart, O
Steffen, B
机构：
[1] Univ Edinburgh, JCMB, LFCS, Edinburgh EH9 3JZ, Midlothian, Scotland
[2] Univ Passau, FMI, D-94032 Passau, Germany
来源：
AUTOMATA, LANGUAGES AND PROGRAMMING | 1997年 / 1256卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we develop a new exponential algorithm for model-checking infinite sequential processes, including contest-free processes, pushdown processes, and regular graphs, that decides the full modal mu-calculus. Whereas the actual model checking algorithm results from considering conditional semantics together with backtracking caused by alternation, the corresponding correctness proof requires a stronger framework, which uses dynamic environments modelled by finite-state automata.
引用
收藏
页码：419 / 429
页数：11
相关论文
共 50 条
12345