{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T17:56:08Z","timestamp":1790877368271,"version":"4.1.0"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2006,5,11]],"date-time":"2006-05-11T00:00:00Z","timestamp":1147305600000},"content-version":"unspecified","delay-in-days":10,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2006,5]]},"abstract":"<jats:p>The theory of <jats:italic>Petri Nets<\/jats:italic> provides a general framework to specify the behaviors of real-time reactive systems and <jats:italic>Time Petri Nets<\/jats:italic> were introduced to take also temporal specifications into account. We present in this paper a forward zone-based algorithm to compute the state space of a bounded Time Petri Net: the method is different and more efficient than the classical State Class Graph. We prove the algorithm to be exact with respect to the reachability problem. Furthermore, we propose a translation of the computed state space into a Timed Automaton, proved to be timed bisimilar to the original Time Petri Net. As the method produce a single Timed Automaton, syntactical clocks reduction methods (D<jats:sc>AWS<\/jats:sc> and Y<jats:sc>OVINE<\/jats:sc> for instance) may be applied to produce an automaton with fewer clocks. Then, our method allows to model-check T-TPN by the use of efficient Timed Automata tools.<\/jats:p>","DOI":"10.1017\/s147106840600264x","type":"journal-article","created":{"date-parts":[[2006,5,11]],"date-time":"2006-05-11T11:22:00Z","timestamp":1147346520000},"page":"301-320","source":"Crossref","is-referenced-by-count":28,"title":["State space computation and analysis of Time Petri Nets"],"prefix":"10.1017","volume":"6","author":[{"given":"GUILLAUME","family":"GARDEY","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"OLIVIER H.","family":"ROUX","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"OLIVIER F.","family":"ROUX","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2006,5,11]]},"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S147106840600264X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T15:43:32Z","timestamp":1554047012000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S147106840600264X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,5]]},"references-count":0,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,5]]}},"alternative-id":["S147106840600264X"],"URL":"https:\/\/doi.org\/10.1017\/s147106840600264x","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,5]]}}}