Promptness and Bounded Fairness in Concurrent and Parameterized Systems

  • Swen JacobsEmail author
  • Mouhammad Sakr
  • Martin Zimmermann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11990)


We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (\({\text {Prompt-LTL}}\)) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds on the satisfaction of eventualities, thus adding a quantitative aspect to the specification language. We establish a connection between bounded fairness, bounded stutter equivalence, and the satisfaction of \({\text {Prompt-LTL}} {\setminus }\mathbf{X} \) formulas. Based on this connection, we prove the first cutoff results for different classes of systems with a parametric number of components and quantitative specifications, thereby identifying previously unknown decidable fragments of the parameterized model checking problem.


  1. 1.
    Alur, R., Etessami, K., La Torre, S., Peled, D.A.: Parametric temporal logic for “model measuring”. ACM Trans. Comput. Log. 2(3), 388–407 (2001). Scholar
  2. 2.
    Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 262–281. Springer, Heidelberg (2014). Scholar
  3. 3.
    Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. Distrib. Comput. 31(3), 187–222 (2018). Scholar
  4. 4.
    Außerlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. CoRR abs/1505.03273 (2015).
  5. 5.
    Außerlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 476–494. Springer, Heidelberg (2016). Scholar
  6. 6.
    Baier, C., Katoen, J.P.: Principles of Model Checking. vol. 26202649. MIT press Cambridge (2008)Google Scholar
  7. 7.
    Bloem, R., Jacobs, S., Khalimov, A.: Parameterized synthesis case study: AMBA AHB. In: SYNT. EPTCS, vol. 157, pp. 68–83 (2014).
  8. 8.
    Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2015).
  9. 9.
    Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000). Scholar
  10. 10.
    Clarke, E., Talupur, M., Touili, T., Veith, H.: Verification by network decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 276–291. Springer, Heidelberg (2004). Scholar
  11. 11.
    Clarke, E., Talupur, M., Veith, H.: Proving ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 33–47. Springer, Heidelberg (2008). Scholar
  12. 12.
    Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS, pp. 361–370. IEEE Computer Society (2003).
  13. 13.
    Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Found. Comput. Sci. 14(4), 527–549 (2003). Scholar
  14. 14.
    Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 236–254. Springer, Heidelberg (2000). Scholar
  15. 15.
    Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS, pp. 352–359. IEEE Computer Society (1999).
  16. 16.
    Esparza, J.: Keeping a crowd safe: on the complexity of parameterized verification (invited talk). In: STACS. LIPIcs, vol. 25, pp. 1–10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014).
  17. 17.
    Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. J. ACM 63(1), 10:1–10:48 (2016). Scholar
  18. 18.
    Etessami, K.: Stutter-invariant languages, \(\omega \)-automata, and temporal logic. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 236–248. Springer, Heidelberg (1999). Scholar
  19. 19.
    Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic. Inf. Comput. 253, 237–256 (2017). Scholar
  20. 20.
    German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992). Scholar
  21. 21.
    Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10, 1–29 (2014). Scholar
  22. 22.
    Jacobs, S., Sakr, M.: Analyzing guarded protocols: better cutoffs, more systems, more expressivity. Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 247–268. Springer, Cham (2018). Scholar
  23. 23.
    Jacobs, S., Sakr, M., Zimmermann, M.: Promptness and bounded fairness in concurrent and parameterized systems. CoRR abs/1911.03122 (2019).
  24. 24.
    Jacobs, S., Tentrup, L., Zimmermann, M.: Distributed synthesis for parameterized temporal logics. Inf. Comput. 262, 311–328 (2018). Scholar
  25. 25.
    Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645–659. Springer, Heidelberg (2010). Scholar
  26. 26.
    Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 108–127. Springer, Heidelberg (2013). Scholar
  27. 27.
    Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods Syst. Des. 34(2), 83–103 (2009)CrossRefGoogle Scholar
  28. 28.
    Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. Inf. Comput. 117(1), 1–11 (1995). Scholar
  29. 29.
    Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299–313. Springer, Heidelberg (2007). Scholar
  30. 30.
    Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001). Scholar
  31. 31.
    Spalazzi, L., Spegni, F.: Parameterized model-checking of timed systems with conjunctive guards. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 235–251. Springer, Cham (2014). Scholar
  32. 32.
    Spalazzi, L., Spegni, F.: On the existence of cutoffs for model checking disjunctive timed networks. In: CEUR Workshop Proceedings ICTCS/CILC, vol. 1949, pp. 174–185. (2017)Google Scholar
  33. 33.
    Suzuki, I.: Proving properties of a ring of finite state machines. Inf. Process. Lett. 28(4), 213–214 (1988). Scholar
  34. 34.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322–331. IEEE Computer Society (1986)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.CISPA Helmholtz Center for Information SecuritySaarbrückenGermany
  2. 2.Saarland UniversitySaarbrückenGermany
  3. 3.University of LiverpoolLiverpoolUK

Personalised recommendations