Diagnosis of Hybrid Systems with SMT: Opportunities and Challenges
Alban Grastien · Frontiers in artificial intelligence and applications · 2014
We propose a new approach to diagnosis of hybrid systems. In this approach, questions about the behavior of the system are asked and translated into Satisfiability Modulo Theory (SMT) problems, which are then solved by an SMT solver. We show the reduction to SMT. We also discuss the benefits and the drawbacks of this approach and conclude with a number of research directions that will make this approach applicable to large systems.