Timed CTL: TCTL and tCTL

(Has to be rewritten because the semantics has changed)

If one accepts the assumption that the execution time of an automaton can be zero than one has the problem how to manage the dense real-time points within the system. In this case a run becomes a mapping from the real numbers into the set of possible states organized as an execution. Because in this scenario a definite succesor of a processing state q at time point t does no longer exist, because there can be infinite many possible time points as successors, one changed the definitions of CTL in a way, that in the extended version timed CTL (TCTL) the description of a run can be done without an explicit next operator X.

The other difference between CTL and TCTL is given by the fact that you can in TCTL extend the quantified formulas as follows:

or

or

where , , and any fraction of integers like .

This means e.g. that an expression like does not only talk about an execution where you have two different properties at position and at position with , but you can also give a numerical bound with . This numerical bound means that the property has to be reached in the run latest after 5 time units.

Because we are holding in this course the assumption that the processing time is always greater than zero we do not really need this special version of TCTL. Otherwise the explicit numerical bound has some practical flavor. Therefore we will define here a variant of timed CTL which is between CTL and TCTL, we call it tiny temporal CTL (tCTL). In the tiny CTL specification language we have all expressions from TCTL, but the main difference is that the indices used in tCTL correspond in the model structure to the operation cycles of the automaton (the above mentioned discrete automata time, DAT).

Before we define the syntax and semantics for the tCTL-expressions we have to extend our definition for the automaton with clocks by an additional term for properties, because the tCTL-expressions presuppose the existence of properties connected to the states.

Def.: Automata with Clocks and Properties

with

and

Thus, if we have a run of the automaton then we can deduce from this run for every state the set of attached properties as well as the implied output. We can then use the set of all possible executions of th automaton alpha as our model to define an interpretation relation for an tCTL-expression like

.

• If then
• or or with , , and (We assume a weaker version than usual assumed for TCTL!)..
• iff there is a state s Q which occurs in a run of and
• iff there is no state s Q with
• iff and
• iff or
• iff ) or

• (there is a state coming up in the execution having property , but the upcoming occurence must agree with the numerical bound): There is a run . From a point of time onwards there can be another point of time with and and at there is a state and . Also written as

• (all upcoming possible states having property , but the upcoming occurence must agree with the numerical bound ): There is a run . From a point of time onwards all indices with are valid and must agree as . Every index identifies with a state with . Also written as

• (at point j is property true and before j until some k property , but the upcoming occurence at j must agree with the numerical bound): There is a run . From a point of time onwards there can be another point of time with and and at there is a state and .There is a with and there is a state and . Also written as

Example: We merge the automaton having properties like those in figure 3.4 with an automaton having clocks (cf. figure 5.4).

with

and

1. =
2. = .
3. =
4. = .
5. = .

We want to check whether the following tCTL-formula is valid for this concrete automaton:

Question:

Answer: We construct a run as follows (we write the complete state description to show why the run is working):

This shows the following: there is a run . There is a position with state and according to we have there the attached property . Furthermore does hold . therefore we can conclude that the tCTL-formula is satisfied in , i.e. the formula is true in the model.

Gerd Doeben-Henisch 2010-03-03