Improving the Translation from ECTL to SAT

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Zbrzezny, Andrzej

Affiliations: Institute of Mathematics and Computer Science Jan Długosz University in Cz�stochowa Armii Krajowej 13/15, 42-200 Cz�stochowa, Poland. a.zbrzezny@ajd.czest.pl

Note: [] Address for correspondence: Institute of Mathematics and Computer Science, Jan Długosz University in Cz�stochowa, Armii Krajowej 13/15, 42-200 Cz�stochowa, Poland

Abstract: The objective of this paper is to offer an improvement to the translation from ECTL to SAT introduced in [14] and show that the improvement proposed substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made preliminary experimental results, which demonstrate the efficiency of the method.

Keywords: ECTL, Bounded Model Checking, translation to SAT

Journal: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 513-531, 2008