OBDRŽÁLEK, Jan. Fast Mu-calculus Model Checking when Tree-width is Bounded. In CAV 2003. Berlin Heidelberg: Springer-Verlag, 2003. p. 80-92, 13 pp. ISBN 3-540-40524-0.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Fast Mu-calculus Model Checking when Tree-width is Bounded
Authors OBDRŽÁLEK, Jan (203 Czechia, guarantor).
Edition Berlin Heidelberg, CAV 2003, p. 80-92, 13 pp. 2003.
Publisher Springer-Verlag
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/03:00008708
Organization unit Faculty of Informatics
ISBN 3-540-40524-0
Keywords in English parity games; mu-calculus; model-checking; tree-width
Tags Model-Checking, mu-calculus, parity games, tree-width
Changed by Changed by: doc. Mgr. Jan Obdržálek, PhD., učo 1552. Changed: 26/5/2004 11:18.
Abstract
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.
Links
GA201/03/1161, research and development projectName: Verifikace nekonečně stavových systémů
Investor: Czech Science Foundation, Standard Projects
MSM 143300001, plan (intention)Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Research Intents
PrintDisplayed: 3/8/2020 17:34