Model Checking Using Tabled Rewriting: for IJCAR2004 Doctoral Programme

Physics Opportunities For The Fixed-Target Tevatron

材料科学;生物科学

Zhiyao Liang ; Rakesh M. Verma

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

来源: CEUR

【 摘 要 】

LRR [3] is a rewriting system developed at the Computer Science DepartmentofUniversityofHouston.LRRhastwosubsystems: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 totheirnormalizedforms.HoweverthepracticalityofusingLRRasa framework for implementing model checking has not been experimented before.WehaveimplementedLTLandCTLmodelcheckingalgorithmsusingLRR. ThecurrentresultofthisresearchshowsthatLRRcanprovideaconvenient programmingframework,andthemodelcheckerhasalreadyinsomeaspects achievedtheefficiencycomparabletothoseleadingmodelcheckerssuchas SPIN. The model checker also has the potential to be improved significantly.