Computation Tree Logic Die kurz CTL ist eine Temporale Logik deren Modell der Zeit eine baumartige Struktur hat Die zeit

Computation Tree Logic

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.

CTL-Formeln visualisiert

Die CTL wird zur Verifikation von Hard- und Software verwendet, üblicherweise von Model Checkern.

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

Syntax Bearbeiten

Minimale Grammatik Bearbeiten

Sei eine Menge von atomaren Aussagen (Behauptungen), dann ist jedes Element eine CTL-Formel. Sind und Formeln, dann auch , , , und . Dies definiert die minimale Grammatik von CTL. In der Regel wird diese allerdings um die gängigen booleschen Operatoren , und , sowie einigen weiteren temporalen Operatoren erweitert.

Temporale Operatoren Bearbeiten

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

Pfadoperatoren:
- – auf allen Pfaden folgt (englisch: All)
- – auf mindestens einem Pfad folgt (englisch: Exists)
Pfad-spezifische Operatoren:
- – unmittelbar folgt (englisch: neXt state)
- – irgendwann folgt (englisch: some Future state oder Finally)
- – auf dem folgenden Pfad folgt in jedem Zustand (englisch: Globally)
- – folgt bis zum Erreichen des Zustands (englisch: Until)
- – folgt immer oder bis zum Erreichen des Zustands (englisch: Weak Until)

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

– in (mind.) einem nächsten Zustand gilt
– in (mind.) einem der folgenden Zustände gilt
– es gibt (mind.) einen Pfad, so dass entlang des ganzen Pfades gilt
– es gibt einen Pfad, für den gilt: bis zum ersten Auftreten von gilt
– in jedem nächsten Zustand gilt
– man erreicht immer einen Zustand, in dem gilt
– auf allen Pfaden gilt in jedem Zustand
– es gilt immer bis zum ersten Auftreten von

Semantik Bearbeiten

CTL Formeln werden über Transitionssysteme definiert. Für eine gegebene Folge von Zuständen des Systems (beginnend in Zustand ) sind die Operatoren formal wie folgt definiert, dabei steht für erfüllt :

Die oben genannten Umformungen erlauben es, Formeln ineinander umzuwandeln.

Literatur Bearbeiten

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
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

wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele

Veröffentlichungsdatum: Dezember 01, 2023, 19:11 pm

