Verification of current state opacity using switching output automata

Liu T.

Primo

;Seatzu C.

Penultimo

;Giua A.

Ultimo

2023-01-01

---

Abstract

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