{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:19:41Z","timestamp":1777645181283,"version":"3.51.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"4","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Fundamenta Informaticae"],"published-print":{"date-parts":[[2014,12]]},"abstract":"<jats:p>Time Petri nets by Merlin and Farber are a powerful modelling formalism. However, symbolic model checking methods for them consider in most cases the nets which are 1-safe, i.e., allow the places to contain at most one token. In our paper we present an approach which applies symbolic verification to testing reachability for time Petri nets without this restriction. We deal with the class of bounded nets restricted to disallow multiple enabledness of transitions, and present the method of reachability testing based on a translation into a satisfiability modulo theory (SMT).<\/jats:p>","DOI":"10.3233\/fi-2014-1135","type":"journal-article","created":{"date-parts":[[2019,12,3]],"date-time":"2019-12-03T01:21:47Z","timestamp":1575336107000},"page":"467-482","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":3,"title":["SMT-Based Reachability Checking for Bounded Time Petri Nets"],"prefix":"10.1177","volume":"135","author":[{"given":"Agata","family":"P\u00f3\u0142rola","sequence":"first","affiliation":[{"name":"Faculty of Mathematics and Computer Science, University of \u0141\u00f3d\u017a, Banacha 22, 90-238 \u0141\u00f3d\u017a, Poland. {polrola,cybula}@math.uni.lodz.pl"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Cybula","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics and Computer Science, University of \u0141\u00f3d\u017a, Banacha 22, 90-238 \u0141\u00f3d\u017a, Poland. {polrola,cybula}@math.uni.lodz.pl"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"M\u0119ski","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics and Computer Science, University of \u0141\u00f3d\u017a, Banacha 22, 90-238 \u0141\u00f3d\u017a, Poland"},{"name":"Institute of Computer Science, PAS, Warsaw, Poland. meski@ipipan.waw.pl"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2014,1]]},"container-title":["Fundamenta Informaticae"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2014-1135","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2014-1135","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:31:33Z","timestamp":1777444293000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/FI-2014-1135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1]]},"references-count":0,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["10.3233\/FI-2014-1135"],"URL":"https:\/\/doi.org\/10.3233\/fi-2014-1135","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,1]]}}}