SMT-Based Validation of Timed Failure Propagation Graphs


  • Marco Bozzano Fondazione Bruno Kessler
  • Alessandro Cimatti Fondazione Bruno Kessler
  • Marco Gario Fondazione Bruno Kessler
  • Andrea Micheli Fondazione Bruno Kessler



Satisfiability Modulo Theories, Timed Failure Propagation Graphs, Model Validation, Diagnosis


Timed Failure Propagation Graphs (TFPGs) are a formalism used in industry to describe failure propagation in a dynamic partially observable system. TFPGs are commonly used to perform model-based diagnosis. As in any model-based diagnosis approach, however, the quality of the diagnosis strongly depends on the quality of the model. Approaches to certify the quality of the TFPG are limited and mainly rely on testing. In this work we address this problem by leveraging efficient Satisfiability Modulo Theories (SMT) engines to perform exhaustive reasoning on TFPGs. We apply model-checking techniques to certify that a given TFPG satisfies (or not) a property of interest. Moreover, we discuss the problem of refinement and diagnosability testing and empirically show that our technique can be used to efficiently solve them.




How to Cite

Bozzano, M., Cimatti, A., Gario, M., & Micheli, A. (2015). SMT-Based Validation of Timed Failure Propagation Graphs. Proceedings of the AAAI Conference on Artificial Intelligence, 29(1).



Main Track: Search and Constraint Satisfaction