Skip to main content

2016 | OriginalPaper | Buchkapitel

Approaching the Coverability Problem Continuously

verfasst von : Michael Blondin, Alain Finkel, Christoph Haase, Serge Haddad

Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems

Verlag: Springer Berlin Heidelberg

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

search-config
loading …

Abstract

The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward-coverability framework. A cornerstone of our approach is the efficient encoding of a recently developed polynomial-time algorithm for reachability in continuous Petri nets into SMT. We demonstrate the effectiveness of our approach on standard benchmarks from the literature, which shows that our approach decides significantly more instances than any existing tool and is in addition often much faster, in particular on large instances.

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!

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!

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!

Fußnoten
1
This problem is commonly referred to as the symbolic state explosion problem, cf. [8].
 
2
In fact, the original definition allows for real numbers, however for studying decidability and complexity issues, rational numbers are more convenient.
 
3
In [14, Corollary 19], an algorithm is presented that basically computes \({{\mathrm{lfp}}}({ incfs }_{\mathcal {N}_{T'}, \varvec{w}})\).
 
Literatur
1.
Zurück zum Zitat Cerans, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1–2), 109–127 (2000)MathSciNetMATH Cerans, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1–2), 109–127 (2000)MathSciNetMATH
2.
Zurück zum Zitat Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously (2015). CoRR, abs/1510.05724 Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously (2015). CoRR, abs/​1510.​05724
3.
Zurück zum Zitat Bozzelli, L., Ganty, P.: Complexity analysis of the backward coverability algorithm for VASS. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 96–109. Springer, Heidelberg (2011)CrossRef Bozzelli, L., Ganty, P.: Complexity analysis of the backward coverability algorithm for VASS. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 96–109. Springer, Heidelberg (2011)CrossRef
4.
Zurück zum Zitat Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets, commutative semigroups: preliminary report. In: Symposium on Theory of Computing, STOC, pp. 50–54 (1976) Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets, commutative semigroups: preliminary report. In: Symposium on Theory of Computing, STOC, pp. 50–54 (1976)
5.
Zurück zum Zitat David, R., Alla, H.: Continuous Petri nets. In: Proceedings of the 8th European Workshop on Application and Theory of Petri nets, pp. 275–294 (1987) David, R., Alla, H.: Continuous Petri nets. In: Proceedings of the 8th European Workshop on Application and Theory of Petri nets, pp. 275–294 (1987)
6.
Zurück zum Zitat de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRef de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRef
7.
Zurück zum Zitat Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking symbolic state explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 298. Springer, Heidelberg (2001)CrossRef Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking symbolic state explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 298. Springer, Heidelberg (2001)CrossRef
8.
Zurück zum Zitat Delzanno, G., Raskin, J.-F., Van Begin, L.: Covering sharing trees: a compact data structure for parameterized verification. STTT 5(2–3), 268–297 (2004)CrossRef Delzanno, G., Raskin, J.-F., Van Begin, L.: Covering sharing trees: a compact data structure for parameterized verification. STTT 5(2–3), 268–297 (2004)CrossRef
9.
Zurück zum Zitat D’Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of erlang-style concurrency. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 454–476. Springer, Heidelberg (2013)CrossRef D’Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of erlang-style concurrency. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 454–476. Springer, Heidelberg (2013)CrossRef
10.
Zurück zum Zitat Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An SMT-based approach to coverability analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 603–619. Springer, Heidelberg (2014) Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An SMT-based approach to coverability analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 603–619. Springer, Heidelberg (2014)
11.
Zurück zum Zitat Esparza, J., Melzer, S.: Verification of safety properties using integer programming: beyond the state equation. Formal Meth. Syst. Des. 16(2), 159–189 (2000)CrossRef Esparza, J., Melzer, S.: Verification of safety properties using integer programming: beyond the state equation. Formal Meth. Syst. Des. 16(2), 159–189 (2000)CrossRef
12.
Zurück zum Zitat Finkel, A., Raskin, J.-F., Samuelides, M., Van Begin, L.: Monotonic extensions of Petri nets: forward and backward search revisited. Electr. Notes Theor. Comput. Sci. 68(6), 85–106 (2002)CrossRefMATH Finkel, A., Raskin, J.-F., Samuelides, M., Van Begin, L.: Monotonic extensions of Petri nets: forward and backward search revisited. Electr. Notes Theor. Comput. Sci. 68(6), 85–106 (2002)CrossRefMATH
13.
14.
Zurück zum Zitat Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundam. Informaticae 137(1), 1–28 (2015)MathSciNetMATH Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundam. Informaticae 137(1), 1–28 (2015)MathSciNetMATH
15.
Zurück zum Zitat Ganty, P.: Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles (in French). Master’s thesis, Université Libre de Bruxelles, Belgium (2002) Ganty, P.: Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles (in French). Master’s thesis, Université Libre de Bruxelles, Belgium (2002)
16.
Zurück zum Zitat Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J.-F., Van Begin, L.: Symbolic data structure for sets of \(k\)-uples. Technical report 570, Université Libre de Bruxelles, Belgium (2007) Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J.-F., Van Begin, L.: Symbolic data structure for sets of \(k\)-uples. Technical report 570, Université Libre de Bruxelles, Belgium (2007)
17.
Zurück zum Zitat Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)MathSciNetCrossRefMATH Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)MathSciNetCrossRefMATH
18.
Zurück zum Zitat Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the efficient computation of the minimal coverability set of petri nets. Int. J. Found. Comput. Sci. 21(2), 135–165 (2010)MathSciNetCrossRefMATH Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the efficient computation of the minimal coverability set of petri nets. Int. J. Found. Comput. Sci. 21(2), 135–165 (2010)MathSciNetCrossRefMATH
20.
Zurück zum Zitat Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36(4), 1–29 (2014)CrossRef Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36(4), 1–29 (2014)CrossRef
21.
Zurück zum Zitat Karp, R.M., Miller, R.E.: Parallel program schemata: a mathematical model for parallel computation. In Switching and Automata Theory, pp. 55–61. IEEE Computer Society (1967) Karp, R.M., Miller, R.E.: Parallel program schemata: a mathematical model for parallel computation. In Switching and Automata Theory, pp. 55–61. IEEE Computer Society (1967)
22.
Zurück zum Zitat Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 158–173. Springer, Heidelberg (2013)CrossRef Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 158–173. Springer, Heidelberg (2013)CrossRef
23.
Zurück zum Zitat Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: Logic in Computer Science, LICS, pp. 56–67. IEEE (2015) Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: Logic in Computer Science, LICS, pp. 56–67. IEEE (2015)
24.
25.
Zurück zum Zitat Reynier, P.-A., Servais, F.: Minimal coverability set for petri nets: karp and miller algorithm with pruning. Fundam. Inform. 122(1–2), 1–30 (2013)MathSciNetMATH Reynier, P.-A., Servais, F.: Minimal coverability set for petri nets: karp and miller algorithm with pruning. Fundam. Inform. 122(1–2), 1–30 (2013)MathSciNetMATH
27.
Zurück zum Zitat Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. Fundam. Inform. 131(1), 1–25 (2014)MathSciNetMATH Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. Fundam. Inform. 131(1), 1–25 (2014)MathSciNetMATH
28.
Zurück zum Zitat Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 337–352. Springer, Heidelberg (2005)CrossRef Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 337–352. Springer, Heidelberg (2005)CrossRef
Metadaten
Titel
Approaching the Coverability Problem Continuously
verfasst von
Michael Blondin
Alain Finkel
Christoph Haase
Serge Haddad
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-49674-9_28