Commit 2156f1be authored by Theo von Arx's avatar Theo von Arx

Add Computation Tree Logic (CTL)

parent 72ad4b11
......@@ -265,3 +265,4 @@
......@@ -177,7 +177,34 @@ We define the following characteristic functions for two automatas $A$ and $B$ w
\subsection{Computation Tree Logic (CTL)}
Sei $\phi$ eine Eigenschaft eines Systems. Dann definieren wir:
\text{E}\phi :\quad& \text{There exists at least one path from the current}\\
& \text{state where $\phi$ holds.}\\
\text{X}\phi :\quad &\text{$\phi$ has to hold at the next state.}\\
\text{G}\phi :\quad & \text{$\phi$ has to hold on the entire subsequent path.}\\
\phi_1 \text{U}\phi_2 :\quad & \text{$\phi_1$ has to hold at least until at some state $\phi_2$ holds.}
There are more quantifiers, but they can be replaced by the above ones:
\text{F} \phi :\quad & \text{$\phi$ eventually has to hold (somewhere on the subsequent path).}\\
\text{A} \phi :\quad & \text{$\phi$ has to hold on all paths starting from the current state.}
Zustand ist schwarz $\equiv$ Eigenschaft $p$ ist erfüllt.\\
Zustand ist rot $\equiv$ Eigenschaft $q$ ist erfüllt.\\
Im Gegensatz zu hierarchischen State Maschinen (State Charts), Zustandsübergange in einem Petri-Netz sind asynchron. Die Reihenfolge der Übergänge ist zum Teil unkoordiniert. Sie ist gegeben durch eine Teilreihenfolge. \\
Petri-Netze können deshalb dafür benutzt werden verteilte gleichzeitige Prozesse zu modellieren.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment