2024/08/12 by Kuize Zhang, Xiaoguang Han, Zhang, Kuize +5
Computer Science · Engineering · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Radiation Effects in Electronics
paper · pdf · doi:10.48550/arxiv.2408.06141
openalex publication_date 2024/08/12 · openalex created_date 2024/09/11 · openalex updated_date 2026/07/28
In this paper, we consider labeled finite-state automata (LFSAs), extend some state estimation-based properties from a single agent to a finite ordered set of agents. We also extend the notion of observer to high-order observer using our concurrent composition. As a result, a general framework for characterizing high-order estimation-based properties is built, in which each agent infers its preceding agent's estimation via all agents in front. The high-order observer plays the role of a basic tool to verify such properties. In more detail, in our general framework, the system's structure is publicly known to all agents A1,…,An; each agent Ai has its own observable event set Ei, 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 to characterize what agent An knows about what An-1 knows about … what A2 knows about A1's state estimate of the system. This general framework can be regarded as an automata representation of dynamic epistemic logic. Compared with the classical representation of dynamic epistemic logic based on fragments of logic, our representation has advantages in property verification and flexibly changing agents to enforce properties. As case studies, this general framework applies to basic properties such as current-state opacity, strong current-state opacity, regular-language-based opacity, critical observability, high-order opacity, etc. Special cases for which verification can be done more efficiently are also discussed.