Sidebar

Main

Internal

Trace:

Differences

This shows you the differences between two versions of the page.

--- alvis:ltsgraphs [2015/12/12 23:36]
marcin [LTS graphs]
+++ — (current)
@@ Line 1: / Line 1: @@
-====== LTS graphs ======
-Execution of any step is expressed as a transition between formally defined states of an Alvis model. States of a model and transitions among them are represented using a **labelled transition system** (**LTS graph** for short).
-**Definition 1.** For a pair of states $S$, $S'$ we say that $S'$ is **directly reachable** from $S$ iff there exists a step $t$ such that $S-t\to S'$.
-**Definition 2.** For a pair of states $S$, $S'$ we say that $S'$ is **reachable** from  $S$ iff there exist a sequence of states $S^1,\dots,S^{k+1}$ and a sequence of steps $t^1,\dots,t^k$ such that $S = S^1 -t^1\to S^2 -t^2\to\dots -t^k\to S{^k+1} = S'$.
-The set of all states that are reachable from the initial state $S_0$ is denoted by $\mathcal{R}(S_0)$.
-**Definition 3.** A **Labelled Transition System** is a tuple LTS = (//S//, //A//, ->, //s//_0), where:
-  * //S// is the set of **states**,
-  * //A// is the set of **actions**,
-  * -> ⊆ //S// × //A// × //S// is the **transition relation**,
-  * //s//_0 is the **initial state**.
-For an Alvis model we have:
-  * //S// = //R//(//S//_0),
-  * //A// = //T// - the set of all possible steps for a given model,
-  * //E// = {(//S//, //t//, //S//'): //S//--//t//->//S//' ∧ //S//, //S//' ∈ //R//(//S//_0)}
-  * //S//_0 is the initial state.
-===== Example =====
-{{:alvis:alvis1.png|}}
-<code>
-agent X1 {
-  loop {        -- 1
-    out p; }}   -- 2
-agent X2 {
-  loop {        -- 1
-    in q; }}    -- 2
-</code>
-{{:alvis:alvis1lts.png|}}
-**[[:alvis:manual|Go back]]**