Model Checking Using Tabled Rewriting

LRR [3] is a rewriting system developed at the Computer Science Department of University of Houston. LRR has two subsystems: Smaran (for tabled rewriting), and TGR (for untabled rewriting). It can utilize the history of computation to eliminate the redundant work in the process of reducing terms to their normalized forms. However the practicality of using LRR as a framework 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 convenient programming framework, and the model checker has already in some aspects achieved the efficiency comparable to those leading model checkers such as SPIN. The model checker also has the potential to be improved significantly.

• Type: Conference
• Year: 2004
• Where: CADE
• Authors: Zhiyao Liang
• Keywords: Automated Reasoning, CADE 2004, Computer Science Department, Convenient Programming Framework, Model Checking Algorithms