Efficient Multi-Valued Bounded Model Checking for LTL over Quasi-Boolean Algebras
-
- ANDRADE Jefferson O.
- Department of Informatics, Campus Serra, Federal Institute of Espírito Santo
-
- KAMEYAMA Yukiyoshi
- Department of Computer Science, University of Tsukuba
この論文をさがす
抄録
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.
収録刊行物
-
- IEICE Transactions on Information and Systems
-
IEICE Transactions on Information and Systems E95.D (5), 1355-1364, 2012
一般社団法人 電子情報通信学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390282679354569088
-
- NII論文ID
- 10030942823
-
- NII書誌ID
- AA10826272
-
- BIBCODE
- 2012IEITI..95.1355A
-
- ISSN
- 17451361
- 09168532
-
- HANDLE
- 2241/118271
-
- 本文言語コード
- en
-
- データソース種別
-
- JaLC
- IRDB
- Crossref
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可