nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation

verfasst von : Andreas E. Dalsgaard, Søren Enevoldsen, Peter Fogh, Lasse S. Jensen, Tobias S. Jepsen, Isabella Kaufmann, Kim G. Larsen, Søren M. Nielsen, Mads Chr. Olesen, Samuel Pastva, Jiří Srba

Erschienen in: Application and Theory of Petri Nets and Concurrency

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

Equivalence and model checking problems can be encoded into computing fixed points on dependency graphs. Dependency graphs represent causal dependencies among the nodes of the graph by means of hyper-edges. We suggest to extend the model of dependency graphs with so-called negation edges in order to increase their applicability. The graphs (as well as the verification problems) suffer from the state space explosion problem. To combat this issue, we design an on-the-fly algorithm for efficiently computing fixed points on extended dependency graphs. Our algorithm supplements previous approaches with the possibility to back-propagate, in certain scenarios, the domain value 0, in addition to the standard back-propagation of the value 1. Finally, we design a distributed version of the algorithm, implement it in an open-source tool, and demonstrate the efficiency of our general approach on the benchmark of Petri net models and CTL queries from the Model Checking Contest 2016.

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 Petri Nets Repository: A Tool to Benchmark and Debug Petri Net Tools

Nächstes Kapitel Model Checking Concurrency and Causality

The organizers of MCC’17 allow the tools to utilize 4 cores in the competition.

Barnat J. et al.: DiVinE 3.0 – an explicit-state model checker for multithreaded C & C++ programs. In: Sharygina N., Veith H. (eds) CAV 2013. LNCS, vol 8044, pp. 863–868. Springer, Heidelberg (2013)

Bellettini, C., Camilli, M., Capra, L., Monga, M.: Distributed CTL model checking in the cloud. arXiv preprint arXiv:1310.6670 (2013)

Bollig, B., Leucker, M., Weber, M.: Local parallel model checking for the alternation-free \(\mu \)-calculus. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 128–147. Springer, Heidelberg (2002). doi:10.1007/3-540-46017-9_11 CrossRef

Brim, L., Crhova, J., Yorav, K.: Using assumptions to distribute CTL model checking. ENTCS 68(4), 559–574 (2002)MATH

Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). doi:10.1007/11539452_9 CrossRef

Christoffersen, P., Hansen, M., Mariegaard, A., Ringsmose, J.T., Larsen, K.G., Mardare, R.: Parametric verification of weighted systems. In: SynCoP 2015, vol. 44, pp. 77–90. OASIcs, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Wilhelm, R. (ed.) Informatics. LNCS, vol. 2000, pp. 176–194. Springer, Heidelberg (2001). doi:10.1007/3-540-44577-3_12 CrossRef

Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.1007/BFb0025774 CrossRef

Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74–84 (2009)CrossRef

10.

Dalsgaard, A.E., Enevoldsen, S., Larsen, K.G., Srba, J.: Distributed computation of fixed points on dependency graphs. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 197–212. Springer, Cham (2016). doi:10.1007/978-3-319-47677-3_13 CrossRef

11.

David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K.Y., Møller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc Petri nets. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492–497. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_36 CrossRef

12.

Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 34(2), 85–107 (1997)MathSciNetCrossRefMATH

13.

Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89–107 (2013)CrossRefMATH

14.

Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_13 CrossRef

15.

Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallel Computation: P-Completeness Theory, vol. 200. Oxford University Press Inc, New York (1995)MATH

16.

Groote, J., Mousavi, M.: Modeling and Analysis of Communicating Systems. The MIT Press, Cambridge (2014)MATH

17.

Grumberg, O., Heyman, T., Schuster, A.: Distributed symbolic model checking for \(\mu \)-calculus. Formal Methods Syst. Des. 26(2), 197–219 (2005)CrossRefMATH

18.

Heiner, M., Rohr, C., Schwarick, M.: MARCIE – model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389–399. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38697-8_21 CrossRef

19.

Holzmann, G.: Spin Model Checker, the: Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)

20.

Jensen, J., Larsen, K., Srba, J., Oestergaard, L.: Efficient model checking of weighted CTL with upper-bound constraints. STTT 18(4), 409–426 (2016)CrossRef

21.

Jensen, J.F., Nielsen, T., Oestergaard, L.K., Srba, J.: TAPAAL and reachability analysis of P/T nets. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 307–318. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53401-4_16 CrossRef

22.

Joubert, C., Mateescu, R.: Distributed on-the-fly model checking and test case generation. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 126–145. Springer, Heidelberg (2006). doi:10.1007/11691617_8 CrossRef

23.

Kant, G., Laarman, A., Meijer, J., Pol, J., Blom, S., Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_61

24.

Keinänen, M.: Techniques for solving boolean equation systems. Research Report A105, Doctoral dissertation, Laboratory for Theoretical Computer Science, Helsinki University of Technology, pp. xii+95 (2006)

25.

Keiren, J.J.A.: Advanced reduction techniques for model checking. Ph.D. thesis, Eindhoven University of Technology (2013)

26.

Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A., Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Trinh, G., Wolf, K.: Complete results for the 2016th edition of the model checking contest. http://mcc.lip6.fr/2016/results.php

27.

Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Linard, A., Beccuti, M., Hamez, A., Lopez-Bobeda, E., Jezequel, L., Meijer, J., Paviot-Adet, E., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Wolf, K.: Complete results for the 2015th edition of the model checking contest (2015)

28.

Kozen, D.: Results on the propositional \(\mu \)-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982). doi:10.1007/BFb0012782 CrossRef

29.

Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: ICALP 1998. LNCS, vol. 1443, pp. 53–66. Springer, Heidelberg (1998)

30.

Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455–470. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_37 CrossRef

31.

Wolf, K.: Running LoLA 2.0 in a model checking competition. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 274–285. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53401-4_13 CrossRef

Titel: Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation
verfasst von: Andreas E. Dalsgaard
Søren Enevoldsen
Peter Fogh
Lasse S. Jensen
Tobias S. Jepsen
Isabella Kaufmann
Kim G. Larsen
Søren M. Nielsen
Mads Chr. Olesen
Samuel Pastva
Jiří Srba
Verlag: Springer International Publishing
Buch: Application and Theory of Petri Nets and Concurrency
Print ISBN: 978-3-319-57860-6

Electronic ISBN: 978-3-319-57861-3

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-57861-3_10

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"