Personnes présentes

• Frédéric Boulanger
• Safouan Taha
• Burkhart Wolff
• Lina Ye

A Theory on Temporal Patterns following Dwyer

Safouan presents his recent work of his formalization of Dwyer Temporal Patterns. These patterns should ease the task of temporal modeling (rather than hacking directly LTL formulas) by adding more intuitive concepts such as scope and order.

In addition to earlier discussions, Safouan has advanced the theory significantly such that it covers now the finite and the infinite case.

Occurrence (Absence/Presence of Events) Patterns

• never
• eventually n times
  • at least
  • at most
  • exactly
• always

Order Patterns(Order between events)

• precedence
• response

Put patterns in scopes

• globally
• before
• after
• between Q and R
• …

Proposition bu: The theories between the finite / infinite definitions of Property/Order/Scope seem to be very similar (just the difference between 'a list sets and (nat -> 'a) sets); wouldn't it be interesting to define locales for factoring out the theoretic basis for the finite / infinite model case ?

Discussion: What is the business case for patterns over the infinite model ?

Discussion: What could be an interesting scenario for TESL as an architectural glue language, gluing together this type of LTL patterns with Lustre and Automata and whatever ... ? Well, it seems that the sustain operator in TESL (which is currently restricted to implies) should be generalized to s.th. like a scope operator.