RERS 2018: CTL, LTL, and reachability

This paper is dedicated to the Rigorous Examination of Reactive Systems (RERS) Challenge 2018. We focus on changes and improvements compared to previous years. RERS again provided a large variety of verification benchmarks that foster the comparison of validation tools while featuring both sequential and parallel programs. In addition to reachability questions, the RERS Challenge is known for its linear temporal logic (LTL) properties, and RERS'18 extends the portfolio of verification tasks to computational tree logic (CTL). Modifications compared to the previous iteration include an enhanced generation of sequential benchmarks, an improved automation of the construction of parallel benchmarks, a redesigned penalty for wrong answers, and the addition of CTL properties. We illustrate our newly applied generation of parallel benchmarks in detail.