Model Checking Using Tabled Rewriting*(for IJCAR2004 Doctoral Programme)

2nd International Joint Conference on Automated Reasoning

Zhiyao Liang

Others  :  http://CEUR-WS.org/Vol-106/10-liang.pdf

来源: CEUR

【 摘 要 】

LRR [3] is a rewriting system developed at the Computer Science Department of University of Houston. LRR has two subsystems: Smaran (fortabled rewriting), and TGR (for untabled rewriting). It can utilize the history ofcomputation to eliminate the redundant work in the process of reducing termsto their normalized forms. However the practicality of using LRR as aframework for implementing model checking has not been experimented before. We have implemented LTL and CTL model checking algorithms using LRR.The current result of this research shows that LRR can provide a convenientprogramming framework, and the model checker has already in some aspectsachieved the efficiency comparable to those leading model checkers such as