Operatorami tej logiki są: (globally ) mówiący, że zachodzi w tej chwili, oraz że będzie zachodziło w każdym momencie w przyszłości (choć być może nie zachodziło w przeszłości), (finally ) mówiący, że kiedyś w przyszłości zajdzie (next ) mówiący, że w następnej chwili czasu zajdzie ( until ) mówiący, że kiedyś w przyszłości zajdzie a do tego czasu będzie zachodzić ( release ) mówiący, że zachodzi tak długo, aż zajdzie lub zachodzi zawsze, gdy nigdy nie zajdzie.
Wszystkie operatory można wyrazić za pomocą oraz
Zawsze będzie Nieprawda, że kiedyś nastąpi nie-
Kiedyś nastąpi Kiedyś nastąpi a do tego czasu zawsze będzie zachodziło prawda. (negacja przeniesiona na drugą stronę dla łatwiejszego zrozumienia) Nieprawda, że będzie zachodziło aż do momentu, w którym nastąpi Zajdzie kiedyś nie- a do czasu, w którym zajdzie, zawsze będzie zachodziło nie-
Logika CTL*
Logika (computation tree logic) to rozszerzenie logiki LTL na rozgałęziające się modele czasu. Do operatorów LTL dochodzą jeszcze: – dla każdej ścieżki zachodzi – istnieje taka ścieżka obliczeń, że