[Draft] High-order observers and high-order state-estimation-based properties of discrete-event systems

State-estimation-based properties are central properties in discrete-event systems modeled by labeled finite-state automata studied over the past 3 decades. Most existing results are based on a single agent who knows the structure of a system and can observe a subset of events and estimate the system's state based on the system's structure and the agent's observation to the system. The main tool used to do state estimation and verify state-estimation-based properties is called observer which is the powerset construction originally proposed by Rabin and Scott in 1959, used to determinize a nondeterministic finite automaton with ε-transitions. In this paper, we consider labeled finite-state automata, extend the state-estimation-based properties from a single agent to a finite ordered set of agents and also extend the original observer to high-order observer based on the original observer and our concurrent composition. As a result, a general framework on high-order state-estimation-based properties have been built and a basic tool has also been built to verify such properties. This general framework contains many basic properties as its members such as state-based opacity, critical observability, determinism, high-order opacity, etc. Special cases for which verification can be done more efficiently are also discussed. In our general framework, the system's structure is publicly known to all agents A₁,,Aₙ, each agent Aᵢ has its own observable event set Eᵢ, and additionally knows all its preceding agents' observable events but can only observe its own observable events. The intuitive meaning of our high-order observer is what agent Aₙ knows about what Aₙ₋₁ knows about what A₂ knows about A₁'s state estimate of the system.