{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T02:27:25Z","timestamp":1786760845671,"version":"build-2736575974"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T00:00:00Z","timestamp":1786752000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T00:00:00Z","timestamp":1786752000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2026,12]]},"DOI":"10.1007\/s11334-026-00653-5","type":"journal-article","created":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T01:46:29Z","timestamp":1786758389000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Factorization of the state space construction for cyclic systems with data"],"prefix":"10.1007","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9979-3829","authenticated-orcid":false,"given":"Johan","family":"Arcile","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Raymond","family":"Devillers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hanna","family":"Klaudel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,8,15]]},"reference":[{"issue":"1","key":"653_CR1","doi-asserted-by":"publisher","first-page":"204","DOI":"10.3390\/su11010204","volume":"11","author":"S Ahmad","year":"2019","unstructured":"Ahmad S, Malik S, Ullah I, Park D-H, Kim K, Kim DH (2019) Towards the design of a formal verification and evaluation tool of real-time tasks scheduling of IoT applications. Sustainability 11(1):204","journal-title":"Sustainability"},{"issue":"2","key":"653_CR2","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 DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"653_CR3","doi-asserted-by":"crossref","unstructured":"Andr\u00e9\u00c9, Fribourg L, K\u00fchne U, Soulat R (2012) IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In: Dimitra G, Dominique M (eds) FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, vol 7436 of Lecture Notes in Computer Science. Springer, pp. 33\u201336","DOI":"10.1007\/978-3-642-32759-9_6"},{"issue":"6","key":"653_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3534967","volume":"55","author":"J Arcile","year":"2023","unstructured":"Arcile J, Andr\u00e9 \u00c9 (2023) Timed automata as a formalism for expressing security: a survey on theory and practice. ACM Comput Surv 55(6):1\u201336","journal-title":"ACM Comput Surv"},{"issue":"3","key":"653_CR5","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/s10458-019-09409-x","volume":"33","author":"J Arcile","year":"2019","unstructured":"Arcile J, Devillers RR, Klaudel H (2019) Verifcar: a framework for modeling and model checking communicating autonomous vehicles. Auton Agents Multi Agent Syst 33(3):353\u2013381","journal-title":"Auton Agents Multi Agent Syst"},{"issue":"1\u20134","key":"653_CR6","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3233\/FI-2020-1948","volume":"175","author":"J Arcile","year":"2020","unstructured":"Arcile J, Devillers RR, Klaudel H (2020) Dynamic exploration of multi-agent systems with periodic timed tasks. Fundam Informaticae 175(1\u20134):59\u201395","journal-title":"Fundam Informaticae"},{"key":"653_CR7","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.46.680","author":"JE Barnes","year":"2011","unstructured":"Barnes JE (2011) Experiences in the industrial use of formal methods. Commun Eur Assoc Softw Sci Technol Electron. https:\/\/doi.org\/10.14279\/tuj.eceasst.46.680","journal-title":"Commun Eur Assoc Softw Sci Technol Electron"},{"key":"653_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/3-540-36577-X_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7\u201311, 2003, Proceedings","author":"G Behrmann","year":"2003","unstructured":"Behrmann G, Bouyer P, Fleury E, Larsen KG (2003) Static guard analysis in timed automata verification. In: Garavel H, Hatcliff J (eds) Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7\u201311, 2003, Proceedings, vol 2619. Lecture Notes in Computer Science. Springer, pp 254\u2013277"},{"key":"653_CR9","doi-asserted-by":"crossref","unstructured":"Berthomieu B, Vernadat F (2006) Time petri nets analysis with TINA. In: Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 11-14 September 2006, Riverside, California, USA. IEEE Computer Society, pp. 123\u2013124","DOI":"10.1109\/QEST.2006.56"},{"key":"653_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0055357","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems, 5th International Symposium, FTRTFT\u201998, Lyngby, Denmark, September 14\u201318, 1998, Proceedings","author":"M Bozga","year":"1998","unstructured":"Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) KRONOS: A model-checking tool for real-time systems (tool-presentation for FTRTFT \u201998). In: Ravn AP, Rischel H (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems, 5th International Symposium, FTRTFT\u201998, Lyngby, Denmark, September 14\u201318, 1998, Proceedings, vol 1486. Lecture Notes in Computer Science. Springer, pp 298\u2013302"},{"key":"653_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/3-540-45416-0_21","volume-title":"Computer Safety, Reliability and Security, 20th International Conference, SAFECOMP 2001, Budapest, Hungary, September 26\u201328, 2001, Proceedings","author":"P Caspi","year":"2001","unstructured":"Caspi P, Mazuet C, Paligot NR (2001) About the design of distributed control systems: The quasi-synchronous approach. In: Voges U (ed) Computer Safety, Reliability and Security, 20th International Conference, SAFECOMP 2001, Budapest, Hungary, September 26\u201328, 2001, Proceedings, vol 2187. Lecture Notes in Computer Science. Springer, pp 215\u2013226"},{"issue":"3\/4","key":"653_CR12","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1504\/IJES.2006.014854","volume":"2","author":"AMK Cheng","year":"2006","unstructured":"Cheng AMK (2006) A survey of formal verification methods and tools for embedded and real-time systems. Int J Embed Syst 2(3\/4):184\u2013195","journal-title":"Int J Embed Syst"},{"key":"653_CR13","doi-asserted-by":"crossref","unstructured":"Dabaghchian M, Rakamaric Z (2019) A timeless model for the verification of quasi-periodic distributed systems. In: Roop PS, Zhan N, Gao S, Nuzzo P (eds) Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2019, La Jolla, CA, USA, October 9-11, 2019. ACM, pp. 4:1\u20134:11","DOI":"10.1145\/3359986.3361201"},{"key":"#cr-split#-653_CR14.1","doi-asserted-by":"crossref","unstructured":"Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: Steffen B","DOI":"10.1007\/BFb0054180"},{"key":"#cr-split#-653_CR14.2","unstructured":"(ed) Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, vol 1384. Lecture Notes in Computer Science. Springer, pp 313-329"},{"key":"653_CR15","doi-asserted-by":"crossref","unstructured":"Dutertre B, Sorea M (2004) Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata. In Lakhnech Y, Yovine S (eds) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings, volume 3253 of Lecture Notes in Computer Science. Springer, pp. 199\u2013214","DOI":"10.1007\/978-3-540-30206-3_15"},{"key":"653_CR16","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft JE, Ullman JD (1979) Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company"},{"key":"653_CR17","unstructured":"Verifcar models. https:\/\/forge.ibisc.univ-evry.fr\/jarcile\/VerifCar. Accessed 29 May 2023"},{"key":"653_CR18","doi-asserted-by":"crossref","unstructured":"Marta Z, Kwiatkowska, Norman G, Parker D (2004) PRISM 2.0: a tool for probabilistic model checking. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), 27-30 September 2004, Enschede, The Netherlands. IEEE Computer Society, pp. 322\u2013323","DOI":"10.1109\/QEST.2004.1348048"},{"issue":"1\u20132","key":"653_CR19","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1\u20132):134\u2013152","journal-title":"Int J Softw Tools Technol Transf"},{"key":"653_CR20","doi-asserted-by":"crossref","unstructured":"Legay A, Delahaye B, Bensalem S (2010) Statistical model checking: an overview. In: Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (eds) Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings, vol. 6418 of Lecture Notes in Computer Science. Springer, pp. 122\u2013135","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"653_CR21","doi-asserted-by":"crossref","unstructured":"Lime D, Roux OH, Seidner C, Traonouez L-M (2009) Romeo: A parametric model-checker for petri nets with stopwatches. In: Kowalewski S, Philippou A (eds) Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, vol. 5505 of Lecture Notes in Computer Science. Springer, pp. 54\u201357","DOI":"10.1007\/978-3-642-00768-2_6"},{"issue":"3","key":"653_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3323212","volume":"52","author":"C Maiza","year":"2019","unstructured":"Maiza C, Rihani H, Rivas JM, Goossens J, Altmeyer S, Davis RI (2019) A survey of timing verification techniques for multi-core real-time systems. ACM Comput Surv 52(3):1\u201338","journal-title":"ACM Comput Surv"},{"key":"653_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/978-3-540-75596-8_21","volume-title":"Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22\u201325, 2007, Proceedings","author":"I Saha","year":"2007","unstructured":"Saha I, Misra J, Roy S (2007) Timeout and calendar based finite state modeling and verification of real-time systems. In: Namjoshi KS, Yoneda T, Higashino T, Okamura Y (eds) Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22\u201325, 2007, Proceedings, vol 4762. Lecture Notes in Computer Science. Springer, pp 284\u2013299"},{"issue":"4","key":"653_CR24","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/S0950-5849(00)00166-X","volume":"43","author":"CF Snook","year":"2001","unstructured":"Snook CF, Harrison R (2001) Practitioners\u2019 views on the use of formal methods: an industrial survey by structured interview. Inf Softw Technol 43(4):275\u2013283","journal-title":"Inf Softw Technol"},{"issue":"4","key":"653_CR25","doi-asserted-by":"publisher","first-page":"2614","DOI":"10.1109\/JSYST.2015.2496293","volume":"11","author":"X Zheng","year":"2017","unstructured":"Zheng X, Julien C, Kim M, Khurshid S (2017) Perceptions on the state of the art in verification and validation in cyber-physical systems. IEEE Syst J 11(4):2614\u20132627","journal-title":"IEEE Syst J"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-026-00653-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-026-00653-5","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-026-00653-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T01:46:32Z","timestamp":1786758392000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-026-00653-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8,15]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,12]]}},"alternative-id":["653"],"URL":"https:\/\/doi.org\/10.1007\/s11334-026-00653-5","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,8,15]]},"assertion":[{"value":"25 September 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 August 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 August 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"23"}}