Efficient Multi-Valued Bounded Model Checking for LTL over Quasi-Boolean Algebras

Jefferson O. ANDRADE  Yukiyoshi KAMEYAMA 

Publication
IEICE TRANSACTIONS on Information and Systems  Vol.E95-D  No.5  pp.1355-1364
Publication Date: 2012/05/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
multi-valued model checking,  bounded model checking,  quasi-boolean logic, 

Full Text: PDF(807.5KB)

Summary: 
Multi-valued Model Checking extends classical, two-valued model checking to multi-valued logic such as Quasi-Boolean logic. The added expressivity is useful in dealing with such concepts as incompleteness and uncertainty in target systems, while it comes with the cost of time and space. Chechik and others proposed an efficient reduction from multi-valued model checking problems to two-valued ones, but to the authors' knowledge, no study was done for multi-valued bounded model checking. In this paper, we propose a novel, efficient algorithm for multi-valued bounded model checking. A notable feature of our algorithm is that it is not based on reduction of multi-values into two-values; instead, it generates a single formula which represents multi-valuedness by a suitable encoding, and asks a standard SAT solver to check its satisfiability. Our experimental results show a significant improvement in the number of variables and clauses and also in execution time compared with the reduction-based one.