Advertisement

The Ideal Theory for WSTS

  • Alain FinkelEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9899)

Abstract

We begin with a survey on well structured transition systems and, in particular, we present the ideal framework [FG09a, BFM14] which was recently used to obtain new deep results on Petri nets and extensions. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm. We then recall the completion of WSTS which leads to defining a conceptual Karp-Miller procedure that terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets.

Keywords

Transition System Finite Union Reachability Problem Finite Representation Forward Procedure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgement

I would like to thank Michael Blondin, Jean Goubault-Larrecq and Pierre McKenzie for fruitful discussions and for having allowed me to use some parts of common papers.

References

  1. [ABJ98]
    Abdulla, P., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy Fifo channels. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1898. LNCS, vol. 1427, pp. 305–318. Springer, Heidelberg (1998)Google Scholar
  2. [ACABJ04a]
    Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. Formal Methods Syst. Des. 25(1), 39–65 (2004)CrossRefzbMATHGoogle Scholar
  3. [AČJT00]
    Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1–2), 109–127 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  4. [AČJYK96]
    Abdulla, P.A., Čerāns, K., Jonsson, B., Yih-Kuen, T.: General decidability theorems for infinite-state systems. In: 11th LICS, pp. 313–321 (1996)Google Scholar
  5. [ADB07]
    Abdulla, P.A., Delzanno, G., Van Begin, L.: Comparing the expressive power of well-structured transition systems. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 99–114. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. [ADMN04]
    Abdulla, P.A., Deneux, J., Mahata, P., Nylén, A.: Forward reachability analysis of timed Petri nets. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 343–362. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. [AJ93]
    Abdulla, P., Jonsson, B.: Verifying programs with unreliable channels. In: Proceedings of the 8th LICS, pp. 160–170 (1993)Google Scholar
  8. [AJ94]
    Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, pp. 1–168. Oxford University Press (1994)Google Scholar
  9. [AL78]
    Arnold, A., Latteux, M.: Recursivite et cones rationnels fermes par intersection. Calcolo 15(4), 381–394 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  10. [AN00]
    Abdulla, P.A., Nylén, A.: Better is better than well: on efficient verification of infinite-state systems. In: Proceedings of 14th IEEE Symposium, LICS 2000, pp. 132–140 (2000)Google Scholar
  11. [BDK+12]
    Bertrand, N., Delzanno, G., König, B., Sangnier, A., Stückrath, J.: On the decidability status of reachability and coverability in graph transformation systems. In: Tiwari, A. (ed.) 23rd RTA 2012, Nagoya, Japan, 28 May–2 June 2012. LIPIcs, vol. 15, pp. 101–116. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  12. [BFHR11]
    Bonnet, R., Finkel, A., Haddad, S., Rosa-Velardo, F.: Ordinal theory for expressiveness of well structured transition systems. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 153–167. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  13. [BFM14]
    Blondin, M., Finkel, A., McKenzie, P.: Handling infinitely branching WSTS. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 13–25. Springer, Heidelberg (2014)Google Scholar
  14. [BFM16a]
    Blondin, M., Finkel, A., McKenzie, P.: Well Behaved Transition Systems (2016, in preparation)Google Scholar
  15. [BFM16b]
    Blondin, M., Finkel, A., McKenzie, P.: Handling infinitely branching well-structured transition systems. Inf. Comput. (2016, submitted)Google Scholar
  16. [BG14]
    Baldan, P., Gorla, D. (eds.): CONCUR 2014. LNCS, vol. 8704. Springer, Heidelberg (2014)zbMATHGoogle Scholar
  17. [BHM15]
    Badouel, E., Hélouët, L., Morvan, C.: Petri nets with structured data. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 212–233. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  18. [BLP15]
    Bojanczyk, M., Lasota, S., Potapov, I. (eds.): RP 2015. LNCS, vol. 9328. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-24537-9_7 Google Scholar
  19. [Bon75]
    Bonnet, R.: On the cardinality of the set of initial intervals of a partially ordered set. In: Infinite, Finite Sets: To Paul Erdös on His 60th Birthday, pp. 189–198 (1975)Google Scholar
  20. [CFS11]
    Chambart, P., Finkel, A., Schmitz, S.: Forward analysis and model checking for trace bounded WSTS. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol. 6709, pp. 49–68. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  21. [DFS98]
    Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  22. [DJS99]
    Dufourd, C., Jančar, P., Schnoebelen, P.: Boundedness of reset P/T nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 301–310. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  23. [EFM99]
    Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th LICS, pp. 352–359 (1999)Google Scholar
  24. [EN98]
    Allen Emerson, E., Namjoshi, K.S.: On model-checking for non-deterministic infinite-state systems. In: 13th LICS, pp. 70–80 (1998)Google Scholar
  25. [ET43]
    Erdös, P., Tarski, A.: On families of mutually exclusive sets. Ann. Math. 2(44), 315–329 (1943)MathSciNetCrossRefzbMATHGoogle Scholar
  26. [FFSS11]
    Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson’s lemma. In: 26th Annual IEEE LICS, Toronto, Ontario, Canada, 21–24 June 2011, pp. 269–278. IEEE Computer Society (2011)Google Scholar
  27. [FG09a]
    Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: completions. In: Albers, S., Marion, J.-Y. (eds.) 26th Annual STACS 2009. Leibniz International Proceedings in Informatics, vol. 3, pp. 433–444. Leibniz-Zentrum für Informatik, Freiburg (2009)Google Scholar
  28. [FG09b]
    Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: complete WSTS. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 188–199. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  29. [FG12]
    Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part II: complete WSTS. Logical Methods Comput. Sci. 8(3:28), 1–35 (2012)MathSciNetzbMATHGoogle Scholar
  30. [Fin87]
    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)Google Scholar
  31. [Fin90]
    Finkel, A.: Reduction and covering of infinite reachability trees. Inf. Comput. 89(2), 144–179 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  32. [FMP04]
    Finkel, A., McKenzie, P., Picaronny, C.: A well-structured framework for analysing Petri net extensions. Inf. Comput. 195(1–2), 1–29 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  33. [Fra86]
    Fraïssé, R.: Theory of relations. Stud. Logic Found. Math. 118, 1–456 (1986)CrossRefzbMATHGoogle Scholar
  34. [FS01]
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theoret. Comput. Sci. 256(1–2), 63–92 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  35. [GHK+03]
    Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: Continuous lattices and domains. In: Encyclopedia of Mathematics and its Applications, vol. 93. Cambridge University Press (2003)Google Scholar
  36. [GLS16]
    Goubault-Larrecq, J., Schmitz, S.: Deciding piecewise testable separability for regular tree languages. In: Calamoneri, T., Gorla, D., Rabani, Y., Sangiorgi, D., Mitzenmacher, M. (eds.) 43rd ICALP 2016, Proceedings Leibniz International Proceedings in Informatics, Rome, Italy, 12–15 July 2016, pp. 97:1–97:14. Leibniz-Zentrum für Informatik (2016)Google Scholar
  37. [GRB04]
    Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge, and check: new algorithms for the coverability problem of WSTS. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 287–298. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  38. [GRB07]
    Geeraerts, G., Raskin, J.-F., Van Begin, L.: Well-structured languages. Acta Inf. 44(3–4), 249–288 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  39. [GRvB06a]
    Ganty, P., Raskin, J.-F., Van Begin, L.: A complete abstract interpretation framework for coverability properties of WSTS. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 49–64. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  40. [GRvB06b]
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  41. [GRvB07]
    Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the efficient computation of the minimal coverability set for Petri nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 98–113. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  42. [HLL+16]
    Hofman, P., Lasota, S., Lazic, R., Leroux, J., Schmitz, S., Totzke, P.: Coverability trees for Petri nets with unordered data. In: Jacobs, B., Löding, C. (eds.) FOSSACS 2016. LNCS, vol. 9634, pp. 445–461. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49630-5_26 CrossRefGoogle Scholar
  43. [HMM14]
    Hüchting, R., Majumdar, R., Meyer, R.: Bounds on mobility. In: Baldan and Gorla [BG14], pp. 357–371Google Scholar
  44. [HP07]
    Haddad, S., Poitrenaud, D.: Recursive Petri nets. Acta Inf. 44(7–8), 463–508 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  45. [HSS12]
    Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal-recursive complexity of timed-arc petri nets, data nets, and other enriched nets. In: 27th Annual IEEE LICS, Dubrovnik, Croatia, 25–28 June 2012, pp. 355–364. IEEE Computer Society (2012)Google Scholar
  46. [Jan99]
    Jančar, P.: A note on well quasi-orderings for powersets. Inf. Process. Lett. 72(5–6), 155–160 (1999)MathSciNetzbMATHGoogle Scholar
  47. [KM69]
    Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)MathSciNetCrossRefzbMATHGoogle Scholar
  48. [KS96]
    Kouchnarenko, O., Schnoebelen, P.: A model for recursive-parallel programs. Electron. Notes Theor. Comput. Sci. 5, 30 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  49. [KS14]
    König, B., Stückrath, J.: A general framework for well-structured graph transformation systems. In: Baldan and Gorla [BG14], pp. 467–481Google Scholar
  50. [Las16]
    Lasota, S.: Decidability border for Petri nets with data: WQO dichotomy conjecture. In: Kordon, F., Moldt, D. (eds.) PETRI NETS 2016. LNCS, vol. 9698, pp. 20–36. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-39086-4_3 CrossRefGoogle Scholar
  51. [Laz13]
    Lazić, R.: The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767 (2013)Google Scholar
  52. [LNO+07]
    Lazić, R.S., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.B.: Nets with tokens which carry data. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 301–320. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  53. [LS15a]
    Lazić, R., Schmitz, S.: The ideal view on rackoff’s coverability technique. In: Bojanczyk et al. [BLP15], pp. 76–88Google Scholar
  54. [LS15b]
    Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: 30th Annual ACM/IEEE LICS, Kyoto, Japan, 6–10 July 2015, pp. 56–67. IEEE Computer Society (2015)Google Scholar
  55. [LS16a]
    Lazić, R., Schmitz, S.: The complexity of coverability in -Petri nets. In: LICS 2016. ACM Press, New York (2016)Google Scholar
  56. [LS16b]
    Leroux, J., Schmitz, S.: Ideal decompositions for vector addition systems (invited talk). In: Ollinger, N., Vollmer, H. (eds.) 33rd STACS 2016, Orléans, France, 17–20 February 2016. LIPIcs, vol. 47, pp. 1:1–1:13 (2016)Google Scholar
  57. [LST15a]
    Leroux, J., Sutre, G., Totzke, P.: On boundedness problems for pushdown vector addition systems. In: Bojanczyk et al. [BLP15], pp. 101–113Google Scholar
  58. [LST15b]
    Leroux, J., Sutre, G., Totzke, P.: On the coverability problem for pushdown vector addition systems in one dimension. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 324–336. Springer, Heidelberg (2015)Google Scholar
  59. [Mar94]
    Marcone, A.: Foundations of BQO theory. Trans. Am. Math. Soc. 345(2), 641–660 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  60. [May00]
    Mayr, R.: Process rewrite systems. Inf. Comput. 156(1–2), 264–286 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  61. [Mey08]
    Meyer, R.: On boundedness in depth in the pi-calculus. In: Ausiello, G., Karhumäki, J., Mauri, G., Luke Ong, C.-H. (eds.) TCS 2008. IFIP, vol. 273, pp. 477–489. Springer, Heidelberg (2008)Google Scholar
  62. [Rad54]
    Rado, R.: Partial well-ordering of sets of vectors. Mathematika 1, 89–95 (1954)MathSciNetCrossRefzbMATHGoogle Scholar
  63. [RdF07]
    Rosa-Velardo, F., de Frutos-Escrig, D.: Name creation vs. replication in Petri net systems. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 402–422. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  64. [RHB+10]
    Rogers, J., Heinz, J., Bailey, G., Edlefsen, M., Visscher, M., Wellcome, D., Wibel, S.: On languages piecewise testable in the strict sense. In: Ebert, C., Jäger, G., Michaelis, J. (eds.) MOL 10/11. LNCS, vol. 6149, pp. 255–265. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  65. [RMdF11]
    Rosa-Velardo, F., Martos-Salgado, M., de Frutos-Escrig, D.: Accelerations for the coverability set of Petri nets with names. Fundam. Inform. 113(3–4), 313–341 (2011)MathSciNetzbMATHGoogle Scholar
  66. [RS04]
    Robertson, N., Seymour, P.D.: Graph minors. XX. Wagner’s conjecture. J. Comb. Theory Ser. B 92(2), 325–357 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  67. [SS11]
    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)CrossRefGoogle Scholar
  68. [Val78]
    Valk, R.: Self-modidying nets, a natural extension of Petri nets. In: Ausiello, G., Böhm, C. (eds.) ICALP 1978. LNCS, vol. 62, pp. 464–476. Springer, Heidelberg (1978)Google Scholar
  69. [WZH10]
    Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  70. [ZWH12]
    Zufferey, D., Wies, T., Henzinger, T.A.: Ideal abstractions for well-structured transition systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 445–460. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.LSV, ENS Cachan and CNRSUniversité Paris-SaclayCachanFrance

Personalised recommendations