{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T14:48:06Z","timestamp":1648738086779},"reference-count":9,"publisher":"World Scientific Pub Co Pte Lt","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2006,8]]},"abstract":"<jats:p> In the development of real-time communicating hardware\/embedded-software systems, it is frequently the case that we want to refine\/optimize the system's internal behavior while preserving the external timed I\/O behavior. In such a design refinement, modification of the systems' internal branching structures, as well as re-scheduling of internal actions, may frequently occur. Our goal is, then, to ensure that such modification of internal branching structures and re-scheduling of internal actions preserve the systems' external timed behavior, which is typically formalized by the notion of (timed) failure equivalence since it is less sensitive to the difference of internal branching structures than (timed) weak bisimulation. In order to know the degree of freedom of such re-scheduling, parametric analysis is useful. One of the models suitable for such an analysis is a parametric time-interval automaton(PTIA), which is a subclass of the existing model, a parametric timed automaton. It has only a time interval with upper- and lower-bound parameters as a relative timing constraint between consecutive actions. In this paper, at first, we propose an abstraction algorithm of PTIA which preserves timed failure equivalence. Timed failure equivalence is strictly weaker than timed weak bisimulation in the sense that it does not distinguish the difference of the timing when the internal resolution of nondeterminism has occurred, but it does distinguish the difference of the refusals of communicating actions observed by an external environment. Then, we also show that after applying our algorithm, the reduced PTIA has no internal actions, and thus the problem deriving a parameter condition in order that given two models are timed failure equivalent can be reduced to the existing parametric strong bisimulation equivalence checking. <\/jats:p>","DOI":"10.1142\/s0129054106004133","type":"journal-article","created":{"date-parts":[[2006,8,4]],"date-time":"2006-08-04T22:37:04Z","timestamp":1154731024000},"page":"833-849","source":"Crossref","is-referenced-by-count":0,"title":["A TIMED FAILURE EQUIVALENCE PRESERVING ABSTRACTION FOR PARAMETRIC TIME-INTERVAL AUTOMATA"],"prefix":"10.1142","volume":"17","author":[{"given":"AKIO","family":"NAKATA","sequence":"first","affiliation":[{"name":"Department of Information Networking, Graduate School of Information Science and Technology, Osaka University, Suita, Osaka 565-0871, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"TADAAKI","family":"TANIMOTO","sequence":"additional","affiliation":[{"name":"Department of Information Networking, Graduate School of Information Science and Technology, Osaka University, Suita, Osaka 565-0871, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"SUGURU","family":"SASAKI","sequence":"additional","affiliation":[{"name":"Department of Information Networking, Graduate School of Information Science and Technology, Osaka University, Suita, Osaka 565-0871, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"TERUO","family":"HIGASHINO","sequence":"additional","affiliation":[{"name":"Department of Information Networking, Graduate School of Information Science and Technology, Osaka University, Suita, Osaka 565-0871, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00169-J"},{"key":"rf5","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"rf6","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00172-F"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1041"},{"key":"rf8","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"rf13","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989"},{"key":"rf15","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00214-X"},{"key":"rf16","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1014"},{"key":"rf17","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0086"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054106004133","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T00:40:28Z","timestamp":1565138428000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054106004133"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8]]},"references-count":9,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2006,8]]}},"alternative-id":["10.1142\/S0129054106004133"],"URL":"https:\/\/doi.org\/10.1142\/s0129054106004133","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,8]]}}}