The search functionality is under construction.
The search functionality is under construction.

Author Search Result

[Author] Hikaru RYUBA(1hit)

1-1hit
  • CTL Model Checking of Time Petri Nets Using Geometric Regions

    Tomohiro YONEDA  Hikaru RYUBA  

     
    PAPER-Fault Tolerant Computing

      Vol:
    E81-D No:3
      Page(s):
    297-306

    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.