Study On The Method Of Aptl Model Checking And The Verification Of Multi-Agent Systems

Model checking is an automatic technique for verifying the the properties of concurrent systems,where the formalized representation of systems is specified by temporal logic formulas,and the process of model checking depends on efficient and flexible algorithms of reachability problem based on graph theory.Model checking technique has attracted great attention from universal scholars and has got a rapid development.Model checking has been widely used in various fields of society,such as circuit design and protocol verification,etc.With the development of artificial intelligence technology,intelligent products also appear in our daily life,such as smart home,intelligent route planning of Baidu map,recommending and filtering website goods,robotic soccer game.Although these intelligent products bring great convenience to people's daily life,they also bring a lot of security risks simultaneously.Therefore,many scholars have devoted themselves to the research on how to ensure the security of intelligent products in recent years.The model checking method has been applied to the field of artificial intelligence and has achieved notable results.The properties of system are formally described by temporal logic formulas,so temporal logic plays a vital role in model checking.Alternating temporal logic(ATL)is a temporal logic,which is proposed by Alur and he used it to verify the properties of reactive systems,as well as it regards the interactive process of a reactive system as a game process between an open system and its environment.Proposition projection temporal logic(PPTL)can conveniently describe the properties of finite and infinite state paths.PPTL formulas are simple and intuitive,and can express completely regular properties;PPTL plays an important role in the field of model checking.Alternating projection temporal logic(APTL)is an extended logic of PPTL,it is able to not only express properties specified in classical temporal logic LTL,but also express interval related sequential and periodical properties,as well as express game related properties of open systems and multi-agent systems.In this paper,the logic laws of APTL are improved,an improved method for checking the satisfiability of APTL formulas is studied,and the APTL symbolic model checking approach is designed.In order to achieve the checking process automatically,a tool for checking satisfiability of APTL formulas and an APTL model checker are developed.The specific works are described as follows.Firstly,we perfect and prove the logic laws of APTL in this paper.The algorithms of transforming APTL formula into its normal form is developed based on the research of APTL logic laws.An improved method for checking the satisfiability of APTL formulas is designed,and the detailed checking process is given as following:(i)transforming APTL formula into normal form and constructing Labeled Normal Form Graph(LNFG)of the formula according to the normal form,and transforming the LNFG to an automata;(ii)transforming and simplifying the automata;(iii)checking whether the simplest automata is empty or not.The APTL formula cannot be satisfied if the automata is empty,and vice versa.Secondly,we develop a symbolic model checking algorithm based on BDD for APTL,the details are shown as follows:(i)describing the system with the interpreted system programming language and specifying the property of the system by an APTL formula;(ii)symbolically representing the system and transforming the negation of the formula into normal form;(iii)calculating the set of states from which there is at least one existing path satisfying the negation of the APTL formula.If the obtained state set contains an initial state,the system does not satisfy the formula;otherwise,the system satisfies the APTL formula.Thirdly,checking the satisfiability of APTL formulas is the prerequisite for further system verification,the tool APTL2 BCG is implemented according to the algorithm for checking APTL formula satisfiability.The powerful working ability of the tool is demonstrated through the task of checking three groups of representative APTL formulas.And we implemented tool MCMAS APTL to automate the checking process.The symbolic parts in MCMAS for multi-agent systems are used in the tool MCMAS APTL since the immense complexity to develop a complete model checker from the original bottom.Fourthly,in order to apply APTL model checking method to verify more complex systems,we modify the function of checker MCMAS APTL and improve the efficiency of the tool.This paper demonstrates the practicability and efficiency of MCMAS PTL by verifying the Open ID protocol of single sign-on in cloud computing and a scene of robot soccer game.