How can we convert a Label Transition System model to a Kripke Structure model?
for example, we can use Pi-Calculus for formal specification of a model. the Pi-Calculus is LTS based. also for formal verification of a model we can use the SMV model checker that is based on State-transition (KS).
When ignoring the transition labels completely, or representing them by additional variables in the target states, you do not preserve the information how you are reaching a target state (in the LTS, multiple transitions with different labels may lead to the same target state).
Instead, you can use the translation as defined originally by DeNicola and Vaandrager in their paper "Action versus State Based Logics for Transition Systems" from 1990. It works as follows: for every occurrence in the LTS of a transition with label a leading to target state s', you introduce a new state in the Kripke structure (let us call it (a,s')). Now, each transition in the LTS from a state s to a state s' with label a (s-a->s') is translated to two transitions in the Kripke structure: 1. a transition from s to (a,s'), and 2. a transition from (a,s') to s'.
If you also work with the special tau-labels in the LTS representing internal behaviour, then tau-transitions can be directly translated to single transitions in the Kripke structure, i.e. s-tau->s' is translated to s->s'.
Finally, I can recommend to also look at the paper by Reniers, Schoren and Willemse from 2012 called "Results on Embeddings Between State-Based and Event-Based Systems". It thoroughly compares the two formalisms and their relevant equivalence relations.
Dear Anton,
thank you for your extra comments.
However, the "multiple transitions with different labels leading to the same target state" argument may not be a problem in general. I mean, it depends on the specific decision problem you are facing. The pushing-label technique, for example, works well in LTL formal verification. In branching time temporal logic verification such as CTL and the like, one can even use the pushing-label technique along with the tree-like unwinding with a duplication of the states (one for each label). Do you agree?
Surely for other decision problems/logics one may need to consider more complex translations and also the one you are proposing can be not sufficient. For example it may not work for logics with graded and backward modalities.
Dear Yasir
Thank you very much for your answer
can you suggest to me these model transformations as a tool, App or program?
Dear Yasir
Thank you very much for your answer
can you suggest to me these model transformations as a tool, App or program?
- Badges
- Science topic
- Similar topics
- Engineering
- Modeling