Die Computation Tree Logic kurz CTL ist eine Temporale Logik deren Modell der Zeit eine baumartige Struktur hat Die zeitliche Anderung von Zustanden 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 konnen Aussagen uber die mogliche Entwicklungen getroffen werden CTL Formeln visualisiertDie CTL wird zur Verifikation von Hard und Software verwendet ublicherweise von Model Checkern Zu der Familie der temporalen Logiken gehort auch die Linear temporale Logik LTL wobei hier nur eine Zukunft moglich ist Eine Verallgemeinerung der beiden Logiken wird als CTL bezeichnet Inhaltsverzeichnis 1 Syntax 1 1 Minimale Grammatik 1 2 Temporale Operatoren 2 Semantik 3 LiteraturSyntax BearbeitenMinimale Grammatik Bearbeiten Sei A P displaystyle AP nbsp eine Menge von atomaren Aussagen Behauptungen dann ist jedes Element p A P displaystyle p in AP nbsp eine CTL Formel Sind ϕ displaystyle phi nbsp und ps displaystyle psi nbsp Formeln dann auch ϕ displaystyle neg phi nbsp ϕ ps displaystyle phi lor psi nbsp EX ϕ displaystyle text EX phi nbsp EG ϕ displaystyle text EG phi nbsp und ϕ EU ps displaystyle phi text EU psi nbsp Dies definiert die minimale Grammatik von CTL In der Regel wird diese allerdings um die gangigen booleschen Operatoren displaystyle land nbsp displaystyle implies nbsp und displaystyle Leftrightarrow nbsp sowie einigen weiteren temporalen Operatoren erweitert Temporale Operatoren Bearbeiten Die Erweiterung der minimalen Grammatik um folgende Operatoren erhoht nicht die Machtigkeit der Sprache da alle Operatoren durch Umformungen zuruckgefuhrt werden konnen Pfadoperatoren A ϕ displaystyle A phi nbsp auf allen Pfaden folgt ϕ displaystyle phi nbsp englisch All E ϕ displaystyle E phi nbsp auf mindestens einem Pfad folgt ϕ displaystyle phi nbsp englisch Exists Pfad spezifische Operatoren X ϕ displaystyle X phi nbsp unmittelbar folgt ϕ displaystyle phi nbsp englisch neXt state F ϕ displaystyle F phi nbsp irgendwann folgt ϕ displaystyle phi nbsp englisch some Future state oder Finally G ϕ displaystyle G phi nbsp auf dem folgenden Pfad folgt in jedem Zustand ϕ displaystyle phi nbsp englisch Globally ϕ U ps displaystyle phi U psi nbsp ϕ displaystyle phi nbsp folgt bis zum Erreichen des Zustands ps displaystyle psi nbsp englisch Until ϕ W ps displaystyle phi W psi nbsp ϕ displaystyle phi nbsp folgt immer oder bis zum Erreichen des Zustands ps displaystyle psi nbsp englisch Weak Until Pfad und pfad spezifische Operatoren konnen miteinander kombiniert werden sodass sich beispielsweise folgende Formeln ergeben E X ϕ displaystyle EX phi nbsp in mind einem nachsten Zustand gilt ϕ displaystyle phi nbsp E F ϕ displaystyle EF phi nbsp in mind einem der folgenden Zustande gilt ϕ displaystyle phi nbsp E G ϕ displaystyle EG phi nbsp es gibt mind einen Pfad so dass ϕ displaystyle phi nbsp entlang des ganzen Pfades gilt E ϕ U ps displaystyle E phi U psi nbsp es gibt einen Pfad fur den gilt bis zum ersten Auftreten von ps displaystyle psi nbsp gilt ϕ displaystyle phi nbsp A X ϕ displaystyle AX phi nbsp in jedem nachsten Zustand gilt ϕ displaystyle phi nbsp A F ϕ displaystyle AF phi nbsp man erreicht immer einen Zustand in dem ϕ displaystyle phi nbsp gilt A G ϕ displaystyle AG phi nbsp auf allen Pfaden gilt in jedem Zustand ϕ displaystyle phi nbsp A ϕ U ps displaystyle A phi U psi nbsp es gilt immer ϕ displaystyle phi nbsp bis zum ersten Auftreten von ps displaystyle psi nbsp Semantik BearbeitenCTL Formeln werden uber Transitionssysteme definiert Fur eine gegebene Folge von Zustanden des Systems T s 0 s 0 s 1 displaystyle T s 0 s 0 s 1 ldots nbsp beginnend in Zustand s 0 displaystyle s 0 nbsp sind die Operatoren formal wie folgt definiert dabei steht T s 0 ϕ displaystyle T s 0 models phi nbsp fur T s 0 displaystyle T s 0 nbsp erfullt ϕ displaystyle phi nbsp T s 0 ϕ T s 0 ϕ displaystyle T s 0 models neg phi quad Leftrightarrow quad T s 0 not models phi nbsp T s 0 ϕ ps T s 0 ϕ oder T s 0 ps displaystyle T s 0 models phi lor psi quad Leftrightarrow quad T s 0 models phi text oder T s 0 models psi nbsp T s 0 E X ϕ T s 1 ϕ displaystyle T s 0 models EX phi quad Leftrightarrow quad T s 1 models phi nbsp T s 0 E G ϕ i T s i ϕ displaystyle T s 0 models EG phi quad Leftrightarrow quad forall i T s i models phi nbsp T s 0 ϕ E U ps k T s k ps i lt k T s i ϕ displaystyle T s 0 models phi EU psi quad Leftrightarrow quad exists k T s k models psi land forall i lt k T s i models phi nbsp Die oben genannten Umformungen erlauben es Formeln ineinander umzuwandeln A ϕ E ϕ displaystyle neg A phi equiv E neg phi nbsp A F ϕ E G ϕ displaystyle neg AF phi equiv EG neg phi nbsp E F ϕ A G ϕ displaystyle neg EF phi equiv AG neg phi nbsp A X ϕ E X ϕ displaystyle neg AX phi equiv EX neg phi nbsp A G ϕ ϕ A X A G ϕ displaystyle AG phi equiv phi land AXAG phi nbsp E G ϕ ϕ E X E G ϕ displaystyle EG phi equiv phi land EXEG phi nbsp A F ϕ ϕ A X A F ϕ displaystyle AF phi equiv phi lor AXAF phi nbsp E F ϕ ϕ E X E F ϕ displaystyle EF phi equiv phi lor EXEF phi nbsp A ϕ U ps ps ϕ A X A ϕ U ps displaystyle A phi U psi equiv psi lor phi land AXA phi U psi nbsp E ϕ U ps ps ϕ E X E ϕ U ps displaystyle E phi U psi equiv psi lor phi land EXE phi U psi nbsp Literatur BearbeitenClarke 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 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 Abgerufen von https de wikipedia org w index php title Computation Tree Logic amp oldid 206067653