Other formats:
BibTeX
LaTeX
RIS
@inproceedings{555218, author = {Obdržálek, Jan}, address = {Berlin Heidelberg}, booktitle = {CAV 2003}, keywords = {parity games; mucalculus; modelchecking; treewidth}, language = {eng}, location = {Berlin Heidelberg}, isbn = {3540405240}, pages = {8092}, publisher = {SpringerVerlag}, title = {Fast Mucalculus Model Checking when Treewidth is Bounded}, year = {2003} }
TY  JOUR ID  555218 AU  Obdržálek, Jan PY  2003 TI  Fast Mucalculus Model Checking when Treewidth is Bounded PB  SpringerVerlag CY  Berlin Heidelberg SN  3540405240 KW  parity games KW  mucalculus KW  modelchecking KW  treewidth N2  We show that the model checking problem for mucalculus on graphs of bounded treewidth can be solved in time linear in the size of the system. Since control flow graphs of programs written in highlevel languages are usually of bounded treewidth, 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 treewidth can be decided in polynomial time. Modification of this algorithm gives us a completely new algorithm for mucalculus model checking. Finally, we discuss some implications and future work. ER 
OBDRŽÁLEK, Jan. \textit{Fast Mucalculus Model Checking when Treewidth is Bounded}. In \textit{CAV 2003}. Berlin Heidelberg: SpringerVerlag, 2003. p.~8092, 13 pp. ISBN~3540405240.
