nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Promptness and Bounded Fairness in Concurrent and Parameterized Systems

verfasst von : Swen Jacobs, Mouhammad Sakr, Martin Zimmermann

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

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.

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 Language Inclusion for Finite Prime Event Structures

Nächstes Kapitel Solving Using Approximations

\({\text {Prompt-LTL}}\) can be seen as a fragment of parametric LTL, a logic introduced by Alur et al. [1]. However, since most decision problems for parametric LTL, including model checking, can be reduced to those for \({\text {Prompt-LTL}}\), we can restrict our attention to the simpler logic.

By similar arguments as in Emerson and Kahlon [14], our results can be extended to systems with an arbitrary (but fixed) number of process templates. The same holds for open process templates that can receive inputs from an environment, as considered by Außerlechner et al. [5].

This restriction has already been considered by Außerlechner et al. [5], and was necessary to support global fairness assumptions.

This is only slightly more restrictive than the assumption that they are initializing, as stated in the definition of conjunctive systems in Sect. 3.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). https://doi.org/10.1145/377978.377990MathSciNetCrossRefMATH

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

Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. Distrib. Comput. 31(3), 187–222 (2018). https://doi.org/10.1007/s00446-017-0302-6MathSciNetCrossRefMATH

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

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). https://doi.org/10.1007/978-3-662-49122-5_23CrossRef

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

Bloem, R., Jacobs, S., Khalimov, A.: Parameterized synthesis case study: AMBA AHB. In: SYNT. EPTCS, vol. 157, pp. 68–83 (2014). https://doi.org/10.4204/EPTCS.157.9MathSciNetCrossRef

Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2015). https://doi.org/10.2200/S00658ED1V01Y201508DCT013CrossRef

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). https://doi.org/10.1007/10722167_31CrossRef

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). https://doi.org/10.1007/978-3-540-28644-8_18CrossRef

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). https://doi.org/10.1007/978-3-540-78800-3_4CrossRefMATH

12.

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

13.

Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Found. Comput. Sci. 14(4), 527–549 (2003). https://doi.org/10.1142/S0129054103001881MathSciNetCrossRefMATH

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). https://doi.org/10.1007/10721959_19CrossRef

15.

Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS, pp. 352–359. IEEE Computer Society (1999). https://doi.org/10.1109/LICS.1999.782630

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). https://doi.org/10.4230/LIPIcs.STACS.2014.1

17.

Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. J. ACM 63(1), 10:1–10:48 (2016). https://doi.org/10.1145/2842603MathSciNetCrossRefMATH

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). https://doi.org/10.1007/3-540-48683-6_22CrossRef

19.

Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic. Inf. Comput. 253, 237–256 (2017). https://doi.org/10.1016/j.ic.2016.07.009MathSciNetCrossRefMATH

20.

German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992). https://doi.org/10.1145/146637.146681MathSciNetCrossRefMATH

21.

Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10, 1–29 (2014). https://doi.org/10.2168/LMCS-10(1:12)2014MathSciNetCrossRefMATH

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). https://doi.org/10.1007/978-3-319-73721-8_12CrossRef

23.

Jacobs, S., Sakr, M., Zimmermann, M.: Promptness and bounded fairness in concurrent and parameterized systems. CoRR abs/1911.03122 (2019). http://arxiv.org/abs/1911.03122

24.

Jacobs, S., Tentrup, L., Zimmermann, M.: Distributed synthesis for parameterized temporal logics. Inf. Comput. 262, 311–328 (2018). https://doi.org/10.1016/j.ic.2018.09.009MathSciNetCrossRefMATH

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). https://doi.org/10.1007/978-3-642-14295-6_55CrossRef

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). https://doi.org/10.1007/978-3-642-35873-9_9CrossRef

27.

Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods Syst. Des. 34(2), 83–103 (2009)CrossRef

28.

Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. Inf. Comput. 117(1), 1–11 (1995). https://doi.org/10.1006/inco.1995.1024MathSciNetCrossRefMATH

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). https://doi.org/10.1007/978-3-540-69738-1_22CrossRefMATH

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). https://doi.org/10.1007/3-540-45319-9_7CrossRef

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). https://doi.org/10.1007/978-3-319-12154-3_15CrossRef

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. CEUR-WS.org (2017)

33.

Suzuki, I.: Proving properties of a ring of finite state machines. Inf. Process. Lett. 28(4), 213–214 (1988). https://doi.org/10.1016/0020-0190(88)90211-6MathSciNetCrossRefMATH

34.

Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322–331. IEEE Computer Society (1986)

Titel: Promptness and Bounded Fairness in Concurrent and Parameterized Systems
verfasst von: Swen Jacobs
Mouhammad Sakr
Martin Zimmermann
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-39321-2

Electronic ISBN: 978-3-030-39322-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-39322-9_16

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"