Researches On Some Fundamental Problems Of Linear Temporal Logic

Linear Temporal Logic (LTL) has now been widely used in Computer Science (CS). It is often used as a property language to describe system behaviors in program verifica-tion, synthesis, AI and etc. For example, to verify whether a system satisfies the property (usually written in LTL), the model checking technique transfers the negation of the prop-erty to an automaton, intersects with the system model, and then checks the result by checking the emptiness of the product automaton. From applications of LTL in CS, we can obtain two fundamental problems:First is the translation from LTL formulas to the equivalent automata, which is widely used in program verification and synthesis; And the second is the satisfiability checking of LTL formulas-because of that unsatisfiable formulas are meaningless in application. This thesis thus focuses on these two issues, proposing some novel algorithms and solutions.We first explore the translation from LTL formulas to the equivalent Biichi automata, and present a new translating algorithm (Chapter3). Compared to other approaches, ours avoid the generation of intermediate automata, which potentially fasten the construction. We implement the algorithm and compare the tool with SPOT, which is considered to be the best LTL-to-Biichi translator. Experiments show that our results are competitive with those from SPOT-This is quite encouraging since SPOT is well optimized and maintained for more than ten year, while our tool is only a prototype.Moreover, we obtain a new LTL reasoning framework from the translation algorithm, and successfully apply it for LTL satisfiability checking (Chapter4).The observation is that under the framework there is an obvious optimization that can accelerate the checking process. By leveraging the concept of "obligation set" of an LTL formula, we can check the satisfiable formulas very quickly. We compare the algorithm with that using BDD-based model checking, and found ours successfully outperform it.Beyond that, we set up a comprehensive comparison with all existed LTL satisfiabil-ity checking solutions, and preliminary experimental results show no single approach can dominate others. To produce a more competitive solver, we follow in two ways:First is to create a portfolio LTL satisfiability solver, named Polsat (Chapter7). The tool integrates existed LTL checking solvers based on different checking approaches, and is designed to obtain the best checking results among integrated solvers for the given formula. In this way we can develop a portfolio LTL satisfiability solver that always output the best checking results; The second is to encode our framework into the SAT one such that we can utilize the power of modern SAT solvers (Chapter5). The evaluations show that our new approach takes the best cases among different solutions, and gets a best performance on the whole.To extend the application of our framework, we also adapt it for LTLf satisfiability checking (Chapter6). LTLf is a variant of LTL, which is interpreted over finite traces. It can be used more often in AI area. Existed LTLf satisfiability checking can be achieved by reduction to LTL satisfiability checking. However checking the satisfiability of LTL formulas needs to find a fair cycle-this is not the case in LTLf checking. So the existed approach may cause an overhead. Our contribution here is to find a directly strategy for LTLf checking based on the framework we have proposed. The strategy used in LTLf satisfiability checking is simpler than that for LTL, but inherits all advantages from our previous one. Experiments show that our new approach absolutely outperforms the strat-egy by reduction to LTL checking.