Approximate Model Checking Using a Subset of First-order Logic

スポンサーリンク

概要

• 論文の詳細を見る

• In order to reduce the computational complexity of model checking, we can use a subset of first-order logic, called EUF, but the model checking problem using EUF is generally undecidable. In our previous work, we proposed a technique for checking invariant property for an over-approximate set of states including all the reachable states. In this paper, we extend this technique for handling not only invariants but also temporal properties written in computational tree logic with EUF extension. We show that model checking becomes possible for designs which are hard to handle without the proposed technique.

• 一般社団法人情報処理学会の論文
• 2010-08-16

著者

• Kiyoharu Hamaguchi

  Osaka University

• Toshinobu Kashiwabara

  Osaka University

• Kazuya Masuda

  Osaka University

関連論文

• Checker Generation of Assertions with Local Variables for Model Checking
• Approximate Model Checking Using a Subset of First-order Logic
• Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
• Symbolic Discord Computation for Efficient Analysis of Message Sequence Charts

スポンサーリンク