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. Fast Mu-calculus Model Checking when Tree-width is Bounded. In \textit{CAV 2003}. Berlin Heidelberg: Springer-Verlag, 2003, p.~80-92. ISBN~3-540-40524-0.
|