A Distributed Fixed-Point Algorithm for Extended Dependency Graphs

• Autorzy: Dalsgaard A. E. , Enevoldsen S. , Fogh P. , Jensen L. S. , Jensen P. G. , Jepsen T. S. , Kaufmann I. , Larsen K. G. , Nielsen S. M. , Olesen M. C. , Pastva S. , Srba J.

Identyfikatory

DOI

10.3233/FI-2018-1707

• Konferencja: International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (Petri Nets 2017) (31; School of Engineering and Architecture of Zaragoza University; 25.30.07.2017; Spain)
• Języki publikacji: EN

Abstrakty

EN

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 our open-source tool TAPAAL, and demonstrate the efficiency of our general approach on the benchmark of Petri net models and CTL queries from the annual Model Checking Contest.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 161, nr 4
• Strony: 351--381
• Opis fizyczny: Bibliogr. 35 poz., rys., tab.

Twórcy

autor

Dalsgaard A. E.

• Department of Computer Science, Aalborg University, Denmark

autor

Enevoldsen S.

• Department of Computer Science, Aalborg University, Denmark

autor

Fogh P.

• Department of Computer Science, Aalborg University, Denmark

autor

Jensen L. S.

• Department of Computer Science, Aalborg University, Denmark

autor

Jensen P. G.

• Department of Computer Science, Aalborg University, Denmark

autor

Jepsen T. S.

• Department of Computer Science, Aalborg University, Denmark

autor

Kaufmann I.

• Department of Computer Science, Aalborg University, Denmark

autor

Larsen K. G.

• Department of Computer Science, Aalborg University, Denmark

autor

Nielsen S. M.

• Department of Computer Science, Aalborg University, Denmark

autor

Olesen M. C.

• Department of Computer Science, Aalborg University, Denmark

autor

Pastva S.

• Faculty of Informatics, Masaryk University, Czech Republic

autor

Srba J.

• Department of Computer Science, Aalborg University, Denmark

Bibliografia

