Comparison of Algorithms for Checking Emptiness on Buechi Automata

Details Comparison of Algorithms for Checking Emptiness on Buechi Automata Comparison of Algorithms for Checking Emptiness on Buechi Automata

2009-10-20

arxiv.org/abs/0910.3766v1

Computer Science

Logic in Computer Science

Technical Report, 15 pages

Scientific paper

We re-investigate the problem of LTL model-checking for finite-state systems. Typical solutions, like in Spin, work on the fly, reducing the problem to Buechi emptiness. This can be done in linear time, and a variety of algorithms with this property exist. Nonetheless, subtle design decisions can make a great difference to their actual performance in practice, especially when used on-the-fly. We compare a number of algorithms experimentally on a large benchmark suite, measure their actual run-time performance, and propose improvements. Compared with the algorithm implemented in Spin, our best algorithm is faster by about 33 % on average. We therefore recommend that, for on-the-fly explicit-state model checking, nested DFS should be replaced by better solutions.

Affiliated with

Also associated with

No associations

Rating

Comparison of Algorithms for Checking Emptiness on Buechi Automata 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 Comparison of Algorithms for Checking Emptiness on Buechi Automata, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Comparison of Algorithms for Checking Emptiness on Buechi Automata will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-143927