Does any one know how to implement the simulation relation on two labelled transition systems (LTS)?

I know how to do it for branching bi-simulation. The signature refinement theorem is used for that purpose which has the time complexity of $O(n^3)$ on cyclic LTSs. Is the signature refinement technique useful for simulation also?

Is there any binary relation called branching simulation? Any idea how to implement it?

What I would like to do is to write a program such that:

  • Input: Given two labelled transition systems with silent steps
  • Output1: Does one simulates the other one?
  • Output2: Are they bisimilar?
  • Output3: Are they branching bisimilar?
  • Output4: Does one branching simulate the other one?

The following illustrates the definitions of the above relations:

  1. simulate: An LTS ($L_1$) simulates another LTS ($L_2$) if there exists a binary relation $R$ over the states of the two transition systems such that every transition of $L_2$ can be matched by a transition of $L_1$. Note that simulation is not an equivalence relation.

  2. bisimilar: An LTS ($L_1$) and an LTS ($L_2$) are said to be bisimular if there exists a relation $R$ between the states of these transition systems such that both $R$ and $R^{-1}$ are simulations. Note that bisimularity is an equivalence relation.

  3. branching bisimilarity: is same as bisimilarity but transition systems may have silent steps. Those silent steps ($\tau$ actions) that do not change the behavior of the process are eliminated. Note that branching bisimilarity is an equivalence relation.

  4. branching similarity: I actually have never seen the definition of branching similarity in any context, but it should be the same as similarity. However, the transition systems may have the silent steps.

The paper Distributed Branching Bisimulation Reduction of State Spaces by S. Blom and S. Orzan explains an algorithm to reduce the size of an LTS with respect to branching bisimilarity. The signature refinement theorem is used for that purpose. How it works is roughly as follows:

the algorithm starts by constructing a partition (a set of blocks) of states and terminates once the partition is stable. In a stable partition, two states are branching bisimilar if they belong to the same block.

The above algorithm can also be used to verify whether two LTSs are branching bisimilar or bisimilar. How it works is as follows:

Let LTS, $L_3 = L_1 \cup L_2$, then if after branching reduction, using the above algorithm, the initial states of $L_1$ and $L_2$ both belong to the same block then they are branching bisimular. The above algorithm has time complexity $O(n^3)$ and space complexity $O(n^2)$.

Question: How can I do the same with branching simulate and simulate relations?

  • $\begingroup$ What do you mean by "implement a simulation relation"? Find one? Test that a relation is a simulation relation? Something else? $\endgroup$ – Dave Clarke Aug 1 '12 at 12:01

If you have doubts about whether a certain type of relation exists, a good place to search is Rob van Glabbeek's extensive catalogue of such relations. That article is a bit dated by now, but still extremely comprehensive.

There are several papers on the algorithmic aspect. I would suggest the one below.

This paper provides a design-pattern for implementing partition-refinement style algorithms for checking bisimulation and simulation. The later sections of the paper are quite algorithmic. You could contact the authors and ask about their implementation.

You asked about branching and not stuttering, but I think the contents of the above paper are very related to what you want.

There are some implementations that may help your study.

  1. The Edinburgh Concurrency Workbench
  2. The Concurrency Workbench of the New Century
  3. Concurrency Workbench, Aalborg Edition

All the tools above implement checking equivalences of processes with respect to preorders; the third one is more recent and is also offered online.

  • $\begingroup$ Thanks for the papers Vijay D. My research area is not abstract interpretation, but the papers look very useful. I have already used stuttering techniques to implement branching bisimulation to reduce the size of LTSs. What I am looking for is to define a binary relation between two LTSs. This relation should be only transitive and it's not an equivalence relation. The relation should verify whether an LTS (corresponding to a server process) simulates anopther LTS (corresponding to the client process). $\endgroup$ – Nima Aug 2 '12 at 17:36
  • $\begingroup$ Still I am not sure if such a relation exists! But it should be close to the definition of "simulates" with the difference that the LTSs may contain $\tau$ actions. $\endgroup$ – Nima Aug 2 '12 at 17:40
  • $\begingroup$ I think you are looking for stuttering simulation, or a variant of stuttering simulation. Stuttering simulation is a preorder but not an equivalence relation. $\endgroup$ – Vijay D Aug 3 '12 at 21:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.