[6-30]An Efficient Model Checking Algorithm of FG-LTL
Date:2014-06-30
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,
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.