The problems listed here represent smaller versions of the actual problems used during the RERS Challenge 2022. Problems 1 – 2 resemble problems from the Sequential LTL track. As with the challenge problems, C99 versions are available for each training problem.

This year, we have fine-tuned the depth of LTL counterexamples, meaning the number of steps required to falsify a given property, based on a newly conceived approach for safety properties. Therefore, the new training problems below only feature safety properties. Actual challenge problems might also include other properties. For examples, please consider looking at training problems from previous RERS iterations such as 2019.

For further information on these problems, please refer to the problem description and the C99 code description.

LTL Training Problems

A zip containing the LTL training problems and solutions can be downloaded here.

The following files are contained in each problem's directory:

• .c file: C99 version of the source code.
• "...alphabet_mapping_C_version.txt" file: Bijection between the integer values in the C99 version and the input/output symbols in the property descriptions.
• .constraints-... (.txt file): LTL properties that participants of RERS have to check on the given program. See the problem description for details.
• constraints-solution-... (.txt file): Lists the correct "true"/"false" answers for each property, including exemplary counterexample traces for violated properties. This will not be available for actual challenge problems.

plain, small	arithmetic, small
Problem1	Problem2

---

Reachability Training Problems

A zip containing the reachability training problems and solutions can be downloaded here.

plain, small	arithmetic, small
Problem11	Problem12