# More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D^{3})

#### Rohit Dureja and Kristin Yvonne Rozier

This webpage contains details and artifacts for reproducibility of the experiments in "More Scalable LTL Model Checking via Discovering Design-Space Dependencies" by R. Dureja and K.Y. Rozier.

**=> Proofs of theorems appearing in the paper can be found here <=**### Abstract

Modern system design often requires comparing several models
over a large design space. Different models arise out of a need to
weigh different design choices, to check core capabilities of versions with
varying features, or to analyze a future version against previous ones.
Model checking can compare different models; however, applying model
checking off-the-shelf may not scale due to the large size of the design
space for today’s complex systems. We exploit relationships between different
models of the same (or related) systems to optimize the model checking
search. Our algorithm, D^{3}, preprocesses the design space and
checks fewer model-checking instances, e.g., using nuXmv. It automatically
prunes the search space by reducing both the number of models
to check, and the number of LTL properties that need to be checked for
each model in order to provide the complete model-checking verdict for
every individual model-property pair. We formalize heuristics that improve
the performance of D^{3}. We demonstrate the scalability of D^{3} by
extensive experimental evaluation, e.g., by checking 1,620 real-life models
for NASA’s NextGen air traffic control system. Compared to checking
each model-property pair individually, D^{3} is up to 9.4× faster.

### Algorithm

The algorithm,
Discover Design-Space Dependencies (D^{3}), reduces both the number
of models to check, and the number of LTL properties that need to be checked
for each model. Rather than using a custom model checker, D^{3} works with any
off-the-shelf checker. We reason about a set
of system models by introducing the notion of a Combinatorial Transition System
(CTS). Each individual model, or instance, can be derived from the CTS
by configuring it with a set of parameters. Each transition in the CTS is enabled/disabled
by the parameters. We model check each instance of the CTS
against sets of properties. We assume the properties are in Linear Temporal
Logic (LTL) and are independent of the choice of parameters, though not all
properties may apply to all instances. D^{3} preprocesses the CTS to find relationships
between parameters and minimizes the number of instances that need to be
checked to produce results for the whole set. It uses LTL satisfiability checking to determine the dependencies between pairs of LTL properties, then reduces
the number of properties that are checked for each instance. D^{3}
returns results
for every model-property pair in the design space, aiming to compose these results
from a reduced series of model-checking runs compared to the classical
approach of checking every model-property pair.