Skip to main content
Springer Nature Link
Log in

RERS 2018: CTL, LTL, and Reachability

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Verification (ISoLA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11245))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
CHF34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
CHF 24.95
Price includes VAT (Switzerland)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
CHF 47.00
Price excludes VAT (Switzerland)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
CHF 59.00
Price excludes VAT (Switzerland)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    http://www.rers-challenge.org/.

  2. 2.

    As stated online at http://www.rers-challenge.org/2018/.

  3. 3.

    https://github.com/LearnLib/automatalib/.

  4. 4.

    Our parallel composition operator will be specified in Definition 1 (Sect. 3.1).

  5. 5.

    https://tacas.info/toolympics.php.

References

  1. Bartocci, E., et al.: First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. STTT, 1–40 (2017). https://doi.org/10.1007/s10009-017-0454-5

  2. Beyer, D.: Competition on software verification. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_38

    Chapter  Google Scholar 

  3. Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401–416. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_31

    Chapter  Google Scholar 

  4. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774

    Chapter  Google Scholar 

  5. Erickson, K.T.: Programmable logic controllers. IEEE Potentials 15(1), 14–17 (1996)

    Article  Google Scholar 

  6. Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., van de Pol, J.: RERS 2016: parallel and sequential benchmarks with focus on LTL verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 787–803. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_59

    Chapter  Google Scholar 

  7. Gropp, W.D., Gropp, W., Lusk, E., Skjellum, A.: Using MPI: Portable Parallel Programming with the Message-Passing Interface, vol. 1. MIT Press, Cambridge (1999)

    Book  Google Scholar 

  8. Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)

    Google Scholar 

  9. Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Păsăreanu, C.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. STTT 16(5), 457–464 (2014)

    Article  Google Scholar 

  10. Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012. STTT 17(6), 647–657 (2015)

    Article  Google Scholar 

  11. Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487–495. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_32

    Chapter  Google Scholar 

  12. Jasper, M., et al.: The RERS 2017 challenge and workshop (invited paper). In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017, pp. 11–20. ACM (2017)

    Google Scholar 

  13. Jasper, M., Steffen, B.: Synthesizing subtle bugs with known witnesses. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 235–257. Springer, Cham (2018)

    Google Scholar 

  14. Kordon, F.: Report on the model checking contest at Petri nets 2011. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 169–196. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35179-2_8

    Chapter  Google Scholar 

  15. Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_19

    Chapter  Google Scholar 

  16. Liao, C., Lin, P.H., Asplund, J., Schordan, M., Karlin, I.: DataRaceBench: a benchmark suite for systematic evaluation of data race detection tools. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2017, pp. 11:1–11:14. ACM (2017)

    Google Scholar 

  17. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). https://doi.org/10.1007/BFb0017309

    Chapter  Google Scholar 

  18. Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River (1981)

    MATH  Google Scholar 

  19. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46–57, October 1977

    Google Scholar 

  20. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1989, pp. 179–190. ACM, New York (1989)

    Google Scholar 

  21. Steffen, B., Jasper, M., Meijer, J., van de Pol, J.: Property-preserving generation of tailored benchmark Petri nets. In: 17th International Conference on Application of Concurrency to System Design (ACSD), pp. 1–8, June 2017

    Google Scholar 

  22. Steffen, B., Howar, F., Isberner, M., Naujokat, S., Margaria, T.: Tailored generation of concurrent benchmarks. STTT 16(5), 543–558 (2014)

    Article  Google Scholar 

  23. Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. STTT 16(5), 465–479 (2014)

    Article  Google Scholar 

  24. Steffen, B., Jasper, M.: Property-preserving parallel decomposition. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 125–145. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_7

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TU Dortmund University, Dortmund, Germany

    Marc Jasper, Malte Mues, Maximilian Schlüter, Bernhard Steffen & Falk Howar

Authors
  1. Marc Jasper
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Malte Mues
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maximilian Schlüter
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Bernhard Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Falk Howar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marc Jasper .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Jasper, M., Mues, M., Schlüter, M., Steffen, B., Howar, F. (2018). RERS 2018: CTL, LTL, and Reachability. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification. ISoLA 2018. Lecture Notes in Computer Science(), vol 11245. Springer, Cham. https://doi.org/10.1007/978-3-030-03421-4_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03421-4_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03420-7

  • Online ISBN: 978-3-030-03421-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation

  NODES
Bugs 1
INTERN 5
Note 3
Verify 1