Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Robots at the Edge of the Cloud Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Approaching the Coverability Problem Continuously

Authors : Michael Blondin, Alain Finkel, Christoph Haase, Serge Haddad

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

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets)
next chapter On Atomicity in Presence of Non-atomic Writes
Footnotes
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}})\).
 
Literature
1.
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.
Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously (2015). CoRR, abs/​1510.​05724
3.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundam. Informaticae 137(1), 1–28 (2015)MathSciNetMATH
15.
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.
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.
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.
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
19.
20.
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.
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.
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.
Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: Logic in Computer Science, LICS, pp. 56–67. IEEE (2015)
24.
25.
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
26.
27.
Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. Fundam. Inform. 131(1), 1–25 (2014)MathSciNetMATH
28.
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
Metadata
Title
Approaching the Coverability Problem Continuously
Authors
Michael Blondin
Alain Finkel
Christoph Haase
Serge Haddad
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Tools and Algorithms for the Construction and Analysis of Systems

Print ISBN: 978-3-662-49673-2

Electronic ISBN: 978-3-662-49674-9

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-662-49674-9_28

Premium Partner

    Image Credits