{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T05:02:12Z","timestamp":1698037332578},"reference-count":14,"publisher":"Wiley","issue":"1","license":[{"start":{"date-parts":[[2007,3,21]],"date-time":"2007-03-21T00:00:00Z","timestamp":1174435200000},"content-version":"vor","delay-in-days":5923,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems &amp; Computers in Japan"],"published-print":{"date-parts":[[1991,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 <jats:italic>k<\/jats:italic>\u2010weak bisimulation equivalence and the canonical 1\u2010weak bisimulation are introduced.<\/jats:p><jats:p>It is shown that those concepts are mutually necessary and sufficient. Then, based on the canonical 1\u2010weak 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.<\/jats:p>","DOI":"10.1002\/scj.4690220102","type":"journal-article","created":{"date-parts":[[2007,7,7]],"date-time":"2007-07-07T19:35:04Z","timestamp":1183836904000},"page":"10-20","source":"Crossref","is-referenced-by-count":0,"title":["An equivalence in lotos and its decision method"],"prefix":"10.1002","volume":"22","author":[{"given":"Hiroaki","family":"Kaminaga","sequence":"first","affiliation":[]},{"given":"Kaoru","family":"Takahashi","sequence":"additional","affiliation":[]},{"given":"Norio","family":"Shiratori","sequence":"additional","affiliation":[]},{"given":"Shoichi","family":"Noguchi","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2007,3,21]]},"reference":[{"issue":"4","key":"e_1_2_1_2_2","first-page":"472","article-title":"Recent trends on OSI standardization","volume":"28","author":"Naemura K.","year":"1987","journal-title":"Inf. Proc."},{"issue":"11","key":"e_1_2_1_3_2","first-page":"1143","article-title":"Network architecture","volume":"70","author":"Kawaoka T.","year":"1987","journal-title":"Proc. I.E.I.C.E., Japan"},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1983.12778"},{"key":"e_1_2_1_5_2","unstructured":"CCITT.Functional specification and description language (SDL). CCITT Recommendations Z.100\u2013Z.104 (1984)."},{"key":"e_1_2_1_6_2","unstructured":"ISO. Estelle (formal description technique based on an extended state transition model). ISO\/DIS9074 (1987)."},{"key":"e_1_2_1_7_2","unstructured":"ISO. LOTOS (formal description technique based on the temporal ordering of observational behavior). ISO\/DIS8807 (1987)."},{"key":"e_1_2_1_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(87)90085-7"},{"issue":"2","key":"e_1_2_1_9_2","first-page":"120","article-title":"Abstract data types and algebraic specification","volume":"27","author":"Inagaki Y.","year":"1986","journal-title":"Inf. Proc."},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1982.235736"},{"key":"e_1_2_1_11_2","unstructured":"ISO. Formal specification in LOTOS of ISO 8073. ISO\/TC97\/SC6\/WG4 (March1987)."},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676697"},{"key":"e_1_2_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"issue":"3","key":"e_1_2_1_14_2","first-page":"374","article-title":"External description of a communication protocol and its property","volume":"71","author":"Murakami T.","year":"1988","journal-title":"Trans. (B), I.E.I.C.E., Japan"},{"key":"e_1_2_1_15_2","unstructured":"H.Kaminaga K.Takahashi N.Shiratori andS.Noguchi.Construction of LOTOS verification system. Papers of Technical Group on Information Networks I.E.I.C.E. Japan IN87\u2010106 (Jan.1988)."}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690220102","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690220102","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T00:05:24Z","timestamp":1698019524000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690220102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,1]]},"references-count":14,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,1]]}},"alternative-id":["10.1002\/scj.4690220102"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690220102","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"value":"0882-1666","type":"print"},{"value":"1520-684X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,1]]}}}