Research On Spatio-Temporal Logic PPTL^SL And Its Applications

The solutions of many real world problems have been involved with both temporal and spa-tial information,thus the emergence of spatio-temporal reasoning.In recent years,spatio-temporal reasoning has become an active research area and has extensive applications in the fields of geographic information system,navigation of autonomous robot,spatio-temporal database,image understanding,formal verification and artificial intelligence etc.Spatio-temporal reasoning is originated from temporal reasoning and spatial reasoning.Simply speaking,the task of spatio-temporal reasoning is to reason objects which occupy some s-pace that changes over time from both temporal dimension and spatial dimension.There are many studies respectively on temporal reasoning and spatial reasoning so far.How to combine these two kinds of reasoning is one of the most important research focuses in cur-rent spatio-temporal reasoning,and transformation from basic theories to application fields is also the main objective of spatio-temporal reasoning.Within this dissertation we do a re-search and discussion on logic based spatio-temporal reasoning,and the main contributions are summarized as follows:First of all,this dissertation proposes a spatio-temporal logic system,namely PPTL^SLthat results from temporalising separation logic with PPTL?Propositional Projection Temporal Logic?.PPTL^SLhas the ability of expressing information on two dimensions?spatial and temporal?.The spatial dimension of PPTL^SLis realized by an expressive fragment of sepa-ration logic while PPTL whose expressive power is full regular is employed to characterize the temporal dimension.The decidability and complexity issues of PPTL^SLare studied.The important conclusions are that PPTL^SLis decidable and its complexity is the same with PPTL.In order to prove the decidability of PPTL^SL,we present an equisatisfiable translation from PPTL^SLto its subset,called RPPTL^SL(Restricted PPTL^SL),then prove that the deci-sion procedure of PPTL can be reused for RPPTL^SL.Moreover,we analyze the complexity of the decision procedure of PPTL^SL.The complexity of the equisatisfiable translation is polynomial and of RPPTL^SLis non-elementary since it reuses the PPTL's decision proce-dure.Therefore,the complexity of PPTL^SLis also non-elementary.The proposed decision procedure for PPTL^SLlays a solid theoretical foundation for its applications.Secondly,aiming at the existing problems on pointer-manipulating programs?pointer pro-grams for short?verification that rarely consider the information in temporal dimension,we investigate a model checking approach based on PPTL^SLand MSVL?Modeling,Simulation and Verification Language?.Memory can be regarded as an instance of space,and varia-tions of memory structure during program execution are the reflections of spatio-temporal information,that are commonly called memory evolution properties.The model checking approach introduced in this dissertation uses MSVL to encode pointer programs and PPTL^SLL to describe memory evolution properties.Based on the decision procedure of PPTL^SL,any PPTL^SLformula can be translated into an equisatisfiable RPPTL^SLformula,further we know RPPTL^SLand MSVL both lie in the scope of PTL?Projection Temporal Logic?,thus the program and the specification belong to the same logic system which avoids extra task of extracting the program model and simplifies the model checking process.Based on the normal form technique,the Normal Form Graphs?NFG?of program and specification are established respectively,and then the product of the program NFG and specification NFG are generated by the automata theory so as to check whether the specification satisfies the program.We consider a classical concurrent program and a real world application as case studies to demonstrate the effectiveness and feasibility of the proposed approach.Finally,we apply PPTL^SLin the field of artificial intelligence planning?planning in short?and present a planning approach on the basis of PPTL^SL.Traditional temporal logic based planning methods can only describe the temporal Search Control Knowledge?SCK?of a spe-cific planning problem,without any spatial information if existed.Such method cannot alle-viate the most difficult problem encountered in planning,i.e.the state explosion.Therefore,the planning approach presented in this dissertation aims at reducing the search space,and employs PPTL^SLto describe the spatio-temporal SCK which are in fact the spatio-temporal constraints the planning problem must satisfy.We realize the corresponding planning algo-rithm supplemented with a forward chaining mechanism,and develop a prototype planner.We select some typical benchmark problems which are widely accepted standards from the IPC?International Planning Competition?and experiment with them.The experiments show that our approach is suitable to solve the planning problems involving both temporal and spa-tial information,and our planner is more effective than most of the state-of-the-art planners in the world and can obtain much better plans.