{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:58:37Z","timestamp":1762459117555},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,5,15]],"date-time":"2013-05-15T00:00:00Z","timestamp":1368576000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,12]]},"DOI":"10.1007\/s10703-013-0188-2","type":"journal-article","created":{"date-parts":[[2013,5,14]],"date-time":"2013-05-14T09:51:14Z","timestamp":1368525074000},"page":"493-519","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic unfolding of parametric stopwatch Petri nets"],"prefix":"10.1007","volume":"43","author":[{"given":"Claude","family":"Jard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Didier","family":"Lime","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier H.","family":"Roux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louis-Marie","family":"Traonouez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,5,15]]},"reference":[{"key":"188_CR1","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/10722167_37","volume-title":"Proceedings of CAV","author":"PA Abdulla","year":"2000","unstructured":"Abdulla PA, Iyer SP, Nylen A (2000) Unfoldings of unbounded Petri nets. In: Proceedings of CAV. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 495\u2013507"},{"issue":"2","key":"188_CR2","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1016\/S0304-3975(99)00114-0","volume":"243","author":"T Aura","year":"2000","unstructured":"Aura T, Lilius J (2000) A causal semantics for time Petri nets. Theor Comput Sci 243(2):409\u2013447","journal-title":"Theor Comput Sci"},{"key":"188_CR3","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"442","DOI":"10.1007\/3-540-44618-4_32","volume-title":"CONCUR","author":"P Baldan","year":"2000","unstructured":"Baldan P, Busi N, Corradini A, Pinna GM (2000) Functorial concurrent semantics for Petri nets with read and inhibitor arcs. In: CONCUR. Lecture notes in computer science, vol 1877. Springer, Berlin, pp\u00a0442\u2013457"},{"issue":"3","key":"188_CR4","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B Berthomieu","year":"1991","unstructured":"Berthomieu B, Diaz M (1991) Modeling and verification of time dependent systems using time Petri nets. IEEE Trans Softw Eng 17(3):259\u2013273","journal-title":"IEEE Trans Softw Eng"},{"issue":"2","key":"188_CR5","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s10626-006-0011-y","volume":"17","author":"B Berthomieu","year":"2007","unstructured":"Berthomieu B, Lime D, Roux OH, Vernadat F (2007) Reachability problems and abstract state spaces for time Petri nets with stopwatches. Discrete Event Dyn Syst 17(2):133\u2013158","journal-title":"Discrete Event Dyn Syst"},{"key":"188_CR6","series-title":"IFIP congress series","first-page":"41","volume-title":"Information processing: proceedings of the IFIP congress 1983","author":"B Berthomieu","year":"1983","unstructured":"Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time Petri nets. In: Mason REA (ed) Information processing: proceedings of the IFIP congress 1983. IFIP congress series, vol 9. Elsevier Science, Amsterdam, pp 41\u201346"},{"key":"188_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/11901914_23","volume-title":"Proceedings of the 4th international symposium on automated technology for verification and analysis (ATVA\u201906)","author":"P Bouyer","year":"2006","unstructured":"Bouyer P, Haddad S, Reynier PA (2006) Timed unfoldings for networks of timed automata. In: Graf S, Zhang W (eds) Proceedings of the 4th international symposium on automated technology for verification and analysis (ATVA\u201906), Beijing, China. Lecture notes in computer science, vol 4218. Springer, Berlin, pp 292\u2013306"},{"key":"188_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/11901914_24","volume-title":"Proceedings of the 4th international symposium on automated technology for verification and analysis (ATVA\u201906)","author":"F Cassez","year":"2006","unstructured":"Cassez F, Chatain T, Jard C (2006) Symbolic unfoldings for networks of timed automata. In: Graf S, Zhang W (eds) Proceedings of the 4th international symposium on automated technology for verification and analysis (ATVA\u201906), Beijing, China. Lecture notes in computer science, vol 4218. Springer, Berlin, pp 307\u2013321"},{"key":"188_CR9","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/11767589_8","volume-title":"Proceedings of ICATPN","author":"T Chatain","year":"2006","unstructured":"Chatain T, Jard C (2006) Complete finite prefixes of symbolic unfoldings of safe time Petri nets. In: Proceedings of ICATPN. Lecture notes in computer science, vol 4024. Springer, Berlin, pp 125\u2013145"},{"issue":"4","key":"188_CR10","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/j.ipl.2007.06.002","volume":"104","author":"T Chatain","year":"2007","unstructured":"Chatain T, Khomenko V (2007) On the well-foundedness of adequate orders used for construction of complete unfolding prefixes. Inf Process Lett 104(4):129\u2013136","journal-title":"Inf Process Lett"},{"key":"188_CR11","first-page":"197","volume-title":"Proceedings of workshop on computer aided verification methods for finite state systems","author":"D Dill","year":"1989","unstructured":"Dill D (1989) Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of workshop on computer aided verification methods for finite state systems, vol 407, pp 197\u2013212"},{"key":"188_CR12","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0167-6423(94)00019-0","volume":"23","author":"J Esparza","year":"1994","unstructured":"Esparza J (1994) Model checking using net unfoldings. Sci Comput Program 23:151\u2013195","journal-title":"Sci Comput Program"},{"key":"188_CR13","series-title":"Monographs in theoretical computer science","volume-title":"Unfoldings, a partial-order approach to model checking","author":"J Esparza","year":"2008","unstructured":"Esparza J, Heljanko K (2008) Unfoldings, a partial-order approach to model checking. Monographs in theoretical computer science. Springer, Berlin"},{"issue":"3","key":"188_CR14","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1023\/A:1014746130920","volume":"20","author":"J Esparza","year":"2002","unstructured":"Esparza J, R\u00f6mer S, Vogler W (2002) An improvement of McMillan\u2019s unfolding algorithm. Form Methods Syst Des 20(3):285\u2013310","journal-title":"Form Methods Syst Des"},{"issue":"1","key":"188_CR15","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10626-005-5238-5","volume":"15","author":"E Fabre","year":"2005","unstructured":"Fabre E, Benveniste A, Haar S, Jard C (2005) Distributed monitoring of concurrent and asynchronous systems. Discrete Event Dyn Syst 15(1):33\u201384","journal-title":"Discrete Event Dyn Syst"},{"issue":"3","key":"188_CR16","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1017\/S147106840600264X","volume":"6","author":"G Gardey","year":"2006","unstructured":"Gardey G, Roux OH, Roux OF (2006) State space computation and analysis of time Petri nets. Theory Pract Log Program 6(3):301\u2013320. Special issue on specification analysis and verification of reactive systems","journal-title":"Theory Pract Log Program"},{"key":"188_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-642-15297-9_12","volume-title":"8th international conference on formal modelling and analysis of timed systems (FORMATS 2010)","author":"B Grabiec","year":"2010","unstructured":"Grabiec B, Traonouez LM, Jard C, Lime D, Roux OH (2010) Diagnosis using unfoldings of parametric time Petri nets. In: Chatterjee K, Henzinger TA (eds) 8th international conference on formal modelling and analysis of timed systems (FORMATS 2010), Vienna, Austria. Lecture notes in computer science, vol 6246. Springer, Berlin, pp 137\u2013151"},{"key":"188_CR18","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T Henzinger","year":"1998","unstructured":"Henzinger T, Kopke P, Puri A, Varaiya P (1998) What\u2019s decidable about hybrid automata? J Comput Syst Sci 57:94\u2013124","journal-title":"J Comput Syst Sci"},{"key":"188_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1007\/3-540-36577-X_34","volume-title":"Proceedings of TACAS","author":"V Khomenko","year":"2003","unstructured":"Khomenko V, Koutny M (2003) Branching processes of high-level Petri nets. In: Proceedings of TACAS. Lecture notes in computer science, vol 2619. Springer, Berlin, pp 458\u2013472"},{"key":"188_CR20","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1109\/REAL.2004.9","volume-title":"25th IEEE real-time systems symposium (RTSS 2004)","author":"D Lime","year":"2004","unstructured":"Lime D, Roux OH (2004) A translation-based method for the timed analysis of scheduling extended time Petri nets. In: 25th IEEE real-time systems symposium (RTSS 2004), Lisbon, Portugal. IEEE Computer Society Press, Los Alamitos, pp 187\u2013196"},{"issue":"2","key":"188_CR21","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s10626-006-8133-9","volume":"16","author":"D Lime","year":"2006","unstructured":"Lime D, Roux OH (2006) Model checking of time Petri nets using the state class timed automaton. Discrete Event Dyn Syst 16(2):179\u2013205","journal-title":"Discrete Event Dyn Syst"},{"issue":"2","key":"188_CR22","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/s11241-008-9059-0","volume":"41","author":"D Lime","year":"2009","unstructured":"Lime D, Roux OH (2009) Formal verification of real-time systems with preemptive scheduling. Real-Time Syst 41(2):118\u2013151","journal-title":"Real-Time Syst"},{"key":"188_CR23","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-642-00768-2_6","volume-title":"15th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2009)","author":"D Lime","year":"2009","unstructured":"Lime D, Roux OH, Seidner C, Traonouez LM (2009) Romeo: a parametric model-checker for Petri nets with stopwatches. In: Kowalewski S, Philippou A (eds) 15th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2009), York, United Kingdom. Lecture notes in computer science, vol 5505. Springer, Berlin, pp 54\u201357"},{"key":"188_CR24","series-title":"Lecture notes in computer science","volume-title":"An improvement of McMillan\u2019s unfolding algorithm","year":"1996","unstructured":"Margaria T, Steffen B (eds) (1996) An improvement of McMillan\u2019s unfolding algorithm, Passau, Germany. Lecture notes in computer science, vol 1055. Springer, Berlin"},{"key":"188_CR25","series-title":"Lecture notes in computer science","first-page":"164","volume-title":"Proceedings of computer aided verification (CAV\u201992)","author":"KL McMillan","year":"1992","unstructured":"McMillan KL (1992) Using unfolding to avoid the state space explosion problem in the verification of asynchronous circuits. In: Proceedings of computer aided verification (CAV\u201992). Lecture notes in computer science, vol 663. Springer, Berlin, pp 164\u2013177"},{"key":"188_CR26","unstructured":"Merlin PM (1974) A study of the recoverability of computing systems. PhD thesis, Department of Information and Computer Science, University of California, Irvine, CA"},{"key":"188_CR27","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-642-15643-4_22","volume-title":"8th international symposium on automated technology for verification and analysis (ATVA 2010)","author":"LM Traonouez","year":"2010","unstructured":"Traonouez LM, Grabiec B, Jard C, Lime D, Roux OH (2010) Symbolic unfolding of parametric stopwatch Petri nets. In: Bouajjani A, Chin WN (eds) 8th international symposium on automated technology for verification and analysis (ATVA 2010), Singapore. Lecture notes in computer science, vol 6252. Springer, Berlin, pp 291\u2013305"},{"issue":"17","key":"188_CR28","first-page":"3273","volume":"15","author":"LM Traonouez","year":"2009","unstructured":"Traonouez LM, Lime D, Roux OH (2009) Parametric model-checking of stopwatch Petri nets. J Univers Comput Sci 15(17):3273\u20133304","journal-title":"J Univers Comput Sci"},{"key":"188_CR29","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/BFb0055644","volume-title":"9th international conference on concurrency theory (CONCUR\u201998)","author":"W Vogler","year":"1998","unstructured":"Vogler W, Semenov AL, Yakovlev A (1998) Unfolding and finite prefix for nets with read arcs. In: Sangiorgi D, de Simone R (eds) 9th international conference on concurrency theory (CONCUR\u201998), Nice, France. Lecture notes in computer science, vol 1466. Springer, Berlin, pp 501\u2013516"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0188-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0188-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0188-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:53Z","timestamp":1559253953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0188-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,15]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["188"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0188-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5,15]]}}}