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)

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)