How to implement simulation on two LTSs?

Question

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?

Answer 1

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.

• Linear Time-Branching Time Spectrum II, Robert J. van Glabbeek, 1993.

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

• Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation, by Francesco Ranzato and Francesco Tapparo

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.

• Computing Stuttering Simulations by Francesco Ranzato and Francesco Tapparo

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.