{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T17:42:16Z","timestamp":1648834936813},"reference-count":22,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. &amp; Syst."],"published-print":{"date-parts":[[2020,3,1]]},"DOI":"10.1587\/transinf.2019edl8086","type":"journal-article","created":{"date-parts":[[2020,2,29]],"date-time":"2020-02-29T22:10:34Z","timestamp":1583014234000},"page":"702-705","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking"],"prefix":"10.1587","volume":"E103.D","author":[{"given":"Nao","family":"IGAWA","sequence":"first","affiliation":[{"name":"Okayama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomoyuki","family":"YOKOGAWA","sequence":"additional","affiliation":[{"name":"Okayama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sousuke","family":"AMASAKI","sequence":"additional","affiliation":[{"name":"Okayama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masafumi","family":"KONDO","sequence":"additional","affiliation":[{"name":"Kawasaki University of Medical Welfare"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoichiro","family":"SATO","sequence":"additional","affiliation":[{"name":"Okayama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazutami","family":"ARIMOTO","sequence":"additional","affiliation":[{"name":"Okayama Prefectural University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] S. Bernardi, J. Campos, and J. Merseguer, \u201cTiming-Failure Risk Assessment of UML Design Using Time Petri Net Bound Techniques,\u201d IEEE Trans. Industr. Inform., vol.7, no.1, pp.90-104, 2011. 10.1109\/tii.2010.2098415","DOI":"10.1109\/TII.2010.2098415"},{"key":"2","doi-asserted-by":"crossref","unstructured":"[2] Y.H. Kacem, A. Magdich, A. Mahfoudhi, C. Mraidha, and W. Karamti, \u201cUsing MDE and Priority Time Petri Nets for the schedulability analysis of Embedded Systems modeled by UML activity diagrams,\u201d Proc. IEEE 19th Int&apos;l Conf. and Workshops on Eng. Comp. Based Syst. (ECBS 2012), pp.316-323, 2012. 10.1109\/ecbs.2012.6487436","DOI":"10.1109\/ecbs.2012.6487436"},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] P. Merlin and D. Farber, \u201cRecoverability of Communication Protocols-Implications of a Theoretical Study,\u201d IEEE Trans. Comm., vol.24, no.9, pp.1036-1043, Sept. 1976. 10.1109\/tcom.1976.1093424","DOI":"10.1109\/TCOM.1976.1093424"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] B. Berthomieu, P.-O. Ribet, and F. Vernadat, \u201cThe tool TINA-Construction of abstract state spaces for Petri nets and Time Petri nets,\u201d International Journal of Production Research, vol.42, no.14, pp.2741-2756, 2007. 10.1080\/00207540412331312688","DOI":"10.1080\/00207540412331312688"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] D. Lime, O.H. Roux, C. Seidner, and L.-M. Traonouez, \u201cRomeo: A parametric model-checker for petri nets with stopwatches,\u201d Proc. 15th Int&apos;l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), pp.54-57, 2009. 10.1007\/978-3-642-00768-2_6","DOI":"10.1007\/978-3-642-00768-2_6"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani, \u201cSAT-Based bounded model checking for timed systems,\u201d Proc. 22nd IFIP WG 6.1 Int&apos;l Conf. Houston on Formal Tech. for Networked and Distributed Syst. (FORTE 2002), pp.243-259, 2002. 10.1007\/3-540-36135-9_16","DOI":"10.1007\/3-540-36135-9_16"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] M. Sorea, \u201cBounded Model Checking for Timed Automata,\u201d Electron. Notes Theor. Comput. Sci., vol.68, no.5, pp.116-134, May 2003. 10.1016\/s1571-0661(04)80523-1","DOI":"10.1016\/S1571-0661(04)80523-1"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[8] Z. Chen, Z. Xu, J. Du, M. Mei, and J. Guo, \u201cEfficient Encoding for Bounded Model Checking of Timed Automata,\u201d IEEJ Transactions on Electrical and Electronic Engineering, vol.12, no.5, pp.710-720, 2017. 10.1002\/tee.22457","DOI":"10.1002\/tee.22457"},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, \u201cSymbolic Model Checking without BDDs,\u201d Proc. 5th Int&apos;l Conf. Tools and Algorithms for Construction and Analysis of Syst. (TACAS &apos;99), vol.1579, pp.193-207, 1999. 10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] T. Yokogawa, M. Kondo, H. Miyazaki, S. Amasaki, Y. Sato, and K. Arimoto, \u201cBounded model checking of Time Petri Nets using SAT solver,\u201d IEICE Electronics Express, vol.12, no.2, p.20141112, Jan. 2015. 10.1587\/elex.11.20141112","DOI":"10.1587\/elex.11.20141112"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] S. Ogata, T. Tsuchiya, and T. Kikuno, \u201cSAT-Based Verification of Safe Petri Nets,\u201d Proc. Second Int&apos;l Conf. Automated Technology for Verification and Analysis (ATVA 2004), vol.3299, pp.79-92, 2004. 10.1007\/978-3-540-30476-0_11","DOI":"10.1007\/978-3-540-30476-0_11"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] N. Igawa, T. Yokogawa, S. Amasaki, K. Komoku, Y. Sato, and K. Arimoto, \u201cInterpolation Based Unbounded Model Checking for Time Petri Nets,\u201d Proc. 2018 IEEE 7th Global Conf. Consumer Electronics (GCCE), pp.587-591, 2018. 10.1109\/gcce.2018.8574651","DOI":"10.1109\/GCCE.2018.8574651"},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] S. Cotton and O. Maler, \u201cFast and Flexible Difference Constraint Propagation for DPLL(T),\u201d Proc. 9th Int&apos;l Conf. Theory and Applications of Satisfiability Testing (SAT 2006), vol.4121, pp.170-183, 2006. 10.1007\/11814948_19","DOI":"10.1007\/11814948_19"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] J. Sifakis, \u201cPerformance evaluation of systems using nets,\u201d Net Theory and Applications, LNCS, vol.84, pp.307-319, 1980. 10.1007\/3-540-10001-6_30","DOI":"10.1007\/3-540-10001-6_30"},{"key":"15","unstructured":"[15] \u201cSMT-COMP 2018,\u201d http:\/\/smtcomp.sourceforge.net\/2018\/"},{"key":"16","unstructured":"[16] R. Bruttomesso, A. Cimatti, A. Franz\u00e9n, A. Griggio, and R. Sebastiani, \u201cThe M<sub>ATH<\/sub>SAT<sub>4<\/sub> SMT Solver,\u201d Proc. 20th Int&apos;l Conf. Computer Aided Verification (CAV 2008), vol.5123, pp.299-303, 2008. 10.1007\/978-3-540-70545-1_28"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] L. De Moura and N. Bj\u00f8rner, \u201cZ3: An efficient SMT Solver,\u201d Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol.4963, LNCS, pp.337-340, 2008. 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"18","doi-asserted-by":"crossref","unstructured":"[18] J. Christ, J. Hoenicke, and A. Nutz, \u201cSMTInterpol: an Interpolating SMT Solver,\u201d Proc. 19th Int&apos;l SPIN Workshop on Model Checking of Softw. (SPIN 2012), vol.7385, pp.248-254, 2012. 10.1007\/978-3-642-31759-0_19","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"19","doi-asserted-by":"publisher","unstructured":"[19] B. Dutertre, \u201cYices 2.2,\u201d Proc. 26th Int&apos;l Conf.n Computer Aided Verification (CAV 2014), vol.8559, pp.737-744, 2014. 10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"20","doi-asserted-by":"crossref","unstructured":"[20] C. Barrett, C.L. Conway, M. Deters, L. Hadarean, D. Jovanovi\u0107, T. King, A. Reynolds, and C. Tinelli, \u201cCVC4,\u201d Proc. 23rd Int&apos;l Conf. Computer Aided Verification (CAV 2011), pp.171-177, 2011. 10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"21","doi-asserted-by":"crossref","unstructured":"[21] K.L. McMillan, \u201cInterpolation and SAT-Based Model Checking,\u201d Proc. 15th Int&apos;l Conf. Computer Aided Verification (CAV 2003), vol.2725, pp.1-13, 2003. 10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"22","doi-asserted-by":"crossref","unstructured":"[22] B. Li and F. Somenzi, \u201cEfficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking,\u201d Proc. 12th Int&apos;l Conf. Tools and Algorithms for the Construction and Analysis of Syst. (TACAS 2006), vol.3920, pp.227-241, 2006. 10.1007\/11691372_15","DOI":"10.1007\/11691372_15"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E103.D\/3\/E103.D_2019EDL8086\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,7]],"date-time":"2020-03-07T03:26:26Z","timestamp":1583551586000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E103.D\/3\/E103.D_2019EDL8086\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,1]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2019edl8086","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,3,1]]}}}