Logika CTL* – jedna z logik temporalnych. Jest oparta na rozgałęzionej strukturze czasu (rozszerzenie logiki LTL o warianty 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
- 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ł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