Abstract:

The approach followed in this work broaches the state explosion problem within the LOTOS framework, through the development of a representation method and a compact state space exploration algorithm based on it, with several applications. The model proposed allows a compact representation of parallelism, reducing the impact of the interleaving semantics of LOTOS in the state explosion. The algorithm that converts any LOTOS expression into an equivalent expression in the new calculus is called interleaved expansion. The interleaved expansion yields a representation of the labeled transition system where interleaving behaviours are isolated, factored and kept unexpanded. This representation implies an important size reduction with respect to the explicit transition system in those specification with a high degree of interleaving. Hence it is suitable for specifications written in a resource-oriented style. On the other hand, the size of the interleaved expanded form can be bigger than its equivalent transition system in certain cases of specifications written following a constraint-oriented approach. In practice, this is not a major disadvantage, since state explosion appears mainly in resource-oriented specifications. Furthermore, a normal expansion can be applied in such cases. The development presented contains the extension of the model to full LOTOS and a comparison with some related true concurrency semantics models, such as Petri nets and event structures. Finally, the study includes an algorithm for state exploration which preserves interleaving zones and which is compatible with reduction methods based on stubborn sets principles. The implementation of the interleaved expansion has allowed to check the results on medium sized sample specifications. This work has been partially supported by SIGMA and MEDAS projects (finished).