Other formats:
BibTeX
LaTeX
RIS
@inproceedings{555218,
author = {Obdržálek, Jan},
address = {Berlin Heidelberg},
booktitle = {CAV 2003},
keywords = {parity games; mu-calculus; model-checking; tree-width},
language = {eng},
location = {Berlin Heidelberg},
isbn = {3-540-40524-0},
pages = {80-92},
publisher = {Springer-Verlag},
title = {Fast Mu-calculus Model Checking when Tree-width is Bounded},
year = {2003}
}
TY - JOUR
ID - 555218
AU - Obdržálek, Jan
PY - 2003
TI - Fast Mu-calculus Model Checking when Tree-width is Bounded
PB - Springer-Verlag
CY - Berlin Heidelberg
SN - 3540405240
KW - parity games
KW - mu-calculus
KW - model-checking
KW - tree-width
N2 - We show that the model checking problem for mu-calculus on graphs of bounded tree-width can be solved in time linear in the size of the system. Since control flow graphs of programs written in high-level languages are usually of bounded tree-width, this gives us a faster algorithm for software model checking. The result is presented by first showing a related result: the winner in a parity game on a graph of bounded tree-width can be decided in polynomial time. Modification of this algorithm gives us a completely new algorithm for mu-calculus model checking. Finally, we discuss some implications and future work.
ER -
OBDRŽÁLEK, Jan. \textit{Fast Mu-calculus Model Checking when Tree-width is Bounded}. In \textit{CAV 2003}. Berlin Heidelberg: Springer-Verlag, 2003. p.~80-92, 13 pp. ISBN~3-540-40524-0.
|
