2026/06/25 by Kuize Zhang · 1 voice
Computer Science · #cs.FL #cs.CC
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.