Ishikawa, Japan--Model checking helps automatically verify whether hardware and software systems satisfy specified requirements. It has become an important formal verification technique, but two major challenges remain: state-space explosion, which limits the size of systems that can be checked, and long verification times. These challenges are increasingly important as society relies on complex digital technologies whose reliability and safety are essential.
Addressing this challenge, a research team led by Professor Kazuhiro Ogata, together with Associate Professor Tsubasa Takagi and Senior Lecturer Canh Minh Do from the Japan Advanced Institute of Science and Technology, Japan, developed a novel divide-and-conquer approach for model checking linear temporal properties, called DCA2MC. Their findings were published in the journal ACM Transactions on Software Engineering and Methodology on July 31, 2026.
DCA2MC divides the original model checking problem into multiple smaller problems using the tableau method. The reachable state space from each initial state is separated into layers, creating smaller sub-state spaces that can be checked independently. The researchers proved a theorem showing that these smaller model checking problems are equivalent to the original problem, providing a theoretical basis for the approach. "If each sub-state space is much smaller than the original reachable state space, it becomes feasible to conduct model checking, even when directly conducting it for the original reachable state space is infeasible due to the state space explosion problem," Prof. Ogata explains.
To support the approach, the team developed DCA2MC as a tool in Maude, a specification and programming language based on rewriting logic. The tool offers sequential and parallelization modes, allowing smaller verification tasks to be handled simultaneously. It can also integrate external model checkers, including Spin, allowing existing model checkers to benefit from the divide-and-conquer approach to handle larger state spaces without requiring modifications to their underlying algorithms. Case studies involving five mutual exclusion protocols compared DCA2MC with the Maude LTL model checker, Spin, and LTSmin, examining memory consumption and runtime performance. The results showed that DCA2MC could successfully complete several verification tasks that exceeded the memory capacity of other tools, while also achieving substantially shorter verification times than the Maude LTL model checker in several case studies. The parallel structure of the method also offers a natural way to take advantage of multicore computing resources, with independent subproblems handled simultaneously.
The effectiveness of DCA2MC also depends on selecting suitable layer configurations, which determine the depth of each layer. To address this practical challenge, the researchers introduced a semi-automated method for identifying a good configuration, supported by custom commands in DCA2MC. Experimental results demonstrated that the method can find good layer configurations to reduce memory demands and verification time while enabling larger state spaces to be handled more effectively. "The selection of a layer configuration plays a crucial role in maximizing the effectiveness of DCA2MC," Prof. Ogata notes. The semi-automated method helps identify suitable configurations rather than requiring users to select them entirely by trial and error. This makes the approach more practical for researchers and engineers applying model checking to increasingly complex systems.
Overall, the study provides a scalable approach for model checking larger and more complex systems. By making verification more practical, DCA2MC could support the development of more reliable hardware and software, including future autonomous vehicles, digital systems, and industrial control systems. Over the longer term, such advances could contribute to safer and more dependable technologies.
