Ordinal Theory for Expressiveness of Well Structured Transition Systems

  • Remi Bonnet
  • Alain Finkel
  • Serge Haddad
  • Fernando Rosa-Velardo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6604)


To the best of our knowledge, we characterize for the first time the importance of resources (counters, channels, alphabets) when measuring expressiveness of WSTS. We establish, for usual classes of wpos, the equivalence between the existence of order reflections (non-monotonic order embeddings) and the simulations with respect to coverability languages. We show that the non-existence of order reflections can be proved by the computation of order types. This allows us to solve some open problems and to unify the existing proofs of the WSTS classification.


  1. 1.
    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
  2. 2.
    Abdulla, P.A., Delzanno, G., Van Begin, L.: A Language-Based Comparison of Extensions of Petri Nets with and without Whole-Place Operations. In: Dediu, A.H., Ionescu, A.M., Martín-Vide, C. (eds.) LATA 2009. LNCS, vol. 5457, pp. 71–82. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  3. 3.
    Abdulla, P.A., Nylen, A.: Timed Petri Nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–70. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Alur, R., Courcoubetis, C., Henzinger, T.A.: The Observational Power of Clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 162–177. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  5. 5.
    Finkel, A., Bonnet, R., Haddad, S., Rosa-Velardo, F.: Comparing Petri Data Nets and Timed Petri Nets. LSV Research Report 10-23 (2010)Google Scholar
  6. 6.
    Finkel, A., Bonnet, R., Haddad, S., Rosa-Velardo, F.: Ordinal Theory for Expresiveness of Well-Structured Transition Systems. LSV Research Report 11-01 (2011)Google Scholar
  7. 7.
    Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermann and Primitive-Recursive Bounds with Dickson’s Lemma. CoRR abs/1007.2989 (2010)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Finkel, A., McKenzie, P., Picaronny, C.: A well-structured framework for analysing petri net extensions. Information and Computation 195(1-2), 1–29 (2004)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Geeraerts, G., Raskin, J., Van Begin, L.: Well-structured languages. Acta Informatica 44, 249–288 (2007)MathSciNetCrossRefGoogle Scholar
  11. 11.
    de Jongh, D.H.J., Parikh, R.: Well partial orderings and hierarchies. Indagationes Mathematicae (Proceedings) 80, 195–207 (1977)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Kouchnarenko, O., Schnoebelen, P.: A Formal Framework for the Analysis of Recursive-Parallel Programs. In: Malyshkin, V.E. (ed.) PaCT 1997. LNCS, vol. 1277, pp. 45–59. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. 13.
    Lazic, R., Newcomb, T.C., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with Tokens Which Carry Data. Fund. Informaticae 88(3), 251–274 (2008)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Rosa-Velardo, F., de Frutos-Escrig, D.: Name creation vs. replication in Petri Net systems. Fund. Informaticae 88(3), 329–356 (2008)MathSciNetzbMATHGoogle Scholar
  15. 15.
    Rosa-Velardo, F., Delzanno, G.: Language-Based Comparison of Petri Nets with black tokens, pure names and ordered data. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 524–535. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  16. 16.
    Rosa-Velardo, F., de Frutos-Escrig, D.: Forward Analysis for Petri Nets with Name Creation. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 185–205. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  17. 17.
    Schmidt, D.: Well-partial orderings and their maximal order types. Fakultät für Mathematik der Ruprecht-Karls-Universität Heidelberg. Habilitationsschrift (1979)Google Scholar
  18. 18.
    Weiermann, A.: A Computation of the Maximal Order Type of the Term Ordering on Finite Multisets. In: Ambos-Spies, K., Löwe, B., Merkle, W. (eds.) CiE 2009. LNCS, vol. 5635, pp. 488–498. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Remi Bonnet
    • 1
  • Alain Finkel
    • 1
  • Serge Haddad
    • 1
  • Fernando Rosa-Velardo
    • 2
  1. 1.LSV, CNRS UMR 8643Ecole Normale Supérieure de CachanCachanFrance
  2. 2.Sistemas Informáticos y ComputaciónUniversidad Complutense de MadridSpain

Personalised recommendations