  In this paper, we consider the problem of verifying pre-opacity for
discrete-time control systems. Pre-opacity is an important information-flow
security property that secures the intention of a system to execute some secret
behaviors in the future. Existing works on pre-opacity only consider non-metric
discrete systems, where it is assumed that intruders can distinguish different
output behaviors precisely. However, for continuous-space control systems whose
output sets are equipped with metrics (which is the case for most real-world
applications), it is too restrictive to assume precise measurements from
outside observers. In this paper, we first introduce a concept of approximate
pre-opacity by capturing the security level of control systems with respect to
the measurement precision of the intruder. Based on this new notion of
pre-opacity, we propose a verification approach for continuous-space control
systems by leveraging abstraction-based techniques. In particular, a new
concept of approximate pre-opacity preserving simulation relation is introduced
to characterize the distance between two systems in terms of preserving
pre-opacity. This new system relation allows us to verify pre-opacity of
complex continuous-space control systems using their finite abstractions. We
also present a method to construct pre-opacity preserving finite abstractions
for a class of discrete-time control systems under certain stability
assumptions.
