DCA2MC research method splits model checking to cut memory demands

In the team’s schematic, one large verification problem starts with an initial state and unfolds into a reachable state space. DCA2MC, developed by Professor Kazuhiro Ogata, Associate Professor Tsubasa Takagi and Senior Lecturer Canh Minh Do at the Japan Advanced Institute of Science and Technology in Japan, cuts that space into layers and checks the smaller pieces independently.

Model checking is an automated way to verify whether hardware or software satisfies specified requirements. Its central obstacle is state-space explosion: as systems become more complex, the number of states to examine can make direct verification too demanding in memory or time. DCA2MC addresses that bottleneck for linear temporal properties, requirements about how a system behaves over time, by using a divide-and-conquer strategy.

The researchers built the tool in Maude, a language based on rewriting logic. It can handle subproblems sequentially or in parallel, allowing independent checks to use multicore computing resources. It can also connect to external model checkers, including Spin, without requiring changes to their underlying algorithms. In case studies of five mutual exclusion protocols, DCA2MC completed several verification tasks that other tools could not finish within their available memory, while taking substantially less time than the Maude LTL model checker in several cases.

And so, concretely? Engineers and researchers could attempt verification of larger digital systems before simplifying or abandoning the analysis because of hardware limits. The potential beneficiaries include developers working on autonomous vehicles, digital systems and industrial control systems, but the study reports experiments rather than deployment in those settings. A semiautomated command system also helps users choose layer configurations, reducing reliance on trial and error when balancing memory use and runtime.

The result is a research-stage tool and method, not evidence that every large system can now be verified automatically. Performance depends on choosing suitable layer depths, and the reported comparisons cover the five protocol case studies. The team’s findings were published in ACM Transactions on Software Engineering and Methodology on July 31, 2026.