Development and Evaluation of Symbolic Model-Checker Based on Approximation for Real-Time Systems

スポンサーリンク

概要

• 論文の詳細を見る

• This paper adresses a symbolic model-checking method for real-time systems, which checks CTL properties without computing exact state sets. The method reduces the state explosion using approximation method. In this paper, we introduce an approximation-based greatest fix-point computation and state sets manipulation for CTL formulae. We present a symbolic model-checking algorithm based on approximation. We have implemented the algorithm and experimented with CSMA/CD protocol. We also compared with other real-time symbolic model-checkers. Experimental results shows the effectiveness of approximation-based symbolic model-checking method.

• 社団法人電子情報通信学会の論文
• 2003-04-01

著者

• Yamane Satoshi

  Kanazawa University

• Nakamura Kazuhiro

  Nagoya University

関連論文

• Development and Evaluation of Symbolic Model-Checker Based on Approximation for Real-Time Systems
• Special section on concurrent/real-time and hybrid systems: Theory and applications

スポンサーリンク