mały|Przykład modelu logiki CTL Logika CTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu.
Język taki sam, jak w logice CTL*
Formuły w porównaniu do logiki CTL*, każdy operator temopralny musi być poprzedzony przez operator ścieżkowy ( bądź ): formuła poprawna zarówno w CTL*, jak i w CTL: formuła poprawna w CTL*, ale niepoprawna w CTL: każda taka para operatorów: tworzy operator logiki CTL. operatory są podstawowe, a z nich można wyprowadzić pozostałe:
Prawdziwość formuł oznaczenia: – formuła jest prawdziwa w strukturze w stanie
warunki prawdziwości podstawowych formuł:
Linki zewnętrzne
Kategoria:Logika temporalna