• [1] Dalsgaard AE, Enevoldsen S, Fogh P, Jensen L, Jepsen TS, Kaufmann I, Larsen KG, Nielsen SM, Olesen MC, Pastva S, Srba J. Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation. In: Proceedings of Petri Nets’17, volume 10258 of LNCS. Springer-Verlag, 2017 pp. 139-158. doi:10.1007/978-3-319-57861-3_10.
• [2] Clarke EM, Emerson EA, Sifakis J. Model checking: algorithmic verification and debugging. Commun. ACM, 2009. 52(11):74-84. doi:10.1145/1592761.1592781.
• [3] Clarke E, Grumberg O, Jha S, Lu Y, Veith H. Informatics: 10 Years Back, 10 Years Ahead, volume 2000 of LNCS, chapter Progress on the State Explosion Problem in Model Checking, pp. 176-194. Springer, Berlin, Heidelberg, 2001. doi:10.1007/3-540-44577-3_12.
• [4] Kant G, Laarman A, Meijer J, van de Pol J, Blom S, van Dijk T. LTSmin: High-Performance Language-Independent Model Checking. In: TACAS 2015, volume 9035 of LNCS. Springer, 2015 pp. 692-707. doi:10.1007/978-3-662-46681-0_61.
• [5] Barnat J, Brim L, Havel V, Havlíček J, Kriho J, Lenčo M, Ročkai P, Štill V, Weiser J. DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs. In: Computer Aided Verification (CAV’13), volume 8044 of LNCS. Springer, 2013 pp. 863-868. doi:10.1007/978-3-642-39799-8_60.
• [6] Liu X, Smolka SA. Simple Linear-Time Algorithms for Minimal Fixed Points. In: ICALP’98, volume 1443 of LNCS. Springer, 1998 pp. 53-66. doi:10.1007/BFb0055040.
• [7] Jensen JF, Larsen KG, Srba J, Oestergaard LK. Efficient Model Checking of Weighted CTL with Upper-Bound Constraints. STTT, 2016. 18(4):409-426. doi:10.1007/s10009-014-0359-5.
• [8] Keiren JJA. Advanced Reduction Techniques for Model Checking. Ph.D. thesis, Eindhoven University of Technology, 2013. doi:10.6100/IR757862.
• [9] Christoffersen P, Hansen M, Mariegaard A, Ringsmose JT, Larsen KG, Mardare R. Parametric Verification of Weighted Systems. In: André É, Frehse G (eds.), SynCoP’15, volume 44 of OASIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2015 pp. 77-90. doi:10.4230/OASIcs.SynCoP.2015.77.
• [10] Clarke EM, Emerson EA. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In: Logic of Programs, Workshop. Springer, London, UK, 1982 pp. 52-71. doi:10.1007/BFb0025774.
• [11] Kozen D. Results on the propositional μ-calculus. In: ICALP’82, volume 140 of LNCS. Springer, Berlin, Heidelberg, 1982 pp. 348-359. doi:10.1007/BFb0012782.
• [12] Dalsgaard AE, Enevoldsen S, Larsen KG, Srba J. Distributed Computation of Fixed Points on Dependency Graphs. In: SETTA’16, volume 9984 of LNCS. Springer, 2016 pp. 197-212. doi:10.1007/978-3-319-47677-3_13.
• [13] Cassez F, David A, Fleury E, Larsen KG, Lime D. Efficient on-the-fly algorithms for the analysis of timed games. In: CONCUR’05, volume 3653 of LNCS. Springer, 2005 pp. 66-80. doi:10.1007/11539452_9.
• [14] Keinänen M. Techniques for Solving Boolean Equation Systems. Research Report A105, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2006. Doctoral dissertation.
• [15] Greenlaw R, Hoover HJ, Ruzzo WL. Limits to parallel computation: P-completeness theory, volume 200. Oxford University Press, Inc., New York, NY, USA, 1995.
• [16] David A, Jacobsen L, Jacobsen M, Jørgensen K, Møller M, Srba J. TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets. In: TACAS’12, volume 7214 of LNCS. Springer, 2012 pp. 492-497. doi:10.1007/978-3-642-28756-5_36.
• [17] Jensen J, Nielsen T, Oestergaard L, Srba J. TAPAAL and Reachability Analysis of P/T Nets. LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), 2016. 9930:307-318. doi:10.1007/978-3-662-53401-4_16.
• [18] Kordon F, Garavel H, Hillah LM, 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, Trįnh G, Wolf K. Complete Results for the 2016 Edition of the Model Checking Contest, 2016. URL http://mcc.lip6.fr/2016/results.php.
• [19] Wolf K. Running LoLA 2.0 in a Model Checking Competition, volume 9930 of LNCS, pp. 274-285. Springer, 2016. doi:10.1007/978-3-662-53401-4_13.
• [20] Brim L, Crhova J, Yorav K. Using Assumptions to Distribute CTL Model Checking. ENTCS, 2002. 68(4):559-574. doi:10.1016/S1571-0661(05)80758-3.
• [21] Bellettini C, Camilli M, Capra L, Monga M. Distributed CTL model checking in the cloud. arXiv preprint arXiv:1310.6670, 2013. doi:10.1109/SYNASC.2014.52.
• [22] Kordon F, Garavel H, Hillah LM, Hulin-Hubard F, Berthomieu B, Ciardo G, Colange M, Dal Zilio S, Amparore E, Beccuti M, Liebke T, Meijer J, Miner A, Rohr C, Srba J, Thierry-Mieg Y, van de Pol J, Wolf K. Complete Results for the 2017 Edition of the Model Checking Contest, 2017. URL http://mcc.lip6.fr/2017/results.php.
• [23] Heiner M, Rohr C, Schwarick M. MARCIE-model checking and reachability analysis done efficiently. In: Petri Nets’13, volume 7927 of LNCS, pp. 389-399. Springer, 2013. doi:10.1007/978-3-642-38697-8_21.
• [24] Kordon F, Garavel H, Hillah LM, 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 2015 Edition of the Model Checking Contest, 2015. URL http://mcc.lip6.fr/2015/results.php.
• [25] Thierry-Mieg Y. Symbolic Model-Checking Using ITS-Tools. In: Proceedings of TACAS’15, volume 9035 of LNCS. Springer, 2015 pp. 231-237. doi:10.1007/978-3-662-46681-0_20.
• [26] Bollig B, Leucker M, Weber M. SPIN’02, volume 2318 of LNCS, chapter Local Parallel Model Checking for the Alternation-Free µ-Calculus, pp. 128-147. Springer. ISBN 978-3-540-46017-6, 2002. doi:10.1007/3-540-46017-9_11.
• [27] Grumberg O, Heyman T, Schuster A. Distributed Symbolic Model Checking for µ-Calculus. Formal Methods in System Design, 2005. 26(2):197-219. doi:10.1007/s10703-005-1493-1.
• [28] Joubert C, Mateescu R. Distributed On-the-Fly Model Checking and Test Case Generation. In: SPIN’06, volume 3925 of LNCS. Springer, 2006 pp. 126-145. doi:10.1007/11691617_8.
• [29] Tan L, Cleaveland R. Evidence-Based Model Checking. In: International Conference on Computer Aided Verification (CAV’02), volume 2404 of LNCS. Springer, 2002 pp. 455-470. doi:10.1007/3-540-45657-0_37.
• [30] Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe A. FDR3—A Modern Refinement Checker for CSP. In: TACAS’14, volume 8413 of LNCS. Springer, 2014 pp. 187-201. doi:10.1007/978-3-642-54862-8_13.
• [31] Garavel H, Lang F, Mateescu R, Serwe W. CADP 2011: A toolbox for the construction and analysis of distributed processes. STTT, 2013. 15(2):89-107. doi:10.1007/s10009-012-0244-z.
• [32] Holzmann G. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, first edition, 2003. ISBN 0-321-22862-6.
• [33] Groote J, Mousavi M. Modeling and Analysis of Communicating Systems. The MIT Press, 2014.
• [34] Esparza J. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 1997. 34(2):85-107. doi:10.1007/s002360050074.
• [35] Jensen PG, Larsen KG, Srba J. PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing. In: Proceedings of the 14th International Colloquium on Theoretical Aspects of Computing (ICTAC’17), volume 10580 of LNCS. Springer, 2017 pp. 248-265. doi:10.1007/978-3-319-67729-3_15.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).