Order-2 bygone-state opacity of labeled finite-state automata
For researchers in discrete event systems and security, this extends opacity analysis from single-agent to two-agent scenarios, though the result is incremental.
The paper introduces order-2 bygone-state opacity, a property ensuring an agent cannot be certain another agent can uniquely determine the automaton's state from current and past observations, and provides a verification method in doubly exponential time.
In this paper, we formulate a scenario that an agent can never be sure that another agent can uniquely determine the state of a finite-state automaton based on its observations to the automaton at the current and any past time as the property of order-2 bygone-state opacity. Based on our concurrent composition and the classical observer, we derive a tool to verify this property in doubly exponential time. The interest of this result lies in that we extend inference of finite automata from a single agent to two ordered agents.