Decision Procedures For Fragments Of Linear Time Mu-Calculus

Temporal logic plays a crucial part in both program verification and AI planning.As one of the most representative temporal logics,Linear Temporal Logic(LTL)has been extensively used for specifying and verifying various properties of reactive and concurrent systems,as well as for expressing temporally extended goals(TEGs)in planning.Although LTL is convenient to use,its expressive power is only star-free regular.Therefore,some important properties cannot be characterized as LTL formulas.Linear Time μ-Calculus(νTL)is an extension of LTL with the least and greatest fixpoint operators.It is able to express allω-regular properties with the syntax being succinct.Fixpoints not only nicely capture the recursive and nonterminating behaviors of a system,but also allow one to express a much wider range of temporal properties than LTL does.However,the nesting of fixpoint operators makes νTL’s decision problems difficult to solve,which hinders the use of νTL in practice.Motivated by this observation,this thesis investigates two fragments of νTL,G-mu and νTL interpreted over finite traces(νTLf),and presents efficient decision procedures for them.G-mu is defined by adding restrictions on the occurrences of each least fixpoint subformula in a νTL formula.A function is presented which is capable of translating any ω-regular expression into a closed G-mu formula.Therefore,the expressive power of G-mu is ω-regular.Goal Progression Form(GPF)is defined for G-mu formulas and it is shown that every closed G-mu formula can be converted into this form.GPF decomposes a formula into the present and future parts.The present part is the conjunction of atomic propositions or their negations,stating what should be satisfied at the current state;while the future part is the conjunction of elements in the closure of a given formula,declaring what should be satisfied at the next state.Based on GPF,Goal Progression Form Graph(GPG)is defined and an algorithm for constructing GPGs is presented.GPG is a useful formalism describing models of a formula.Further,an intuitive GPG-based decision procedure running in 2O(|?|)for checking satisfiability of G-mu formulas is proposed,which is achieved by finding aν-path from a GPG where no least fixpoint unfolds itself infinitely.This makes the decision problems of G-mu and LTL have the same time complexity.However,compared with LTL,G-mu can be used to specify a richer class of temporal properties.In addition,an algorithm for building the product of a Kripke structure and a GPG is presented and the notion of ν-paths in GPGs is applied to the product graphs.Consequently,a GPG-based model checking approach is obtained.Another fragment of νTL focused on in this thesis is νTLf,which is LTL interpreted over finite traces(LTLf)augmented with the least and greatest fixpoint operators.Present Future Form(PFF)for νTLfformulas is defined and it is proved that every closed νTLfformula can be transformed into this form.Also,an algorithm for converting νTLfformulas into PFF is presented.Like GPF,PFF also decomposes a formula into two parts: what to be satisfied at the current state and what to be satisfied at the next one.Based on PFF,an algorithm for constructing Present Future Form Graph(PFG)that can be employed to depict models of a formula is provided.In addition,it is shown that a closed νTLfformula is satisfiable iff an ε-path can be found in its PFG.As a result,the satisfiability problem of a formula can be reduced to an ε-path searching problem from its PFG,and then further reduced to the problem of checking the existence of the ε node in the PFG.A PFG-based decision procedure running in 2O(|?|)for checking satisfiability of νTLfformulas is finally formalized and the corresponding model checking approach is obtained.This makes νTLf an attractive alternative for representing TEGs in planning.The problem of solving parity games is polynomial time equivalent to the μ-calculus model checking problem.Better algorithms for parity games may lead to better model checkers.Therefore,this thesis also provides an improved recursive algorithm for solving parity games to reduce the total number of recursive calls.To do so,on one hand,atomic winning regions are defined and a preprocessing algorithm is proposed for searching and pruning atomic winning regions from a game graph before they bring any bad effect on the subsequent recursion.On the other hand,an extra conditional statement is inserted before the second recursive call of the original recursive algorithm.When the condition holds,the winning regions can be acquired directly without preforming the second recursive call in virtue of some intermediate results generated in the process of recursion.