Logika CTL* – jedna z logik temporalnych. Jest oparta na rozgałęzionej strukturze czasu (rozszerzenie logiki LTL o warianty czasu).
Struktura czasu Strukturą czasu w CTL* jest drzewiasta struktura gdzie: – zbiór stanów – relacja między stanami (następstwo czasu) – wartościowanie (przypisanie każdemu ze stanów wyrażeń, które są prawdziwe w tym stanie) – zbiór wyrażeń atomowych ścieżką jest w jest każda sekwencja momentów czasu:
oznacza ścieżkę rozpoczynającą się w stanie
Język wszystkie składniki logiki LTL, operatory ścieżkowe: – dla każdej ścieżki czasu prawdziwe jest – istnieje taka ścieżka czasu, dla której prawdziwe jest
Formuły Niech będzie zbiorem wyrażeń atomowych. każde wyrażenie jest formułą stanową jeśli i są formułami stanowymi, to i też są formułami stanowymi jeśli i są formułami stanowymi, to i też są formułami stanowymi jeśli jest formułą ścieżkową, to i są formułami stanowymi jeśli i są formułami ścieżkowymi, to i też są formułami ścieżkowymi każda formuła stanowa jest formułą ścieżkową
Oznacza to, że każda formuła w CTL* musi zaczynać się od operatora ścieżkowego lub
Prawdziwość formuł oznaczenia: – formuła stanowa jest prawdziwa w strukturze w stanie – formuła ścieżkowa jest prawdziwa w strukturze na ścieżce
warunki prawdziwości podstawowych formuł:
jest prawdziwe dla jakiejś ścieżki rozpoczynającej się w stanie jest prawdziwe dla każdej ścieżki rozpoczynającej się w stanie
Linki zewnętrzne Model Checking II Temporal Logic Model Checking
Kategoria:Logika temporalna