Computation Tree Logic - Versionsgeschichte

Aka: /* Temporale Operatoren */ Leerzeichen

2020-11-29T18:27:23Z

Temporale Operatoren: Leerzeichen

← Nächstältere Version		Version vom 29. November 2020, 20:27 Uhr
Zeile 26:		Zeile 26:
	Pfad und pfad-spezifische Operatoren können miteinander kombiniert werden, sodass sich beispielsweise folgende Formeln ergeben:		Pfad und pfad-spezifische Operatoren können miteinander kombiniert werden, sodass sich beispielsweise folgende Formeln ergeben:

	* <math>EX\phi</math> –''in (mind.) einem nächsten Zustand gilt'' <math>\phi</math>		* <math>EX\phi</math> – ''in (mind.) einem nächsten Zustand gilt'' <math>\phi</math>
	* <math>EF\phi</math> – ''in (mind.) einem der folgenden Zustände gilt'' <math>\phi</math>		* <math>EF\phi</math> – ''in (mind.) einem der folgenden Zustände gilt'' <math>\phi</math>
	* <math>EG\phi</math> – ''es gibt (mind.) einen Pfad, so dass <math>\phi</math> entlang des ganzen Pfades gilt''		* <math>EG\phi</math> – ''es gibt (mind.) einen Pfad, so dass <math>\phi</math> entlang des ganzen Pfades gilt''

Hydro: form, typo

2020-08-27T09:26:54Z

form, typo

Aka: Tippfehler entfernt, Links optimiert, Kleinkram

2020-02-22T17:33:27Z

Tippfehler entfernt, Links optimiert, Kleinkram

Raynswor: Artikel umgeschrieben; Hinweis auf Real Time Logic entfernt, da keine Informationen darüber auffindbar sind; neue ISBN eingefügt; Informationen ohne Anwendungen und Quellen (Vergangenheitsoperationen) entfernt.

2020-01-30T21:42:13Z

Artikel umgeschrieben; Hinweis auf Real Time Logic entfernt, da keine Informationen darüber auffindbar sind; neue ISBN eingefügt; Informationen ohne Anwendungen und Quellen (Vergangenheitsoperationen) entfernt.

Änderungen zeigen

Vorwald: /* Atomare Aussagen */ Zeichensetzung

2018-09-03T07:27:29Z

Atomare Aussagen: Zeichensetzung

