Equivalence in LOTOS and its decision method

Hiroaki Kaminaga, Kaoru Takahashi, Norio Shiratori, Shoichi Noguchi

    Research output: Contribution to journalArticle

    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 languageEnglish
    Pages (from-to)10-20
    Number of pages11
    JournalSystems and Computers in Japan
    Volume22
    Issue number1
    Publication statusPublished - 1991

    Fingerprint

    Specification languages
    Bisimulation
    Equivalence
    Specifications
    Equivalence classes
    Finite automata
    Specification
    Communication systems
    Network protocols
    Finite Automata
    Equivalence class
    Communication Systems
    Partitioning
    Heuristics
    Sufficient
    Necessary
    Arbitrary

    ASJC Scopus subject areas

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

    Cite this

    Kaminaga, H., Takahashi, K., Shiratori, N., & Noguchi, S. (1991). Equivalence in LOTOS and its decision method. Systems and Computers in Japan, 22(1), 10-20.

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

    In: Systems and Computers in Japan, Vol. 22, No. 1, 1991, p. 10-20.

    Research output: Contribution to journalArticle

    Kaminaga, H, Takahashi, K, Shiratori, N & Noguchi, S 1991, 'Equivalence in LOTOS and its decision method', Systems and Computers in Japan, vol. 22, no. 1, pp. 10-20.
    Kaminaga H, Takahashi K, Shiratori N, Noguchi S. Equivalence in LOTOS and its decision method. Systems and Computers in Japan. 1991;22(1):10-20.
    Kaminaga, Hiroaki ; Takahashi, Kaoru ; Shiratori, Norio ; Noguchi, Shoichi. / Equivalence in LOTOS and its decision method. In: Systems and Computers in Japan. 1991 ; Vol. 22, No. 1. pp. 10-20.
    @article{71b39b32edfe4ea288bfeaef0780a0fa,
    title = "Equivalence in LOTOS and its decision method",
    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.",
    author = "Hiroaki Kaminaga and Kaoru Takahashi and Norio Shiratori and Shoichi Noguchi",
    year = "1991",
    language = "English",
    volume = "22",
    pages = "10--20",
    journal = "Systems and Computers in Japan",
    issn = "0882-1666",
    publisher = "John Wiley and Sons Inc.",
    number = "1",

    }

    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 -