Skip to main content
SpringerLink
Log in
Book cover

International Conference on Concurrency Theory

CONCUR 2013: CONCUR 2013 – Concurrency Theory pp 5–24Cite as

The Power of Well-Structured Systems

  • Conference paper

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

Abstract

Well-structured systems, aka WSTS, are computational models where the set of possible configurations is equipped with a well-quasi-ordering which is compatible with the transition relation between configurations. This structure supports generic decidability results that are important in verification and several other fields.

This paper recalls the basic theory underlying well-structured systems and shows how two classic decision algorithms can be formulated as an exhaustive search for some “bad” sequences. This lets us describe new powerful techniques for the complexity analysis of WSTS algorithms. Recently, these techniques have been successful in precisely characterizing the power, in a complexity-theoretical sense, of several important WSTS models like unreliable channel systems, monotonic counter machines, or networks of timed systems.

Work supported by the ReacHard project, ANR grant 11-BS02-001-01.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bull. Symbolic Logic 16(4), 457–515 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  2. Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasi-ordered domains. Inform. and Comput. 160(1/2), 109–127 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  3. Abdulla, P.A., Delzanno, G., Van Begin, L.: A classification of the expressive power of well-structured transition systems. Inform. and Comput. 209(3), 248–279 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  4. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inform. and Comput. 127(2), 91–101 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  5. Abriola, S., Figueira, S., Senno, G.: Linearizing bad sequences: upper bounds for the product and majoring well quasi-orders. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 110–126. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL 2010, pp. 7–18. ACM (2010)

    Google Scholar 

  7. Barceló, P., Figueira, D., Libkin, L.: Graph logics with rational relations and the generalized intersection problem. In: LICS 2012, pp. 115–124. IEEE Press (2012)

    Google Scholar 

  8. Bertrand, N., Schnoebelen, P.: Computable fixpoints in well-structured symbolic model checking. Form. Methods in Syst. Des. (to appear, 2013)

    Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. Bresolin, D., Della Monica, D., Montanari, A., Sala, P., Sciavicco, G.: Interval temporal logics over finite linear orders: The complete picture. In: ECAI 2012. Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 199–204. IOS (2012)

    Google Scholar 

  11. Cardoza, E., Lipton, R., Meyer, A.R.: Exponential space complete problems for Petri nets and commutative subgroups. In: STOC 1976, pp. 50–54. ACM (1976)

    Google Scholar 

  12. Chambart, P., Schnoebelen, P.: Post embedding problem is not primitive recursive, with applications to channel systems. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 265–276. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Chambart, P., Schnoebelen, P.: The ordinal recursive complexity of lossy channel systems. In: LICS 2008, pp. 205–216. IEEE Press (2008)

    Google Scholar 

  14. Cichoń, E.A., Tahhan Bittar, E.: Ordinal recursive bounds for Higman’s Theorem. Theor. Comput. Sci. 201(1-2), 63–84 (1998)

    Article  MATH  Google Scholar 

  15. Clote, P.: On the finite containment problem for Petri nets. Theor. Comput. Sci. 43, 99–105 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  16. Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS 1998, pp. 70–80. IEEE Press (1998)

    Google Scholar 

  17. Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352–359. IEEE Press (1999)

    Google Scholar 

  18. Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124–140. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  19. Figueira, D.: Alternating register automata on finite words and trees. Logic. Meth. in Comput. Sci. 8(1), 22 (2012)

    MathSciNet  Google Scholar 

  20. Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In: LICS 2011, pp. 269–278. IEEE Press (2011)

    Google Scholar 

  21. Finkel, A.: A generalization of the procedure of Karp and Miller to well structured transition systems. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 499–508. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  22. Finkel, A.: Decidability of the termination problem for completely specificied protocols. Distributed Computing 7(3), 129–135 (1994)

    Article  Google Scholar 

  23. Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: Complete WSTS. Logic. Meth. in Comput. Sci. 8(4:28) (2012)

    Google Scholar 

  24. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  25. Goubault-Larrecq, J.: On a generalization of a result by Valk and Jantzen. Research Report LSV-09-09, Laboratoire Spécification et Vérification, ENS Cachan, France (2009)

    Google Scholar 

  26. Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 5–24. Springer, Heidelberg (2013)

    Google Scholar 

  27. Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In: LICS 2012, pp. 355–364. IEEE Press (2012)

    Google Scholar 

  28. Jančar, P.: Nonprimitive recursive complexity and undecidability for Petri net equivalences. Theor. Comput. Sci. 256(1-2), 23–30 (2001)

    Article  MATH  Google Scholar 

  29. Jurdziński, M., Lazić, R.: Alternating automata on data trees and XPath satisfiability. ACM Trans. Comput. Logic 12(3) (2011)

    Google Scholar 

  30. Kruskal, J.B.: The theory of well-quasi-ordering: A frequently discovered concept. J. Comb. Theory A 13(3), 297–305 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  31. Kurucz, A.: Combining modal logics. In: Handbook of Modal Logics, ch. 15, pp. 869–926. Elsevier Science (2006)

    Google Scholar 

  32. Lasota, S., Walukiewicz, I.: Alternating timed automata. ACM Trans. Comput. Logic 9(2), 10 (2008)

    Article  MathSciNet  Google Scholar 

  33. Lazić, R., Ouaknine, J., Worrell, J.: Zeno, Hercules and the Hydra: Downward rational termination is Ackermannian. In: MFCS 2013. LNCS. Springer (to appear, 2013)

    Google Scholar 

  34. Löb, M., Wainer, S.: Hierarchies of number theoretic functions. I. Arch. Math. Logic 13, 39–51 (1970)

    Article  MATH  Google Scholar 

  35. Mayr, E.W., Meyer, A.R.: The complexity of the finite containment problem for Petri nets. J. ACM 28(3), 561–576 (1981)

    MathSciNet  MATH  Google Scholar 

  36. McAloon, K.: Petri nets and large finite sets. Theor. Comput. Sci. 32(1-2), 173–183 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  37. Milner, R.: Operational and algebraic semantics of concurrent processes. In: Handbook of Theoretical Computer Science, ch. 19, pp. 1201–1242. Elsevier Science (1990)

    Google Scholar 

  38. Ouaknine, J., Worrell, J.: On the decidability and complexity of Metric Temporal Logic over finite words. Logic. Meth. in Comput. Sci. 3(1), 8 (2007)

    MathSciNet  Google Scholar 

  39. Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6(2), 223–231 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  40. Schmitz, S., Schnoebelen, P.: Multiply-recursive upper bounds with Higman’s Lemma. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 441–452. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  41. Schmitz, S., Schnoebelen, P.: Algorithmic aspects of wqo theory. Lecture notes (2012), http://cel.archives-ouvertes.fr/cel-00727025

  42. Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  43. Schwichtenberg, H., Wainer, S.S.: Proofs and Computation. Perspectives in Logic. Cambridge University Press (2012)

    Google Scholar 

  44. Urquhart, A.: The complexity of decision procedures in relevance logic II. J. Symb. Log. 64(4), 1774–1802 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  45. Weiermann, A.: Complexity bounds for some finite forms of Kruskal’s Theorem. J. Symb. Comput. 18(5), 463–488 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Cachan & CNRS, Cachan, France

    Sylvain Schmitz & Philippe Schnoebelen

Authors
  1. Sylvain Schmitz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Philippe Schnoebelen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Facultad de Matemáticas, Astronomía y Física, Universidad Nacional de Córdoba – CONICET, Medina Allende s/n,, X5000HUA, Córdoba, Argentina

    Pedro R. D’Argenio

  2. Departamento de Computación,, Universidad de Buenos Aires - Conicet, Intendente Güirales 2160, C1428EGA, Ciudad Autónoma de Buenos Aires, Argentina

    Hernán Melgratti

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schmitz, S., Schnoebelen, P. (2013). The Power of Well-Structured Systems. In: D’Argenio, P.R., Melgratti, H. (eds) CONCUR 2013 – Concurrency Theory. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40184-8_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40183-1

  • Online ISBN: 978-3-642-40184-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation