A support tool for the L+1-layer divide & conquer approach to leads-to model checking

The paper describes a support tool for a technique that alleviates the notorious state space explosion problem in model checking. The technique is called the L + 1-layer divide & conquer approach to leads-to model checking. As indicated by the name, the technique is dedicated to leads-to properties. In a temporal logic called UNITY designed by Chandy and Misra, the leads-to temporal connective plays an important role and many case studies have been conducted in UNITY, demonstrating that many systems requirements can be expressed as leads-to properties. Hence, it is worth dedicating to the properties. The paper also reports on some experiments that demonstrate that the tool can alleviate the state space explosion problem to some extent.