Today we present the result of our open discussions up to and
including at the SYNT workshop, and some internal discussions
afterwards.

Basic Format

We think that, in order to have a successful competition at CAV/SYNT
2014, the three most important things are: i) keeping the format
simple, ii) having sufficiently many competing tools, iii) supplying
the community with a format, benchmark set and framework for testing
their tools as early as possible.

These three points led us to choosing the AIGER format — restricted to
safety specifications, like in the main category of the HWMCC — both
as input and ouput format for the synthesis competition. For the input
format, we need to add a partition of inputs into controllable and
uncontrollable, but otherwise we can build on a
well-known language with a clear semantics and existing tool
support. For the output format, choosing AIGER allows us to almost
directly check the synthesized artifacts with any model checker that
supports the format (in particular, any that competes in the HWMCC). A
description of how we plan to use the AIGER format in
reactive synthesis can be found here: Format Proposal (v0.1).

In the coming weeks, we will be working on
i) converting as many benchmarks as possible to the AIGER format, with
bounded approximation of liveness properties by safety properties
ii) implementing a framework that allows potential participants to
adapt their tools to the new in- and ouput format, and test them in
an environment that resembles that of the competition itself
iii) developing a formal description of the format and a detailed
ruleset for the competition.

Extended Format

The discussions in St. Petersburg made clear that there is an interest
in more expressive specifications, like full LTL. There are a number
of additional problems to be solved for supporting this in the
competition. Most importantly, on the one hand LTL poses a rather high
entry barrier, even with existing tools for conversion to different
automata formats, and on the other hand we cannot expect the resulting
artifacts to be verified formally by existing model checkers. Thus, it
will be much more difficult to assess and rank
solutions. Still, we are thinking about how we could include a full
LTL track into the competition, and are open to suggestions on how to
best achieve this.

As always, questions, comments, and suggestions are very welcome!