# Formal Models TL;DR ## Automata 5-Tuple automaton spec = {`S`tates, `I`nitial, `∑`alphabet, `F`accept, `T`ransitions} ### Properties #### Deterministic - At most one path per symbol #### Complete - At least one path per symbol ### Automata Types #### Power automaton - Advantage: always deterministic & complete; same alphabet - Disadvantage: exponential state space - TODO: table of original; then make new table of all reachable states, including ∅ if original was incomplete #### Oracle automaton - Advantage: linear state space; deterministic (if original has only 1 initial state) - Disadvantage: can become incomplete; has a different & bigger alphabet; needs external oracle for choices - TODO: just add the targets state to the transition name #### Optimized oracle automaton - Advantage: linear state space; deterministic & complete (if original has only 1 initial state); smaller alphabet than unoptimized - Disadvantage: still different alphabet; needs external oracle for choices - TODO: minimize oracle alphabet by mapping transition targets to the smallest possible set of numeric indices; n has to be minimal on a per-state and per-alphabet-symbol level #### Complement automaton - If deterministic & complete - Just flip the final states - Else if deterministic & incomplete - make complete via a sink ∅ - then just flip the final states - Else (assert nondeterministic) - Make power automaton - Then just flip the final states #### Product automaton - TODO: make a merger of both, walking through all transitions simultaneously - A transition can only be taken if both have the transition - The product accepts only if both originals accept - Uses the synchronous parallel composition - NTS: takes a lot of time and thinking; do last in exam --- ## Machines (Moore & Mealy) #### Moore machine - Output bound to state (NTS: while stuck in a moor) - Convert to Mealy: - Make it deterministic and complete if necessary (power automaton) - Move the output (accept/reject) to all outgoing transitions (NTS: last step) - If a state accepts, all outgoing transitions have /1 - If a state rejects, all outgoing transitions have /0 #### Mealy machine - Output bound to transition (NTS: while eating a meal) - Convert to Moore: - Determinism and completeness do not matter - The incoming accept/reject value is put into the states - This can require an extra state ## Subset checking ```math L(A_1) \subseteq L(A_2) \iff L(A_1) \cap \overline{L(A_2)} = \varnothing ``` In words: A1 is a subset of A2 exactly when no word is accepted by A1 and rejected by A2. 1. Build the complete deterministic power automaton P(A2). 2. Complement it to obtain C(P(A2)). 3. Build the product automaton A1 × C(P(A2)). - **No accepting state is reachable:** L(A1) ⊆ L(A2). - **An accepting state is reachable:** L(A1) ⊈ L(A2); the path to it gives a counterexample. --- ## Condition Event Nets (CEN) 4-Tuple CEN spec = {`C`onditions, `I`nitial, `E`vents, `G`raph} #### Markings A CEN with |C| conditions has 2^|C| possible markings. - Each event consumes exactly 1 token - Each node can hold exactly 1 token ### Conditions - **Precondition G^-1 of e**: What needs to hold to make a transition possible (incoming arrows). - **Postcondition G of e**: What holds after a transition happened (outgoing arrows). --- ## Place Transition Net (PTN) 5-Tuple PTN spec = {`P`laces, `T`ransitions, `F`low relation, edge `W`eight mapping, Initial `M`arkings} #### PTN vs. CEN - Can have multiple tokens per place - The limit is the number next to the places - If a transition would exceed the limit, it is blocked - The default is ∞ - Can consume and produce multiple tokens per event - The number is shown next to the edges - The default is 1 --- #### Labeled Transition System (LTS) Just a graph of nodes (=states) whose directed edges (=state transitions) have labels (=actions/events) that trigger them. --- ## Process Algebra (PA) ### Terminology | Syntax | Name | Meaning | | ------------- | ---------- | ------------------------------------------------------------------ | | `a`, `b`, `c` | action | A step that can be performed. | | `P`, `Q`, `R` | process | A behavior that may perform actions. | | `a.P` | prefix | Perform `a`, then continue as `P`. | | `P + Q` | choice | Choose either `P` or `Q`, then discard the other. | | `P || Q` | parallel | Do `P` and `Q` simultaneously; if one is not affected, it is kept. | | `Σ(P)` | alphabet | Set of all actions that can occur in `P`. | | `P -a-> Q` | transition | `P` can perform `a` and become `Q`. | #### Prefix ```math a.Q \xrightarrow{a} Q ``` #### Choice Choose to perform the action on one side; the other side can then be discarded. ```math \begin{aligned} a.P + b.Q &\xrightarrow{a} P \\ a.P + b.Q &\xrightarrow{b} Q \end{aligned} ``` #### Parallel For this example: ```math P_0 = a.b.P,\quad Q_0 = b.c.C ``` 1. compute the synchronization set: ```math \Theta = \Sigma(P_0) \cap \Sigma(Q_0) = \{a,b\} \cap \{b,c\} = \{b\} ``` 2. decide which rule applies. - Interleaving / Asynchronous If the action is not in `\Theta`, only one side performs the action. The other side stays unchanged. ```math \begin{aligned} a.b.P \parallel b.c.C &\xrightarrow{a} b.P \parallel b.c.C \qquad (a \notin \Theta) \\ P \parallel c.C &\xrightarrow{c} P \parallel C \qquad (c \notin \Theta) \end{aligned} ``` - Rendez-vous / Synchronization If the action is in `\Theta`, both sides must perform the action simultaneously. ```math b.P \parallel b.c.C \xrightarrow{b} P \parallel c.C \qquad (b \in \Theta) ``` ### Composition #### Alphabet Just a set of all action symbols of the given process. ```math \begin{aligned} P &= a.b.b.P & \Sigma(P) &= \{a,b\} \\ Q &= a.R \parallel c.Q & \Sigma(Q) &= \{a,c\} \\ S &= a.P + c.R & \Sigma(S) &= \{a,b,c\} \\ \Sigma(P+Q) &= \Sigma(P\parallel Q) = \Sigma(P)\cup\Sigma(Q) = \{a,b\}\cup\{a,c\} = \{a,b,c\} \end{aligned} ``` #### Synchronization set Forces all actions in it to happen in lockstep. If `P` and `Q` share `a`, this makes it a rendezvous point, meaning `a` can never happen in only one process. All other actions, such as `b` and `c`, can interleave freely. ```math \Theta_{pq} = \Sigma(P)\cap\Sigma(Q) = \{a,b\}\cap\{a,c\} = \{a\} ``` ### Specifications #### Satisfiable - For every allowed input, there exists at least one valid output. - NTS: At least one solution exists. #### Underspecification - Multiple outputs are possible for the same input. - NTS: Too many solutions. --- ## CTL Operators ### Operators #### Combined operators | Formula | Meaning | NTS | | ---------- | ---------------------------------------------------- | -------------------------- | | `EX φ` | There exists a successor with `φ` | one step reachable | | `AX φ` | All successors have `φ` | all next states | | `EF φ` | There exists a path where `φ` eventually occurs | can reach `φ` | | `AF φ` | On every path `φ` eventually occurs | all must reach `φ` | | `EG φ` | There exists a path where `φ` holds forever | find a `φ`-only cycle | | `AG φ` | On every path `φ` holds forever | `φ` is never violated | | `E(φ U ψ)` | There exists a path where `φ` holds until `ψ` occurs | stay in `φ` until `ψ` | | `A(φ U ψ)` | On every path `φ` holds until `ψ` occurs | must stay in `φ` until `ψ` | #### Operator symbols | Symbol | Meaning | | ------ | ------------------- | | `E` | there exists a path | | `A` | all paths | | `X` | next state | | `F` | eventually / future | | `G` | always / globally | | `U` | until | ### Equivalences | Formula | Equivalent | | ------- | ---------- | | `AG φ` | `¬EF(¬φ)` | | `AF φ` | `¬EG(¬φ)` | | `EG φ` | `¬AF(¬φ)` | | `EF φ` | `¬AG(¬φ)` | --- ## TLA+ TLA+ describes a state machine with logic: variables are the state, actions are the transitions. ### Syntax | Syntax | Meaning | | ------------- | --------------------------------------------- | | `/\`, `\/` | and, or | | `x` | value in the current state (eg. precondition) | | `x'` | value in the next state (eg. postcondition) | | `UNCHANGED x` | shorthand for `x' = x` | | `Init` | allowed initial states | | `Next` | disjunction of all actions | ### Structure ```haskell ---- MODULE Vending ---- EXTENDS Naturals VARIABLES coins, brewing vars == <> Init == /\ coins = 0 /\ brewing = FALSE InsertCoin == /\ coins = 0 /\ coins' = 1 /\ UNCHANGED brewing Next == \/ InsertCoin Spec == Init /\ [][Next]_vars ``` ### Model checking #### Invariants and reachability ```haskell TypeOK == coins \in 0..1 /\ brewing \in BOOLEAN BrewingNotReachable == brewing = FALSE ``` - **Invariant:** - Must hold in every reachable state. - **Reachability:** - Negate the target and check it as an invariant. A violation gives the path to the target. - **Counterexample:** - Read the error top-to-bottom - Each step shows the action and changed variables. - **Deadlock:** - The system is stuck because no actions in `Next` are enabled in this state. #### Refinement ```c Abstract == INSTANCE Vending THEOREM Spec1 => Abstract!Spec ``` - A refinement adds detail but must preserve the abstract behavior. - Check `Spec1` and add `Abstract!Spec` under Properties; `THEOREM` alone is not run by TLC. - Use `INSTANCE ... WITH x <- expression` when the refined representation differs. - Time is explicit: use a bounded counter in a wait action. More counter values mean more states. ### Operators | Syntax | Meaning | Classifies | | -------- | ---------------------------- | ---------- | | `[]P` | always `P` | safety | | `<>P` | eventually `P` | liveness | | `P ~> Q` | whenever `P`, eventually `Q` | leads-to | ### Definitions - **Stuttering:** An enabled action may be ignored forever. - **Fairness:** May be required to prove liveness when the model contains non-deterministic transitions that allow the system to stall or stutter forever. - **Liveness:** Is the guarantee that progress eventually happens. ### Fairness - **No Fairness:** - Use this when the action is optional for the liveness. - An external event that is not required to occur. - **Weak fairness:** - If an action is continuously enabled, it must eventually fire. - It is not enough when the precondition keeps becoming false and true. - **Strong fairness:** - If an action is infinitely often enabled, it must eventually fire. - Use if the action flickers between false and true.