High-order observers and high-order state-estimation-based properties of labeled finite-state automata ---Computing “know what” in a sequence of labeled finite-state automata
时间  Datetime
2025-11-29 10:15 — 11:30
地点  Venue
会议室(703)
报告人  Speaker
张奎泽
单位  Affiliation
西安交通大学
邀请人  Host
备注  remarks
张奎泽教授个人主页：
报告摘要  Abstract

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 A_1, …, A_n; each agent A_i has its own observable event set E_i, 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_n knows about what A_{n-1} knows about … what A_2 knows about A_1's state estimate of the system. 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.
--
FROM 202.120.11.*