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*
- 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:
![{\displaystyle AFAG\alpha \Rightarrow EFEG\beta }](https://wikimedia.org/api/rest_v1/media/math/render/svg/7b67da1fe023bc3e1dae66eab539222a832930d3)
- formuła poprawna w CTL*, ale niepoprawna w CTL:
![{\displaystyle AFG\alpha \Rightarrow EFG\beta }](https://wikimedia.org/api/rest_v1/media/math/render/svg/673641e541c4caffff75e1be37e58b5a456e2696)
- każda taka para operatorów:
tworzy operator logiki CTL. - operatory
są podstawowe, a z nich można wyprowadzić pozostałe:
![{\displaystyle AF\alpha \equiv A(\top U\alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/50cfc851b5e1adf6bfbf8a04051381b678f3fb73)
![{\displaystyle EF\alpha \equiv E(\top U\alpha )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/44289bbb6a2361590ba94217a178be36517a5d87)
![{\displaystyle AG\alpha \equiv A(\alpha U\bot )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a9ab503ce0878bd7656b355ce9b95e0588074d61)
![{\displaystyle EG\alpha \equiv E(\alpha U\bot )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4aa78e94deb2e37e16bb0066d69c1aab64135b1e)
![{\displaystyle A(\alpha R\beta )\equiv A(\neg (\neg \alpha U\neg \beta ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/52ac09c2f21606664b58f89ef495f55c9222ee77)
![{\displaystyle E(\alpha R\beta )\equiv E(\neg (\neg \alpha U\neg \beta ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4917ad3709e0f005ee2cd9a80a24044eb215c7e8)
– formuła
jest prawdziwa w strukturze
w stanie ![{\displaystyle s_{i}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cfda82668232cbdc0874ed28ab8b6079420d1ffe)
- warunki prawdziwości podstawowych formuł:
![{\displaystyle (M,s_{i})\models p\Leftrightarrow p\in L(s_{i})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cd713485c5da617e1cdd07802d6bbe18e750b84d)
![{\displaystyle (M,s_{i})\models \alpha _{1}\wedge \alpha _{2}\Leftrightarrow (M,s_{i})\models \alpha _{1}\wedge (M,s_{i})\models \alpha _{2}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/853d3229ea985234e604de7dce6c3e153fff4bfe)
![{\displaystyle (M,s_{i})\models \neg \alpha \Leftrightarrow \neg (M,s_{i})\models \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/7578b34e6bae5d81fc64a44727fd7dfcbc370adb)
![{\displaystyle (M,s_{i})\models A(\alpha _{1}U\alpha _{2})\Leftrightarrow \forall x_{i}\ \exists (k\geqslant i):(s_{k}\models \alpha _{2}\wedge \forall j:(i\leqslant j<k)(s_{j}\models \alpha _{1})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/559acfe4df21f312c3f48529222bba1ba62f774e)
![{\displaystyle (M,s_{i})\models E(\alpha _{1}U\alpha _{2})\Leftrightarrow \exists x_{i}\ \exists (k\geqslant i):(s_{k}\models \alpha _{2}\wedge \forall j:(i\leqslant j<k)(s_{j}\models \alpha _{1})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aff176f2eef77b2445c9e206e1d2fbd147232732)
![{\displaystyle (M,s_{i})\models AX\alpha \Leftrightarrow \forall x_{i}\ (M,s_{i+1})\models \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/f05542afac7223dc31c9cebbd70d2708906858c3)
![{\displaystyle (M,s_{i})\models EX\alpha \Leftrightarrow \exists x_{i}\ (M,s_{i+1})\models \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/84541519e4c875c61948aa1bb04719e5686a44fc)
Linki zewnętrzne
- PawełP. Głuchowski PawełP., Temporal Logic and Timed Automata, CTL logic [online], Politechnika Wrocławska [dostęp 2020-06-27] (ang.).
- Temporal Logics [online] (ang.).