Model checking, a technique that automatically tests whether hardware and software obey formal requirements, has long promised a way to catch dangerous design flaws before systems reach the real world. Yet its greatest strength—examining every state a system can reach—also creates its central weakness. As systems become more connected and autonomous, the number of possible states can grow explosively, overwhelming available memory and turning verification into a race against computational limits. Researchers at the Japan Advanced Institute of Science and Technology (JAIST) have now developed a divide-and-conquer strategy designed to make this enormous verification task more manageable, potentially allowing engineers to analyze systems that conventional model checkers cannot handle.
The method, called DCA2MC, was developed by a research team led by Professor Kazuhiro Ogata, together with Associate Professor Tsubasa Takagi and Senior Lecturer Canh Minh Do. It is designed for model checking linear temporal properties, a formal language used to describe how system behavior unfolds over time. Such properties can express requirements such as “a request is eventually acknowledged,” “a critical section is never entered by two processes simultaneously,” or “once an alarm is activated, the system will eventually reach a safe state.” Rather than treating the entire reachable state space as one massive verification problem, DCA2MC breaks it into smaller sub-state spaces that can be analyzed independently.
The underlying challenge is easier to appreciate by considering a concurrent system with several components, each capable of changing independently. Every combination of component states may represent a distinct global state, and every possible transition between those states can generate still more behaviors. Even a system with a modest number of variables can therefore produce millions or billions of reachable configurations. Traditional model checking explores this state graph while searching for a violation of the specified property. When the graph exceeds the computer’s memory, verification may stop before a definitive answer is obtained. DCA2MC addresses this state-space explosion by organizing the reachable behavior from an initial state into layers, effectively constructing a collection of smaller verification domains.
The researchers’ approach uses the tableau method, a formal procedure that transforms temporal-logic reasoning into structured sets of states and transitions. In DCA2MC, the reachable state space is divided according to layer configurations that determine how deeply the behavior is partitioned. Each resulting sub-state space contains a limited portion of the system’s possible evolution, allowing the model checker to examine it without loading the full state graph into memory. The process resembles dividing a vast map into independently searchable regions, except that the regions are created according to the system’s transition behavior and the logical structure of the property being checked. This division is not merely a practical shortcut: the researchers proved a theorem establishing that the collection of smaller model-checking problems is equivalent to the original problem.
That equivalence is critical. A verification method would be of limited value if it reduced memory use by silently overlooking behaviors that cross the boundaries between layers. According to the researchers, their theoretical result ensures that checking the independently generated sub-state spaces can preserve the answer that would be obtained by checking the original reachable state space as a whole. If any subproblem reveals a violation, the overall system fails the property; if all the required subproblems satisfy the property under the method’s formal conditions, the original model is also verified. The result gives DCA2MC a mathematical foundation rather than relying solely on empirical evidence that the partitioning appears to work.
To turn the concept into a usable verification system, the team implemented DCA2MC in Maude, a specification and programming language based on rewriting logic. Rewriting logic is well suited to describing systems whose states evolve through rule-based transformations, making it possible to represent both the system being analyzed and the operations used to divide its state space. DCA2MC supports sequential execution, in which subproblems are processed one after another, and parallel execution, in which independent tasks can run simultaneously on multiple processor cores. This structure could be particularly valuable for modern verification environments, where adding computational capacity is often easier than redesigning the underlying model-checking algorithm.
The tool can also work with external model checkers, including Spin, one of the best-known platforms for verifying concurrent and distributed software. This interoperability means that researchers and engineers may be able to apply DCA2MC’s decomposition strategy without rewriting the algorithms inside their preferred verification tools. In tests involving five mutual-exclusion protocols, the researchers compared DCA2MC with the Maude LTL model checker, Spin, and LTSmin. Mutual exclusion protocols are designed to ensure that competing processes do not enter a protected critical section at the same time, a fundamental requirement in operating systems, embedded controllers, communication protocols, and distributed computing.
The experiments indicated that DCA2MC completed several verification tasks that exceeded the memory capacity of other tools. In multiple case studies, it also required substantially less time than the Maude LTL model checker. The results suggest that dividing the state space can deliver two related benefits: each individual task becomes small enough to fit within available memory, and the tasks can be distributed across processors rather than being handled by a single monolithic computation. However, the researchers emphasize that performance depends on how the division is configured. A poor partition may produce too many subproblems, create unnecessary overhead, or fail to reduce the size of the most demanding portions of the state space.
To address that limitation, the team introduced a semi-automated procedure for identifying effective layer configurations. These configurations specify how the reachable space should be divided and how deep each layer should extend. DCA2MC includes custom commands that help users explore candidate configurations and identify those likely to reduce memory consumption and verification time. Experimental results showed that the procedure could find useful configurations without forcing users to rely entirely on trial and error. This feature is important for practical adoption because the best configuration may depend on the model’s structure, the temporal property under examination, the number of available processor cores, and the memory resources of the verification machine.
The researchers say the approach could help extend formal verification to larger and more complex systems, including autonomous vehicles, industrial control platforms, and safety-critical digital infrastructure. Model checking does not replace testing or engineering judgment, but it can examine classes of behaviors that are difficult to cover through conventional testing alone. By making exhaustive reasoning more scalable, DCA2MC may help developers detect synchronization failures, unsafe transitions, and violations of temporal requirements earlier in the design process. The method is not a universal solution to state-space explosion, and its effectiveness remains tied to suitable partitioning and the characteristics of each model. Nevertheless, the combination of a formal equivalence theorem, parallel computation, external-tool integration, and semi-automated configuration offers a promising route toward verification systems capable of confronting the rapidly expanding complexity of modern technology.
Subject of Research: Model checking and formal verification of software and hardware systems
Article Title: A Divide and Conquer Approach to Model Checking Linear Temporal Properties
News Publication Date: July 31, 2026
Web References: https://doi.org/10.1145/3836770
References: Canh Minh Do, Tsubasa Takagi, and Kazuhiro Ogata, “A Divide and Conquer Approach to Model Checking Linear Temporal Properties,” ACM Transactions on Software Engineering and Methodology. DOI: 10.1145/3836770
Image Credits: Prof. Kazuhiro Ogata from the Japan Advanced Institute of Science and Technology (JAIST)
Keywords: Model checking, formal verification, linear temporal logic, state-space explosion, divide-and-conquer algorithms, DCA2MC, Maude, Spin, LTSmin, software engineering, computer science, concurrent systems, mutual exclusion protocols
