Why rules are a good interface
A semantic rule is a compact piece of documentation: it says exactly when a system step is allowed and what the result is. The rule is local, but the semantics it defines is global: the behaviour of the whole system is the closure of all rule applications.
This locality is valuable for compositional reasoning. If you can isolate a rule that describes an interaction pattern, you can study it, adapt it, and connect it to properties. For complex systems, the difference between “a big monolithic semantics” and “many small rules” is the difference between a document that can be maintained and one that cannot.
Graph rewriting as structured state
Graph rewriting replaces “the state is a big tuple” with “the state has structure”. Nodes represent entities; edges represent relationships or allowed interactions. A rewrite rule matches a pattern and replaces it with another pattern.
The benefit is that many system properties are naturally structural. For example, “this resource is owned by at most one component” is a statement about edges. “Two components are connected via this glue” is a statement about connectivity. Structure lets you express and check such properties directly.
Diagram: rule application
How SOS and rewriting connect to verification
Rules define a transition system, and transition systems are what many verification methods consume. Model checking can operate directly on the induced transition system, while proof techniques can reason about invariants preserved by each rule.
In practice, structure helps with abstraction. If the state is structured, you can often abstract by collapsing parts of the structure while preserving the parts relevant to the property. That can be more natural than inventing a new flat state representation.
Key definitions
- SOS ruleA rule of the form “premises / conclusion” describing an allowed step.
- Rewrite ruleA pattern replacement on a structured state (often a graph).
- MatchFinding an occurrence of the rule’s left-hand pattern in the current state.
- InvariantA property preserved by each allowed step (and thus by all reachable behaviours).
- AbstractionA simplification that preserves the property you care about while shrinking behaviour space.
Common pitfalls
- Rules that hide assumptionsIf a rule applies “magically”, the environment assumptions are probably missing.
- Overly expressive stateIf everything is in the graph, analysis becomes infeasible; keep structure purposeful.
- Forgetting concurrencyMany interleavings correspond to independent rule applications; model independence explicitly if needed.
- Confusing syntax with behaviourA rewrite is a semantic step only if it has an interpretation in the model.
Internal links
- Model checking primerHow transition systems are explored.
- Research: formal methodsThemes and compositionality.
- Projects: component reasoningWhy structure and glue matter.