{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T20:14:38Z","timestamp":1761855278598,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319998091"},{"type":"electronic","value":"9783319998107"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99810-7_12","type":"book-chapter","created":{"date-parts":[[2018,9,23]],"date-time":"2018-09-23T17:13:00Z","timestamp":1537722780000},"page":"242-262","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["$$TCTL^{\\varDelta }_h$$ Model Checking of Time Petri\u00a0Nets"],"prefix":"10.1007","author":[{"given":"Naima","family":"Jbeli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohra","family":"Sba\u00ef","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rahma","family":"Ben Ayed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,24]]},"reference":[{"unstructured":"Alur, R.: Techniques for automatic verification of Real-Time System. Ph.D. thesis, Stanford University (1991)","key":"12_CR1"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. (TCS) 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci. (TCS)"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B Berthomieu","year":"1991","unstructured":"Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Softw. Eng. 17, 259\u2013273 (1991)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-36577-X_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Berthomieu","year":"2003","unstructured":"Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of time Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 442\u2013457. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_33"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"1509","DOI":"10.1093\/logcom\/exp036","volume":"19","author":"H Boucheneb","year":"2009","unstructured":"Boucheneb, H., Gardey, G., Roux, O.H.: TCTL model checking of time Petri nets. J. Log. Comput. 19, 1509\u20131540 (2009)","journal-title":"J. Log. Comput."},{"issue":"1:7","key":"12_CR7","first-page":"1","volume":"3","author":"V Bruy\u00e8re","year":"2007","unstructured":"Bruy\u00e8re, V., Raskin, J.F.: Real-time model-checking: parameters everywhere. Log. Methods Comput. Sci. 3(1:7), 1\u201330 (2007)","journal-title":"Log. Methods Comput. Sci."},{"issue":"4","key":"12_CR8","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E. A. Emerson","year":"1992","unstructured":"Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. In: Automatic Verification Methods for Finite State Systems, Grenoble, France, vol. 4, pp. 331\u2013352 (1992)","journal-title":"Real-Time Systems"},{"doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Trefler, J.R.: Parametric quantitative temporal reasoning. In: Logic in Computer Science, pp. 336\u2013343 (1999)","key":"12_CR9","DOI":"10.1109\/LICS.1999.782628"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-40903-8_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G Gardey","year":"2004","unstructured":"Gardey, G., Roux, O.H., Roux, O.F.: Using zone graph method for computing the state space of a time Petri net. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 246\u2013259. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-40903-8_20"},{"unstructured":"Giua, A., DiCesare, F., Silva, M.: Generalized mutual exclusion constraints on nets with uncontrollable transitions. In: IEEE International Conference on SMC (1992)","key":"12_CR11"},{"issue":"42","key":"12_CR12","doi-asserted-by":"publisher","first-page":"4241","DOI":"10.1016\/j.tcs.2009.06.019","volume":"410","author":"R Hadjidj","year":"2009","unstructured":"Hadjidj, R., Boucheneb, H.: On the fly TCTL model checking for time Petri nets. Theor. Comput. Sci. 410(42), 4241\u20134261 (2009)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Hopcroft, J., Ullman, J.: Introduction to Automata Theory. Addison-Wesley, Reading (1979)","key":"12_CR13"},{"unstructured":"David Jansen, N., Roel Wieringa, J.: Reducing the extensions of CTL with actions and real time. Technical report, University of Twente, CTIT (2000)","key":"12_CR14"},{"unstructured":"Jbeli, N., Sba\u00ef, Z., Ben Ayed, R.: $$TCTL^{\\Delta }_{h}$$ for quantitative verification of information systems. In: 4th International Workshop on Advanced Information Systems for Enterprises (IWAISE 2016) (2016)","key":"12_CR15"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-45243-2_30","volume-title":"Computational Collective Intelligence","author":"N Jbeli","year":"2016","unstructured":"Jbeli, N., Sba\u00ef, Z., Ben Ayed, R.: On expressiveness of TCTL$$^{\\varDelta }_h$$ for model checking distributed systems. In: Nguyen, N.-T., Manolopoulos, Y., Iliadis, L., Trawi\u0144ski, B. (eds.) ICCCI 2016. LNCS (LNAI), vol. 9875, pp. 323\u2013332. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45243-2_30"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/3-540-61604-7_73","volume-title":"CONCUR 1996: Concurrency Theory","author":"TA Henzinger","year":"1996","unstructured":"Henzinger, T.A., Kupferman, O., Vardi, M.Y.: A space-efficient on-the-fly algorithm for real-time model checking. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 514\u2013529. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61604-7_73"},{"unstructured":"Laroussinie, F.: Model checking temporis\u00e9: Algorithmes efficaces et complexit\u00e9. Master\u2019s thesis, ENSCachan, D\u00e9cembre 2005","key":"12_CR18"},{"doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Turuani, M., Schnoebelen, Ph.: On the expressivity and complexity of quantitative branching-time temporal logics. Theor. Comput. Sci. 297(1\u20133), 437\u2013446 (2000)","key":"12_CR19","DOI":"10.1007\/10719839_43"},{"issue":"2","key":"12_CR20","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10626-006-8133-9","volume":"16","author":"D Lime","year":"2006","unstructured":"Lime, D., Roux, O.H.: Model checking of time Petri nets using the state class timed automaton. J. Discret. Events Dyn. Syst.-Theory Appl. (DEDS) 16(2), 179\u2013205 (2006)","journal-title":"J. Discret. Events Dyn. Syst.-Theory Appl. (DEDS)"},{"unstructured":"LSV: Dossier scientifique. Ecole Normale Sup\u00e9rieure de Cachan (2004)","key":"12_CR21"},{"unstructured":"Mathieu, S.: M\u00e9thodes qualitatives et quantitatives pour la d\u00e9tection d\u2019information cach\u00e9e. Ph.D. thesis, Universit\u00e9 Pierre et Marie Curie (2011)","key":"12_CR22"},{"unstructured":"Mokadem, H.B.: V\u00e9rification des propri\u00e9t\u00e9s temporis\u00e9es des automates programmables industriels. Ph.D. thesis, Ecole normale superieure de Cachan (2006)","key":"12_CR23"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11539452_12","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"HB Mokadem","year":"2005","unstructured":"Mokadem, H.B., B\u00e9rard, B., Bouyer, P., Laroussinie, F.: A new modality for almost everywhere properties in timed automata. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 110\u2013124. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11539452_12"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/11901914_26","volume-title":"Automated Technology for Verification and Analysis","author":"HB Mokadem","year":"2006","unstructured":"Mokadem, H.B., B\u00e9rard, B., Bouyer, P., Laroussinie, F.: Timed temporal logics for abstracting transient states. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 337\u2013351. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901914_26"},{"issue":"3","key":"12_CR26","first-page":"297","volume":"E99\u2013D","author":"T Yoneda","year":"1998","unstructured":"Yoneda, T., Ryuba, H.: CTL model checking of time Petri nets using geometric regions. IEICE Trans. Inf. Syst. E99\u2013D(3), 297\u2013396 (1998)","journal-title":"IEICE Trans. Inf. Syst."}],"container-title":["Lecture Notes in Computer Science","Transactions on Computational Collective Intelligence XXX"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99810-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T20:27:46Z","timestamp":1752006466000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99810-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319998091","9783319998107"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99810-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}