PNer: A Petri-Net-Based Model Checker for Computation Tree Logic

We develop a tool PNer, a model checker for verifying Computation Tree Logic based on Petri nets. This tool includes three parts. The first one can verify concurrent systems that are modeled by Petri nets for their properties/requirements specified by Computation Tree Logic. The second one can verify multi-agent systems that are modeled by knowledge-oriented Petri nets for their properties/requirements specified by Computation Tree Logic of Knowledge. The last one can verify real-time systems that are modeled by prioritized time-point-interval Petri nets for their properties/requirements specified by Timed Computation Tree Logic. For the first and second ones, PNer supports efficient symbolic techniques based on Ordered Binary Decision Diagrams to alleviate the state explosion problem. For the last one, PNer can quantitatively analyse time-related requirements of a real-time system, i.e., computers the minimum or maximum time bound ensuring a real-time system satisfies such a time-related requirement. In this paper we introduce PNer.