a \models \varphi

satisfaction

Sat printed a ⊨ φ; with parameters, MSat a ⊨[ρ] φ, CSat a ⊨ᶜ[rules | atoms | ρ] φ, TSat a ⊨ₜ[trs | ρ] φ, PSat a ⊨ₚ[trs | ρ | σ] φ

from source, bridged, new

\langle L, \lambda \rangle \varphi, [L, \lambda] \varphi

located modalities: some, respectively every, transition with label L at location \lambda leads to \varphi

Form.dia, MForm.dia printed ⟨L, loc⟩ φ; MForm.box printed [L, loc]ₘ φ

bridged

\Diamond \varphi, \Box \varphi

some reaction, respectively every reaction, leads to \varphi

◇ φ, □ φ (CForm, MForm.rdia, MForm.rbox, PForm)

from source, bridged, new

\Diamond_t \varphi, \Box_t \varphi

the same for reactions tagged t; with a superscript w, up to silent steps

◇[t] φ, □[t] φ; weak ◇ʷ[t] φ, □ʷ[t] φ (TForm, PForm)

bridged, new

\mu.\varphi, \nu.\varphi

least and greatest fixpoints (de Bruijn: no bound variable is named)

μ. φ, ν. φ (MForm, CForm, TForm, PForm)

from source, bridged, new

a \equiv_{\mathcal{L}} b

logical equivalence: the same formulas hold of a and b

LEquiv, printed a ≡ₗ b

bridged

a \sim b, a \approx b

strong and weak bisimilarity of closed systems over rule tags, each side with its own rule set; not the library's bisimilarity \sim of the previous table, and not a congruence (C3.c3_tagged)

TBisim printed a ∼[trs₁ | trs₂] b; WBisim printed a ≈[trs₁ | trs₂] b

from source

a \sim_t b, a \sim_r b, a \sim_\ell b

in the section Congruence: strong bisimilarity over rule tags, the same with tags forgotten, and the largest bisimulation of a labelled reaction family

TBisim with one rule list, printed a ∼[trs | trs] b; Congr.LBisim

from source, bridged

a \sim_{\mathrm{sat}} b, Q^c

saturated bisimilarity; the closure of a relation Q under all contexts composable with both sides

Congr.SatBisim, Congr.CtxCl

bridged

a \equiv_{\mathcal{R}} b, (\mathcal{R}_1, a) \equiv (\mathcal{R}_2, b), \equiv^{\forall}

logical equivalence for the tracked logic: closed formulas, one rule list; closed formulas, two rule lists; all formulas at all valuations

LEq printed a ≡ₚ[trs] b; LEq2; Congr.PEquiv

bridged

C \triangleright \varphi, \equiv_{\mathrm{top}}, \equiv_{\triangleright}

the context modality (a satisfies it when a translate of C composed with a satisfies \varphi), and logical equivalence with it at top level and anywhere

Congr.ASat, Congr.SSat; Congr.AEquiv, Congr.SEquiv

unbridged

a \xrightarrow{t} a', \mathcal{R}^{-}

tagged reaction, and the rule list with its tags dropped

TReact

new

a \approx_e b

weak bisimilarity relative to an environment (Larsen)

RelWBisim, printed a ≈ₑ[E, e | trs₁ | trs₂] b

unbridged

a \approx_\Pi b

public weak tracked bisimilarity

PubWBisim, printed a ≈ᴾ[Pb, N, n | trs₁ | trs₂] b

new

c \simeq c'

the channels Ch, Ch' (started from c, c') are equivalent for the sender–replier pair: the rule lists that compose produces for SR with Ch and with Ch', ports hidden, are weakly bisimilar (alternating bit protocol, stage 2); this composition is on rule lists, not the library's parallel product

ABPStage2.SREq, printed c ≃ₛᵣ[Ch | Ch'] c'

new