← Nächstältere Version		Version vom 3. September 2018, 09:27 Uhr
Zeile 10:		Zeile 10:
	''(siehe auch den Abschnitt "Umgangssprachliche Einleitung" im Artikel [[Aussagenlogik#Umgangssprachliche Einleitung\|Aussagenlogik]])''		''(siehe auch den Abschnitt "Umgangssprachliche Einleitung" im Artikel [[Aussagenlogik#Umgangssprachliche Einleitung\|Aussagenlogik]])''

	Ausgangspunkt sind Eigenschaften von Zuständen. Ist ''AP'' eine Menge von atomaren Aussagen (Behauptungen), so ist jedes Element ''p'' von ''AP'' eine Zustandsformel. Jedes ''p'' von ''AP'' ist eine Abbildung von der Zustandsmenge in die Menge der [[Wahrheitswert\|Wahrheitswerte]] {''W''ahr, ''F''alsch}. Man sagt ein Zustand ''s'' erfüllt ein ''p'' aus ''AP'' genau dann, wenn <math>p(s)=W</math>.		Ausgangspunkt sind Eigenschaften von Zuständen. Ist ''AP'' eine Menge von atomaren Aussagen (Behauptungen), so ist jedes Element ''p'' von ''AP'' eine Zustandsformel. Jedes ''p'' von ''AP'' ist eine Abbildung von der Zustandsmenge in die Menge der [[Wahrheitswert\|Wahrheitswerte]] {''W''ahr, ''F''alsch}. Man sagt, ein Zustand ''s'' erfüllt ein ''p'' aus ''AP'' genau dann, wenn <math>p(s)=W</math>.

	=== Boolesche Operatoren ===		=== Boolesche Operatoren ===

DerSpezialist: /* Temporaloperatoren */ Typographie, Mathe

2018-04-16T13:56:04Z

Temporaloperatoren: Typographie, Mathe

Aka: Abkürzung korrigiert

2018-01-31T18:23:11Z

Abkürzung korrigiert

← Nächstältere Version		Version vom 31. Januar 2018, 20:23 Uhr
Zeile 46:		Zeile 46:
	# <math>\phi R \psi</math> : = <math>\exist i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a \leq i \} \quad \forall k \in \{a:a \in \N \land i < a \}: \psi</math> erfüllt <math>x_j \land \phi</math> erfüllt <math>x_k</math>		# <math>\phi R \psi</math> : = <math>\exist i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a \leq i \} \quad \forall k \in \{a:a \in \N \land i < a \}: \psi</math> erfüllt <math>x_j \land \phi</math> erfüllt <math>x_k</math>

	Für '''F''', '''G''' und '''U''' gilt die Prämisse "Zukunft schließt Gegenwart mit ein", d.h. wird eine Formel in einem der folgenden Zustände erfüllt, so gilt das auch für den Startzustand.		Für '''F''', '''G''' und '''U''' gilt die Prämisse "Zukunft schließt Gegenwart mit ein", d. h. wird eine Formel in einem der folgenden Zustände erfüllt, so gilt das auch für den Startzustand.
	Die bis hier definierten Formeln bilden die sogenannten Pfadformeln und die schon oben erwähnte ''Linear Time Temporal Logic''.		Die bis hier definierten Formeln bilden die sogenannten Pfadformeln und die schon oben erwähnte ''Linear Time Temporal Logic''.

194.96.98.250: /* Temporaloperatoren */

2018-01-21T10:19:33Z

Temporaloperatoren

← Nächstältere Version		Version vom 21. Januar 2018, 12:19 Uhr
Zeile 36:		Zeile 36:
	# alle Zustände <math>\phi</math> erfüllen ('''G''' <math>\phi</math>),		# alle Zustände <math>\phi</math> erfüllen ('''G''' <math>\phi</math>),
	# <math>\phi</math> gilt, bis ein Folgezustand erreicht wird, an dem <math>\psi</math> erfüllt ist (<math>\phi</math> '''U''' <math>\psi</math>),		# <math>\phi</math> gilt, bis ein Folgezustand erreicht wird, an dem <math>\psi</math> erfüllt ist (<math>\phi</math> '''U''' <math>\psi</math>),
	# <math>\~~psi~~</math> gilt bis (einschließlich) zu dem Zustand, an dem <math>\~~phi~~</math> erfüllt ist (<math>\phi</math> '''R''' <math>\psi</math>).		# <math>\phi</math> gilt bis (einschließlich) zu dem Zustand, an dem <math>\psi</math> erfüllt ist (<math>\phi</math> '''R''' <math>\psi</math>).

	Für eine gegebene Folge von Zuständen <math>x_0, x_1, x_2, \ldots</math> sind die Operatoren formal wie folgt definiert:		Für eine gegebene Folge von Zuständen <math>x_0, x_1, x_2, \ldots</math> sind die Operatoren formal wie folgt definiert:
Zeile 43:		Zeile 43:
	# <math>F\phi</math> : = <math>\exists i\in \N: x_i</math> erfüllt <math>\phi</math>,		# <math>F\phi</math> : = <math>\exists i\in \N: x_i</math> erfüllt <math>\phi</math>,
	# <math>G\phi</math> : = <math>\forall i\in \N: x_i</math> erfüllt <math>\phi</math>,		# <math>G\phi</math> : = <math>\forall i\in \N: x_i</math> erfüllt <math>\phi</math>,
	# <math>\phi U \psi</math> : = <math>\exists i\in \N \quad \forall j \in \{a:a \in \N \land 0 < a ~~\leq~~ i\}: x_j </math> erfüllt <math>\phi \land x_i </math> erfüllt <math>\psi </math>,		# <math>\phi U \psi</math> : = <math>\exists i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a < i\}: x_j </math> erfüllt <math>\phi \land x_i </math> erfüllt <math>\psi </math>,
	# <math>\phi R \psi</math> : = <math>\exist i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a \leq i \} \quad \forall k \in \{a:a \in \N \land i < a \}: \psi</math> erfüllt <math>x_j \land \phi</math> erfüllt <math>x_k</math>		# <math>\phi R \psi</math> : = <math>\exist i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a \leq i \} \quad \forall k \in \{a:a \in \N \land i < a \}: \psi</math> erfüllt <math>x_j \land \phi</math> erfüllt <math>x_k</math>

194.96.98.250: /* Temporaloperatoren */

2018-01-21T10:14:56Z

Temporaloperatoren

← Nächstältere Version		Version vom 21. Januar 2018, 12:14 Uhr
Zeile 43:		Zeile 43:
	# <math>F\phi</math> : = <math>\exists i\in \N: x_i</math> erfüllt <math>\phi</math>,		# <math>F\phi</math> : = <math>\exists i\in \N: x_i</math> erfüllt <math>\phi</math>,
	# <math>G\phi</math> : = <math>\forall i\in \N: x_i</math> erfüllt <math>\phi</math>,		# <math>G\phi</math> : = <math>\forall i\in \N: x_i</math> erfüllt <math>\phi</math>,
	# <math>\phi U \psi</math> : = <math>\exists i\in \N \quad \forall j \in \{a:a \in \N \land 0 ~~\leq~~ a \leq i\}: x_j </math> erfüllt <math>\phi \land x_i </math> erfüllt <math>\psi </math>,		# <math>\phi U \psi</math> : = <math>\exists i\in \N \quad \forall j \in \{a:a \in \N \land 0 < a \leq i\}: x_j </math> erfüllt <math>\phi \land x_i </math> erfüllt <math>\psi </math>,
	# <math>\phi R \psi</math> : = <math>\exist i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a \leq i \} \quad \forall k \in \{a:a \in \N \land i < a \}: \psi</math> erfüllt <math>x_j \land \phi</math> erfüllt <math>x_k</math>		# <math>\phi R \psi</math> : = <math>\exist i\in \N \quad \forall j \in \{a:a \in \N \land 0 \leq a \leq i \} \quad \forall k \in \{a:a \in \N \land i < a \}: \psi</math> erfüllt <math>x_j \land \phi</math> erfüllt <math>x_k</math>

176.198.150.23: Änderung 170180314 von 176.198.150.23 rückgängig gemacht;

2017-10-21T10:27:28Z

Änderung 170180314 von 176.198.150.23 rückgängig gemacht;

← Nächstältere Version		Version vom 21. Oktober 2017, 12:27 Uhr
Zeile 88:		Zeile 88:
	* M. Huth and M. Ryan: ''Logic in Computer Science - Modelling and Reasoning about Systems''. Cambridge, 2004, ISBN 0-521-54310-X		* M. Huth and M. Ryan: ''Logic in Computer Science - Modelling and Reasoning about Systems''. Cambridge, 2004, ISBN 0-521-54310-X

			[[Kategorie:Mathematische Logik]]
	[[Kategorie:Temporale Logik]]		[[Kategorie:Temporale Logik]]

← Nächstältere Version		Version vom 27. August 2020, 11:26 Uhr
Zeile 1:		Zeile 1:
	[[Datei:Computational Tree Logic Example.png\|~~miniatur~~\|hochkant=1.25\|CTL-Formeln visualisiert]]		[[Datei:Computational Tree Logic Example.png\|mini\|hochkant=1.25\|CTL-Formeln visualisiert]]

	Die '''Computation Tree Logic''' (kurz CTL) ist eine [[Temporale Logik]], deren Modell der Zeit eine baumartige Struktur hat. Die zeitliche Änderung von Zuständen und deren Eigenschaften wird durch Pfade innerhalb dieser Baumstruktur modelliert. Hierbei hat die Zukunft mehrere Pfade, wobei nicht festgelegt ist, welche letztendlich realisiert werden. Demnach können Aussagen über die mögliche Entwicklungen getroffen werden.		Die '''Computation Tree Logic''' (kurz CTL) ist eine [[Temporale Logik]], deren Modell der Zeit eine baumartige Struktur hat. Die zeitliche Änderung von Zuständen und deren Eigenschaften wird durch Pfade innerhalb dieser Baumstruktur modelliert. Hierbei hat die Zukunft mehrere Pfade, wobei nicht festgelegt ist, welche letztendlich realisiert werden. Demnach können Aussagen über die mögliche Entwicklungen getroffen werden.
Zeile 5:		Zeile 5:
	Die CTL wird zur [[Verifizierung\|Verifikation]] von Hard- und Software verwendet, üblicherweise von [[Model Checking\|Model Checkern]].		Die CTL wird zur [[Verifizierung\|Verifikation]] von Hard- und Software verwendet, üblicherweise von [[Model Checking\|Model Checkern]].

	Zu der Familie der temporalen Logiken gehört auch die [[Lineare temporale Logik\|Linear temporale Logik]] (LTL), wobei hier nur eine Zukunft möglich ist. Eine Verallgemeinerung der beiden Logiken wird ~~als~~ als CTL* bezeichnet.		Zu der Familie der temporalen Logiken gehört auch die [[Lineare temporale Logik\|Linear temporale Logik]] (LTL), wobei hier nur eine Zukunft möglich ist. Eine Verallgemeinerung der beiden Logiken wird als CTL* bezeichnet.

	== Syntax ==		== Syntax ==

	=== Minimale Grammatik ===		=== Minimale Grammatik ===
	Sei <math>AP</math> eine Menge von [[Aussage (Logik)#Einfach – zusammengesetzt\|atomaren Aussagen]] (Behauptungen), dann ist jedes Element <math>p \in AP</math> eine CTL-Formel. Sind <math>\phi</math> und <math>\psi</math> Formeln, dann auch <math>\neg\phi</math>, <math>\phi \lor \psi</math>, <math>\text{EX}\phi</math>, <math>\text{EG} \phi</math> und <math>\phi \text{EU} \psi</math>. Dies definiert die minimale [[Formale Grammatik\|Grammatik]] von CTL. In der Regel wird diese allerdings um die gängigen [[Boolescher Operator\|booleschen Operatoren]] <math>\land</math>, <math>\implies</math>und <math>\Lrarr</math>, sowie einigen weiteren temporalen Operatoren erweitert.		Sei <math>AP</math> eine Menge von [[Aussage (Logik)#Einfach – zusammengesetzt\|atomaren Aussagen]] (Behauptungen), dann ist jedes Element <math>p \in AP</math> eine CTL-Formel. Sind <math>\phi</math> und <math>\psi</math> Formeln, dann auch <math>\neg\phi</math>, <math>\phi \lor \psi</math>, <math>\text{EX}\phi</math>, <math>\text{EG} \phi</math> und <math>\phi \text{EU} \psi</math>. Dies definiert die minimale [[Formale Grammatik\|Grammatik]] von CTL. In der Regel wird diese allerdings um die gängigen [[Boolescher Operator\|booleschen Operatoren]] <math>\land</math>, <math>\implies</math>und <math>\Lrarr</math>, sowie einigen weiteren temporalen Operatoren erweitert.
Zeile 16:		Zeile 15:

	* Pfadoperatoren:		* Pfadoperatoren:
	** <math>A\phi</math> – ''auf allen Pfaden folgt <math>\phi</math>'' (englisch: ''All'')		** <math>A\phi</math> – ''auf allen Pfaden folgt <math>\phi</math>'' (englisch: ''All'')
	** <math>E\phi</math> – ''auf mindestens einem Pfad folgt <math>\phi</math>'' (englisch: ''Exists'')		** <math>E\phi</math> – ''auf mindestens einem Pfad folgt <math>\phi</math>'' (englisch: ''Exists'')
	* Pfad-spezifische Operatoren:		* Pfad-spezifische Operatoren:
	** <math>X\phi</math> – ''unmittelbar folgt <math>\phi</math>'' (englisch: ''neXt state'')		** <math>X\phi</math> – ''unmittelbar folgt <math>\phi</math>'' (englisch: ''neXt state'')
Zeile 39:		Zeile 38:
	CTL Formeln werden über [[Transitionssystem]]e definiert. Für eine gegebene Folge von Zuständen des Systems <math>T(s_0) = s_0, s_1, \ldots</math> (beginnend in Zustand <math>s_0</math>) sind die Operatoren formal wie folgt definiert, dabei steht <math>T(s_0) \models \phi</math> für <math>T(s_0)</math> erfüllt <math>\phi</math>:		CTL Formeln werden über [[Transitionssystem]]e definiert. Für eine gegebene Folge von Zuständen des Systems <math>T(s_0) = s_0, s_1, \ldots</math> (beginnend in Zustand <math>s_0</math>) sind die Operatoren formal wie folgt definiert, dabei steht <math>T(s_0) \models \phi</math> für <math>T(s_0)</math> erfüllt <math>\phi</math>:

	* <math>T(s_0) \models \neg \phi \quad \Lrarr \quad T(s_0) \not\models \phi </math>		* <math>T(s_0) \models \neg \phi \quad \Lrarr \quad T(s_0) \not\models \phi </math>
	* <math>T(s_0) \models \phi \lor \psi \quad \Lrarr \quad T(s_0) \models \phi \text{ oder } T(s_0) \models \psi </math>		* <math>T(s_0) \models \phi \lor \psi \quad \Lrarr \quad T(s_0) \models \phi \text{ oder } T(s_0) \models \psi </math>
	* <math>T(s_0) \models EX\phi \quad \Lrarr \quad T(s_1) \models \phi </math>		* <math>T(s_0) \models EX\phi \quad \Lrarr \quad T(s_1) \models \phi </math>
	* <math>T(s_0) \models EG\phi \quad \Lrarr \quad \forall i: T(s_i) \models \phi </math>		* <math>T(s_0) \models EG\phi \quad \Lrarr \quad \forall i: T(s_i) \models \phi </math>
	* <math>T(s_0) \models \phi EU \psi \quad \Lrarr \quad \exists k: T(s_k) \models \psi \land \forall i < k: T(s_i) \models \phi</math>		* <math>T(s_0) \models \phi EU \psi \quad \Lrarr \quad \exists k: T(s_k) \models \psi \land \forall i < k: T(s_i) \models \phi</math>
Zeile 58:		Zeile 57:

	== Literatur ==		== Literatur ==
	* Clarke, Grumberg, Peled: ''Model Checking''. MIT Press, 2000. ISBN 0-262-03270-8		* Clarke, Grumberg, Peled: ''Model Checking''. MIT Press, 2000, ISBN 0-262-03270-8
	* Rohit Kapur: ''CTL for Test Information of Digital ICS'', Springer, 2002, ISBN 978-1-4020-7293-2		* Rohit Kapur: ''CTL for Test Information of Digital ICS''. Springer, 2002, ISBN 978-1-4020-7293-2
	* B. Berard, Michel Bidoit, Alain Finkel: ''Systems and Software Verification''. Model-~~Checking~~ Techniques and Tools.: ''~~Model-checking Techniques and Tools''.~~ Springer, 2001, ISBN 3-540-41523-8		* B. Berard, Michel Bidoit, Alain Finkel: ''Systems and Software Verification. Model-checking Techniques and Tools.'' Springer, 2001, ISBN 3-540-41523-8
	* M. Huth and M. Ryan: ''Logic in Computer Science - Modelling and Reasoning about Systems''. Cambridge, 2004, ISBN 0-521-54310-X		* M. Huth and M. Ryan: ''Logic in Computer Science - Modelling and Reasoning about Systems''. Cambridge, 2004, ISBN 0-521-54310-X

← Nächstältere Version		Version vom 22. Februar 2020, 19:33 Uhr
Zeile 5:		Zeile 5:
	Die CTL wird zur [[Verifizierung\|Verifikation]] von Hard- und Software verwendet, üblicherweise von [[Model Checking\|Model Checkern]].		Die CTL wird zur [[Verifizierung\|Verifikation]] von Hard- und Software verwendet, üblicherweise von [[Model Checking\|Model Checkern]].

	Zu der Familie der temporalen Logiken gehört auch die [[Lineare temporale Logik\|Linear temporale Logik]] (LTL), wobei hier nur eine Zukunft möglich ist. Eine Verallgemeinerung der beiden Logiken wird als als CTL* bezeichnet.		Zu der Familie der temporalen Logiken gehört auch die [[Lineare temporale Logik\|Linear temporale Logik]] (LTL), wobei hier nur eine Zukunft möglich ist. Eine Verallgemeinerung der beiden Logiken wird als als CTL* bezeichnet.

	== Syntax ==		== Syntax ==

	=== Minimale Grammatik ===		=== Minimale Grammatik ===
	Sei <math>AP</math> eine Menge von [[Aussage (Logik)#Einfach – zusammengesetzt\|atomaren Aussagen]] (Behauptungen), dann ist jedes Element <math>p \in AP</math> eine CTL-Formel. Sind <math>\phi</math> und <math>\psi</math> Formeln, dann auch <math>\neg\phi</math>, <math>\phi \lor \psi</math>, <math>\text{EX}\phi</math>, <math>\text{EG} \phi</math> und <math>\phi \text{EU} \psi</math>. Dies definiert die minimale [[Formale Grammatik\|Grammatik]] von CTL. In der Regel wird diese allerdings um die gängigen [[Boolescher Operator\|~~boolschen~~ Operatoren]] <math>\land</math>, <math>\implies</math>und <math>\Lrarr</math>, sowie einigen weiteren temporalen Operatoren erweitert.		Sei <math>AP</math> eine Menge von [[Aussage (Logik)#Einfach – zusammengesetzt\|atomaren Aussagen]] (Behauptungen), dann ist jedes Element <math>p \in AP</math> eine CTL-Formel. Sind <math>\phi</math> und <math>\psi</math> Formeln, dann auch <math>\neg\phi</math>, <math>\phi \lor \psi</math>, <math>\text{EX}\phi</math>, <math>\text{EG} \phi</math> und <math>\phi \text{EU} \psi</math>. Dies definiert die minimale [[Formale Grammatik\|Grammatik]] von CTL. In der Regel wird diese allerdings um die gängigen [[Boolescher Operator\|booleschen Operatoren]] <math>\land</math>, <math>\implies</math>und <math>\Lrarr</math>, sowie einigen weiteren temporalen Operatoren erweitert.

	=== Temporale Operatoren ===		=== Temporale Operatoren ===
	Die Erweiterung der minimalen Grammatik um folgende Operatoren erhöht nicht die Mächtigkeit der [[Formale Sprache\|Sprache]], da alle Operatoren durch Umformungen zurückgeführt werden können.		Die Erweiterung der minimalen Grammatik um folgende Operatoren erhöht nicht die Mächtigkeit der [[Formale Sprache\|Sprache]], da alle Operatoren durch Umformungen zurückgeführt werden können.

	*Pfadoperatoren:		* Pfadoperatoren:
	**<math>A\phi</math> – ''auf allen Pfaden folgt <math>\phi</math>'' (englisch: ''All'')		** <math>A\phi</math> – ''auf allen Pfaden folgt <math>\phi</math>'' (englisch: ''All'')
	**<math>E\phi</math> – ''auf mindestens einem Pfad folgt <math>\phi</math>'' (englisch: ''Exists'')		** <math>E\phi</math> – ''auf mindestens einem Pfad folgt <math>\phi</math>'' (englisch: ''Exists'')
	*Pfad-spezifische Operatoren:		* Pfad-spezifische Operatoren:
	**<math>X\phi</math> – ''unmittelbar folgt <math>\phi</math>'' (englisch: ''neXt state'')		** <math>X\phi</math> – ''unmittelbar folgt <math>\phi</math>'' (englisch: ''neXt state'')
	**<math>F\phi</math> – ''irgendwann folgt <math>\phi</math>'' (englisch: ''some Future state'' oder ''Finally'')		** <math>F\phi</math> – ''irgendwann folgt <math>\phi</math>'' (englisch: ''some Future state'' oder ''Finally'')
	**<math>G\phi</math> – ''auf dem folgenden Pfad folgt in jedem Zustand <math>\phi</math>'' (englisch: ''Globally'')		** <math>G\phi</math> – ''auf dem folgenden Pfad folgt in jedem Zustand <math>\phi</math>'' (englisch: ''Globally'')
	**<math>\phi U \psi</math> – ''<math>\phi</math> folgt bis zum Erreichen des Zustands <math>\psi</math>'' (englisch: ''Until'')		** <math>\phi U \psi</math> – ''<math>\phi</math> folgt bis zum Erreichen des Zustands <math>\psi</math>'' (englisch: ''Until'')
	**<math>\phi W \psi</math> – ''<math>\phi</math> folgt immer oder bis zum Erreichen des Zustands <math>\psi</math>'' (englisch: ''Weak Until'')		** <math>\phi W \psi</math> – ''<math>\phi</math> folgt immer oder bis zum Erreichen des Zustands <math>\psi</math>'' (englisch: ''Weak Until'')

	Pfad und pfad-spezifische Operatoren können miteinander kombiniert werden, sodass sich beispielsweise folgende Formeln ergeben:		Pfad und pfad-spezifische Operatoren können miteinander kombiniert werden, sodass sich beispielsweise folgende Formeln ergeben:

	*<math>EX\phi</math> –''in (mind.) einem nächsten Zustand gilt'' <math>\phi</math>		* <math>EX\phi</math> –''in (mind.) einem nächsten Zustand gilt'' <math>\phi</math>
	*<math>EF\phi</math> – ''in (mind.) einem der folgenden Zustände gilt'' <math>\phi</math>		* <math>EF\phi</math> – ''in (mind.) einem der folgenden Zustände gilt'' <math>\phi</math>
	*<math>EG\phi</math> – ''es gibt (mind.) einen Pfad, so dass <math>\phi</math> entlang des ganzen Pfades gilt''		* <math>EG\phi</math> – ''es gibt (mind.) einen Pfad, so dass <math>\phi</math> entlang des ganzen Pfades gilt''
	*<math>E[\phi U \psi ]</math> – ''es gibt einen Pfad, für den gilt: bis zum ersten Auftreten von <math>\psi</math> gilt'' <math>\phi</math>		* <math>E[\phi U \psi ]</math> – ''es gibt einen Pfad, für den gilt: bis zum ersten Auftreten von <math>\psi</math> gilt'' <math>\phi</math>
	*<math>AX \phi</math> – ''in jedem nächsten Zustand gilt'' <math>\phi</math>		* <math>AX \phi</math> – ''in jedem nächsten Zustand gilt'' <math>\phi</math>
	*<math>AF \phi</math> – ''man erreicht immer einen Zustand, in dem <math>\phi</math> gilt''		* <math>AF \phi</math> – ''man erreicht immer einen Zustand, in dem <math>\phi</math> gilt''
	*<math>AG \phi</math> – ''auf allen Pfaden gilt in jedem Zustand'' <math>\phi</math>		* <math>AG \phi</math> – ''auf allen Pfaden gilt in jedem Zustand'' <math>\phi</math>
	*<math>A [ \phi U \psi ]</math> – ''es gilt immer <math>\phi</math> bis zum ersten Auftreten von'' <math>\psi</math>		* <math>A [ \phi U \psi ]</math> – ''es gilt immer <math>\phi</math> bis zum ersten Auftreten von'' <math>\psi</math>

	== Semantik ==		== Semantik ==
	CTL Formeln werden über [[Transitionssystem~~\|Transitionssysteme~~]] definiert. Für eine gegebene Folge von Zuständen des Systems <math>T(s_0) = s_0, s_1, \ldots</math> (beginnend in Zustand <math>s_0</math>) sind die Operatoren formal wie folgt definiert, dabei steht <math>T(s_0) \models \phi</math> für <math>T(s_0)</math> erfüllt <math>\phi</math>:		CTL Formeln werden über [[Transitionssystem]]e definiert. Für eine gegebene Folge von Zuständen des Systems <math>T(s_0) = s_0, s_1, \ldots</math> (beginnend in Zustand <math>s_0</math>) sind die Operatoren formal wie folgt definiert, dabei steht <math>T(s_0) \models \phi</math> für <math>T(s_0)</math> erfüllt <math>\phi</math>:

	*<math>T(s_0) \models \neg \phi \quad \Lrarr \quad T(s_0) \not\models \phi </math>		* <math>T(s_0) \models \neg \phi \quad \Lrarr \quad T(s_0) \not\models \phi </math>
	*<math>T(s_0) \models \phi \lor \psi \quad \Lrarr \quad T(s_0) \models \phi \text{ oder } T(s_0) \models \psi </math>		* <math>T(s_0) \models \phi \lor \psi \quad \Lrarr \quad T(s_0) \models \phi \text{ oder } T(s_0) \models \psi </math>
	*<math>T(s_0) \models EX\phi \quad \Lrarr \quad T(s_1) \models \phi </math>		* <math>T(s_0) \models EX\phi \quad \Lrarr \quad T(s_1) \models \phi </math>
	*<math>T(s_0) \models EG\phi \quad \Lrarr \quad \forall i: T(s_i) \models \phi </math>		* <math>T(s_0) \models EG\phi \quad \Lrarr \quad \forall i: T(s_i) \models \phi </math>
	*<math>T(s_0) \models \phi EU \psi \quad \Lrarr \quad \exists k: T(s_k) \models \psi \land \forall i < k: T(s_i) \models \phi</math>		* <math>T(s_0) \models \phi EU \psi \quad \Lrarr \quad \exists k: T(s_k) \models \psi \land \forall i < k: T(s_i) \models \phi</math>

	Die oben genannten Umformungen erlauben es, Formeln ineinander umzuwandeln.		Die oben genannten Umformungen erlauben es, Formeln ineinander umzuwandeln.
	*<math>\neg A\phi \equiv E \neg \phi </math>		* <math>\neg A\phi \equiv E \neg \phi </math>
	*<math>\neg AF\phi \equiv EG\neg\phi</math>		* <math>\neg AF\phi \equiv EG\neg\phi</math>
	*<math>\neg EF\phi \equiv AG\neg\phi</math>		* <math>\neg EF\phi \equiv AG\neg\phi</math>
	*<math>\neg AX\phi \equiv EX\neg\phi</math>		* <math>\neg AX\phi \equiv EX\neg\phi</math>
	*<math>AG\phi \equiv \phi \land AX AG \phi</math>		* <math>AG\phi \equiv \phi \land AX AG \phi</math>
	*<math>EG\phi \equiv \phi \land EX EG \phi</math>		* <math>EG\phi \equiv \phi \land EX EG \phi</math>
	*<math>AF\phi \equiv \phi \lor AX AF \phi</math>		* <math>AF\phi \equiv \phi \lor AX AF \phi</math>
	*<math>EF\phi \equiv \phi \lor EX EF \phi</math>		* <math>EF\phi \equiv \phi \lor EX EF \phi</math>
	*<math>A[\phi U \psi] \equiv \psi \lor (\phi \land AX A [\phi U \psi])</math>		* <math>A[\phi U \psi] \equiv \psi \lor (\phi \land AX A [\phi U \psi])</math>
	*<math>E[\phi U \psi] \equiv \psi \lor (\phi \land EX E [\phi U \psi])</math>		* <math>E[\phi U \psi] \equiv \psi \lor (\phi \land EX E [\phi U \psi])</math>

	== Literatur ==		== Literatur ==

← Nächstältere Version		Version vom 16. April 2018, 15:56 Uhr
Zeile 18:		Zeile 18:
	Statt einzelner Zustände kann man nun unendliche Folgen solcher Zustände betrachten und darauf eine [[Semantik]] definieren. Die bisher definierten Formeln werden von einem Pfad erfüllt, wenn der erste Zustand des Pfades sie erfüllt. Diese Formeln werden nun durch die folgenden einstelligen Operationen erweitert:		Statt einzelner Zustände kann man nun unendliche Folgen solcher Zustände betrachten und darauf eine [[Semantik]] definieren. Die bisher definierten Formeln werden von einem Pfad erfüllt, wenn der erste Zustand des Pfades sie erfüllt. Diese Formeln werden nun durch die folgenden einstelligen Operationen erweitert:
	* '''X''' für den ''unmittelbar folgenden Zustand'' (englisch: ''neXt state'')		* '''X''' für den ''unmittelbar folgenden Zustand'' (englisch: ''neXt state'')
	* '''F''' für einen ''irgendwann folgenden Zustand'' (englisch: ''some Future state'')		* '''F''' für einen ''irgendwann folgenden Zustand'' (englisch: ''some Future state'' oder ''Finally'')
	* '''G''' für ''alle folgenden Zustände'' (englisch: ''Globally'')		* '''G''' für ''alle folgenden Zustände'' (englisch: ''Globally'')

	Und die beiden zweistelligen Operatoren:		Und die beiden zweistelligen Operatoren:
	* '''U''' für ''bis zum Erreichen des Zustands'' (englisch: ''Until'')		* '''U''' für ''bis zum Erreichen des Zustands'' (englisch: ''Until'')
	* '''R''' (englisch: ''Release'')		* '''R''' (englisch: ''Release'')

	Selten definiert man zusätzlich noch die Vergangenheitsformen:		Selten definiert man zusätzlich noch die Vergangenheitsformen:
	* '''P''' für ''vorheriger'', (englisch: ''previous'')		* '''P''' für ''vorheriger'', (englisch: ''previous'')
	* '''O''' für ''war einmal'' (englisch: ''once'')		* '''O''' für ''war einmal'' (englisch: ''once'')
	* '''B''' für ''war immer'' (englisch: ''always been'')		* '''B''' für ''war immer'' (englisch: ''always been'')
	* '''S''' für ''seit'' (englisch: ''since'').		* '''S''' für ''seit'' (englisch: ''since'').

	Pfade erfüllen diese Formeln nun genau dann, wenn (umgangssprachlich)		Pfade erfüllen diese Formeln nun genau dann, wenn (umgangssprachlich)
Zeile 38:		Zeile 38:
	# <math>\phi</math> gilt bis (einschließlich) zu dem Zustand, an dem <math>\psi</math> erfüllt ist (<math>\phi</math> '''R''' <math>\psi</math>).		# <math>\phi</math> gilt bis (einschließlich) zu dem Zustand, an dem <math>\psi</math> erfüllt ist (<math>\phi</math> '''R''' <math>\psi</math>).

	Für eine gegebene Folge von Zuständen <math>x_0, x_1, x_2, \ldots</math> sind die Operatoren formal wie folgt definiert:		Für eine gegebene Folge von Zuständen <math>x_0, x_1, x_2, \ldots</math> sind die Operatoren formal wie folgt definiert, dabei steht <math>x \models \phi</math> für <math>x</math> erfüllt <math>\phi</math>:

	# <math>X\phi~~</math>~~ : = ~~<math>~~x_1~~</math>~~ ~~erfüllt~~ ~~<math>~~\phi</math>,		# <math>\operatorname{\mathbf{X}}\phi := (x_1 \models \phi)</math>,
	# <math>F\phi~~</math>~~ : = ~~<math>~~\exists i\in \N: x_i~~</math>~~ ~~erfüllt~~ ~~<math>~~\phi</math>,		# <math>\operatorname{\mathbf{F}}\phi := \exists i\in \N \colon (x_i \models \phi)</math>,
	# <math>G\phi~~</math>~~ : = ~~<math>~~\forall i\in \N: x_i~~</math>~~ ~~erfüllt~~ ~~<math>~~\phi</math>,		# <math>\operatorname{\mathbf{G}}\phi := \forall i\in \N \colon (x_i \models \phi)</math>,
	# <math>\phi U \psi~~</math>~~ : = ~~<math>~~\exists i\in \N \~~quad~~ \forall j ~~\in \{a:a \in \N \land 0 \leq a~~ < i\}: x_j ~~</math>~~ ~~erfüllt~~ ~~<math>~~\phi \land x_i ~~</math>~~ ~~erfüllt~~ ~~<math>~~\psi </math>,		# <math>\phi \operatorname{\mathbf{U}} \psi := \exists i\in \N \; \forall j < i \colon (x_j \models \phi) \land (x_i \models \psi)</math>,
	# <math>\phi R \psi~~</math>~~ : = ~~<math>~~\~~exist~~ i\in \N \~~quad~~ \forall j ~~\in \{a:a \in \N \land 0 \leq a~~ \leq i \~~} \quad~~ \forall k ~~\in~~ ~~\{a:a~~ \in \N \~~land i < a~~ \}: \~~psi</math>~~ ~~erfüllt <math>x_j~~ \~~land~~ \phi~~</math> erfüllt <math>x_k~~</math>		# <math>\phi \operatorname{\mathbf{R}} \psi := \exists i\in \N \; \forall j \leq i \; \forall k > i \colon (x_j \models \psi) \land (x_k \models \phi)</math>

	Für '''F''', '''G''' und '''U''' gilt die Prämisse "Zukunft schließt Gegenwart mit ein", d. h. wird eine Formel in einem der folgenden Zustände erfüllt, so gilt das auch für den Startzustand.		Für '''F''', '''G''' und '''U''' gilt die Prämisse ''Zukunft schließt Gegenwart mit ein'', d. h. wird eine Formel in einem der folgenden Zustände erfüllt, so gilt das auch für den Startzustand.
	Die bis hier definierten Formeln bilden die sogenannten Pfadformeln und die schon oben erwähnte ''Linear Time Temporal Logic''.		Die bis hier definierten Formeln bilden die sogenannten Pfadformeln und die schon oben erwähnte ''Linear Time Temporal Logic''.