SMLogic is the temporal-logic companion library for cubical-sm.

Where cubical-sm provides machines, homomorphisms, simulations, and nested abstractions, SMLogic provides the language for stating temporal properties about them.

Semantic Core

The central object is TemporalModel: a Kripke-style transition system with:

• a state set;
• an atom set;
• a step relation;
• an atom valuation;
• an initial-state predicate.

The formula layers separate CTL*, LTL, and CTL. CTL* is the semantic core; LTL and CTL are convenient fragments. The semantics are proof-oriented and live in hProp. Existential temporal claims use propositional truncation, which is appropriate when formulas are specifications rather than executable model-checker programs.

Growing Compatibility Surface

The library extends beyond the first proof-only layer:

• finite and decidable temporal models;
• finite paths, cycles, lassos, and periodic paths;
• positive untruncated evidence for supported constructive fragments;
• reachability evidence and replay records;
• labelled transition systems preserving inputs, outputs, or pairs as actions;
• fairness-restricted CTL, LTL, and CTL* semantics;
• TLA-style action predicates and weak/strong fairness;
• an abstract checker-capability layer;
• a NuSMV-specific trusted-result boundary with property manifests, generated job formats, and accepted verdict records.

This does not make Agda a full model checker. It creates a disciplined boundary where external checker runs can be represented as trusted artifacts and connected to Agda-side claims.

How It Fits

SMLogic is the temporal-claim layer for the state-machine stack. It supplies the language for CTL, LTL, CTL*, fairness, evidence, and trusted checker boundaries without claiming to be a full Agda model checker.

cubical-sm can describe how a machine runs. SMLogic asks what should always, eventually, or possibly be true about those runs.

That distinction matters for product work. A state-machine diagram can show transitions. A temporal claim can say that every request is eventually resolved, that an unsafe state is unreachable, that a circuit eventually recovers, or that a service controller never violates a guard.

The checker boundary is deliberate. External model checkers can search finite systems, but their results are represented as trusted artifacts rather than silently becoming Agda proofs. Finite paths, lassos, replay records, fairness, labelled systems, and NuSMV manifests all support that disciplined integration.

The staged story is:

visual machine -> canonical nested model -> temporal model -> checked claim or trusted checker result