The Design And Implementation Of Linear Temporal Logic Satisfiability Tool

Linear Temporal Logic(LTL) has been developed a lot since it was introduced to computer science in 1970s. Nowadays, It is widely used in various fields such as program verification and analysis, program synthesis, database and artificial intelligence.LTL is a kind of logic language, of which the main issue is satisfiability problem. Meanwhile, satisfiability problem is also important in industry because in terms of program verification, program synthesis and artificial intelligence, an unsatisfiable formula is meaningless.In this paper, a new algorithm named OFOA(which in chapter 3) aimed at satisfiability problem is proposed. This new algorithm provides a new set of reasoning framework that satisfiability judgement and formula expansion proceed at the same time, which is a significant optimization regarding to the traditional method that satisfiability judgement can’t be conducted until an equivalent Buchi automata has been converted. According to the "on the fly" idea, we defined a new concept for LTL formula, "obligation set", which greatly accelerates the satisfiability judgement process.Aalta, a new satisfiability tool based on OFOA algorithm was implemented which will be discussed later in the latter part of this paper about its design framework, data structure and core algorithm. To verify the efficiency of this algorithm, we designed a set of comparison experiments. We choose three most excellent satisfiability checking tools so far (PANDA, Cadence SMV and SPOT) to do these comparison experiments and the results eventually demonstrated our tool’s correctness and good performance.