{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:03:24Z","timestamp":1754481804484,"version":"3.33.0"},"reference-count":9,"publisher":"Wiley","issue":"12","license":[{"start":{"date-parts":[[2007,3,22]],"date-time":"2007-03-22T00:00:00Z","timestamp":1174521600000},"content-version":"vor","delay-in-days":5924,"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":[[1991,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A verification method based on time Petri nets automatically proves the correctness of quantitative timing properties for hard real\u2010time systems. However, the previously proposed method sometimes takes a very long time or requires considerable memory space to complete verifications. This is because the method generates the whole state space of time Petri nets.<\/jats:p><jats:p>This paper proposes an efficient verification method based on the single\u2010place zero\u2010reachability problem of time Petri nets, but it may be restricted by given time Petri nets. The single\u2010place zero\u2010reachability problem can be solved only by checking whether or not some prescribed transitions can finally fire. This does not require extracting the whole state space of time Petri nets.<\/jats:p><jats:p>The method proposed herein: (1) reduces the verification problem to the single\u2010place zero\u2010reachability problem of time Petri nets; and (2) generates reduced state space sufficient to check the possibility of the firings of all enabled transitions. This paper also contains an example of verifying a simple LAN protocol and compares the performance of both the proposed method and the previous method.<\/jats:p>","DOI":"10.1002\/scj.4690221204","type":"journal-article","created":{"date-parts":[[2007,7,7]],"date-time":"2007-07-07T20:03:25Z","timestamp":1183838605000},"page":"37-52","source":"Crossref","is-referenced-by-count":8,"title":["Acceleration of timing verification method based on time petri nets"],"prefix":"10.1002","volume":"22","author":[{"given":"Tomohiro","family":"Yoneda","sequence":"first","affiliation":[]},{"given":"Yoshihiro","family":"Tohma","sequence":"additional","affiliation":[]},{"given":"Yutaka","family":"Kondo","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2007,3,22]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1987.5009519"},{"key":"e_1_2_1_3_2","unstructured":"B.BerthomieuandM.Menasche.An Enumerative Approach for Analyzing Time Petri Nets. Information Processing 83 IFIP pp.41\u201346(1983)."},{"key":"e_1_2_1_4_2","unstructured":"J\u2010L.RouxandB.Berthomieu.Verification of a Local Area Network Protocol with TINA: A Software Package for Time Petri Nets. 7th European Workshop on Application and Theory of Petri Nets Oxford England pp.183\u2013205(1986)."},{"key":"e_1_2_1_5_2","doi-asserted-by":"crossref","unstructured":"J. S.Ostroff.Automatic verification of timed transition modes. Proc. of the Workshop on Automatic Verification Methods for Finite State Systems (1989).","DOI":"10.1007\/3-540-52148-8_20"},{"key":"e_1_2_1_6_2","doi-asserted-by":"crossref","unstructured":"T.Yoneda K.Nakade andY.Tohma.A Fast Timing Verification Method Based on the Independence of Units pp.134\u2013141. Proc. of 19th International Symposium on Fault\u2010Tolerant Computing (1989).","DOI":"10.1109\/FTCS.1989.105556"},{"issue":"6","key":"e_1_2_1_7_2","article-title":"Automatic verification method of protocols based on time sequential machines","volume":"73","author":"Yoneda T.","journal-title":"Trans. I.E.I.C.E., Japan"},{"volume-title":"Petri Net Theory and the Modeling of Systems","year":"1981","author":"Peterson J. L.","key":"e_1_2_1_8_2"},{"key":"e_1_2_1_9_2","doi-asserted-by":"crossref","unstructured":"B.AspvallandY.Shiloach.A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with Two Variable per Inequality. 20th Annual Symp. on Foundations of Computer Sciences pp.205\u2013217(Oct.1979).","DOI":"10.1109\/SFCS.1979.1"},{"volume-title":"Graph Theory: An Algorithmic Approach","year":"1975","author":"Christofides N.","key":"e_1_2_1_10_2"}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690221204","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690221204","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T17:05:51Z","timestamp":1737219951000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690221204"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,1]]},"references-count":9,"journal-issue":{"issue":"12","published-print":{"date-parts":[[1991,1]]}},"alternative-id":["10.1002\/scj.4690221204"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690221204","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"type":"print","value":"0882-1666"},{"type":"electronic","value":"1520-684X"}],"subject":[],"published":{"date-parts":[[1991,1]]}}}