### Abstract

This paper considers the specification described in LOTOS, which is the formal description language for the communication system. A decision method is proposed for the equivalence between two arbitrary systems (between definition of service and the protocol specifications, for example). In this paper, based on the definition of the weak bisimulation equivalence, which is the definition of equivalence in LOTOS, the concepts of the k-weak bisimulation equivalence and the canonical 1-weak bisimulation are introduced. It is shown that those concepts are mutually necessary and sufficient. Then, based on the canonical 1-weak bisimulation equivalence, the decision algorithm is presented for the weak bisimulation equivalence between two LOTOS specifications with finite states by the same method as in the equivalence class partitioning of the equivalent states in a finite automaton. The traditional decision of the equivalence using the transformation by algebraic rules is heuristic and often does not succeed in the decision. By contrast, the proposed method has a merit in that it is always applicable to the system with finite states.

Original language | English |
---|---|

Pages (from-to) | 10-20 |

Number of pages | 11 |

Journal | Systems and Computers in Japan |

Volume | 22 |

Issue number | 1 |

Publication status | Published - 1991 |

### Fingerprint

### ASJC Scopus subject areas

- Computational Theory and Mathematics
- Hardware and Architecture
- Information Systems
- Theoretical Computer Science

### Cite this

*Systems and Computers in Japan*,

*22*(1), 10-20.

**Equivalence in LOTOS and its decision method.** / Kaminaga, Hiroaki; Takahashi, Kaoru; Shiratori, Norio; Noguchi, Shoichi.

Research output: Contribution to journal › Article

*Systems and Computers in Japan*, vol. 22, no. 1, pp. 10-20.

}

TY - JOUR

T1 - Equivalence in LOTOS and its decision method

AU - Kaminaga, Hiroaki

AU - Takahashi, Kaoru

AU - Shiratori, Norio

AU - Noguchi, Shoichi

PY - 1991

Y1 - 1991

N2 - This paper considers the specification described in LOTOS, which is the formal description language for the communication system. A decision method is proposed for the equivalence between two arbitrary systems (between definition of service and the protocol specifications, for example). In this paper, based on the definition of the weak bisimulation equivalence, which is the definition of equivalence in LOTOS, the concepts of the k-weak bisimulation equivalence and the canonical 1-weak bisimulation are introduced. It is shown that those concepts are mutually necessary and sufficient. Then, based on the canonical 1-weak bisimulation equivalence, the decision algorithm is presented for the weak bisimulation equivalence between two LOTOS specifications with finite states by the same method as in the equivalence class partitioning of the equivalent states in a finite automaton. The traditional decision of the equivalence using the transformation by algebraic rules is heuristic and often does not succeed in the decision. By contrast, the proposed method has a merit in that it is always applicable to the system with finite states.

AB - This paper considers the specification described in LOTOS, which is the formal description language for the communication system. A decision method is proposed for the equivalence between two arbitrary systems (between definition of service and the protocol specifications, for example). In this paper, based on the definition of the weak bisimulation equivalence, which is the definition of equivalence in LOTOS, the concepts of the k-weak bisimulation equivalence and the canonical 1-weak bisimulation are introduced. It is shown that those concepts are mutually necessary and sufficient. Then, based on the canonical 1-weak bisimulation equivalence, the decision algorithm is presented for the weak bisimulation equivalence between two LOTOS specifications with finite states by the same method as in the equivalence class partitioning of the equivalent states in a finite automaton. The traditional decision of the equivalence using the transformation by algebraic rules is heuristic and often does not succeed in the decision. By contrast, the proposed method has a merit in that it is always applicable to the system with finite states.

UR - http://www.scopus.com/inward/record.url?scp=0025842586&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0025842586&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0025842586

VL - 22

SP - 10

EP - 20

JO - Systems and Computers in Japan

JF - Systems and Computers in Japan

SN - 0882-1666

IS - 1

ER -