Skip to main content
SpringerLink
Log in

Model Verification Through Dependency Graphs

  • Conference paper
  • First Online:
Book cover Model Checking Software (SPIN 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11636))

Included in the following conference series:

Abstract

Dependency graphs, as introduced more than 20 years ago by Liu and Smolka, are oriented graphs with hyperedges that connect nodes with sets of target nodes in order to represent causal dependencies in the graph. Numerous verification problems can be reduced into the problem of computing a minimum or maximum fixed-point assignment on dependency graphs. In the original definition, assignments link each node with a Boolean value, however, in the recent work the assignment domains have been extended to more general setting, even including infinite domains. We present an overview of the recent results on extensions of dependency graphs in order to deal with verification of quantitative, probabilistic and timed systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://wktool.jonasfj.dk/.

  2. 2.

    http://caal.cs.aau.dk/.

References

  1. Algayres, B., Coelho, V., Doldi, L., Garavel, H., Lejeune, Y., Rodríguez, C.: VESAR: a pragmatic approach to formal specification and verification. Comput. Netw. ISDN Syst. 25(7), 779–790 (1993). https://doi.org/10.1016/0169-7552(93)90048-9

    Article  Google Scholar 

  2. Andersen, H.R.: Model checking and boolean graphs. In: Krieg-Brückner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 1–19. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55253-7_1

    Chapter  Google Scholar 

  3. Andersen, H.R., Winskel, G.: Compositional checking of satisfaction. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 24–36. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55179-4_4

    Chapter  Google Scholar 

  4. Andersen, J.R., et al.: CAAL: concurrency workbench, Aalborg edition. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 573–582. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_33

    Chapter  Google Scholar 

  5. Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press (2008)

    Google Scholar 

  6. Balcázar, J.L., Gabarró, J., Santha, M.: Deciding bisimilarity is P-complete. Formal Asp. Comput. 4(6A), 638–648 (1992)

    Article  Google Scholar 

  7. Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_14

    Chapter  Google Scholar 

  8. Bønneland, F.M., Jensen, P.G., Larsen, K.G., Muñiz, M., Srba, J.: Partial order reduction for reachability games. In: CONCUR 2019 (2019, to appear)

    Google Scholar 

  9. Børjesson, A., Larsen, K.G., Skou, A.: Generality in design and compositional verification using TAV. In: Diaz, M., Groz, R. (eds.) Formal Description Techniques, V, Proceedings of the IFIP TC6/WG6.1 Fifth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE 1992, Perros-Guirec, France, 13–16 October 1992. IFIP Transactions, vol. C-10, pp. 449–464. North-Holland (1992)

    Google Scholar 

  10. Bradfield, J.C., Stirling, C.: Local model checking for infinite state spaces. Theor. Comput. Sci. 96(1), 157–174 (1992). https://doi.org/10.1016/0304-3975(92)90183-G

    Article  MathSciNet  MATH  Google Scholar 

  11. 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., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). https://doi.org/10.1007/11539452_9

    Chapter  Google Scholar 

  12. Čerāns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification—theory and tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253–267. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56922-7_21

    Chapter  Google Scholar 

  13. Christoffersen, P., Hansen, M., Mariegaard, A., Ringsmose, J.T., Larsen, K.G., Mardare, R.: Parametric verification of weighted systems. In: André, É., Frehse, G. (eds.) 2nd International Workshop on Synthesis of Complex Parameters (SynCoP 2015). OpenAccess Series in Informatics (OASIcs), vol. 44, pp. 77–90. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2015). https://doi.org/10.4230/OASIcs.SynCoP.2015.77. http://drops.dagstuhl.de/opus/volltexte/2015/5611

  14. Claus Jensen, M., Mariegaard, A., Guldstrand Larsen, K.: Symbolic model checking of weighted PCTL using dependency graphs. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 298–315. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-20652-9_20

    Chapter  Google Scholar 

  15. Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 24–37. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_3

    Chapter  Google Scholar 

  16. Cleaveland, R., Steffen, B.: Computing behavioural relations, logically. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 127–138. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54233-7_129

    Chapter  Google Scholar 

  17. Dalsgaard, A., et al.: A distributed fixed-point algorithm for extended dependency graphs. Fundamenta Informaticae 161(4), 351–381 (2018). https://doi.org/10.3233/FI-2018-1707

    Article  MathSciNet  MATH  Google Scholar 

  18. Dalsgaard, A.E., et al.: Extended dependency graphs and efficient distributed fixed-point computation. In: van der Aalst, W., Best, E. (eds.) PETRI NETS 2017. LNCS, vol. 10258, pp. 139–158. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57861-3_10

    Chapter  Google Scholar 

  19. 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). https://doi.org/10.1007/978-3-319-47677-3_13

    Chapter  Google Scholar 

  20. 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). https://doi.org/10.1007/978-3-642-28756-5_36

    Chapter  MATH  Google Scholar 

  21. Enevoldsen, S., Guldstrand Larsen, K., Srba, J.: Abstract dependency graphs and their application to model checking. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 316–333. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_18

    Chapter  Google Scholar 

  22. Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039066

    Chapter  Google Scholar 

  23. Godskesen, J., Larsen, K., Zeeberg, M.: TAV (tools for automatic verification) - user manual. Aalborg University, Technical report (1989)

    Google Scholar 

  24. Groote, J.F., Willemse, T.: Parameterised Boolean equation systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 308–324. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_20

    Chapter  Google Scholar 

  25. Jensen, J., Larsen, K., Srba, J., Oestergaard, L.: Efficient model checking of weighted CTL with upper-bound constraints. Int. J. Softw. Tools Technol. Transfer (STTT) 18(4), 409–426 (2016). https://doi.org/10.1007/s10009-014-0359-5

    Article  Google Scholar 

  26. Jensen, J.F., Larsen, K.G., Srba, J., Oestergaard, L.K.: Local model checking of weighted CTL with upper-bound constraints. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 178–195. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39176-7_12

    Chapter  Google Scholar 

  27. Jensen, P.G., Larsen, K.G., Srba, J.: Discrete and continuous strategies for timed-arc petri net games. Int. J. Softw. Tools Technol. Transfer 20(5), 529–546 (2018). https://doi.org/10.1007/s10009-017-0473-2

    Article  Google Scholar 

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

    Chapter  Google Scholar 

  29. Larsen, K.G.: Proof systems for Hennessy-Milner Logic with recursion. In: Dauchet, M., Nivat, M. (eds.) CAAP 1988. LNCS, vol. 299, pp. 215–230. Springer, Heidelberg (1988). https://doi.org/10.1007/BFb0026106

    Chapter  Google Scholar 

  30. Larsen, K.G.: Proof systems for satisfiability in hennessy-milner logic with recursion. Theor. Comput. Sci. 72(2&3), 265–288 (1990). https://doi.org/10.1016/0304-3975(90)90038-J

    Article  MathSciNet  MATH  Google Scholar 

  31. Larsen, K.G.: Efficient local correctness checking. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 30–43. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56496-9_4

    Chapter  Google Scholar 

  32. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1–2), 134–152 (1997). https://doi.org/10.1007/s100090050010

    Article  MATH  Google Scholar 

  33. Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53–66. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055040

    Chapter  Google Scholar 

  34. Mariegaard, A., Larsen, K.G.: Symbolic dependency graphs for \({\rm PCTL}^{>}_{\le }\) model-checking. In: Abate, A., Geeraerts, G. (eds.) FORMATS 2017. LNCS, vol. 10419, pp. 153–169. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-65765-3_9

    Chapter  Google Scholar 

  35. Mateescu, R.: Efficient diagnostic generation for Boolean equation systems. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 251–265. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_18

    Chapter  MATH  Google Scholar 

  36. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10235-3

    Book  MATH  Google Scholar 

  37. Steffen, B.: Characteristic formulae. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 723–732. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0035794

    Chapter  Google Scholar 

  38. Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. Theor. Comput. Sci. 89(1), 161–177 (1991). https://doi.org/10.1016/0304-3975(90)90110-4

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  40. Winskel, G.: A note on model checking the modal \(\upnu \)-calculus. Theor. Comput. Sci. 83(1), 157–167 (1991). https://doi.org/10.1016/0304-3975(91)90043-2

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

We would like to thank to Hubert Garavel and Radu Mateescu for sharing the French history of on-the-fly model checking with us. The last author is partially affiliated with FI MU. The work of the second author has taken place in the context of the ERC Advanced Grant LASSO.

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Selma Lagerlofs Vej 300, 9220, Aalborg East, Denmark

    Søren Enevoldsen, Kim Guldstrand Larsen & Jiří Srba

Authors
  1. Søren Enevoldsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jiří Srba
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jiří Srba .

Editor information

Editors and Affiliations

  1. Avast Software, Prague, Czech Republic

    Fabrizio Biondi

  2. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Thomas Given-Wilson

  3. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Axel Legay

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Enevoldsen, S., Guldstrand Larsen, K., Srba, J. (2019). Model Verification Through Dependency Graphs. In: Biondi, F., Given-Wilson, T., Legay, A. (eds) Model Checking Software. SPIN 2019. Lecture Notes in Computer Science(), vol 11636. Springer, Cham. https://doi.org/10.1007/978-3-030-30923-7_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30923-7_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30922-0

  • Online ISBN: 978-3-030-30923-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation