{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T12:50:24Z","timestamp":1770814224591,"version":"3.50.1"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T00:00:00Z","timestamp":1649030400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T00:00:00Z","timestamp":1649030400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100002322","name":"Coordena\u00e7\u00e3o de Aperfei\u00e7oamento de Pessoal de N\u00edvel Superior","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004586","name":"Funda\u00e7\u00e3o Carlos Chagas Filho de Amparo \u00e0 Pesquisa do Estado do Rio de Janeiro","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004586","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2022,9]]},"DOI":"10.1007\/s10626-022-00360-w","type":"journal-article","created":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T09:03:07Z","timestamp":1649062987000},"page":"399-433","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Diagnosability verification using LTL model checking"],"prefix":"10.1007","volume":"32","author":[{"given":"Thiago M.","family":"Tuxi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0629-7194","authenticated-orcid":false,"given":"Lilian K.","family":"Carvalho","sequence":"additional","affiliation":[]},{"given":"Eduardo V. L.","family":"Nunes","sequence":"additional","affiliation":[]},{"given":"Antonio E. C. da","family":"Cunha","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,4,4]]},"reference":[{"key":"360_CR1","unstructured":"Alves LVR, Martins LRR, Pena PN (July 2017) UltraDES \u2013 a library for modeling, analysis and control of discrete event systems. In: Proceedings of the 20th World Congress of the International Federation of Automatic Control, Toulose, France, pp 5996\u20132001"},{"key":"360_CR2","doi-asserted-by":"crossref","unstructured":"Athanasopoulou E, Li L, Hadjicostis CN (July 2006) Probabilistic failure diagnosis in finite state machines under unreliable observations. In: 2006 8th international workshop on discrete event systems. IEEE, Ann Arbor, MI, USA, pp 301\u2013306","DOI":"10.1109\/WODES.2006.1678446"},{"key":"360_CR3","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"360_CR4","doi-asserted-by":"crossref","unstructured":"Basile F, De Tommasi G, Sterle C, Boussif A, Ghazel M (2018) Efficient diagnosability assessment via ilp optimization: a railway benchmark. In: 2018 IEEE 23rd international conference on emerging technologies and factory automation (ETFA), vol 1, pp 441\u2013448","DOI":"10.1109\/ETFA.2018.8502532"},{"key":"360_CR5","doi-asserted-by":"crossref","unstructured":"Basilio JC, Lafortune S (2009) Robust codiagnosability of discrete event systems. In: Proc. American control conference, St. Louis, MO, USA, pp 2202\u20132209","DOI":"10.1109\/ACC.2009.5160208"},{"issue":"3","key":"360_CR6","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10626-012-0129-z","volume":"22","author":"JC Basilio","year":"2012","unstructured":"Basilio JC, Lima STS, Lafortune S, Moreira MV (2012) Computation of minimal event bases that ensure diagnosability. Discret Event Dyn Syst 22(3):249\u2013292","journal-title":"Discret Event Dyn Syst"},{"key":"360_CR7","first-page":"1","volume":"19","author":"F Bassino","year":"2009","unstructured":"Bassino F, David J, Nicaud C (2009) Enumeration and random generation of possibly incomplete deterministic automata. Pure Math Appl 19:1\u201316","journal-title":"Pure Math Appl"},{"key":"360_CR8","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1016\/j.tcs.2007.04.001","volume":"381","author":"F Bassino","year":"2007","unstructured":"Bassino F, Nicaud C (2007) Enumeration and random generation of accessible automata. Theor Comput Sci 381:86\u2013104","journal-title":"Theor Comput Sci"},{"key":"360_CR9","doi-asserted-by":"crossref","unstructured":"Bermeo LE, Basilio JC, Carvalho LK (2012) DESLAB: a scientific computing program for analysis and synthesis of discrete-event systems. In: Preprints of the 11th international workshop on discrete event systems, Guadalajara, Mexico, pp 349\u2013355","DOI":"10.3182\/20121003-3-MX-4033.00056"},{"key":"360_CR10","doi-asserted-by":"crossref","unstructured":"Berthomieu B, Ribet P-O, Vernadat F (2004) The tool TINA \u2013 construction of abstract state spaces for Petri nets and time Petri nets. Int J Prod Res 42(14)","DOI":"10.1080\/00207540412331312688"},{"issue":"7","key":"360_CR11","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.ifacol.2015.06.475","volume":"48","author":"A Boussif","year":"2015","unstructured":"Boussif A, Ghazel M (2015) Diagnosability analysis of input\/output discrete-event systems using model-checking. IFAC-PapersOnLine 48(7):71\u201378. 5th IFAC International Workshop on Dependable Control of Discrete Systems","journal-title":"IFAC-PapersOnLine"},{"key":"360_CR12","unstructured":"Boussif A, Ghazel M (2016) Using model-checking techniques for diagnosability analysis of intermittent faults-a railway case-study.. In: VECOS 2016-10th international workshop on verification and evaluation of computer and communication systems, Tunis, Tunisia, p 11p"},{"issue":"2","key":"360_CR13","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1504\/IJCCBS.2018.096192","volume":"8","author":"A Boussif","year":"2018","unstructured":"Boussif A, Ghazel M (2018) Formal verification of intermittent fault diagnosability of discrete-event systems using model-checking. Int J Crit Comput-Based Syst 8(2):193\u2013213","journal-title":"Int J Crit Comput-Based Syst"},{"issue":"9","key":"360_CR14","doi-asserted-by":"publisher","first-page":"1531","DOI":"10.1016\/j.automatica.2010.06.013","volume":"46","author":"MP Cabasino","year":"2010","unstructured":"Cabasino MP, Giua A, Seatzu C (2010) Fault detection for discrete event systems using Petri Nets with unobservable transitions. Automatica 46 (9):1531\u20131539","journal-title":"Automatica"},{"issue":"9","key":"360_CR15","doi-asserted-by":"publisher","first-page":"2068","DOI":"10.1016\/j.automatica.2012.06.042","volume":"48","author":"LK Carvalho","year":"2012","unstructured":"Carvalho LK, Basilio JOC, Moreira MV (2012) Robust diagnosis of discrete event systems against intermittent loss of observations. Automatica 48 (9):2068\u20132078","journal-title":"Automatica"},{"key":"360_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to discrete event systems","author":"CG Cassandras","year":"2008","unstructured":"Cassandras CG, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer, Massachussets","edition":"2nd edn."},{"issue":"7","key":"360_CR17","doi-asserted-by":"publisher","first-page":"1752","DOI":"10.1109\/TAC.2012.2183169","volume":"57","author":"F Cassez","year":"2012","unstructured":"Cassez F (2012) The complexity of codiagnosability for discrete event and timed systems. IEEE Trans Autom Control 57(7):1752\u20131764","journal-title":"IEEE Trans Autom Control"},{"key":"360_CR18","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, F Giunchiglia MP, M Roveri RS, Tacchella A (2002) NuSMV 2: An opensource tool for symbolic model checking. In: Proceeding of international conference on computer-aided verification","DOI":"10.1007\/3-540-45657-0_29"},{"key":"360_CR19","unstructured":"Cimatti A, Pecheur C, Cavada R (2003) Formal verification of diagnosability via symbolic model checking. In: Workshop on model checking and artificial intelligence (MoChArt-2002), Lyon, France, pp 363\u2013369"},{"key":"360_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of model checking","author":"EM Clarke","year":"2018","unstructured":"Clarke EM, Henzinger TA, Veith H, Bloem R (2018) Handbook of model checking, 1st edn. Springer International Publishing, New York","edition":"1st edn."},{"key":"360_CR21","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/s10626-017-0260-y","volume":"27","author":"LB Clavijo","year":"2017","unstructured":"Clavijo LB, Basilio JC (2017) Empirical studies in the size of diagnosers and verifiers for diagnosability. Discret Event Dyn Syst 27:701\u2013739","journal-title":"Discret Event Dyn Syst"},{"issue":"1-2","key":"360_CR22","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1008335115538","volume":"20","author":"R Debouk","year":"2000","unstructured":"Debouk R, Lafortune S, Teneketzis D (2000) Coordinated decentralized protocols for failure diagnosis of discrete event systems. Discret Event Dyn Syst 20(1-2):33\u201386","journal-title":"Discret Event Dyn Syst"},{"key":"360_CR23","unstructured":"Genc S, Lafortune S (2006) Predictability in discrete-event systems underpartial observation. In: Proc. 6th IFAC safeprocess symposium"},{"key":"360_CR24","doi-asserted-by":"crossref","unstructured":"Genc S, Lafortune S (2003) Distributed diagnosis of discrete-event systems using Petri nets. In: Applications and theory of Petri nets. Springer, Berlin, Heidelberg, pp 316\u2013336","DOI":"10.1007\/3-540-44919-1_21"},{"key":"360_CR25","doi-asserted-by":"crossref","unstructured":"Ghazel M, Liu B (2016) A customizable railway benchmark to deal with fault diagnosis issues in DES. In: Proc. of the 13th international workshop on discrete event systems (WODES\u201916), Xi\u2019an, China, pp 177\u2013182","DOI":"10.1109\/WODES.2016.7497845"},{"key":"360_CR26","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10626-016-0234-5","volume":"27","author":"H-E Gougam","year":"2017","unstructured":"Gougam H-E, Pencol\u00e9 Y, Subias A (2017) Diagnosability analysis of patterns on bounded labeled prioritized Petri nets. Discret Event Dyn Syst 27:143\u2013180","journal-title":"Discret Event Dyn Syst"},{"key":"360_CR27","unstructured":"Grastien A (2009) Symbolic testing of diagnosability. In: 20th international workshop on principles of diagnosis (DX-09), Stockholm, Sweden, pp 131\u2013138"},{"issue":"12","key":"360_CR28","doi-asserted-by":"publisher","first-page":"3070","DOI":"10.1109\/TAC.2013.2275892","volume":"58","author":"A Grastien","year":"2013","unstructured":"Grastien A, Anbulagan A (2013) Diagnosis of discrete event systems using satisfiability algorithms: A theoretical and empirical study. IEEE Trans Autom Control 58(12):3070\u20133083","journal-title":"IEEE Trans Autom Control"},{"key":"360_CR29","doi-asserted-by":"crossref","unstructured":"Hermann M, Pentek T, Otto B (2016) Design principles for industrie 4.0 scenarios. In: 2016 49th Hawaii international conference on system sciences (HICSS), pp 3928\u20133937","DOI":"10.1109\/HICSS.2016.488"},{"key":"360_CR30","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (1997) The model checker spin. IEEE Trans Softw Eng 23(5)","DOI":"10.1109\/32.588521"},{"key":"360_CR31","unstructured":"Holzmann GJ (2004) The spin model checker: Primer and reference manual. Addison-Wesley"},{"issue":"8","key":"360_CR32","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"},{"issue":"6","key":"360_CR33","doi-asserted-by":"publisher","first-page":"934","DOI":"10.1109\/TAC.2004.829616","volume":"49","author":"S Jiang","year":"2004","unstructured":"Jiang S, Kumar R (2004) Failure diagnosis of discrete-event systems with linear-time temporal logic specifications. IEEE Trans Autom Control 49 (6):934\u2013945","journal-title":"IEEE Trans Autom Control"},{"issue":"1","key":"360_CR34","first-page":"47","volume":"3","author":"S Jiang","year":"2006","unstructured":"Jiang S, Kumar R (2006) Diagnosis of repeated failures for discrete event systems with linear-time temporal-logic specifications. IEEE Trans Autom Control 3(1):47\u201358","journal-title":"IEEE Trans Autom Control"},{"issue":"1","key":"360_CR35","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/TAC.2009.2034216","volume":"55","author":"R Kumar","year":"2010","unstructured":"Kumar R, Takai S (2010) Decentralized prognosis of failures in discrete event systems. IEEE Trans Autom Control 55(1):48\u201359","journal-title":"IEEE Trans Autom Control"},{"key":"360_CR36","doi-asserted-by":"crossref","unstructured":"Lin F (1994) Diagnosability of discrete event systems and its applications. J Discret Event Dyn Syst 4(197-212)","DOI":"10.1007\/BF01441211"},{"issue":"1","key":"360_CR37","doi-asserted-by":"publisher","first-page":"5794","DOI":"10.1016\/j.ifacol.2017.08.427","volume":"50","author":"R Malik","year":"2017","unstructured":"Malik R, \u00c5kesson K, Flordal H, Fabian M (2017) Supremica \u2013 an efficient tool for large-scale discrete event systems. IFAC-PapersOnLine 50 (1):5794\u20135799","journal-title":"IFAC-PapersOnLine"},{"issue":"21","key":"360_CR38","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/j.ifacol.2015.09.545","volume":"48","author":"P Marang\u00e9","year":"2015","unstructured":"Marang\u00e9 P, Philippot A, P\u00e9tin JF, Gellot F (2015) Diagnosability evaluation by model-checking. IFAC-PapersOnLine 48(21):308\u2013313","journal-title":"IFAC-PapersOnLine"},{"key":"360_CR39","unstructured":"McGrath N (2018) Verification of the diagnosability of discrete-event systems in waters. Tech. Rep. 04, Department of Computer Science The University of Waikato"},{"issue":"7","key":"360_CR40","doi-asserted-by":"publisher","first-page":"1679","DOI":"10.1109\/TAC.2011.2124950","volume":"56","author":"MV Moreira","year":"2011","unstructured":"Moreira MV, Jesus TC, Basilio JC (2011) Polynomial time verification of decentralized diagnosability of discrete event system. IEEE Trans Autom Control 56(7):1679\u20131684","journal-title":"IEEE Trans Autom Control"},{"key":"360_CR41","unstructured":"Pencol\u00e9 Y, Subias A (2021) Diagnosability of event patterns in safe labeled time Petri Nets: A model-checking approach. IEEE Trans Autom Sci Eng :1\u201312"},{"issue":"1","key":"360_CR42","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJG Ramadge","year":"1989","unstructured":"Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81\u201398","journal-title":"Proc IEEE"},{"issue":"1","key":"360_CR43","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/TASE.2006.872120","volume":"4","author":"A Ramirez-Trevino","year":"2007","unstructured":"Ramirez-Trevino A, Ruiz-Beltran E, Rivera-Rangel I, Lopez-Mellado E (2007) Online fault diagnosis of discrete event systems. a Petri Net-based approach. IEEE Trans Autom Sci Eng 4(1):31\u201339","journal-title":"IEEE Trans Autom Sci Eng"},{"key":"360_CR44","unstructured":"Reis R, Moreira N, Almeida M (2005) On the representation of finite automata. In: Proceedings of the 7th international workshop on descriptional complexity of formal systems, pp 269\u2013276"},{"key":"360_CR45","doi-asserted-by":"crossref","unstructured":"Ricker L, Lafortune S, Genc S (2006) DESUMA: A tool integrating GIDDES and UMDES. In: 2006 8th international workshop on discrete event systems, pp 392\u2013393","DOI":"10.1109\/WODES.2006.382402"},{"key":"360_CR46","doi-asserted-by":"crossref","unstructured":"Rudie K (2006) The integrated discrete-event systems tool. In: 2006 8th international workshop on discrete event systems, Michigan, US, pp 394\u2013395","DOI":"10.1109\/WODES.2006.382403"},{"issue":"9","key":"360_CR47","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":"360_CR48","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":"360_CR49","doi-asserted-by":"crossref","unstructured":"Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis DC (March 1996) Failure diagnosis using discrete-event models. IEEE Trans Control Syst Technol 4(2):105\u2013124","DOI":"10.1109\/87.486338"},{"issue":"12","key":"360_CR50","doi-asserted-by":"publisher","first-page":"1923","DOI":"10.1109\/TAC.2005.860291","volume":"50","author":"R Su","year":"2005","unstructured":"Su R, Wonham WM (2005) Global and local consistencies in distributed fault diagnosis for discrete-event systems. IEEE Trans Autom Control 50 (12):1923\u20131935","journal-title":"IEEE Trans Autom Control"},{"key":"360_CR51","doi-asserted-by":"crossref","unstructured":"Thorsley D, Yoo T-S, Garcia H E (2008) Diagnosability of stochastic discrete-event systems under unreliable observations. In: 2008 American control conference. IEEE, Seattle, WA, USA, pp 1158\u20131165","DOI":"10.1109\/ACC.2008.4586649"},{"key":"360_CR52","unstructured":"Tuxi T (2020) Experiment files. https:\/\/gthub.com\/TuxiThiago\/SPIN_FDIAGNOSIS"},{"key":"360_CR53","doi-asserted-by":"crossref","unstructured":"Tuxi TM, Carvalho LK, Nunes EVL, da Cunha AEC (November 2020) Is LTL model-checking effective for diagnosability verification?. In: Proc. of the 15th international workshop on discrete event systems (WODES\u201920), Rio de Janeiro, Brazil, pp 256\u2013262","DOI":"10.1016\/j.ifacol.2021.04.024"},{"key":"360_CR54","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proceedings of the first symposium on logic in computer science, IEEE Computer Society, pp 322\u2013331"},{"issue":"9","key":"360_CR55","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1109\/TAC.2002.802763","volume":"47","author":"T-S Yoo","year":"2002","unstructured":"Yoo T-S, Lafortune S (2002) Polynomial-time verification of diagnosability of partially observed discrete-event systems. IEEE Trans Autom Control 47 (9):1491\u20131495","journal-title":"IEEE Trans Autom Control"},{"issue":"2","key":"360_CR56","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/j.arcontrol.2013.09.009","volume":"37","author":"J Zaytoon","year":"2013","unstructured":"Zaytoon J, Lafortune S (2013) Overview of fault diagnosis methods for discrete event systems. Annu Rev Control 37(2):308\u2013320","journal-title":"Annu Rev Control"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-022-00360-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-022-00360-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-022-00360-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,21]],"date-time":"2024-09-21T14:53:34Z","timestamp":1726930414000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-022-00360-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,4]]},"references-count":56,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9]]}},"alternative-id":["360"],"URL":"https:\/\/doi.org\/10.1007\/s10626-022-00360-w","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,4]]},"assertion":[{"value":"2 February 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 January 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 April 2022","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 declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interests"}}]}}