Updates

  • Jan. 12th, 2021:
        Results online
  • Oct. 2nd, 2020:
       Parallel problems released
  • Sept 8th, 2020:
       Submission dates changed    (see below)
  • July 27th, 2020:
       Sequential challenge    problems released. Parallel    problems will follow soon.
  • July 17th, 2020:
       Submission dates changed    (August → September)
  • May 18th, 2020:
       Sequential training problems    released
  • May 5th, 2020:
       Important dates announced

Important Dates:

  • Dec. 14th, 2020:
       RERS event (held virtually)
  • Nov. 15th, 2020:
       Submission, parallel tracks
  • Oct. 9th, 2020:
       Final submission, sequential
  • Oct. 2nd, 2020:
       Initial submission, sequential
  • Oct. 2nd, 2020:
       Parallel problems
  • July 27th, 2020:
       Sequential problems
  • May 18th, 2020:
       Training problems

Submission

Parallel LTL/CTL tracks: A submission is possible until November 15th, 2020 anytime on earth.

For information on the submission format (.csv file), please click here.

Apart from submitting an optional description of your approach (evaluation-based award), there are three main submission options to choose from:

  • Regular: Achievements will be published if earned. Ranking scores/positions will be published in tracks of your choice.
  • Achievements only: Achievements will be published if earned. No participation in the ranking.
  • Anonymous: Ranking scores attributed to a generic participant name. No achievements.
Please use the following template to send us an email with your submission file(s) to info@rers-challenge.org. Note that depending on your chosen submission option, this template includes a disclaimer that corresponding results will be published on the RERS website.

Submission E-Mail Template

Dear RERS organizers,

Attached to this e-mail you can find our/my submission to the RERS Challenge 2020.

<optional>
In addition, please find a description of our approach attached as a .pdf-file (submission regarding the evaluation-based award).
</optional>

Participant information:
  • Name_1 (<optional> affilation_1 </optional>)
  • Name_2 (<optional> affilation_2 </optional>)
  • ...
We/I used the following problem versions <delete those that do not apply>:
  • Sequential LTL: C99 / Java
  • Sequential Reachability: C99 / Java
  • Parallel LTL: Promela / Petri net (PNML) / Graphviz (.dot)
  • Parallel CTL: Promela / Petri net (PNML) / Graphviz (.dot)
We/I have used/combined the following tools to generate our submission:
  • Tool_1
  • ...
<Option_1>
We/I would like to participate anonymously. We/I are aware that this means that our/my ranking results will be published under a generic name (e.g. “participant A”) on the RERS website and at the RERS event. We/I understand that we/I will not earn any achievements.
</Option_1>
<OR>
<Option_2>
We/I have reviewed the different submission options. We/I consent that our/my data corresponding to this submission, including awarded achievements and (if selected) ranking scores, will be published on the RERS website. We/I are/am aware of the possibility to inspect how the results of previous iterations of the RERS Challenge are presented online.
</Option_2>

<Option_A>
We/I would like to participate in the ranking of the following tracks <delete those that do not apply>:
  • Sequential LTL
  • Sequential Reachability
  • Parallel LTL
  • Parallel CTL
</Option_A>
<OR>
<Option_B>
We/I would like to not be mentioned in the ranking.
</Option_B>

Best regards,
Name_1, ...



If you have completed all (or some) tasks, we kindly request you to submit your solution in a CSV-style format. Solutions for each of the problems should be specified in the following way:

<number1>,<spec1>,<answer1>
<number2>,<spec2>,<answer2>
...

where

  • <number> is the problem specification number.
  • <spec> is the property specification identifier, where numbers 0 to 99 correspond to the LTL or Reachability properties for each problem or error number respectively.
  • <answer> expresses whether or not you believe this error label to be reachable, or the respective LTL property to be satisfied as true/false.

Hence, a line in this file for a hypothetical problem 0 and the error label 37 might look like this:

0, 37, true

Please choose a name for each of the CSV- which clearly identifies the respective problem along with an ID uniquely identifying the solution as yours such as "problemX-<id>.csv". You are free to generate one file for each problem or combine all solutions into a global CSV file. If you split your solutions into several files, please provide them as a ZIP or (compressed) TAR archive.