Improving the Translation from ECTL to SAT

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.