Coverage analysis of mobile agent trajectory via state-based opacity formulations

This paper performs coverage analysis of mobile agent trajectory utilizing discrete event system models and employing state-based notions of opacity. Non-deterministic finite automata with partial observation on their transitions are used to simultaneously capture both the kinematic model of a mobile agent and the information that becomes available by a set of sensors that are deployed in a given environment. The information provided by the set of sensors is analyzed to track the passage of a mobile agent through certain secret (strategic) locations at specific time instants using state-space notions of opacity, which arise naturally as the way to capture/analyze secrecy and privacy considerations in such settings, and to answer related coverage questions. Realistic examples of two-dimensional environments equipped with sensors monitoring the location of a mobile agent that follows a known kinematic model are subsequently analyzed by adopting existing tools in the discrete event systems area.

Research highlights
► Employed notion of infinite-step opacity to capture information flow leakage.
► Motivated the application of infinite-step opacity and implemented verification algorithm.
► Modeled system as a finite automaton with partial observation of events.
► Implemented method for infinite-step opacity verification using MATLAB and C++.