Notes on a common format for LTL Synthesis

This notes are based on a discussion with Viktor Schuppan, Rüdiger Ehlers, and Barbara Jobstmann.

In order to obtain a common format, we have to discuss the following topics:

  1. Subset definitions (e.g., GR-1, Safety, Reachability,…)
  2. Necessary abbreviations: assume, assert, define, other shortcuts? (see Lily syntax)
  3. Order for BDD-based approaches
  4. XML-format (see Unbeast)
  5. LTL syntax (e.g., Wring syntax from below)
  6. Title and Meta-information about case studies
  7. Information about the target: Mealy, Moore, realizability
  8. Regular expressions or automata?
  9. How to embed controller synthesis? Ways to specify partial models (see NuGat/NuSMV)

Wring LTL-Syntax (used by Lily)

FORMULA ::= TERM {BINARYOP TERM}
TERM ::= {ATOM | (FORMULA) | UNARYOP FORMULA | TEMPORALOP (FORMULA)}
BINARYOP ::= * | + | ^ | → | ↔ | U | R | V
UNARYOP ::= !
TEMPORALOP ::= G | F | X
ATOM ::= VAR=VALUE
VAR ::= \w+
VALUE ::= 0 | 1

Furthermore, Wring allows you to use the keyword define to avoid writing the same formula multiple times.

Extensions in Lily:

  • A formula can range over several lines. A semi-colon indicates the end of the formula.
  • Each formula can be prefixed with the keyword assume or assert
  • In general, a semi-colon acts as conjunction between formulas unless the assume/assert keywords are used. Then, the list of formulas corresponds to an implication between a conjunction of all formulas assumed and a conjunction of all formulas asserted. E.g.,
    assume G(a=1);
    assume G(b=1);
    assert G(c=1);
    corresponds to (G(a=1) * G(b=1)) → G(c=1)