Notation
Basics
| iff | “if and only if” |
| \smash{|{A}|} | Number of elements of A |
| \mathrm{id}_{A} | Identity relation on A |
| 2^{A} | Power set of A |
| A^*, A^{\omega}, A^{\infty} | Language of finite / infinite / finite-or-infinite words over alphabet A |
| \mathcal{R}^{-1} | Inverse relation of \mathcal{R} |
| \operatorname{\mathrm{dom}}(f) | Domain of where function f is defined, \bot counts as undefined (first appearing in Definition 4.1) |
| \mathbb{N}, \mathbb{N}_\infty | Natural numbers / natural numbers extended by \infty as top element |
| \mathrel{≔} | Definitional equality; in the context of CCS, \mathsf{X} \mathrel{≔}P also means \mathcal V(\mathsf{X}) \mathrel{≔}P (Definition 2.3); in the context of algorithms, denotes variable assignment |
Orders and Vectors
| \leq | less‑than‑or‑equal‑to, usually pointwise on vectors |
| \operatorname{\mathrm{Min}}(A), \operatorname{\mathrm{Max}}(A) | Set of minimal / maximal elements in A in the context of a preorder \leq |
| \sqcup / \sup, \sqcap / \inf | Least upper bound / greatest lower bound in the context of a lattice (Definition 3.4) |
| {}\uparrow A, {}\downarrow A | Upward-closure / downward-closure of set A in the context of a preorder \leq (Definition 3.4) |
| \hat{\mathbf{e}}_{k} | Unit vector; component k is 1, all others 0 (in the context of some dimensionality d) |
| \mathbf{0} | Vector of zeros (in the context of some dimensionality d); not to be confused with \mathbf{0} as terminated \textsf{CCS} process in Definition 2.2 |
Transition Systems
| \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}} | Transition relation (in context of a transition system, Definition 2.1), usually due to operational CCS semantics (Definition 2.3); can also connect sets of states |
| \overset{\smash{\raisebox{-2pt}{$\scriptstyle{\alpha}$}}}{\nrightarrow} | Absence of an \alpha-transition |
| \mathrel{\twoheadrightarrow} | Internal transition (Definition 6.1) |
| \xrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{(\alpha)}$}}} | Soft transition (Definition 6.1) |
| \xtwoheadrightarrow{\smash{\raisebox{-2pt}{$\scriptstyle{\vec{w}}$}}} | Weak \vec{w}-word step sequence (Definition 6.1) |
| \operatorname{Der}(p, \alpha) | \alpha-derivatives of p (Definition 2.1) |
| \operatorname{Ini}(p) | Enabled actions of p (Definition 2.1) |
| \langle \alpha \rangle | Modality of observing an \alpha-step (Definition 2.11) |
| ( \alpha ) | Modality of observing a \tau-soft \alpha-step (Definition 6.1 and 6.5) |
| \langle \varepsilon \rangle | Modality of allowing internal behavior (Definition 6.1 and 6.5) |
| \llbracket \varphi \rrbracket | Set of states that fulfill \varphi (Definition 2.12) |
| {\mathcal{S} \! / \!\! \sim} | Quotient system on equivalence classes [\cdot]_{\sim} (Definition 2.10) |
Behavioral Equivalences
| \preceq_{N}, \sim_{N} | Behavioral preorder / equivalence with respect to notion N (full names in Figure 3.8 and 6.5) |
| \sim_\mathrm{T}, \sim_\mathrm{S}, \sim_\mathrm{B} | Strong trace equivalence, similarity, bisimilarity (Definition 2.5 and 2.7) |
| \preceq_{\mathcal{O}^{}_{}}, \sim_{\mathcal{O}^{}_{}} | Behavioral preorder / equivalence derived from a sublogic \mathcal{O}^{}_{}\subseteq \mathsf{HML} (Definition 2.13) |
| \mathcal{O}^{}_{N} | Observation logic for a notion N \in \mathbf{N} in the context of a spectrum (Definition 3.5) |
| \mathcal{O}^{}_{\mathrm{\lfloor B \rfloor}} | Bisimulation observation logic (Definition 2.16) |
| \mathsf{expr}^{}(\varphi) | Syntactic expressiveness price of \varphi in the context of a spectrum (Definition 3.6) |
| “\varphi distinguishes” | Formula \varphi is true for state on left-hand side and not true for state(s) on right-hand side (Definition 2.13 and 7.3) |
Games
| \mathrel{\smash{›\!\!\frac{\scriptstyle{\;\enspace\;}}{}\!\!›}} | Game move (Definition 2.17) |
| \mathrel{\smash{›\!\!\frac{\scriptstyle{\;u\;}}{}\!\!›}} | Game move, labeled by an energy update (Definition 4.1) |
| \mathcal{G}_{\mathrm{B}} | Bisimulation game in the context of a transition system (Definition 2.22) |
| \mathcal{G}_{\mathrm{B}}^{\smash{🗲 }} | Bisimulation energy game (Definition 4.8) |
| \mathsf{Win}_\mathrm{a}, \mathsf{Win}_\mathrm{d} | Attacker / defender winning regions in the context of a reachability game (Definition 2.20), or winning budgets in an energy game (Definition 4.3) |
| \mathsf{Win}^{\mathrm{min}}_\mathrm{a}(g) | Minimal attacker winning budgets for position g in an energy game (Definition 4.3), solution to Problem 4.1 |
| \mathit{upd}, \smash{\mathit{upd}^{↺}} | Updates on energy games (Definition 4.1) and their undo-function in the algorithm for Galois energy games (Algorithm 4.1) |
| \mathbf{En} | Energy levels on declining energy games in the context of a dimensionality d (Definition 4.5) |
| \mathsf{upd}, \smash{\mathsf{upd}^{↺}} | Updates on declining energy games (Definition 4.5) and their undo-version (Definition 4.12) |
| \mathtt{min}_{A} | A special kind of update component in declining energy games (Definition 4.5) |
Spectroscopy
| \mathbf{N}_{p,q} | Notions from \mathbf{N} in the context of a spectrum preordering states p and q (solution to Problem 3.1) |
| \mathcal{G}_{\triangle} | Strong spectroscopy game, in the context of a transition system (Definition 5.1) |
| \mathcal{G}_{\blacktriangle} | Clever spectroscopy game (Definition 5.4) |
| \mathcal{G}_{\triangle N}, \mathcal{G}_{\blacktriangle N} | Equivalence game for N, derived from a spectroscopy game (Definition 5.5) |
| \mathcal{G}_{\nabla} | Weak spectroscopy game, in the context of a transition system with silent steps (Definition 7.1) |
| \mathcal{G}_{\widehat{\nabla}} | Simplified weak spectroscopy game (Figure 7.3) |
| \mathsf{Strat}_\mathrm{B}, \mathsf{Strat}_{\triangle}, \mathsf{Strat}_{\nabla} | Strategy formulas in the context of polynomial / strong / weak spectroscopy (Definition 4.9, 5.2, 7.2) |
Complexity
| \mathit{O}(f) | Set of functions that grow to infinity at most as quickly as function f |
| \textsf{P}, \textsf{NP}, \textsf{PSPACE} | Complexity classes of deterministic polynomial time / nondeterministic polynomial time / polynomial space complexity |
Recurring Examples
| \mathsf{P}, \mathsf{Q} | Two systems of philosophers, differing in their determinism (Example 2.1, 2.2, 2.3) |
| \mathsf{T} | Trolled philosophers with additional \includegraphics[height=1em, alt=q3]{img/trollface.png}-deadlock (Example 2.7) |
| \mathsf{Pe}, \mathsf{Mx} | Implementation of Peterson’s mutual exclusion protocol and its specification (Example 1.1), styled Pe and Mx for their expression in the tool (Application to Peterson’s Mutual Exclusion Protocol) |