Verification of current state opacity using switching output automata

We present a new discrete event model called switching output automaton where with each state is associated a set of discrete output values. The evolution of such a system, as state and output change, produces as observation a piecewise constant signal. The goal of this paper is that of designing a suitable observer for estimating the current discrete state of this model as a function of the observed output signal. In addition, we show how the observer can be used to verify if the system is current-state opaque