Several approaches are explored to give a formal semantics to TESL.

Axiomatic semantics

A preliminary version of the axiomatic semantics of TESL is presented in this report.

Trace composition semantics

This approach generates traces by interleaving clocks and uses the TESL specification to filter the traces and keep only the ones that satisfy the constraints.

Theory of tags

Firstly, a theory of tags defines the tags used to represent ticks on clocks. An order relation is defined on tags.

Interleaving and filtering

The next theory defines all possible interleavings of runs, as well as constraint operators, which model the relation between clocks and between time scales, and which are used to filter the runs that satisfy a set of constraints among all possible runs.