Updates

Important Dates:

  • Nov. 08, 2018:
       RERS at ISoLA'18
  • Oct. 01 – Oct. 14, 2018:
       Solution Submission
  • Aug. 22, 2018:
       Release Parallel LTL
  • Jul. 18, 2018:
       Release Sequential LTL and
       Sequential Reachability
  • Jul. 18, 2018:
       Training benchmarks
       available

Rewards and Achievements

Note to previous participants: The penalty for wrong answers has changed is now quadratic with regards to the number of wrong answers.

RERS has a trifold reward structure:

  1. Achievement certificates in gold, silver and bronze for each category of each track.
  2. Evaluation-based rewards for particularly interesting approaches.
  3. Competition-based ranking for each track separately for those interested.
These reward categories are only available for the Sequential Reachability, Sequential LTL, and Parallel LTL tracks. Participation in each of these reward categories is optional. In addition, achievements are awarded per category, and only earned achievements will be listed in the results. If you are a tool developer you should name your tool with the submission and it will be displayed for the achievements and ranking on the website. The separation between tool developers and users will be highlighted.

1) Achievements

In the RERS challenge achievements

  • Are given from a verifiers perspective: given answers must be correct, but there is no need to answer every question.
  • Require at least as many answers as can be witnessed by (counterexample) paths for each problem/achievement, i.e., reachable error labels and violated LTL properties. Any kind of answer (yes or no) counts for reaching this threshold, which however is unknown to the participants. Missed detected witness paths can well be compensated for by, e.g., claiming unreachability for other error labels.
  • Build upon each other (Bronze, Silver, and Gold): Only the most difficult achievement in a category is reported. In total there are 8 achievement categories: 3 categories within each of the two tracks Sequential Reachability and Sequential LTL, as well as 2 categories in the Parallel LTL track.
    The thresholds for Gold, Silver, and Bronze Achievements are defined as follows for each category:
    T_Bronze=#falsifiable properties of bronze problems
    T_Silver=T_Bronze + #falsifiable properties of silver problems
    T_Gold=T_Silver + #falsifiable properties of gold problems

    Which benchmark corresponds to the threshold of what achievement level (Bronze, Silver, Gold) can be seen in the illustrations on the respective download page. For example, each category from the Sequential Reachability and Sequential LTL tracks consists of one problem per medal value. The participant's score S is computed from all submitted correct verification/falsification results for each category separately.
    Example: Let participant_score("Plain") = #submitted_properties("Plain",bronze_problems) + #submitted_properties("Plain",silver_problems) + #submitted_properties(plain,gold_problems). If participant_score >=T_Bronze and participant_score < T_Silver, then the participant is awarded the Bronze Achievement in the "Plain" category if he or she only submitted correct results in that category.

If one answer is incorrect, the achievement cannot be awarded in the respective category.

2) Evaluation-Based Rewards

In this category winners are chosen according to the employed (combination of) methods (which must not necessarily have scored highest). The submitted descriptions of approaches and solutions will be reviewed and ranked by the challenge organizers. Due to the possible variety of methods there may be several winners in this category. Please submit your contribution as a pdf file according to the submission page. Each participant is invited to shortly present his or her approach to solving the challenge problems at the RERS event.

3) Competition-Based Ranking

There is a separate competition-based ranking for each of the three tracks Sequential Reachability, Sequential LTL, and Parallel LTL. It is possible to opt-out of the competition-based ranking (overall or in individual tracks).

Let n be the number of wrong answers of a participant in a given track. Then the different types of answers to individual properties (100 for each sequential problem) are evaluated as follows:

  • Correct answers: One point for each correct answer
  • Unsubmitted answers ("unknown"): Irrelevant, zero points
  • Wrong answers: Minus n2 points, where n is the number of wrong answers
This quadratic penalty for wrong answers is imposed in order to minimize guessing. This penalty has changed over the years in order to incorporate feedback by the community.