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:
Verified Compilation of Space-Efficient Reversible Circuits Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems

Authors : Marie Fortin, Anca Muscholl, Igor Walukiewicz

Published in: Computer Aided Verification

Publisher: Springer International Publishing

Log in

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

search-config
loading …

Abstract

A parametrized verification problem asks if a parallel composition of a leader process with some number of copies of a contributor process can exhibit a behavior satisfying a given property. We focus on the case of pushdown processes communicating via shared memory. In a series of recent papers it has been shown that reachability in this model is Pspace-complete [Hague’11], [Esparza, Ganty, Majumdar’13], and that liveness is decidable in Nexptime [Durand-Gasselin, Esparza, Ganty, Majumdar’15]. We show that verification of general regular properties of traces of executions, satisfying some stuttering condition, is Nexptime-complete for this model. We also study two interesting subcases of this problem: we show that liveness is actually Pspace-complete, and that safety is already Nexptime-complete.

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 Efficient Parallel Strategy Improvement for Parity Games
next chapter Minimization of Symbolic Transducers
Footnotes
1
By abuse of language we call them \(\omega \)-regular although they may contain finite and infinite sequences.
 
Literature
1.
Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci. 7(4), 1–48 (2011)MathSciNetCrossRefMATH
2.
Ball, T., Chaki, S., Rajamani, S.K.: Parameterized verification of multithreaded software libraries. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 158–173. Springer, Heidelberg (2001). doi:10.​1007/​3-540-45319-9_​12 CrossRef
3.
Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Morgan & Claypool Publishers, San Rafael (2015)
4.
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). doi:10.​1007/​3-540-63141-0_​10
5.
Bouajjani, A., Esparza, J., Schwoon, S., Strejĉek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 348–359. Springer, Heidelberg (2005). doi:10.​1007/​11590156_​28 CrossRef
6.
Bouajjani, A., Müller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 473–487. Springer, Heidelberg (2005). doi:10.​1007/​11539452_​36 CrossRef
7.
Bouyer, P., Markey, N., Randour, M., Sangnier, A., Stan, D.: Reachability in networks of register protocols under stochastic schedulers. In: ICALP 2016, LIPIcs, pp. 106:1–106:14. Leibniz-Zentrum für Informatik (2016)
8.
9.
Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. ACM Trans. Program. Lang. Syst. 19(5), 726–750 (1997)CrossRef
10.
Courcelle, B.: On constructing obstruction sets of words. Bull. EATCS 44, 178–186 (1991)MATH
11.
Delzanno, G.: Parameterized verification and model checking for distributed broadcast protocols. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 1–16. Springer, Cham (2014). doi:10.​1007/​978-3-319-09108-2_​1
12.
Durand-Gasselin, A., Esparza, J., Ganty, P., Majumdar, R.: Model checking parameterized asynchronous shared-memory systems. Form. Methods Syst. Des. 50(2–3), 140–167 (2017). Journal version of CAV 2015CrossRefMATH
13.
Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS 2003, pp. 361–370 (2003)
14.
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352–359. IEEE (1999)
15.
Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. J. ACM 63(1), 10:1–10:48 (2016). Journal version of CAV 2013MathSciNetCrossRef
16.
17.
Fortin, M., Muscholl, A., Walukiewicz, I.: On parametrized verification of asynchronous, shared-memory pushdown systems. CoRR, abs/1606.08707 (2016)
18.
Fürer, M.: The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In: Börger, E., Hasenjaeger, G., Rödding, D. (eds.) LaM 1983. LNCS, vol. 171, pp. 312–319. Springer, Heidelberg (1984). doi:10.​1007/​3-540-13331-3_​48 CrossRef
19.
20.
Hague, M.: Parameterised pushdown systems with non-atomic writes. In: FSTTCS 2011. LIPIcs, pp. 457–468. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)
21.
Kahlon, V.: Parameterization as abstraction: a tractable approach to the dataflow analysis of concurrent programs. In: LICS 2008, pp. 181–192. IEEE (2008)
22.
Kahlon, V., Ivančić, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 505–518. Springer, Heidelberg (2005). doi:10.​1007/​11513988_​49 CrossRef
23.
Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645–659. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14295-6_​55 CrossRef
24.
Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.: Network invariants in action*. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45694-5_​8 CrossRef
25.
La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 629–644. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14295-6_​54 CrossRef
26.
La Torre, S., Madhusudan, P., Parlato, G.: Sequentializing parameterized programs. In: FIT 2012. EPTCS, vol. 87, pp. 34–47 (2012)
27.
La Torre, S., Muscholl, A., Walukiewicz, I.: Safety of parametrized asynchronous shared-memory systems is almost always decidable. In: CONCUR 2015. LIPIcs, vol. 42, pp. 72–84. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)
28.
Lammich, P., Müller-Olm, M.: Conflict analysis of programs with procedures, dynamic thread creation, and monitors. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 205–220. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-69166-2_​14 CrossRef
29.
Lammich, P., Müller-Olm, M., Seidl, H., Wenner, A.: Contextual locking for dynamic pushdown networks. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 477–498. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-38856-9_​25 CrossRef
30.
Lammich, P., Müller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 525–539. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02658-4_​39 CrossRef
31.
Lin, A.W., Rümmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 112–133. Springer, Cham (2016). doi:10.​1007/​978-3-319-41540-6_​7
32.
33.
Namjoshi, K.S., Trefler, R.J.: Analysis of dynamic process networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 164–178. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​11
34.
Peled, D.A., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Process. Lett. 63(5), 243–246 (1997)MathSciNetCrossRefMATH
35.
Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. (TOPLAS) 22(2), 416–430 (2000)CrossRef
Metadata
Title
Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems
Authors
Marie Fortin
Anca Muscholl
Igor Walukiewicz
Copyright Year
2017
Book
Computer Aided Verification

Print ISBN: 978-3-319-63389-3

Electronic ISBN: 978-3-319-63390-9

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63390-9_9

Premium Partner

    Image Credits