Optimization of the translation of labeled transition systems to kripke structures

Abstract

Labeled transition systems (LTSs) and Kripke structures (KSs) are the two most prominent semantic models in concurrency theory. Firstly, the models described by LTSs are usually translated to KSs. Then, an ad hoc model checker is used to verify the properties of the models. The performance of the embedded algorithm and the size of KS have severely confined the verification of LTS models. To address the problem in the translation of LTSs into KSs, a new and optimized algorithm was presented in this study. The new algorithm creates a smaller-scaled KS with a slight increase in time and space cost, thereby relieving the state explosion problem significantly.