Verification of Current State Opacity using Switching Output Automata
Tianyu Liu, Carla Seatzu, Alessandro Giua · 2023
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.