An Efficient Model Checking Algorithm of FG-LTL

Title: An Efficient Model Checking Algorithm of FG-LTL

Speaker:  Lei Song (MPI,Saarbrucken and Saarland U., Germany)       depend.cs.uni-sb.de/~song

Date & Time: 30th June 2014,  14:00-15:00

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

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.