Ordinal Theory for Expressiveness of Well Structured Transition Systems

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 (nonmonotonic 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.

• Type: Journal
• Year: 2011
• Where: FOSSACS
• Authors: Rémi Bonnet, Alain Finkel, Serge Haddad, Fernando Rosa-Velardo
• Keywords: Alphabets, Embeddings, Expressiveness, FOSSACS 2011, Software Engineering