nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Tight Cutoffs for Guarded Protocols with Fairness

verfasst von : Simon Außerlechner, Swen Jacobs, Ayrat Khalimov

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Regular Symmetry Patterns

Nächstes Kapitel A General Modular Synthesis Problem for Pushdown Systems

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.

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.

“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'\).

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.

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.

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 CrossRef

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 CrossRef

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

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

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

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

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 MATHCrossRef

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 CrossRef

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) CrossRef

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) CrossRef

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 MATHCrossRef

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) CrossRef

13.

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

14.

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

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 CrossRef

16.

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

17.

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

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 CrossRef

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 CrossRef

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) CrossRef

21.

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

22.

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

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 CrossRef

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 CrossRef

25.

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

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 CrossRef

Titel: Tight Cutoffs for Guarded Protocols with Fairness
verfasst von: Simon Außerlechner
Swen Jacobs
Ayrat Khalimov
Verlag: Springer Berlin Heidelberg
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-662-49121-8

Electronic ISBN: 978-3-662-49122-5

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-662-49122-5_23

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner