Common use of Background on CTL Clause in Contracts

Background on CTL. ‌ For the specification of properties, we use Computation Tree Logic (CTL). We only provide a brief overview, referring the reader to the classic textbook [4] for a complete and formal presentation. CTL formulas specify properties of execu- tion trees generated by transitions systems. The formulas are built from atomic predicates that represent transitions and statements of the transition system, using several operators, such as EX, AX, EF, AF, EG, AG (unary) and E[ U ], A[ U ], E[ W ], A[ W ] (binary). Each operator consists of a quantifier on the branches of the tree and a temporal modality, which together define when in the exe- cution the operand sub-formulas must hold. The intuition behind the letters is the following: the branch quantifiers are A (for “All”) and E (for “Exists”); the temporal modalities are X (for “neXt”), F (for “some time in the Future”), G (for “Globally”), U (for “Until”) and W (for “Weak until”). A property is satisfied if it holds in the initial state of the transition systems. For instance, the formula A[p W q] specifies that in all execution branches the predicate p must hold up to the first state (not including this latter), where the predicate q holds. Since we used the weak until operator W, if q never holds, p must hold forever. As soon as q holds in one state of an execution branch, p does not need to hold anymore, even if q does not hold. On the contrary, the formula AG A[p W q] specifies that the subformula A[p W q] must hold in all branches at all times. Thus, p must hold whenever q does not hold, i.e., AG A[p W q] = AG (p ∨ q).

Background on CTL. ‌ For the specification of properties, we use Computation Tree Logic (CTL). We only provide a brief overview, referring the reader to the classic textbook [4] for · · · · · · · · a complete and formal presentation. CTL formulas specify properties of execu- tion trees generated by transitions systems. The formulas are built from atomic predicates that represent transitions and statements of the transition system, using several operators, such as EX, AX, EF, AF, EG, AG (unary) and E[ U ], A[ U ], E[ W ], A[ W ] (binary). Each operator consists of a quantifier on the branches of the tree and a temporal modality, which together define when in the exe- cution the operand sub-formulas must hold. The intuition behind the letters is the following: the branch quantifiers are A (for “All”) and E (for “Exists”); the temporal modalities are X (for “neXt”), F (for “some time in the Future”), G (for “Globally”), U (for “Until”) and W (for “Weak until”). A property is satisfied if it holds in the initial state of the transition systems. For instance, the formula A[p W q] specifies that in all execution branches the predicate p must hold up to the first state (not including this latter), where the predicate q holds. Since we used the weak until operator W, if q never holds, p must hold forever. As soon as q holds in one state of an execution branch, p does not need to hold anymore, even if q does not hold. On the contrary, the formula AG A[p W q] specifies that the subformula A[p W q] must hold in all branches at all times. Thus, p must hold whenever q does not hold, i.e., AG A[p W q] = AG (p ∨ q).