Updated benchmarks: Based on feedback from participants, the LTL properties of problems 101 through 110 have been replaced on 20.08.2016 and additional problems 111 through 120 have been added. Please only submit results for the new problems of versions 2.

It is planned to publish an STTT special section on RERS 2016. Winning and interesting approaches will be invited to publish a paper on their challenge approach and contribution. Each participant is invited to shortly present his or her approach on the challenge at the RERS meeting.

For parallel problems only a ranking with the total number of points for this track is provided. Achievements will be added in the future. For further information please take a look at the rewards and achievements page. For further information about syntax and semantic of the properties please read the parallel problem description page. Please note that the syntax and semantic of the properties varies from the sequential problems.

Each of the provided benchmark problems consists of a system of parallel synchronized automata and a list of 20 properties specified in LTL. The 20 problems scale in two different ways. On the one hand, the number of automata per system increases: Problem 101 consists of only one automaton, problem 102 contains a parallel system of two automata and so on. The first problem is therefore a small sequential example, all other problems are parallel programs.

Other useful information can be found on the problem description page.

Provided Files

Each benchmark problem is available in two different formats:

1. A formal definition of labeled transition systems. It consists of two files:
   1. A DOT graph that represents the transition systems as clusters. The parallel system described by these transition systems behaves according to the parallel program description. It can therefore be used to check the LTL properties and to visualize the parallel system (for example using the tool Graphviz, command line: "dot -Tpdf problem1.dot -o problem1.pdf")
   2. a separate list of LTL properties
2. An implementation of the parallel system in Promela. This version already includes the list of LTL properties and can therefore be used to check the validity of these properties, for example when provided as input to the verification tool SPIN. For simplicity, both the automaton-internal transitions and the communication with the environment are triggered by an "Environment" process that sends messages non-deterministically. The automaton-internal transitions labeled with an empty string in the specification are relabeled to "nop", indicating that no communication occurred. A "Listener" process is notified about every occurring communication and always sets the global variable "lastAction" to the label of the most recently triggered transition(s).

---

The problems are provided as a zip file containing all parallel problems. Detailed solutions for the problems (with counterexamples) will be uploaded shortly. A solution with true/false answers can be found in a zip on the results page.

Complexity increases with problem number
Problem101	Problem102	Problem103	Problem104	Problem105
Problem106	Problem107	Problem108	Problem109	Problem110
Problem111	Problem112	Problem113	Problem114	Problem115
Problem116	Problem117	Problem118	Problem119	Problem120