A Method Based On MSVL For Modeling And Verifying The Automated Planning

With the development of artificial intelligence in recent years,automated planning as a traditional direction of artificial intelligence has attracted the attention of researchers.Planning Domain Description Language(PDDL)is widely used in modeling in the field of automated planning due to its concise description ability.Although it is convenient to use PDDL language to build the automated planning model,there are still some problems,the most important one is the completeness and correctness of the model.Automated planning problems often describe complex problems in practice.To build a complete model for such problems,not only users need to have a deep understanding of practical problems,but also many logical boundary conditions need to be considered.In the process of model building,incomplete consideration often leads to errors.It is very important to propose a corresponding logical verification method to detect model errors necessary.Formal method is a modeling and verification method based on rigorous mathematical logic,which is suitable for describing software and hardware systems.It is of great help to improve the reliability of the model.In this paper,model checking in the formal method is applied to the modeling and verification of automated planning,and the completeness and correctness of the model are judged through the property verification of temporal logic,so as to improve the automated planning model.An automated planning modeling and verification method based on Modeling,Simulation and Verification Language(MSVL)is presented in this paper.This method is based on the principle of Unified Model Checking(UMC).The specific process is as follows:1.First,MSVL is used to model the automated planning program written in PDDL language.In order to reduce a lot of manual operation,PDDL2 M conversion system is developed based on ANTLR(ANother Tool for Language Recognition)in the process of modeling,and gives the overall architecture of the conversion system.PDDL lexical and grammar rules of ANTLR style are written.The details in the implementation of four modules in the conversion system are introduced: preprocessing,lexical analysis,syntax analysis and program conversion.2.Then,in order to verify the properties of the automated planning model,Propositional Projection Temporal Logic(PPTL)is used to describe the properties of the model from three aspects of logical correctness,expression consistency and description integrity.3.Finally,the MSVL program for describing the Model and the PPTL formula for describing properties are input into the UMC-based runtime verifier UMC4 M for verification,and the verification results are used as the basis for improving the automatic programming Model to ensure the completeness and correctness of the Model.Through the modeling and verification of a concrete example of automated programming model,the above methods and tools are proved to be feasible and effective.