Guarded Usage of Memory in the
Model-checking of
Incomplete Systems

Model-checking is a cornerstone of formal verification: a real system is first encoded as a formal model, then checked against a specification. The expressiveness of the model class must be rich enough to capture critical properties, yet simple enough to keep analysis tractable.

Many extensions — timed constraints, stochastic behaviour, partial observability, parameters, non-determinism — increase the complexity of analysis, often pushing it into undecidability. Classical responses restrict model parameters (number of clocks, dimensions…), but difficulties can equally stem from unrealistic baseline assumptions. Timed automata, for instance, can execute infinitely many actions in finite time, yielding theoretically correct but practically meaningless results.

GUMMIS takes a different angle: instead of restricting the model structure alone, it introduces finite-memory hypotheses that reflect actual system limitations. The goal is to find the right balance between modelling power and analytical tractability by grounding the formalism in realistic resource constraints.