nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

01.08.2016 | SPIN 2013

Efficient model-checking of weighted CTL with upper-bound constraints

verfasst von: Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiří Srba, Lars Kaerlund Oestergaard

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 4/2016

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We present a symbolic extension of dependency graphs by Liu and Smolka in to model-check weighted Kripke structures against the computation tree logic with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model-checking problem into dependency graphs. We implement all algorithms in a publicly available tool and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of “witnesses”.

Vorheriger Artikel Verifying a quantitative relaxation of linearizability via refinement

Nächster Artikel Guard-based partial-order reduction

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

Exponential in the encoding of the weights in the model and the formula.

A blocking WKS can be turned into a nonblocking one by introducing a new state with no atomic propositions, zero-weight self-loop and with zero-weight transitions from all blocking states into this newly introduced state.

At line 12 we added the assignment \(D(u) = \{ e \}\); the original algorithm sets the dependency set to empty here, leading to an incorrect propagation.

Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)MathSciNetCrossRefMATH

Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP, vol. 443 of LNCS, pp. 322–335. Springer, New York (1990)

Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)MathSciNetCrossRefMATH

Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC’01), vol. 2034 of LNCS, pp. 49–62. Springer, New York (2001)

Andersen, H.R.: Model checking and boolean graphs. Theor. Comput. Sci. 126(1), 3–30 (1994)CrossRefMATH

Kasahara Laboratory at Waseda University. Standard task graph set. http://www.kasahara.elec.waseda.ac.jp/schedule/

Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commun. ACM 12(5), 260–261 (1969)CrossRef

Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC’01), vol. 2034 of LNCS, pp. 147–161. Springer, New York (2001)

Bouyer, P., Larsen, K.G., Markey, N.: Model checking one-clock priced timed automata. Log. Methods Comput. Sci. 4(2) (2008)

10.

Brihaye, T., Bruyère, V., Raskin, J.-F.: Model-checking for weighted timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT, vol. 3253 of LNCS, pp. 277–292. Springer, New York (2004)

11.

Buchholz, P., Kemper, P.: Model checking for a class of weighted automata. Discret. Event Dyn. Syst. 20, 103–137 (2010)MathSciNetCrossRefMATH

12.

Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Proceedings of the 16th International Conference on Concurrency Theory CONCUR’05, vol. 3653 of LNCS, pp. 66–80. Springer, New York (2005)

13.

Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281–283 (1979)CrossRefMATH

14.

Droste, M., Gastin, P.: Weighted automata and weighted logics. Theor. Comput. Sci. 380(1–2), 69–86 (2007)MathSciNetCrossRefMATH

15.

Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata, 1st edn. Springer Publishing Company, Incorporated (2009)CrossRefMATH

16.

Knaster, B.: Un théorème sur les fonctions d’ensembles. Ann. de la Société Polonaise de Mathématique 6, 133–134 (1928)MATH

17.

Kwok, Y.-K., Ahmad, I.: Benchmarking and comparison of the task graph scheduling algorithms. J. Parallel Distrib. Comput. 59(3), 381–422 (1999)CrossRefMATH

18.

Laroussinie, F., Markey, N., Oreiby, G.: Model-checking timed ATL for durational concurrent game structures. In: Asarin, E., Bouyer, P. (eds.) FORMATS, vol. 4202 of LNCS, pp. 245–259. Springer, New York (2006)

19.

Liu, X., Ramakrishnan, C.R., Smolka, S.A.: Fully local and efficient evaluation of alternating fixed points. In: Tools and Algorithms for the Construction and Analysis of Systems. vol. 1384 of LNCS, pp. 5–19. Springer, Berlin (1998)

20.

Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points (extended abstract). In: Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP’98), vol. 1443 of LNCS, pp. 53–66. Springer, New York (1998)

21.

Martello, S., Toth, P.: Knapsack Problems: Algorithms and Computer Implementations. Wiley, New York (1990)MATH

22.

Milner, R.: A calculus of communicating systems. In: LNCS, vol. 92 (1980)

23.

Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)MathSciNetCrossRefMATH

Titel: Efficient model-checking of weighted CTL with upper-bound constraints
verfasst von: Jonas Finnemann Jensen
Kim Guldstrand Larsen
Jiří Srba
Lars Kaerlund Oestergaard
Publikationsdatum: 01.08.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 4/2016
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-014-0359-5

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"

Weitere Artikel der Ausgabe 4/2016

Guided search for hybrid systems based on coarse-grained space abstractions

Model checking unbounded concurrent lists

Preface of the special issue on Model Checking of Software

Guard-based partial-order reduction

Verifying a quantitative relaxation of linearizability via refinement

Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic