Analysis Of Linear Temporal Logic Over Finite Traces

Linear Temporal Logic(LTL)is a widely used system property specification language,which has been used in model checking,program synthesis and other fields.This paper mainly discusses linear temporal logic over finite traces(LTL_f).The difference between LTL_f formula and LTL formula is that one is interpreted on a finite sequence,and the other on an infinite sequence.The core of this paper is to explore the transformation problem of finite linear temporal logic formula to its equivalent automata,and put forward two new algorithms to transform LTL_f formula into the equivalent non-deterministic finite automata(NFA)and deterministic finite automata(DFA).NFA can be applied to LTL_f satisfiability checking and DFA can be applied to program synthesis.Program synthesis is a technology that automatically generates a certain system model whose form conforms to user-defined specifications.In the aspect of program synthesis,the research question is,given a property specification formula,whether there is a model that satisfies the property specification under any circumstance.Model checking techniques are used to verify interactive systems.In the field of model checking,firstly,the given property specification is reversed to generate an equivalent automaton,and then it is intersected with the system model to determine whether the received language of the new automaton is empty.If it is empty,the system satisfies this property.This experiment compares Aaltaf with MONA and SPOT,the two existing LTLto-automata conversion tools with the best performance.Experimental results show that the automata generated by our tool Aaltaf is slightly superior to the other two tools.Considering that MONA and SPOT have been under continuous development and maintenance for over a decade,Aaltaf is currently just a prototype and has a lot of room for improvement.