Does any one know how to implement the simulation relation on two labelled trans

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(n3) 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:

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

bisimilar: An LTS (L1) and an LTS (L2) 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.

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

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, L3=L1?L2, then if after branching reduction, using the above algorithm, the initial states of L1 and L2 both belong to the same block then they are branching bisimular. The above algorithm has time complexity O(n3) and space complexity O(n2).

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

Explanation / Answer

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.

The Edinburgh Concurrency Workbench
The Concurrency Workbench of the New Century

Both the tools above implement checking equivalences of processes with respect to preorders.

Related Questions

Navigate

• Browse (All)
• Browse D
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.