{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T06:41:08Z","timestamp":1698043268975},"reference-count":7,"publisher":"Wiley","issue":"8","license":[{"start":{"date-parts":[[2007,3,22]],"date-time":"2007-03-22T00:00:00Z","timestamp":1174521600000},"content-version":"vor","delay-in-days":6289,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems &amp;amp; Computers in Japan"],"published-print":{"date-parts":[[1990,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A method for extending the behavioral specification and verification of state machine networks by event sequences to non\u2010deterministic behavior is presented. The nondeterministic behavior is described by a function between sets of event sequences instead of between sequences. Both the module composition and loop connection operations are modeled by the function composition and the least fixed point, respectively, just as in the deterministic case. Two application examples are described. The example with alternating bit protocol via unreliable communication lines indicates that the method detects the possibility of message stack just as the verification by temporal logic does, while the proof steps of our method are shorter. The second example discusses the cause of the Brock\u2010Ackerman anomaly and a condition to avoid it.<\/jats:p>","DOI":"10.1002\/scj.4690210803","type":"journal-article","created":{"date-parts":[[2007,7,7]],"date-time":"2007-07-07T19:33:29Z","timestamp":1183836809000},"page":"21-33","source":"Crossref","is-referenced-by-count":0,"title":["Behavioral Specification of Nondeterministic State Machines by Event Sequence Sets"],"prefix":"10.1002","volume":"21","author":[{"given":"Nagatsugu Yamanouchi","family":"Member","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2007,3,22]]},"reference":[{"issue":"8","key":"e_1_2_1_2_2","first-page":"1453","article-title":"Behavioral specification of state machine networks by event sequences","volume":"70","author":"Yamanouchi N.","year":"1987","journal-title":"Trans. I.E.I.C.E., Japan"},{"key":"e_1_2_1_3_2","article-title":"Functional specification of state machine network behavior (2)\u2014Cross\u2010timing and nondeterministic behavior","volume":"85","author":"Yamanouchi N.","year":"1985","journal-title":"I.E.I.C.E., Japan"},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0376-5075(76)90015-5"},{"key":"e_1_2_1_5_2","unstructured":"B. T.Hailpern.Verifying Concurrent Processes Using Temporal Logic. Technical Report 195 Dept. of Electrical Engineering Stanford University (Aug.1980)."},{"issue":"1","key":"e_1_2_1_6_2","article-title":"An anomaly in the specification of nondeterminate packet systems","volume":"33","author":"Brock J. D.","year":"1978","journal-title":"Computation Structures Group Note"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"e_1_2_1_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90048-X"}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690210803","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690210803","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T20:35:21Z","timestamp":1698006921000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690210803"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,1]]},"references-count":7,"journal-issue":{"issue":"8","published-print":{"date-parts":[[1990,1]]}},"alternative-id":["10.1002\/scj.4690210803"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690210803","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"value":"0882-1666","type":"print"},{"value":"1520-684X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,1]]}}}