Subset of lotos with the computational power of place/transition-nets

Abstract

In this paper, we define a subset of Lotos that can be modelled by finite Place/Transition-nets (P/T-nets). That means that specifications in that Lotos subset can be translated into finite P/T-nets and validated using P/T-net verification techniques. An important aspect of our work is that we show that conversely P/T-nets can be simulated in our Lotos subset. It means that the constraints we put on Lotos in order to obtain finite nets are minimally restrictive. We may also conclude that our Lotos subset and P/T-nets have equivalent computational power. To the best of our knowledge, no such bidirectional translation scheme has been published before.