This paper addresses the verification of strong cur-rent-state opacity with respect to real-time observations gener-ated from a discrete-event system that is modeled with time labeled Petri nets. The standard current-state opacity cannot completely characterize higher-level security. To ensure the higher-level security requirements of a time-dependent system, we propose a strong version of opacity known as strong current-state opacity. For any path (state-event sequence with time information) π derived from a real-time observation that ends at a secret state, the strong current-state opacity of the real-time observation signifies that there is a non-secret path with the same real-time observation as π. We propose general and non-secret state class graphs, which characterize the general and non-secret states of time-dependent systems, respectively. To capture the observable behavior of non-secret states, a non-secret observer is proposed. Finally, we develop a structure called a real-time concurrent verifier to verify the strong current-state opacity of time labeled Petri nets. This approach is efficient since the real-time concurrent ver-ifier can be constructed by solving a certain number of linear programming problems.

This work addresses the verification of current-state opacity with respect to a real-time observation generated from time-dependent systems. The secret behavior of a time-dependent system is defined as a set of states in a time labeled Petri net. The current-state opacity of a real-time observation means that a given secret remains opaque to the intruder who can partially observe the system behavior in the framework of a time labeled Petri net at a given time instant. We introduce a novel directed graph, called a parallel state class graph, to represent the parallel evolution of time-dependent systems exhaustively. Based on the parallel state class graph, we design an algorithm for the construction of a critical observer and show that the current-state opacity of a real-time observation in time labeled Petri nets can be efficiently solved by the critical observer. This approach is computationally competitive since the critical observer can be constructed by solving a number of linear programming problems. Note to Practitioners —In computer-integrated real-time systems, their correctness-related properties usually depend on time constraints. System opacity guarantees that particular system information cannot be disclosed or inferred by external observers, which is a generalization of many information flow properties associated with system safety, particularly in aerospace, automotive, and healthcare domains. This research addresses the verification problem of this property for a discrete event system modeled with time labeled Petri nets. By developing a graph-theoretical structure that can be readily managed by security engineers, a type of diagram called a critical observer is derived which is able to detect the privacy of the system at a given time instant. This research provides a systematic and efficient approach for practitioners to check a desired privacy strategy of time-constrained safety systems.

This paper addresses the problem of cyber-attack detection in a discrete event system by proposing a novel model. The model utilizes graph convolutional networks to extract spatial features from event sequences. Subsequently, it employs gated recurrent units to re-extract spatio-temporal features from these spatial features. The obtained spatio-temporal features are then fed into an attention model. This approach enables the model to learn the importance of different event sequences, ensuring that it is sufficiently general for identifying cyber-attacks, obviating the need to specify attack types. Compared with traditional methods that rely on synchronous product computations to synthesize diagnosers, our deep learning-based model circumvents state explosion problems. Our method facilitates real-time and efficient cyber-attack detection, eliminating the necessity to specifically identify system states or distinguish attack types, thereby significantly simplifying the diagnostic process. Additionally, we set an adjustable probability threshold to determine whether an event sequence has been compromised, allowing for customization to meet diverse requirements. Experimental results demonstrate that the proposed method performs well in cyber-attack detection, achieving over $99.9\%$ accuracy at a $1\%$ threshold and a weighted F1-score of 0.8126, validating its superior performance.

Rule–based fuzzy models have modular architectures and come with well-developed design methodologies such that they can build accurate models with good interpretabilities in system modeling. However, a large amount of private data needs to be used for statistical analysis and forecasting in rule–based fuzzy models. The purpose of this study is to build an intelligent model with high accuracy and versatility under the premise of data privacy and model security. To mitigate the risk of malicious attacks on privacy data during the analysis process, we have employed highly regarded differential privacy techniques to devise a novel rule-based fuzzy modeling approach. We propose a function approximation mechanism to reconstruct the objective function and add a perturbation mechanism to the objective function in Takagi-Sugeno rules model. Taking into account the delicate balance between data privacy and utility, we have innovatively introduced a Takagi-Sugeno rule-based model based on differential privacy. This model is applicable to both linear and nonlinear systems, offering protection to sensitive data privacy and model security within the system. We investigate the relationship between the interpretability of the model and the degree of privacy protection. By constructing a reasonable rule base, we achieve higher accuracy than other system modeling methods based on differential privacy. This paper compares the influence of the number of rules on differential privacy, and considers the algorithm performance under various noise distributions. It is shown that the Takagi-Sugeno rules model based on differential privacy has a strong ability to predict and analyze data.