Publication

[LiZPVH13] LTL Satisfiability Checking Revisited Li, J.; Zhang, L.; Pu, G.; Vardi, M. and He, J. In 20th International Symposium on Temporal Representation and Reasoning (TIME), IEEE Comp. Society Press, 2013.
Downloads: pdf, bibURL: http://doi.ieeecomputersociety.org/10.1109/TIME.2013.19 Abstract. We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a Büchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools.