Diagnosability of Input Output Symbolic Transition Systems

Diagnosability checking of discrete-event systems has been extensively studied in the framework of classical nonsymbolic models such as labeled transition systems. It happens that in practice such models tend to need too much space to be efficiently processed. By opposition, symbolic approaches offer an expressive, easy and concise way to model systems, and checking diagnosability from such symbolic models can benefit from this reduction of space complexity.Indeed, though this will generally translate into time complexity,such a tradeoff is advantageous, as diagnosability checking is something that is usually done at design stage.This is why this paper proposes a theoretical frame work to check diagnosability of input-output symbolic transition systems (IOSTS) by adapting the twin plant approach to the symbolic case and relying on the use of a symbolic model checker. This theoretical work is being currently applied to embedded functions inside a vehicle in the context of an industrial project and a simplified version of this problem will serve as a running example throughout the presentation.