Skip to main content
SpringerLink
Log in

Tight Cutoffs for Guarded Protocols with Fairness

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)

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

Abstract

Guarded protocols were introduced in a seminal paper by Emerson and Kahlon (2000), and describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certain local states. We study parameterized model checking and synthesis of guarded protocols, both aiming at formal correctness arguments for systems with any number of processes. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a determined, fixed size. Our work stems from the observation that existing cutoff results for guarded protocols (i) are restricted to closed systems, and (ii) are of limited use for liveness properties because reductions do not preserve fairness. We close these gaps and obtain new cutoff results for open systems with liveness properties under fairness assumptions. Furthermore, we obtain cutoffs for the detection of global and local deadlocks, which are of paramount importance in synthesis. Finally, we prove tightness or asymptotic tightness for the new cutoffs.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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

Notes

  1. 1.

    By only considering inputs that are actually processed, we approximate an action-based semantics. Paths that do not fulfill this requirement are not very interesting, since the environment can violate any interesting specification that involves input signals by manipulating them when the corresponding process is not allowed to move.

  2. 2.

    This assumption is in the same flavor as the restriction that \(\mathsf{init} _A\) and \(\mathsf{init} _B\) appear in all conjunctive guards. Intuitively, the additional restriction makes sense since conjunctive systems model shared resources, and everybody who takes a resource should eventually release it.

  3. 3.

    “Process \(B_1\) starting at moment m carries process \(B_i\) from q to \(q'\)” means: process \(B_i\) mimics the transitions of \(B_1\) starting at moment m at q until \(B_1\) first reaches \(q'\).

  4. 4.

    A careful reader may notice that if \(|\mathsf {Visited}^\textit{inf}_{B_1}\!(x)|=1\) and \(|\mathsf {Visited}^\textit{inf}_{B_2..B_n}\!(x)|=|B|\), then the construction uses \(2|B|+1\) copies of B. But one can slightly modify the construction for this special case, and remove process \(B_{i_{q^\star }'}\) from the pre-requisites.

  5. 5.

    Strictly speaking, in x we might not have two deadlocked processes in a state in \(dead_2\) – one process may be deadlocked, others enter and exit the state infinitely often. In such case, there is always a non-deadlocked process in the state. Then, copy the local run of such infinitely moving process until it enters the deadlocked state, and then deadlock it by providing the same input as the deadlocked process receives.

References

  1. Abdulla, P.A., Haziza, F., Holík, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476–495. Springer, Heidelberg (2013). http://dx.doi.org/10.1007/978-3-642-35873-9_28

    Chapter  Google Scholar 

  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). http://dx.doi.org/10.1007/978-3-642-54013-4_15

    Chapter  Google Scholar 

  3. Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 109–124. Springer, Heidelberg (2014). http://dx.doi.org/10.1007/978-3-662-44584-6_9

    Google Scholar 

  4. Außerlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. CoRR abs/1505.03273 (2015). http://arxiv.org/abs/1505.03273

  5. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)

    MATH  Google Scholar 

  6. Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, p. 175. Morgan & Claypool Publishers, San Rafael (2015). http://www.morganclaypool.com/doi/10.2200/S00658ED1V01Y201508DCT013

    Google Scholar 

  7. Bouajjani, A., Habermehl, P., Vojnar, T.: Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Meth. Syst. Des. 32(2), 129–172 (2008). http://dx.doi.org/10.1007/s10703-008-0048-7

    Article  MATH  Google Scholar 

  8. 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). http://dx.doi.org/10.1007/10722167_31

    Chapter  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  11. Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982). http://dx.doi.org/10.1016/0167-6423(83)90017-5

    Article  MATH  Google Scholar 

  12. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 236–254. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS, pp. 361–370. IEEE Computer Society (2003)

    Google Scholar 

  14. Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Found. Comput. Sci. 14, 527–549 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  15. Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. STTT 8(3), 261–279 (2006). http://dx.doi.org/10.1007/s10009-005-0193-x

    Article  Google Scholar 

  16. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  17. Jacobs, S., Bloem, R.: Parameterized synthesis. Logical Meth. Comput. Sci. 10, 1–29 (2014)

    Article  MathSciNet  Google Scholar 

  18. 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). http://dx.doi.org/10.1007/978-3-642-14295-6_55

    Chapter  Google Scholar 

  19. Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002). http://dx.doi.org/10.1007/3-540-45694-5_8

    Chapter  Google Scholar 

  20. Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928–933. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  21. Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. Inf. Comp. 117(1), 1–11 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  22. Manna, Z., Pnueli, A.: Temporal specification and verification of reactive modules. Weizmann Institute of Science Technical Report (1992)

    Google Scholar 

  23. Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001). http://dx.doi.org/10.1007/3-540-45319-9_7

    Chapter  Google Scholar 

  24. Pnueli, A., Xu, J., Zuck, L.D.: Liveness with \({(0,1,\infty )}\)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002). http://dx.doi.org/10.1007/3-540-45657-0_9

    Chapter  Google Scholar 

  25. Suzuki, I.: Proving properties of a ring of finite state machines. Inf. Process. Lett. 28(4), 213–214 (1988)

    Article  MATH  Google Scholar 

  26. Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1989). http://dx.doi.org/10.1007/3-540-52148-8_6

    Chapter  Google Scholar 

Download references

Acknowledgment

We thank Roderick Bloem, Markus Rabe and Leander Tentrup for comments on drafts of this paper. This work was supported by the Austrian Science Fund (FWF) through the RiSE project (S11406-N23, S11407-N23) and grant nr. P23499-N23, as well as by the German Research Foundation (DFG) through SFB/TR 14 AVACS and project ASDPS (JA 2357/2-1).

Author information

Authors and Affiliations

  1. IAIK, Graz University of Technology, Graz, Austria

    Simon Außerlechner & Ayrat Khalimov

  2. Reactive Systems Group, Saarland University, Saarbrücken, Germany

    Swen Jacobs

Authors
  1. Simon Außerlechner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Swen Jacobs
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ayrat Khalimov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Swen Jacobs .

Editor information

Editors and Affiliations

  1. EPFL IC-DO, Lausanne, Switzerland

    Barbara Jobstmann

  2. Microsoft Research, Redmond, Washington, USA

    K. Rustan M. Leino

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Außerlechner, S., Jacobs, S., Khalimov, A. (2016). Tight Cutoffs for Guarded Protocols with Fairness. In: Jobstmann, B., Leino, K. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2016. Lecture Notes in Computer Science(), vol 9583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-49122-5_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-49121-8

  • Online ISBN: 978-3-662-49122-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation