Title: Functional term rewriting systems towards symbolic model-checking

 

Author: Yohan Boichut, Jean-Michel Couvreur, Duy-Tung Nguyen

 

Addresses:
LIFO, Universite d'Orleans, 45067 Orleans, France.
LIFO, Universite d'Orleans, 45067 Orleans, France.
LIFO, Universite d'Orleans, 45067 Orleans, France

 

Journal: Int. J. of Critical Computer-Based Systems, 2011 Vol.2, No.3/4, pp.378 - 408

 

Abstract: This paper proposes the theoretical foundations of a new formal tool for symbolic verification of finite systems. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs). In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called functional term rewriting systems (FTRSs). First, we show that FTRSs are as expressive as TRSs. Second, we present the implementation of our FTRS-based tool as well as optimisations based on local fixpoint computations. Our experiments show that for well-known protocols (e.g., tree arbiter, percolate, leader election protocol, ...) our tool is more efficient than other rewriting tools such as Timbuk, Maude or Tom. Moreover, it can also be applied to check invariant properties which are a particular subclass of linear temporal logic (LTL) formula.

 

Keywords: model checking; symbolic verification; acceleration techniques; functional term rewriting; modelling; invariant properties; linear temporal logic.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2011.042334

 

Available online 04 Sep 2011

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article