## Abstract

Fault diagnosability (allowing one to determine with certainty whether a given fault has effectively occurred based on the available observations) is a crucial and challenging property in complex system automatic control, which generally requires a high number of sensors, increasing the system cost, since it is quite a strong property. In this paper, we analyze a new system property called manifestability, that is a weaker requirement on system observations for having a chance to identify on-line faults: that a faulty system cannot always appear healthy. We propose an algorithm with PSPACE complexity to automatically verify it for finite automata, and prove that the problem of manifestability verification itself is PSPACE-complete. The experimental results show the feasibility of our algorithm from a practical point of view. Then, we extend our approach to verify manifestability of real-time systems modeled by timed automata, proving that it is undecidable in general but under some restricted conditions it becomes PSPACE-complete. Finally, we encode this property into an SMT formula, whose satisfiability witnesses manifestability, before presenting experimental results showing the scalability of our approach.

This is a preview of subscription content, access via your institution.

## Notes

- 1.
the examples in Tables 1 and 2 can be found in https://www.lri.fr/~linaye/cases.pdf

## References

- 1.
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’12). IFAC, pp 636–641

- 2.
Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183–235

- 3.
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–24

- 4.
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’11), Lecture Notes in Computer Science,vol 6919. Springer

- 5.
Badouel E, Bednarczyk M, Borzyszkowski A, Caillaud B, Darondeau P (2007) Concurrent secrets. Discrete Event Dyn Syst 17(4):425–446

- 6.
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–12, 2009, pp 43–54

- 7.
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–2903

- 8.
Bérard 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–24, 1996, pp 257–268

- 9.
Bertrand N, Fabre E, Haar S, Haddad S, Hélouët L (2014) Active diagnosis for probabilistic systems. In: 17th international conference on foundations of Software science and computation structures—FOSSACS 2014, pp 29–42

- 10.
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–17, 2014, New Delhi, India, pp 417–429

- 11.
Bertrand N, Haddad S, Lefaucheux E (2016) Diagnosis in infinite-state probabilistic systems. In: 27th international conference on concurrency theory, CONCUR 2016, August 23–26, 2016, Québec City, Canada, pp 37:1–37:15

- 12.
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’16), pp 972–978

- 13.
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’16), pp 907–913

- 14.
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–468

- 15.
Bouyer P (2003) Untameable timed automata. In: Proceedings of the annual symposium on theoretical aspects of computer science (STACS’03), Lecture Notes in Computer Science,vol 2607. Springer, pp 620–631

- 16.
Bouyer P, Chevalier F, D’Souza D (2005) Fault diagnosis using timed automata. In: Proceedings of international conference on foundations of software science and computation structures (FoSSaCS’05), Lecture Notes in Computer Science. Springer

- 17.
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’15), pp 3724–3730

- 18.
Büchi JR (1960) On a decision method in restricted second order arithmetic. Z Math Logik Grundlag Math 6:66–92

- 19.
Cassandras CG, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer, Berlin

- 20.
Cassez F (2009) The dark side of timed opacity. In: Proceedings of the 3rd international conference on information security and assurance (ISA’09), Seoul, South Korea, June, 2009, pp 21–30

- 21.
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–367

- 22.
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übeck, Germany, February 1997, pp 583–594

- 23.
Falcone Y, Marchand H (2014) Enforcement and validation (at runtime) of various notions of opacity. Discrete Event Dyn Syst 25(4):531–570

- 24.
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–27, 2006, pp 187–199

- 25.
Gardey G, Mullins J, Roux O (2007) Non-interference control synthesis for security timed automata. Electron Notes Theor Comput Sci 180(1):35–53

- 26.
Germanos V, Haar S, Khomenko V, Schwoon S (2015) Diagnosability under weak fairness. ACM Trans Embed Comput Syst 14(4):132–141

- 27.
Haar S, Haddad S, Melliti T, Schwoon S (2017) Optimal constructions for active diagnosis. J Comput Syst Sci 83(1):101–120

- 28.
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–1066

- 29.
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–19, 2013, pp 990–1005

