| 摘要 |
PROBLEM TO BE SOLVED: To provide an LTL (linear temporal logic) model checking system, an LTL model checking method and an LTL model checking program enabling even a person inexperienced in an LTL expression to easily confirm the LTL expression. SOLUTION: The LTL model checking system 100 includes a variable value sequence set generating means 3 generating a combination of certain variable value sequences, of which variables included in the LTL model have values possible in a predetermined sequence length, and an LTL model checking means 4 determining whether the LTL model is established when the variable value sequence generated by the variable value sequence set generating means 3 is substituted in the LTL model. COPYRIGHT: (C)2009,JPO&INPIT
|
