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.

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.

This paper addresses the liveness enforcement problem of time Petri nets through the control of time intervals of transitions. We design a structure named a critical state class graph, whose nodes contain the critical constraints of the time intervals of transitions. Then, we propose an algorithm to control the time intervals of controllable transitions such that a non-live time Petri net can be transformed into a live time Petri net. The results show that a maximally permissive solution of liveness enforcement can be computed if it exists.

This research analyzes current-state-based opacity in discrete event systems, which is a type of state-based opacity verification. We consider an unbounded Petri net to model this system, in which we assume that each transition is unobservable and partial places are observable (the number of tokens can be measured). A novel coverability graph based on partial markings is proposed, which is used to construct an estimator for current-state estimation. Current-state opacity is verified in this work employing the proposed new coverability graph. This paper proposes a sufficient and necessary condition for the verification of current-state opacity, as well as a concrete example to explain the approach.