Ziyue Ma

Bohan Cui, Ziyue Ma, Alessandro Giua et al.

We investigate the enforcement of opacity in discrete-event systems via supervisory control. A system is said to be opaque if a passive intruder can never unambiguously infer whether the system is in a secret state through its observations. In this context, the intruder's knowledge about the supervisor plays a critical role in both problem formulation and solvability. Existing studies typically assume that the policy of the supervisor is either fully unknown to the intruder or fully known a priori, the latter leading to severe technical challenges and unresolved problems under incomparable observations. This paper investigates opacity supervisory control under a new intermediate information setting, which we refer to as the a priori unknown supervisor setting. In this setting, the supervisor's internal realization is not publicly available, but the intruder can partially infer its behavior by eavesdropping on the control decisions issued online during system execution. We formalize the intruder's information-flow under both observation-triggered and decision-triggered decision-issuance mechanisms and define the corresponding notions of opacity. We provide sound and complete algorithms for synthesizing opacity-enforcing supervisors without imposing any restrictions on the observable or controllable event sets. By constructing an information-state structure that embeds the supervisor's estimate of the intruder's belief, the synthesis problem is reduced to a safety game. Finally, we show that, under strictly finer intruder observations, the proposed setting coincides with the standard a priori known supervisor model.

Pengfei Li, Ziyue Ma, Hong Wang et al.

Background and Objective: In neurosurgery, fusing clinical images and depth images that can improve the information and details is beneficial to surgery. We found that the registration of face depth images was invalid frequently using existing methods. To abundant traditional image methods with depth information, a method in registering with depth images and traditional clinical images was investigated. Methods: We used the dlib library, a C++ library that could be used in face recognition, and recognized the key points on faces from the structure light camera and CT image. The two key point clouds were registered for coarse registration by the ICP method. Fine registration was finished after coarse registration by the ICP method. Results: RMSE after coarse and fine registration is as low as 0.995913 mm. Compared with traditional methods, it also takes less time. Conclusions: The new method successfully registered the facial depth image from structure light images and CT with a low error, and that would be promising and efficient in clinical application of neurosurgery.