publication . Article . 2012

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

Andrade, Jefferson O.; Kameyama, Yukiyoshi;
Open Access English
  • Published: 01 May 2012 Journal: IEICE transactions on information and systems, volume E95-D, issue 5, pages 1,355-1,364 (issn: 0916-8532, Copyright policy)
  • Publisher: 電子情報通信学会
Abstract
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-va...
Subjects
free text keywords: 情報学
Download from
JAIRO
Article . 2012
Provider: JAIRO
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue