CTL Model Checking of Time Petri Nets Using Geometric Regions

摘要

Geometric region method is one of the tech- niques to handle real-time systems which have potentially infi- nite 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 algo- rithm, and compare it with the other methods by using small examples.