View Related Documents

Abstract

An optimization technique is presented that compresses a chain of transitions into a single jump transition, thus making a model smaller prior to model checking. We give compression algorithms, together with conditions that allow such compressions to preserve next-time-free LTL. Experimental results are presented and discussed.

Fulltext Preview

Image of the first page of the fulltext document