Theory Labelled_Transition_Systems
theory Labelled_Transition_Systems
imports
"HOL-Library.Countable_Set"
begin
notation Set.empty (‹∅›)
notation (input)
HOL.eq (infixr "⟺" 25)
section ‹Labelled Transition Systems›
text ‹\label{sec:LTS}›
text ‹A Labelled Transition System (LTS) consists of a set of processes (or states) $\Proc$, a set of actions $\Act$, and a relation of transitions $\cdot\xrightarrow{\cdot}\cdot \subseteq \Proc\times\Act\times\Proc$ which directedly connect two processes by an action (the action being the label of the transition) @{cite reactivesystems}. We call a transition labelled by an action $\alpha$ an \emph{$\alpha$-transition}.
LTSs can model reactive systems, as discussed in \cref{chap:introduction}. A process of an LTS, then, corresponds to a momentary state of a reactive system. The outgoing transitions of each process correspond to the actions the reactive system could perform in that state (yielding a subsequent process/state), if facilitated by the environment. The choice between the facilitated transitions of a process is non-deterministic.
This facilitation can be thought of as a set of actions that the environment allows in a given moment, or, more intuitively, as a set of simultaneous inputs from the environment to which the system may react. We call the actions not allowed by the environment in a given moment \emph{blocked}.
The environment can also observe which transitions a system performs and react by changing the set of allowed actions in response.
In classical treatments of LTSs, the actions that the environment allows, blocks, or reacts to, are often considered only implicitly. The reason we put this emphasis on the environment here will become apparent in \cref{sec:LTSt}.
\example{%
The process $p$ can perform any of the $a$-transitions in environments allowing $a$ and the $b$-transition in environments allowing $b$. All derivative (subsequent) states cannot perform any transition.
\lts{
\node[state] (p0) {$p$};
\node[state] (p1) [below left of=p0] {$p_1$};
\node[state] (p2) [below of=p0] {$p_2$};
\node[state] (p3) [below right of=p0] {$p_3$};
\path (p0) edge node[above left] {$a$} (p1)
edge node[above right] {$a$} (p2)
edge node[above right] {$b$} (p3);
}}
A \emph{hidden action}, denoted by $\tau$, allows for additional semantics: a $\tau$-transition can be performed by a process without any interaction from the environment. Depending on the specific semantic context, the performance of a hidden action may also be unobservable (hence the name), i.e.\@ not part of the observable behaviour of the system.›
subsubsection ‹Some Definitions›
text ‹The $\alpha$-derivatives of a state are those states that can be reached with one $\alpha$-transition:
$$\mathit{Der}(p, \alpha) = \{ p' \mid p \xrightarrow{\alpha} p' \}.$$
An LTS is image-finite iff all derivative sets are finite, i.e.:
$$\forall p \in \Proc, \alpha \in \Act .\; \mathit{Der}(p, \alpha) \text{ is finite}.$$
Similarly, we can say that an LTS is image-countable iff all derivative sets are countable, i.e.:
$$\forall p \in \Proc, \alpha \in \Act .\; \mathit{Der}(p, \alpha) \text{ is countable}.$$›
subsubsection ‹Note on Metavariable usage›
text ‹States of an LTS range over $p, q, p', q', \dots$, where $p$ and $p'$ are used for states connected by some transition (i.e.\@ $p \xrightarrow{\alpha} p'$), whereas $p$ and $q$ are used for states possibly related by some equivalence (e.g.\@ $p \leftrightarrow q$), as will be discussed in the next section.
An arbitrary action of an LTS will be referenced by $\alpha$, whereas an arbitrary \emph{visible} (i.e.\@ non-hidden) action will be referenced by $a$.›
subsubsection ‹Practical Example›
text ‹Let us take a detour away from purely theoretical deliberations and consider a real-world machine that may be modelled as an LTS. We can imagine a very simple snack-selling vending machine that accepts only one type of coin and has individual buttons for each of the snacks. When a coin is inserted and a button pressed, the machine dispenses the desired snack and is then ready to accept coins once again. Because the dispensing of the snack itself requires no interaction from the user, we model it as a $\tau$-transition.
\lts{
\node[state] (p0) {$p$};
\node[state] (p1) [below of=p0] {$p_1$};
\node[state] (p2) [below left of=p1,xshift=-10pt] {$p_2$};
\node[state] (p3) [below of=p1] {$p_3$};
\node[state] (p4) [below right of=p1,xshift=10pt] {$p_4$};
\path (p0) edge node[right] {coin} (p1)
(p1) edge node[above left] {choc} (p2)
edge node[right] {nuts} (p3)
edge node[above right] {crisps} (p4);
\draw (p2) to[out=150, in=210, looseness=1, edge node={node [left] {$\tau$}}] (p0);
\draw (p4) to[out=30, in=-30, looseness=1, edge node={node [right] {$\tau$}}] (p0);
\draw (p3) to[out=-20, in=0, looseness=2.5, edge node={node [right] {$\tau$}}] (p0);
}
\vspace{-1.5cm}›
subsection ‹Isabelle›
text ‹The sets of states and actions are formalised by type variables ‹'s› and ‹'a›, respectively. A specific LTS on these sets is then determined entirely by its set of transitions, denoted by the predicate ‹tran›. We associate it with a more readable notation (‹p ⟼α p'› for $p \xrightarrow{\alpha} p'$).›
locale lts =
fixes tran :: ‹'s ⇒ 'a ⇒ 's ⇒ bool›
("_ ⟼_ _" [70, 70, 70] 80)
begin
text ‹The other definitions can be formalised in a straightforward manner.›
abbreviation derivatives :: ‹'s ⇒ 'a ⇒ 's set›
(‹Der'(_, _')› [50, 50] 1000)
where ‹Der(p, α) ≡ {p'. p ⟼α p'}›
definition image_finite :: ‹bool›
where ‹image_finite ≡ (∀ p α. finite Der(p, α))›
definition image_countable :: ‹bool›
where ‹image_countable ≡ (∀ p α. countable Der(p, α))›
text ‹These two properties concern the entire LTS at hand (given by the locale context) and will be useful when we want to state propositions that only hold for LTSs that satisfy these properties.›
end
text ‹We formalise LTSs with hidden actions as an extension of ordinary LTSs with a fixed action ‹τ›.›
locale lts_tau = lts tran
for tran :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› +
fixes τ :: ‹'a›
end