Please login using the form on menu list.|
It is required to login for Full-Text PDF.
Efficient Multi-Valued Bounded Model Checking for LTL over Quasi-Boolean Algebras
Jefferson O. ANDRADE
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
multi-valued model checking,
bounded model checking,
Full Text: PDF(807.5KB)
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.