2010-07-14
----------

Achim, Dejan, Scott, John, Ed

Where we are:

. We have been studying how to define ideal realtime semantics for digital
  SVA and extensions.

. Realtime semantics for sequences (digital and extensions)
  - this is in pretty good shape
  - we have goodness theorems about recovering digital semantics
  - the work does not include local variables, first_match, or derived operators
  - there have been some implementability questions raised about boolean smear

Volunteer to study first_match?  Dejan.
Volunteer to study implementability of boolean smear?  Ed.
Volunteer to study derived operators?  TBD.

. Local variables
  - we decided to allow local variable assignments only when events occur
  - FSL volunteered to work on adding this to the realtime sequence document,
    but we have not started yet.

Volunteer to work on local variables in realtime sequences?  Scott.

. Realtime LTL operators
  - the belief is that these have already been well understood in previous work
  - the realtime semantics needs to be written down
  - some consideration needs to be given to how they interact with local variables

Volunteer to work on realtime LTL operators and, possibly, interaction 
with local variables?  Dejan.

. Other property operators
  - we have been studying how to give realtime semantics to the existing digital
    SVA property operators
  - we have proposed definitions for strong(R), not, and, or, |->, and clocked
    nexttime
  - we have proved adjoint associativity for the semantics of |-> and ##0, although
    not everyone is convinced that the semantics is good enough
  - we do not have a definition of realtime semantics for |=>
  - we have not looked at derived operators, local variables in realtime properties,
    weak sequential properties, or aborts (for the last two, see below)

Volunteer to work on semantics of |=> and review |->?  Dejan, John.
Volunteer to look at derived operators?  TBD.
Volunteer to look at local variables in realtime properties?  TBD.

. Aborts and special letters
  - the digital semantics of weak sequential property and of aborts uses
    special letters (\top, \bot)
  - presumably, a similar device can be used in realtime semantics, but it
    needs to be written down
  - implementability of aborts with this semantics should be considered

Volunteer to study special letters, semantics of weak sequential properties,
and aborts?  TBD.
Volunteer to study implementability of aborts?  TBD.