An Equivalence in LOTOS and Its Decision Method.

Saved in:

Bibliographic Details
Title:	An Equivalence in LOTOS and Its Decision Method.
Authors:	Kaminaga, Hiroaki¹, Takahashi, Kaoru¹, Shiratori, Norio¹, Noguchi, Shoichi¹
Source:	Systems & Computers in Japan. 1/1/91, Vol. 22 Issue 1, p10-20. 11p.
Subjects:	LOTOS (Computer program language), Programming languages, Algorithms, Algebra, Robots, Industrial robots
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 λ-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 automation. 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. [ABSTRACT FROM AUTHOR]
	Copyright of Systems & Computers in Japan is the property of Wiley-Blackwell and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
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 λ-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 automation. 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. [ABSTRACT FROM AUTHOR]
ISSN:	08821666
DOI:	10.1002/scj.4690220102