equal
deleted
inserted
replaced
1 (*<*)theory CTL = Base:;(*>*) |
1 (*<*)theory CTL = Base:;(*>*) |
2 |
2 |
3 subsection{*Computation Tree Logic---CTL*}; |
3 subsection{*Computation Tree Logic --- CTL*}; |
4 |
4 |
5 text{*\label{sec:CTL} |
5 text{*\label{sec:CTL} |
6 The semantics of PDL only needs reflexive transitive closure. |
6 The semantics of PDL only needs reflexive transitive closure. |
7 Let us be adventurous and introduce a more expressive temporal operator. |
7 Let us be adventurous and introduce a more expressive temporal operator. |
8 We extend the datatype |
8 We extend the datatype |