6 papers
Resilience in labeled real-time automata
Kuize Zhang
In this paper, we characterize resilience for a labeled real-time automaton (LRTA). An LRTA is resilient if whenever a faulty event occurs, after sufficiently many events occur, th…
Verification of - and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions
Jiahui Zhang, Kuize Zhang, Xiaoguang Han +1
Anonymity is an information flow property that provides privacy protection in the sense of non-uniqueness of system information at certain moments with respect to observations. The…
Order-2 bygone-state opacity of labeled finite-state automata
Kuize Zhang
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…
A remark on diagnosability verification
Kuize Zhang
We point out three inaccuracies in paper [M.V. Moreira, T.C. Jesus, and J.C. Basilio. Polynomial time verification of decentralized diagnosability of discrete event systems. IEEE T…
[Draft] High-order estimation-based properties and high-order observers for labeled finite-state automata
Kuize Zhang, Xiaoguang Han, Alessandro Giua +1
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 exten…
Verification and Enforcement of Strong State-Based Opacity for Discrete-Event Systems
Xiaoguang Han, Kuize Zhang, Zhiwu Li
In this paper, we investigate the verification and enforcement of strong state-based opacity (SBO) in discrete-event systems modeled as partially-observed (nondeterministic) finite…