{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T14:10:58Z","timestamp":1771510258402,"version":"3.50.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,4,30]],"date-time":"2018-04-30T00:00:00Z","timestamp":1525046400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Nature Science Foundation of China","doi-asserted-by":"crossref","award":["61572360"],"award-info":[{"award-number":["61572360"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Key R8D Program of China","award":["2017YFB1001804"],"award-info":[{"award-number":["2017YFB1001804"]}]},{"DOI":"10.13039\/501100018558","name":"Shanghai Shuguang Program","doi-asserted-by":"crossref","award":["15SG18"],"award-info":[{"award-number":["15SG18"]}],"id":[{"id":"10.13039\/501100018558","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2018,4,30]]},"abstract":"<jats:p>\n            The correctness of a time-critical system is closely related to the time of responding and performing every event. Our motivation example,\n            <jats:italic>alternating bit protocol<\/jats:italic>\n            , and application example,\n            <jats:italic>multi-track level crossing with sensors<\/jats:italic>\n            , both demonstrate that some nondeterministic behaviours can take place if the time associated with events is configured inappropriately or some concurrent events are controlled imperfectly in an overlapping period. These nondeterministic behaviours decrease the reliability and\/or safety of a time-critical system. Therefore, it is valuable to formalise and check (non)determinacy.\n          <\/jats:p>\n          <jats:p>\n            Time Petri Nets (TPN) in which the firing of every event is limited to a fix time interval are used to model time-critical systems in this article. We proposes a novel notion for TPN named\n            <jats:italic>time-soundness<\/jats:italic>\n            . It guarantees that the system always owns deterministic behaviours after any event is performed no matter when the event is performed. We utilise the notion of bisimulation to prove that the time-soundness can guarantee the behavioural determinacy. We propose an algorithm to check time-soundness, develop the related tool, and do experiments to show the usefulness and effectiveness of our notion and method.\n          <\/jats:p>","DOI":"10.1145\/3185502","type":"journal-article","created":{"date-parts":[[2018,5,23]],"date-time":"2018-05-23T15:08:42Z","timestamp":1527088122000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Time-Soundness of Time Petri Nets Modelling Time-Critical Systems"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7523-4827","authenticated-orcid":false,"given":"Guanjun","family":"Liu","sequence":"first","affiliation":[{"name":"Tongji University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Changjun","family":"Jiang","sequence":"additional","affiliation":[{"name":"Tongji University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengchu","family":"Zhou","sequence":"additional","affiliation":[{"name":"New Jersey Institute of Technology, Newark, NJ"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,5,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/647778.734905"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0161-4"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883623.1883625"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 16th International Conference Application and Theory of Petri Nets. 25--44","author":"Barkaoui Kamel"},{"key":"e_1_2_1_5_1","volume-title":"Lectures on Concurrency and Petri Nets","author":"Bengtsson Johan"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2010.2098415"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.75415"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Federation for Information Processing (IFIP\u201983)","author":"Berthomieu Bernard","year":"1983"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765915"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.489073"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.4"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the International Workshop on Computer Aided Verification. 302--315","author":"Cerans Karlis","year":"1992"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSCI.2014.17"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICOSC.2015.7050790"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.52"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2007.902622"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.2253552"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1590\/S1678-58782011000400010"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems. 246--259","author":"Gardey Guillaume"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2016.7497845"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220900.3221113"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.195"},{"key":"e_1_2_1_23_1","volume-title":"Ullman","author":"Hopcroft John E.","year":"1990"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90014-7"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1987.233170"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-006-8133-9"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the IEEE International Conference on Systems, Man, and Cybernetics. 3039--3044","author":"Ling Sea","year":"2000"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2013.36"},{"key":"e_1_2_1_29_1","first-page":"1","article-title":"Behavioral equivalence of security-oriented interactive systems. IEICE","volume":"8","author":"Liu Guanjun","year":"2016","journal-title":"Trans. Info. Syst. E99-D"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2012.2204741"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2016.2597061"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31131-4_6"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the Conference on Software Engineering and Formal Methods (SEFM\u201914)","author":"Mateo Jos\u00e9 Antonio","year":"2014"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07734-5_4"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1976.1093424"},{"key":"e_1_2_1_37_1","volume-title":"Communicating and Mobile Systems: The Pi-Calculus","author":"Milner Robin"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2013.2258907"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27793-4_4"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2007.41"},{"key":"e_1_2_1_42_1","volume-title":"Myers","author":"Rokicki Tomas G.","year":"1994"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/240518.240530"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.259423"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2015.2426147"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.341845"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.940727"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2014.2301143"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2010.2076397"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/3477.875448"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2010.2047106"},{"key":"e_1_2_1_52_1","first-page":"1127","article-title":"WInternet: From net of things to Internet of Things","volume":"50","author":"Wu Jianjia","year":"2013","journal-title":"J. Comput. Res. Dev."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSCC.2014.11"},{"key":"e_1_2_1_54_1","first-page":"297","article-title":"CTL model checking of time Petri nets using geometric regions. IEICE","volume":"3","author":"Yoneda Tomohiro","year":"1998","journal-title":"Trans. Info. Syst. E99-D"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2015.2497800"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3185502","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3185502","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:36Z","timestamp":1750213596000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3185502"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,30]]},"references-count":54,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4,30]]}},"alternative-id":["10.1145\/3185502"],"URL":"https:\/\/doi.org\/10.1145\/3185502","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,4,30]]},"assertion":[{"value":"2016-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-05-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}