Some Problems in the Paper “Model Checking Using Partial Kripke Structure with 3-Valued Temporal Logic”.

Abstract: A lot of work has been done in the field of multi-valued model checking home and abroad. But some research works are not perfect. Some problems in the semantic definitions of temporal operators and corresponding model checking algorithms are found in the paper “Model Checking Using Partial Kripke Structure with 3-Valued Temporal Logic”. Some counterexamples are given to show these errors. On the basis of the discussion, some sound semantic definitions of temporal operators and correct algorithms of model checking for some temporal operators are given. [Copyright &y& Elsevier]