Truly On-The-Fly LTL Model Checking

Details Truly On-The-Fly LTL Model Checking Truly On-The-Fly LTL Model Checking

2005-11-16

arxiv.org/abs/cs/0511061v1

Dans Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005)

Computer Science

Logic in Computer Science

Scientific paper

We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized B\"{u}chi automaton for the negation of the formula and the emptiness check. Our algorithm first converts the LTL formula into a linear weak alternating automaton; configurations of the alternating automaton correspond to the locations of a generalized B\"{u}chi automaton, and a variant of Tarjan's algorithm is used to decide the existence of an accepting run of the product of the transition system and the automaton. Because we avoid an explicit construction of the B\"{u}chi automaton, our approach can yield significant improvements in runtime and memory, for large LTL formulas. The algorithm has been implemented within the SPIN model checker, and we present experimental results for some benchmark examples.

Affiliated with

Also associated with

No associations

Rating

Truly On-The-Fly LTL Model Checking does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Truly On-The-Fly LTL Model Checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Truly On-The-Fly LTL Model Checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-580884