MuDiv is applicable to satisfaction problems of the form:
(t1 | t2 | t3) ^ L |= A
Meaning "transition system t1 in parallel with t2 and t3, restricted to the actions in L, satisfies the assertion A. The restriction defines the external communication which the transition systems may perform, and the assertion describes the requirements to the system as a sequence of modal equations.
MuDiv can be asked to solve two different kinds of problems. It can prove whether or not the assertion holds or it can calculate the requirements A' for an unknown transition system x like this:
(x | t1 | t2) ^ L |= A <=> x |= A'
As an example, the three transition systems could be a sender, a receiver and a medium, modelling a communication protocol. The sender and the receiver are assumed known, but the medium is still undefined. MuDiv may then be asked to move the sender and receiver systems into the requirements, leaving the exact, necessary and sufficient requirements for the medium. If the sender and receiver are already inconsistent with respect to the requirement A, the result would be the assertion `false.' The name partial model checking is chosen to reflect that MuDiv transfers the transition systems, one by one, into the specifications, thereby building a new specification. So each of these intermediate specifications provides a partial answer to the original problem. Crucial to the success of applying partial model checking is a series of efficient implementable simplification strategies for modal equations. They vary in complexity from simple propagation of constant equations to symbolically determining equivalence of equations.
The implementation of MuDiv is performed in standard C++, and the result is a non-interactive batch program, where the input is provided as one or more input files, describing the model and the requirements. The output is the result of the model check and is presented on the standard output or written to a file.
Some tests with MuDiv, using Milner's Scheduler and a centralized token passing scheme as examples, have shown promising results. Instead of an exponential explosion of the state space, the running time grows as a fourth degree polynomial of the input size, unfortunately, another example illustrating the problem of the dining philosophers shows a clear exponential running time.