Title: An Efficient Model Checking Algorithm of FG-LTL

Speaker:  Lei Song

Date: Seminar on 30th, 2-3pm June 2014

Venue: Seminar room, Level 3, Building 5, Institute of Software, Chinese Academy of Sciences

Abstract:

We present an efficient algorithm for a fragment of Linear Temporal Logic (LTL) with only two modalities: eventually (F) and always (G). Different from classical algorithm, our algorithm is not automata-theoretic, thus has no need to generate Buechi automata. This will save us a significant amount of time especially for long formulas. We also prove that for formulas where each atomic proposition is preceded by at least one F and G, a space efficient algorithm exists. We compare our algorithm with the state-of-art tool Spot, and show that it exceeds Spot, often up to several orders of magnitude, both in time and memory usage. We also show how this algorithm can be extended to probabilistic systems.