ASK-LTL Checker: A Tailored Model Checker for Linear Temporal Logic of CPN State Space

Model checking is a formal method used to verify the correctness of hardware or software system designs and implementations. This kind of algorithm typically involves exhaustively searching the system’s state space to determine if the property is satisfied. Colored Petri Nets (CPN) is a graphical language for building system models and analyzing their properties, which can accurately describe concurrent behavior in software and is suitable for describing complex concurrent systems. At present, some studies extend Computational Tree Logic (CTL) on CPN, but Linear Temporal Logic (LTL) does not, and there are still shortcomings in transition property verification. LTL needs to be combined with the state information and transition firing information of CPN to achieve the model compatible property description. Therefore, this paper proposes an ASK-LTL model detector: ASK-LTL temporal logic is proposed, which is an extension of LTL, and can consider both state information and transition information. The model checking algorithm is proposed. First, simplify the ASK-LTL formula and convert it into a ASK-LTL Büchi automaton (ALGBA). Second, perform calculations using the automaton and CPN state space to generate a product automaton. Third, look for complete paths in the product automaton. This method not only retains the characteristics of LTL, but also can detect the transition information in CPN model. Finally, the correctness and effectiveness of the method are verified by the experiment of vending machine.