We devised the L +1-layer divide & conquer approach to leads-to model checking ( L +1-DCA2L2MC) and its parallel version, and developed sequential and parallel tools for L +1-DCA2L2MC. 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 these properties. Counterexample generation is one of the main tasks in the L +1-DCA2L2MC technique that can be optimized to improve its running performance. This article proposes a technique to find all counterexamples at once in model checking with a new model checker. Furthermore, layer configuration selection is essential to make the best use of the L +1-DCA2L2MC technique. This work also proposes an approach to finding a good layer configuration for the technique with an analysis tool. Some experiments are conducted to demonstrate the power and usefulness of the two optimization techniques, respectively. Moreover, our sequential and parallel tools are compared with SPIN and LTSmin model checkers, showing a promising way to mitigate the state space explosion and improve the running performance of model checking when dealing with large state spaces.

The paper describes a technique to mitigate the notorious state space explosion in model checking.The technique is called a divide & conquer approach to until and until stable model checking.As indicated by the name, the technique is dedicated to until and until stable properties that are expressed as φ1 U φ2 and φ1 U □φ2, respectively, where φ1, φ2 are state propositions.For real-time system analysis, some interesting systems requirements are expressed as until and until stable properties.For example, a clock is running and shows a correct time until a certain time has passed or until the clock stops due to an empty battery or other failures.Therefore, it is worth focusing on the properties.For each property, we prove a theorem that the proposed technique is correct and design an algorithm based on the theorem to support the technique.Index Terms-until properties,

Abstract The paper proposes a new technique to mitigate the state explosion in model checking. The technique is called a divide & conquer approach to leads-to model checking. As indicated by the name, the technique is dedicated to leads-to properties. It is known that many important systems requirements can be expressed as leads-to properties, thus it is worth focusing on leads-to properties. The technique divides an original leads-to model checking problem into multiple smaller model checking problems and tackles each smaller one. We prove a theorem that the multiple smaller model checking problems are equivalent to the original leads-to model checking problem. We conduct two case studies demonstrating the power of the proposed technique.

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.

We have conducted a case study in which an autonomous vehicle intersection control protocol is formally specified in Maude and model checked with Maude model checking facilities.We found that a function used in the protocol should be revised while formally specifying it and a logical clock such that times are total order should be used to avoid deadlock states during model checking experiments.

We formally specify a mobile ad hoc network mutual exclusion protocol designed by Walter, Welch and Vaidya in Maude, a specification/programming language based on rewriting logic, and model check that the protocol enjoys the lockout freedom property. Matching equations that can be used as part of the condition of a conditional rewrite rule make it possible to concisely specify complex state transitions. The protocol needs to take into account link failures and/or recoveries, leading to a huge number of states even when there are a small number of nodes. We propose a technique to alleviate the situation, which is called a divide & conquer approach to leads-to model checking. We are interested in the lockout freedom property as one desired property for the protocol in this paper. The property can be expressed with the LTL leads-to connective.