- 30.
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’15), Cancun, Mexico, May, 2015, pp 174–181

- 31.
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–1321

- 32.
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’2003), Lecture Notes in Computer Science, vol 2885. Springer, pp 491–503

- 33.
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

- 34.
Li Y, O’Neill Z (2018) A critical review of fault modeling of HVAC systems in buildings. Build Simul 11(5):953–975

- 35.
Lin F (2011) Opacity of discrete event systems and its applications. Automatica 47(3):496–503

- 36.
Papineau D (1993) Philosophical naturalism. Blackwell, Oxford

- 37.
Pencolé Y (2004) Diagnosability analysis of distributed discrete event systems. In: Proceedings of the 16th European conference on articifial intelligent (ECAI’04). IOS Press, Nieuwe Hemweg, pp 43–47

- 38.
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

- 39.
Saboori A, Hadjicostis CN (2012) Verification of infinite-step opacity and complexity considerations. IEEE Trans Autom Control 57(5):1265–1269

- 40.
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–5061

- 41.
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’09), Bari, Italy, June, 2009, pp 46–51

- 42.
Saboori A, Hadjicostis CN (2013) Verification of initial-state opacity in security applications of discrete event systems. Inf Sci 246:115–132

- 43.
Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis D (1995) Diagnosability of discrete event system. Trans Autom Control 40(9):1555–1575

- 44.
Schumann A, Huang J (2008) A scalable jointree algorithm for diagnosability. In: Proceedings of the 23rd American national conference on artificial intelligence (AAAI’08). AAAI Press, Menlo Park, pp 535–540

- 45.
Schumann A, Pencolé Y (2007) Scalable diagnosability checking of event-driven system. In: Proceedings of the twentieth international joint conference on artificial intelligence (IJCAI’07). International Joint Conferences on Artificial Intelligence, Inc., Menlo Park, Calif., pp 575–580

- 46.
Shu S, Lin F (2010) Detectability of discrete event systems with dynamic event observation. Syst Control Lett 59(1):9–17

- 47.
Shu S, Lin F (2013) I-Detectability of discrete-event systems. IEEE Trans Autom Sci Eng 10(1):187–196

- 48.
Sistla AP, Vardi MY, Wolper P (1987) The complementation problem for Büchi automata with applications to temporal logic. Theor Comput Sci 49(2–3):217–237

- 49.
Thorsley D, Teneketzis D (2005) Diagnosability of stochastic discrete-event systems. IEEE Trans Autom Control 50(4):476–492

- 50.
Tripakis S (2002) Fault diagnosis for timed automata. In: Proceedings of international symposium on formal techniques in real-time and fault-tolerant systems (FTRTFT’02), Lecture Notes in Computer Science. Springer

- 51.
Wang L, Zhan N, An J (2018) The opacity of real-time automata. IEEE Trans Comput Aided Des Integr Circuits Syst 37(11):2845–2856

- 52.
Wu YC, Lafortune S (2013) Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discrete Event Dyn Syst 23(3):307–339

- 53.
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’10). IOS Press, Nieuwe Hemweg, pp 105–110

- 54.
Ye L, Dague P, Longuet D, Brandán Briones L, Madalinski A (2016) Fault manifestability verification for discrete event systems. In: Proceedings of the 22nd European conference on artificial intelligence (ECAI’16). IOS Press, pp 1718–1719

- 55.
Ye L, Dague P, Longuet D, Brandán 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–129

- 56.
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–171

- 57.
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–769

## Author information

### Affiliations

### Corresponding author

## Additional information

### Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

## Rights and permissions

## About this article

### Cite this article

Dague, P., He, L. & Ye, L. How to be sure a faulty system does not always appear healthy?.
*Innovations Syst Softw Eng* **16, **121–142 (2020). https://doi.org/10.1007/s11334-019-00357-z

Received:

Accepted:

Published:

Issue Date:

### Keywords

- Model-based diagnosis
- Diagnosability and manifestability
- Bounded model checking
- SMT
- Timed automata
- Real-time systems