{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T17:21:30Z","timestamp":1758129690030,"version":"3.44.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:00:00Z","timestamp":1755907200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:00:00Z","timestamp":1755907200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007241","name":"Universit\u00e9 Paris-Saclay","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007241","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this article, we focus on improving the efficiency of diagnosability checking for real-time systems modeled as timed automata. Inspired by a recently introduced extension of the classic CEGAR (CounterExample-Guided Abstraction Refinement) algorithm, namely the RECAR (Recursive Explore and Check Abstraction Refinement) algorithm, we propose new RECAR-like algorithms that combine over-approximation and under-approximation techniques. We use CEGAR to quickly terminate the refinement loop by over-approximation and under-approximation, in the case where the original formula is respectively satisfiable or unsatisfiable, and then show the soundness of our RECAR-like approach applied to an arbitrary formula. We define then several types of parameterized over- and under-approximations along with refinement strategies for the diagnosability problem. Finally, we evaluate the effectiveness of our method and its implementation with the Z3 SMT solver on different benchmarks by comparing it to the direct method without approximation shortcuts.<\/jats:p>","DOI":"10.1007\/s10626-025-00420-x","type":"journal-article","created":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T12:30:36Z","timestamp":1755952236000},"page":"267-299","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An approximation-based incremental SMT approach for diagnosability analysis of real-time systems"],"prefix":"10.1007","volume":"35","author":[{"given":"Lulu","family":"He","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1679-0804","authenticated-orcid":false,"given":"Philippe","family":"Dague","sequence":"additional","affiliation":[]},{"given":"Lina","family":"Ye","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,8,23]]},"reference":[{"issue":"2","key":"420_CR1","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. Theoretical Comput Sci 126(2):183\u2013235","journal-title":"Theoretical Comput Sci"},{"key":"420_CR2","doi-asserted-by":"crossref","unstructured":"Badban B, Lange M (2011) Exact incremental analysis of timed automata with an smt-solver. In: Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS\u201911). LNCS, vol. 6919. Springer, NY, USA","DOI":"10.1007\/978-3-642-24310-3_13"},{"key":"420_CR3","unstructured":"Bittner B, Bozzano M, Cimatti A (2016) Automated synthesis of timed failure propagation graphs. In: Proceedings of the 25th international joint conference on artificial intelligence (IJCAI\u201916), pp 972\u2013978"},{"key":"420_CR4","doi-asserted-by":"crossref","unstructured":"Bittner B, Bozzano M, Cimatti A, Zampedri G (2016) Automated verification and tightening of failure propagation models. In: Proceedings of the 30th conference on artificial intelligence (AAAI\u201916), pp 907\u2013913","DOI":"10.1609\/aaai.v30i1.10094"},{"issue":"2","key":"420_CR5","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/S10009-021-00606-2","volume":"23","author":"P Bouyer","year":"2021","unstructured":"Bouyer P, Henry L, Jaziri S, J\u00e9ron T, Markey N (2021) Diagnosing timed automata using timed markings. Int J Softw Tools Technol Transf 23(2):229\u2013253. https:\/\/doi.org\/10.1007\/S10009-021-00606-2","journal-title":"Int J Softw Tools Technol Transf"},{"key":"420_CR6","doi-asserted-by":"crossref","unstructured":"Bouyer P, Chevalier F, D\u2019Souza D (2005) Fault diagnosis using timed automata. In: Proceedings of international conference on foundations of software science and computation structures (FoSSaCS\u201905). Lecture Notes in Computer Science. Springer, NY, USA","DOI":"10.1007\/978-3-540-31982-5_14"},{"key":"420_CR7","doi-asserted-by":"publisher","unstructured":"Bouyer P, Jaziri S, Markey N (2018) Efficient timed diagnosis using automata with timed domains. In: Colombo C, Leucker M (eds.) Proceedings of the 18th International Conference on Runtime Verification (RV\u201918). LNCS, vol. 11237, pp 205\u2013221. Springer, NY, USA. https:\/\/doi.org\/10.1007\/978-3-030-03769-7_12","DOI":"10.1007\/978-3-030-03769-7_12"},{"key":"420_CR8","doi-asserted-by":"crossref","unstructured":"Bozzano M, Cimatti A, Gario M, Micheli A (2015) Smt-based validation of timed failure propagation graphs. In: Proceedings of the 29th conference on artificial intelligence (AAAI\u201915), pp 3724\u20133730","DOI":"10.1609\/aaai.v29i1.9753"},{"key":"420_CR9","doi-asserted-by":"crossref","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification CAV 2000. Lecture Notes in Computer Science, vol. 1855, Springer, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"420_CR10","doi-asserted-by":"publisher","unstructured":"Dierks H, Kupferschmid S, Larsen KG (2007) Automatic abstraction refinement for timed automata. In: Raskin J, Thiagarajan PS (eds.) Formal Modeling and Analysis of Timed Systems, Proceedings of the 5th International Conference, FORMATS 2007, Salzburg. LNCS, vol. 4763, pp. 114\u2013129. Springer, NY, USA. https:\/\/doi.org\/10.1007\/978-3-540-75454-1_10","DOI":"10.1007\/978-3-540-75454-1_10"},{"issue":"2","key":"420_CR11","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/J.AUTOMATICA.2008.06.022","volume":"45","author":"S Genc","year":"2009","unstructured":"Genc S, Lafortune S (2009) Predictability of event occurrences in partially-observed discrete-event systems. Autom 45(2):301\u2013311. https:\/\/doi.org\/10.1016\/J.AUTOMATICA.2008.06.022","journal-title":"Autom"},{"key":"420_CR12","unstructured":"Grastien A, Anbulagan A, Rintanen J, Kelareva E (2007) Diagnosis of discrete-event systems using satisfiability algorithms. In: Proceedings of the 22nd national conference on artificial intelligence AAAI\u201907, pp 305\u2013310"},{"key":"420_CR13","doi-asserted-by":"crossref","unstructured":"He L, Ye L, Dague P (2018) SMT-based diagnosability analysis of real-time systems. In: Proceedings of the 10th Symposium on Fault Detection, Supervision and Safety for Technical Processes, IFAC SAFEPROCESS 2018","DOI":"10.1016\/j.ifacol.2018.09.721"},{"key":"420_CR14","doi-asserted-by":"publisher","unstructured":"He F, Zhu H, Hung WNN, Song X, Gu M (2010) Compositional abstraction refinement for timed systems. In: Liu J, Peled DA, Wang B, Wang F (eds.) Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2010, pp 168\u2013176. IEEE Computer Society, USA. https:\/\/doi.org\/10.1109\/TASE.2010.27","DOI":"10.1109\/TASE.2010.27"},{"issue":"8","key":"420_CR15","doi-asserted-by":"publisher","first-page":"1318","DOI":"10.1109\/9.940942","volume":"46","author":"S Jiang","year":"2001","unstructured":"Jiang S, Huang Z, Chandra V, Kumar R (2001) A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Trans Autom Control 46(8):1318\u20131321","journal-title":"IEEE Trans Autom Control"},{"key":"420_CR16","doi-asserted-by":"crossref","unstructured":"Kindermann R, Junttila T, Niemela I (2012) Beyond lassos: Complete smt-based bounded model checking for timed automata. In: Proceedings of Joint FMOODS 2012 and FORTE 2012. LNCS, vol. 7273. Springer, NY, USA","DOI":"10.1007\/978-3-642-30793-5_6"},{"key":"420_CR17","doi-asserted-by":"crossref","unstructured":"Lagniez J, Le\u00a0Berre D, Lima T, Montmirail V (2017) A recursive shortcut for CEGAR: application to the modal logic K satisfiability problem. In: Proceedings of the Twenty-Sixth international joint conference on artificial intelligence IJCAI\u201917, pp 674\u2013680","DOI":"10.24963\/ijcai.2017\/94"},{"key":"420_CR18","volume-title":"Introduction to Embedded Systems: A Cyber-Physical Systems Approach","author":"EA Lee","year":"2016","unstructured":"Lee EA, Seshia SA (2016) Introduction to Embedded Systems: A Cyber-Physical Systems Approach. MIT Press, Cambridge, MA, USA"},{"key":"420_CR19","doi-asserted-by":"crossref","unstructured":"Priesterjahn C, Heinzemann C, Sch\u00e4fer W (2013) From timed automata to timed failure propagation graphs. In: Proceedings of the 16th IEEE International Symposium on Object\/component\/service-oriented Real-time distributed Computing (ISORC\u201913)","DOI":"10.1109\/ISORC.2013.6913236"},{"key":"420_CR20","unstructured":"Rintanen J, Grastien A (2007) Diagnosability testing with satisfiability algorithms. In: Proceedings of the 20th international joint conference on artificial intelligence IJCAI\u201907, pp 532\u2013537"},{"key":"420_CR21","doi-asserted-by":"publisher","unstructured":"Roussanaly V, Sankur O, Markey N (2019) Abstraction refinement algorithms for timed automata. In: Dillig I, Tasiran S (eds.) Computer Aided Verification. LNCS, vol. 11561, pp 22\u201340. Springer, NY, USA. https:\/\/doi.org\/10.1007\/978-3-030-25540-4_2","DOI":"10.1007\/978-3-030-25540-4_2"},{"issue":"9","key":"420_CR22","doi-asserted-by":"publisher","first-page":"1555","DOI":"10.1109\/9.412626","volume":"40","author":"M Sampath","year":"1995","unstructured":"Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis D (1995) Diagnosability of discrete-event systems. IEEE Trans Autom Control 40(9):1555\u20131575","journal-title":"IEEE Trans Autom Control"},{"issue":"7","key":"420_CR23","doi-asserted-by":"publisher","first-page":"908","DOI":"10.1109\/9.701089","volume":"43","author":"M Sampath","year":"1998","unstructured":"Sampath M, Lafortune S, Teneketzis D (1998) Active diagnosis of discrete-event systems. IEEE Trans Autom Control 43(7):908\u2013929","journal-title":"IEEE Trans Autom Control"},{"key":"420_CR24","doi-asserted-by":"crossref","unstructured":"Tripakis S (2002) Fault diagnosis for timed automata. In: Proceedings of the international symposium on formal techniques in real-time and fault-tolerant systems (FTRTFT\u201902). LNCS, Springer, NY, USA, pp 205\u2013221","DOI":"10.1007\/3-540-45739-9_14"},{"key":"420_CR25","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-319-74962-4_11","volume-title":"Diagnosability, Security and Safety of Hybrid Dynamic and Cyber-Physical Systems, Chapter 11","author":"H Zaatiti","year":"2018","unstructured":"Zaatiti H, Ye L, Dague P, Gallois J-P, Trav\u00e9-Massuy\u00e8s L (2018) Abstractions refinement for hybrid systems diagnosability analysis. In: Sayed-Mouchaweh M (ed) Diagnosability, Security and Safety of Hybrid Dynamic and Cyber-Physical Systems, Chapter 11. Springer, NY, USA, pp 279\u2013318"},{"issue":"3\u20134","key":"420_CR26","first-page":"579","volume":"79","author":"A Zbrzezny","year":"2007","unstructured":"Zbrzezny A, P\u00f3\u0142rola A (2007) Sat-based reachability checking for timed automata with discrete data. Fundamenta Inf 79(3\u20134):579\u2013593","journal-title":"Fundamenta Inf"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-025-00420-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-025-00420-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-025-00420-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T12:07:51Z","timestamp":1758110871000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-025-00420-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,23]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["420"],"URL":"https:\/\/doi.org\/10.1007\/s10626-025-00420-x","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"type":"print","value":"0924-6703"},{"type":"electronic","value":"1573-7594"}],"subject":[],"published":{"date-parts":[[2025,8,23]]},"assertion":[{"value":"19 December 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}