{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:48:00Z","timestamp":1740142080732,"version":"3.37.3"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:00:00Z","timestamp":1574035200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T00:00:00Z","timestamp":1574035200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s11334-019-00357-z","type":"journal-article","created":{"date-parts":[[2019,11,18]],"date-time":"2019-11-18T08:01:36Z","timestamp":1574064096000},"page":"121-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["How to be sure a faulty system does not always appear healthy?"],"prefix":"10.1007","volume":"16","author":[{"given":"Philippe","family":"Dague","sequence":"first","affiliation":[]},{"given":"Lulu","family":"He","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2217-4752","authenticated-orcid":false,"given":"Lina","family":"Ye","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,18]]},"reference":[{"key":"357_CR1","doi-asserted-by":"crossref","unstructured":"Agarwal A, Madalinski A, Haar S (2012) Effective verification of weak diagnosability. In: Proceedings of the 8th IFAC symposium on fault detection, supervision and safety for technical processes (SAFEPROCESS\u201912). IFAC, pp 636\u2013641","DOI":"10.3182\/20120829-3-MX-2028.00083"},{"issue":"2","key":"357_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":"357_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Madhusudan P (2004) Decision problems for timed automata: a survey. In: Formal methods for the design of real-time systems, international school on formal methods for the design of computer, communication and software systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures, pp 1\u201324","DOI":"10.1007\/978-3-540-30080-9_1"},{"key":"357_CR4","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), Lecture Notes in Computer Science,vol 6919. Springer","DOI":"10.1007\/978-3-642-24310-3_13"},{"issue":"4","key":"357_CR5","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/s10626-007-0020-5","volume":"17","author":"E Badouel","year":"2007","unstructured":"Badouel E, Bednarczyk M, Borzyszkowski A, Caillaud B, Darondeau P (2007) Concurrent secrets. Discrete Event Dyn Syst 17(4):425\u2013446","journal-title":"Discrete Event Dyn Syst"},{"key":"357_CR6","doi-asserted-by":"crossref","unstructured":"Baier C, Bertrand N, Bouyer P, Brihaye T (2009) When are timed automata determinizable? In: Proceedings of automata, languages and programming, 36th international colloquium, (ICALP 2009), Part II, Rhodes, Greece, July 5\u201312, 2009, pp 43\u201354","DOI":"10.1007\/978-3-642-02930-1_4"},{"key":"357_CR7","unstructured":"Basarkar M, Pang X, Wang L, Haves P, Hong T (2011) Modeling and simulation of HVAC faults in EnergyPlus. In: Proceedings of building simulation 2011: 12th conference of international building performance simulation association, pp 2897\u20132903"},{"key":"357_CR8","doi-asserted-by":"crossref","unstructured":"B\u00e9rard B, Gastin P, Petit A (1996) On the power of non-observable actions in timed automata. In: Proceedings of 13th annual symposium on theoretical aspects of computer science (STACS 96), Grenoble, France, February 22\u201324, 1996, pp 257\u2013268","DOI":"10.1007\/3-540-60922-9_22"},{"key":"357_CR9","doi-asserted-by":"crossref","unstructured":"Bertrand N, Fabre E, Haar S, Haddad S, H\u00e9lou\u00ebt L (2014) Active diagnosis for probabilistic systems. In: 17th international conference on foundations of Software science and computation structures\u2014FOSSACS 2014, pp 29\u201342","DOI":"10.1007\/978-3-642-54830-7_2"},{"key":"357_CR10","unstructured":"Bertrand N, Haddad S, Lefaucheux E (2014) Foundation of diagnosis and predictability in probabilistic systems. In: 34th international conference on foundation of software technology and theoretical computer science, FSTTCS 2014, December 15\u201317, 2014, New Delhi, India, pp 417\u2013429"},{"key":"357_CR11","unstructured":"Bertrand N, Haddad S, Lefaucheux E (2016) Diagnosis in infinite-state probabilistic systems. In: 27th international conference on concurrency theory, CONCUR 2016, August 23\u201326, 2016, Qu\u00e9bec City, Canada, pp 37:1\u201337:15"},{"key":"357_CR12","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":"357_CR13","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"},{"key":"357_CR14","doi-asserted-by":"crossref","unstructured":"Bonchi F, Pous D (2013) Checking NFA Equivalence with Bisimulations Up to Congruence. In: Proceedings of 40th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL-2013). ACM, pp 457\u2013468","DOI":"10.1145\/2429069.2429124"},{"key":"357_CR15","doi-asserted-by":"crossref","unstructured":"Bouyer P (2003) Untameable timed automata. In: Proceedings of the annual symposium on theoretical aspects of computer science (STACS\u201903), Lecture Notes in Computer Science,vol 2607. Springer, pp 620\u2013631","DOI":"10.1007\/3-540-36494-3_54"},{"key":"357_CR16","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","DOI":"10.1007\/978-3-540-31982-5_14"},{"key":"357_CR17","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":"357_CR18","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi JR (1960) On a decision method in restricted second order arithmetic. Z Math Logik Grundlag Math 6:66\u201392","journal-title":"Z Math Logik Grundlag Math"},{"key":"357_CR19","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, Berlin","edition":"2"},{"key":"357_CR20","doi-asserted-by":"crossref","unstructured":"Cassez F (2009) The dark side of timed opacity. In: Proceedings of the 3rd international conference on information security and assurance (ISA\u201909), Seoul, South Korea, June, 2009, pp 21\u201330","DOI":"10.1007\/978-3-642-02617-1_3"},{"key":"357_CR21","doi-asserted-by":"crossref","unstructured":"Cassez F, Dubreil J, Marchand H (2009) Dynamic observers for the synthesis of opaque systems. In: Proceedings of the 7th international symposium on automated technology for verification and analysis (ATVA09), Macao, China, October, 2009, pp 352\u2013367","DOI":"10.1007\/978-3-642-04761-9_26"},{"key":"357_CR22","unstructured":"Diekert V, Gastin P, Petit A (1997) Removing $$\\epsilon $$-transitions in timed automata. In: Proceedings of 14th annual symposium on theoretical aspects of computer science (STACS 97), L\u00fcbeck, Germany, February 1997, pp 583\u2013594"},{"issue":"4","key":"357_CR23","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/s10626-014-0196-4","volume":"25","author":"Y Falcone","year":"2014","unstructured":"Falcone Y, Marchand H (2014) Enforcement and validation (at runtime) of various notions of opacity. Discrete Event Dyn Syst 25(4):531\u2013570","journal-title":"Discrete Event Dyn Syst"},{"key":"357_CR24","doi-asserted-by":"crossref","unstructured":"Finkel O (2006) Undecidable problems about timed automata. In: Proceedings of 4th international conference on formal modeling and analysis of timed systems (FORMATS 2006), Paris, France, September 25\u201327, 2006, pp 187\u2013199","DOI":"10.1007\/11867340_14"},{"issue":"1","key":"357_CR25","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2005.05.046","volume":"180","author":"G Gardey","year":"2007","unstructured":"Gardey G, Mullins J, Roux O (2007) Non-interference control synthesis for security timed automata. Electron Notes Theor Comput Sci 180(1):35\u201353","journal-title":"Electron Notes Theor Comput Sci"},{"issue":"4","key":"357_CR26","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1145\/2832910","volume":"14","author":"V Germanos","year":"2015","unstructured":"Germanos V, Haar S, Khomenko V, Schwoon S (2015) Diagnosability under weak fairness. ACM Trans Embed Comput Syst 14(4):132\u2013141","journal-title":"ACM Trans Embed Comput Syst"},{"issue":"1","key":"357_CR27","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.jcss.2016.04.007","volume":"83","author":"S Haar","year":"2017","unstructured":"Haar S, Haddad S, Melliti T, Schwoon S (2017) Optimal constructions for active diagnosis. J Comput Syst Sci 83(1):101\u2013120","journal-title":"J Comput Syst Sci"},{"key":"357_CR28","doi-asserted-by":"crossref","unstructured":"He L, Ye L, Dague P (2018) Smt-based diagnosability analysis of real-time systems. In: Proceedings of 10th IFAC symposium on fault detection, supervision and safety for technical processes (SAFEPROCESS 2018), pp 1059\u20131066","DOI":"10.1016\/j.ifacol.2018.09.721"},{"key":"357_CR29","doi-asserted-by":"crossref","unstructured":"Herbreteau F, Srivathsan B, Walukiewicz I (2013) Lazy abstractions for timed automata. In: Proceedings of 25th international conference on computer aided verification (CAV 2013), Saint Petersburg, Russia, July 13\u201319, 2013, pp 990\u20131005","DOI":"10.1007\/978-3-642-39799-8_71"},{"key":"357_CR30","doi-asserted-by":"crossref","unstructured":"Jacob R, Lesage J-J, Faure J-M (2015) Opacity of discrete event systems: models, validation and quantification. In: Proceedings of 5th IFAC workshop on dependable control of discrete systems (DCDS\u201915), Cancun, Mexico, May, 2015, pp 174\u2013181","DOI":"10.1016\/j.ifacol.2015.06.490"},{"issue":"8","key":"357_CR31","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 time algorithm for testing diagnosability of discrete event systems. Trans Autom Control 46(8):1318\u20131321","journal-title":"Trans Autom Control"},{"key":"357_CR32","unstructured":"Johan B, Wang Y (2003) On clock difference constraints and termination in reachability analysis of timed automata. In: Proceedings of the 5th international conference on formal engineering methods (ICFEM\u20192003), Lecture Notes in Computer Science, vol 2885. Springer, pp 491\u2013503"},{"key":"357_CR33","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, Lecture Notes in Computer Science, vol 7273. Springer","DOI":"10.1007\/978-3-642-30793-5_6"},{"issue":"5","key":"357_CR34","doi-asserted-by":"publisher","first-page":"953","DOI":"10.1007\/s12273-018-0458-4","volume":"11","author":"Y Li","year":"2018","unstructured":"Li Y, O\u2019Neill Z (2018) A critical review of fault modeling of HVAC systems in buildings. Build Simul 11(5):953\u2013975","journal-title":"Build Simul"},{"issue":"3","key":"357_CR35","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1016\/j.automatica.2011.01.002","volume":"47","author":"F Lin","year":"2011","unstructured":"Lin F (2011) Opacity of discrete event systems and its applications. Automatica 47(3):496\u2013503","journal-title":"Automatica"},{"key":"357_CR36","volume-title":"Philosophical naturalism","author":"D Papineau","year":"1993","unstructured":"Papineau D (1993) Philosophical naturalism. Blackwell, Oxford"},{"key":"357_CR37","unstructured":"Pencol\u00e9 Y (2004) Diagnosability analysis of distributed discrete event systems. In: Proceedings of the 16th European conference on articifial intelligent (ECAI\u201904). IOS Press, Nieuwe Hemweg, pp 43\u201347"},{"key":"357_CR38","unstructured":"Saboori A (2011) Verification and enforcement of state-based notions of opacity in discrete event systems. Ph.D. thesis, University of Illinois at Urbana-Champaign"},{"issue":"5","key":"357_CR39","doi-asserted-by":"publisher","first-page":"1265","DOI":"10.1109\/TAC.2011.2173774","volume":"57","author":"A Saboori","year":"2012","unstructured":"Saboori A, Hadjicostis CN (2012) Verification of infinite-step opacity and complexity considerations. IEEE Trans Autom Control 57(5):1265\u20131269","journal-title":"IEEE Trans Autom Control"},{"key":"357_CR40","doi-asserted-by":"crossref","unstructured":"Saboori A, Hadjicostis CN (2007) Notions of security and opacity in discrete event systems. In: Proceedings of 46th IEEE conference on decision and control (CDC07), New Orleans, LA, USA, December, 2007, pp 5056\u20135061","DOI":"10.1109\/CDC.2007.4434515"},{"key":"357_CR41","doi-asserted-by":"crossref","unstructured":"Saboori A, Hadjicostis CN (2009) Verification of infinite-step opacity and analysis of its complexity. In: Proceedings of 2nd IFAC workshop on dependable control of discrete systems (DCDS\u201909), Bari, Italy, June, 2009, pp 46\u201351","DOI":"10.3182\/20090610-3-IT-4004.00013"},{"key":"357_CR42","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.ins.2013.05.033","volume":"246","author":"A Saboori","year":"2013","unstructured":"Saboori A, Hadjicostis CN (2013) Verification of initial-state opacity in security applications of discrete event systems. Inf Sci 246:115\u2013132","journal-title":"Inf Sci"},{"issue":"9","key":"357_CR43","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 system. Trans Autom Control 40(9):1555\u20131575","journal-title":"Trans Autom Control"},{"key":"357_CR44","unstructured":"Schumann A, Huang J (2008) A scalable jointree algorithm for diagnosability. In: Proceedings of the 23rd American national conference on artificial intelligence (AAAI\u201908). AAAI Press, Menlo Park, pp 535\u2013540"},{"key":"357_CR45","unstructured":"Schumann A, Pencol\u00e9 Y (2007) Scalable diagnosability checking of event-driven system. In: Proceedings of the twentieth international joint conference on artificial intelligence (IJCAI\u201907). International Joint Conferences on Artificial Intelligence, Inc., Menlo Park, Calif., pp 575\u2013580"},{"issue":"1","key":"357_CR46","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/j.sysconle.2009.11.001","volume":"59","author":"S Shu","year":"2010","unstructured":"Shu S, Lin F (2010) Detectability of discrete event systems with dynamic event observation. Syst Control Lett 59(1):9\u201317","journal-title":"Syst Control Lett"},{"issue":"1","key":"357_CR47","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1109\/TASE.2012.2215959","volume":"10","author":"S Shu","year":"2013","unstructured":"Shu S, Lin F (2013) I-Detectability of discrete-event systems. IEEE Trans Autom Sci Eng 10(1):187\u2013196","journal-title":"IEEE Trans Autom Sci Eng"},{"issue":"2\u20133","key":"357_CR48","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"AP Sistla","year":"1987","unstructured":"Sistla AP, Vardi MY, Wolper P (1987) The complementation problem for B\u00fcchi automata with applications to temporal logic. Theor Comput Sci 49(2\u20133):217\u2013237","journal-title":"Theor Comput Sci"},{"issue":"4","key":"357_CR49","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1109\/TAC.2005.844722","volume":"50","author":"D Thorsley","year":"2005","unstructured":"Thorsley D, Teneketzis D (2005) Diagnosability of stochastic discrete-event systems. IEEE Trans Autom Control 50(4):476\u2013492","journal-title":"IEEE Trans Autom Control"},{"key":"357_CR50","doi-asserted-by":"crossref","unstructured":"Tripakis S (2002) Fault diagnosis for timed automata. In: Proceedings of international symposium on formal techniques in real-time and fault-tolerant systems (FTRTFT\u201902), Lecture Notes in Computer Science. Springer","DOI":"10.1007\/3-540-45739-9_14"},{"issue":"11","key":"357_CR51","doi-asserted-by":"publisher","first-page":"2845","DOI":"10.1109\/TCAD.2018.2857363","volume":"37","author":"L Wang","year":"2018","unstructured":"Wang L, Zhan N, An J (2018) The opacity of real-time automata. IEEE Trans Comput Aided Des Integr Circuits Syst 37(11):2845\u20132856","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"issue":"3","key":"357_CR52","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10626-012-0145-z","volume":"23","author":"YC Wu","year":"2013","unstructured":"Wu YC, Lafortune S (2013) Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discrete Event Dyn Syst 23(3):307\u2013339","journal-title":"Discrete Event Dyn Syst"},{"key":"357_CR53","unstructured":"Ye L, Dague P (2010) Diagnosability analysis of discrete event systems with autonomous components. In: Proceedings of the 19th European conference on artificial intelligence (ECAI\u201910). IOS Press, Nieuwe Hemweg, pp 105\u2013110"},{"key":"357_CR54","unstructured":"Ye L, Dague P, Longuet D, Brand\u00e1n\u00a0Briones L, Madalinski A (2016) Fault manifestability verification for discrete event systems. In: Proceedings of the 22nd European conference on artificial intelligence (ECAI\u201916). IOS Press, pp 1718\u20131719"},{"key":"357_CR55","doi-asserted-by":"crossref","unstructured":"Ye L, Dague P, Longuet D, Brand\u00e1n Briones L, Madalinski A (2018) How to be sure a faulty system does not always appear healthy? In: Proceedings of 12th international conference on verification and evaluation of computer and communication systems (VECoS 2018), Grenoble, France, September 26-28, 2018, pp 114\u2013129","DOI":"10.1007\/978-3-030-00359-3_8"},{"key":"357_CR56","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.automatica.2017.02.037","volume":"80","author":"X Yin","year":"2017","unstructured":"Yin X, Lafortune S (2017) A new approach for the verification of infinite-step and k-step opacity using two-way observers. Automatica 80:162\u2013171","journal-title":"Automatica"},{"key":"357_CR57","doi-asserted-by":"crossref","unstructured":"Zhang B, Shu S, Lin F (2012) Polynomial algorithms to check opacity in discrete event system. In: Proceedings of the 24th Chinese control and decision conference (CCDC12), pp 763\u2013769","DOI":"10.1109\/CCDC.2012.6244117"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-019-00357-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-019-00357-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-019-00357-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,5]],"date-time":"2022-10-05T21:48:56Z","timestamp":1665006536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-019-00357-z"}},"subtitle":["Fault manifestability analysis for discrete event and timed systems"],"short-title":[],"issued":{"date-parts":[[2019,11,18]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["357"],"URL":"https:\/\/doi.org\/10.1007\/s11334-019-00357-z","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2019,11,18]]},"assertion":[{"value":"25 March 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 October 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 November 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}