This is an old revision of the document!

====== Notes on a common format for LTL Synthesis ====== This notes are based on a discussion with Viktor Schuppan, R&uuml;iger , and Barbara Jobstmann. In order to obtain a common format, we have to discuss the following topics: - Subset definitions (e.g., GR-1, Safety, Reachability,...) - Necessary abbreviations: assume, assert, define, other shortcuts? (see Lily syntax) - Order for BDD-based approaches - XML-format (see Unbeast) - LTL syntax (e.g., Wring syntax from below) - Title and Meta-information about case studies - Information about the target: Mealy, Moore, realizability - Regular expressions? - 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); assume G(b); assert G(c);" corresponds to "(G(a) * G(b)) -> G(b)".