CTL Model Checking of Time Petri Nets Using Geometric Regions

スポンサーリンク

概要

• 論文の詳細を見る

• Geometric region method is one of the techniques to handle real-time systems which have potentially infinite state spaces. However, the original geometric region method gives incorrect results for the CTL model checking of time Petri nets. In this paper, we discuss the sufficient condition for the geometric region graphs to be correct with respect to the CTL model checking of time Petri nets, and then propose a technique to partition given geometric regions so that the graphs satisfy the sufficient condition. Finally, we implement the proposed algorithm, and compare it with the other methods by using small examples.

• 社団法人電子情報通信学会の論文
• 1998-03-25

著者

• Yoneda T

  Soka Univ. Hachioji‐shi Jpn

• YONEDA Tomohiro

  the Department of Computer Science, Tokyo Institute of Technology

• RYUBA Hikaru

  the Department of Computer Science, Tokyo Institute of Technology

• Yoneda T

  Infrastructure Systems Research Division National Institute Of Informatics

• Ryuba Hikaru

  The Department Of Computer Science Tokyo Institute Of Technology:nec

関連論文

• Failure Trace Analysis of Timed Circuits for Automatic Timing Constraints Derivation(Dependable Computing)
• Partial Order Reduction for Timed Circuit Verification Based on Level Oriented Model(Verification and Dependability Analysis)(Dependable Computing)
• Partial Order Reduction for Timed Circuit Verification Based on Level Oriented Model
• Modular Synthesis of Timed Circuits Using Partial Order Reduction
• Automatic Elicitation of Knowledge for Detecting Feature Interactions in Telecommunication Services(Special Issue on Knowledge-Based Software Engineering)
• CTL Model Checking of Time Petri Nets Using Geometric Regions

スポンサーリンク