Functional term rewriting systems towards symbolic model-checking Online publication date: Wed, 11-Mar-2015
by Yohan Boichut, Jean-Michel Couvreur, Duy-Tung Nguyen
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 2, No. 3/4, 2011
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.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook