Keywords: Cyber-security, Supervisory Control Theory, Verification, validation, test
Abstract: We present a framework for the modelling and synthesis of sensor and actuator attacks on discrete event systems. Initially, we consider systems composed of a single plant and supervisor subject to an attack that can modify the supervisor’s observations and control actions. The problem of designing stealthy attacks that can always inflict damage on the system is formulated as a standard supervisory control problem. Next, we show how to apply our framework to a decentralised system. Distributed attackers, one for each subsystem, are realised as nonconflicting supervisors that must coordinate to achieve their individual goals.

Keywords: Cyber-security, Opacity
Abstract: Cyber-Physical Systems (CPS) integrates a physical plant with control and monitoring devices using communication networks. Since communication networks are used in CPS, some of the communication channels may be vulnerable to passive attacks with the objective of eavesdropping secret information. One of the strategies to ensure information security in CPS abstracted as DES is enforcing opacity. In this paper, we propose a new strategy to enforce current-state opacity of a networked DES with multiple channels based only on event replacements, where it is supposed that the attacker eavesdrops part of the communication channels to discover the system secret states. We present a necessary and sufficient condition for the existence of an obfuscation policy based on event replacements (OPER) that ensures current-state opacity of CPS with multiple channels. The method generates an automaton map where all possible obfuscation policies that ensures the security objectives are represented.

Keywords: Cyber-security, Supervisory Control Theory
Abstract: This work is set in the context of systems modeled as discrete-event systems. The system is composed of several subsystems whose behavior is coordinated by the action of a controller, which, in turn, is a structure composed, among other elements, by supervisors. It is considered that the controller and each of the subsystems are connected to a communication network and they are subject to the action of a malicious agent that is able to modify the messages sent and received. A new attack model is presented, which considers the different types of actions an attacker is able to perform in a real system. Additionally, a new class of attackers is introduced, called persistent attackers. Moreover, a new design technique for this class of attackers is presented, where the goal of the attacker is to perform the attack while remaining stealthy.

Keywords: Opacity, Cyber-security, Verification, validation, test
Abstract: Cyber-physical systems (CPS) are formed of physical and computational components that interact to operate safely and efficiently according to a desired behavior. In this paper, we consider that the network used to transmit data from the plant to its monitoring and control device is vulnerable to cyber-attacks. The attacker eavesdrops on the communication channel to infer that the system is in a secret state. We assume that the information transmitted in the network is the status of system components, such as sensors, actuators, and local controllers' memory variables. Therefore, the system can be modeled from the attacker's perspective as a finite state transducer, where each state of the model is associated with an output vector formed of signals associated with system components. Considering that the attacker has full knowledge of the system model and does not know the system's current state when they initiate to eavesdrop on the communication channel, the attacker tries to estimate the system's current state by observing the transmitted state outputs. Thus, in this case, it is necessary to verify if the attacker is never able to detect whenever the system is in a secret state. In the Discrete-Event System literature, the system property associated with the intruder's inability to discover the system secret based on the transmitted information is called opacity. Since in this paper, the attacker observes state outputs of a finite state transducer, a new definition of opacity, called current-state opacity based on state outputs (CSO-SO), is introduced. We also present a method for the verification of this property.

Keywords: Opacity, Verification, validation, test
Abstract: In this paper, we consider timed opacity verification for switching output automata (SOA). We define a subset of global states of the SOA as vulnerable and associate to each of them a secret dwell interval. A SOA is opaque if an intruder, based on the observation of the outputs over time, cannot determine whether the current global state is vulnerable and the corresponding dwell time belongs to the secret dwell interval. We define a secret-dependent evolution automaton as the logical abstraction of the SOA's evolution when incorporating timed secrets. We show how an observer, i.e., the deterministic finite automaton equivalent to the secret-dependent evolution automaton, can be used to verify timed opacity.

Keywords: Cyber-security, Supervisory Control Theory, Modeling tools: Petri nets, automata, ...
Abstract: The problem of cyber attacks in the context of supervisory control layer is considered in this paper. Precisely, monitor based supervisors, largely used to enforce generalized mutual exclusion constraints, are focused on. An attack model to capture a class of deception attacks, where the attacker has the ability to hijack a subset of sensor readings and mislead the supervisor, is proposed in this paper. The model reveals that a monitor supervised system under attack can become not live and can drive the plant to forbidden states. To make a monitor robust against attacks a restriction to its input and output transitions is considered.

Keywords: Algebraic approaches: process algebras, max/plus-algebra, ..., Modeling tools: Petri nets, automata, ...
Abstract: This study compares an existing method with a novel approach for state estimation of Max-Plus Linear systems with bounded uncertainties. Traditional stochastic filtering does not apply to this system class, despite computable posterior probability density function (PDF) support. Existing literature suggests a limited scalability disjunctive approach using differencebound matrices. To overcome this, we study an alternative method recently investigated in Mufid et al. (2022) using Satisfiability Modulo Theory (SMT) techniques, which are known to be NP-hard. We propose a concise method that utilizes a pseudo-polynomial time algorithm using max-plus algebra. We evaluate its efficiency against SMT techniques through numerical experiments involving sparse matrix multiplications for enhanced computational speed.

Keywords: Algebraic approaches: process algebras, max/plus-algebra, ...
Abstract: We consider permutation flow shops with time-window constraints, which consist of several jobs to be processed in a sequence of machines in the same order, where no job overtaking is allowed, and with restrictions on the timing of the operations. The investigated class of permutation flow shops is larger than the one typically considered in scheduling literature. This paper introduces two strategies, based on previous results in the max-plus algebra, to obtain a schedule minimizing the makespan: an exact branch and bound method, and a heuristics inspired from receding-horizon control. Simulations demonstrate the advantages and limitations of the proposed approaches.

Keywords: Algebraic approaches: process algebras, max/plus-algebra, ..., Performance evaluation, optimization, Modeling tools: Petri nets, automata, ...
Abstract: Designing an invariant controller for a Tropical Linear Dynamical System involves formulating a tropical control law to ensure that the system state remains within a tropical subspace whenever the initial condition is situated within that subspace. In this paper, we explore a controller design approach that not only takes into account the invariance property but also optimizes the closed-loop system performance. Also, a preliminary discussion on control robustness is presented along with a new proposition.

Keywords: Algebraic approaches: process algebras, max/plus-algebra, ..., Verification, validation, test
Abstract: P-time event graphs are discrete event systems able to model cyclic production systems where tasks need to be performed within given time windows. Consistency is the property of admitting an infinite execution of such tasks that does not violate any temporal constraints. In this paper, we solve the long-standing problem of characterizing the decidability of consistency by showing that, assuming unary encoding of the initial marking, this property can be verified in strongly polynomial time. The proof is based on a reduction to the problem of detecting paths with infinite weight in infinite weighted digraphs called N-periodic graphs.

Keywords: Algebraic approaches: process algebras, max/plus-algebra, ..., Modeling tools: Petri nets, automata, ...
Abstract: In this paper, we discuss the stability of general time-invariant discrete-event systems modelled as max-min-plus scaling (MMPS) systems. We analyze MMPS systems with two types of states: time states and quantity states. A set of linear programming problems are proposed to find the growth rates of the time states via a normalization of the MMPS system. Then a framework for stability analysis of the general time-invariant MMPS system is discussed with respect to the normalized system. The approach presented in this paper is an efficient way to study the stability of a general MMPS system.

Keywords: Algebraic approaches: process algebras, max/plus-algebra, ..., Modeling tools: Petri nets, automata, ..., Performance evaluation, optimization
Abstract: We propose two new semantics for T-time Petri nets (T-TPN), which fill the gap between strong and weak semantics. By encoding a 2-counter machine, we prove that reachability is not decidable for these semantics in the case of unbounded nets. We then consider safe nets and we propose a translation into interval weighted automata over an interval like semiring, product of (max,+) semiring with itself, that preserves the timed behavior of T-TPN.

Keywords: Modeling tools: Petri nets, automata, ..., Diagnosis, fault tolerance, observability, ...
Abstract: A new approach for the online state estimation of discrete event systems (DESs) modeled by λ-free labeled Petri nets (λf-LPNs) is presented, wherein all events are observable. Instead of exhaustively enumerating all marking vectors consistent with any given event occurrence, we do a representation-based state estimation, where we compute a compact representation structure that characterizes these markings. Our representation structure is based on a representative Petri net (RPN), which is a copy of the system λf-LPN whose single initial marking represents all markings consistent with the sequence. These representations can be directly used to solve other DES-related problems, such as fault diagnosis. Our approach can compute representations of any λf-LPNs. In addition, for a class of unbounded λf-LPNs, our approach can compute representations that do not grow indefinitely as more events occur.

Keywords: Modeling tools: Petri nets, automata, ...
Abstract: This paper presents a timed extension of Synchronized Petri nets that can be controlled and observed. Output Synchronized Petri Nets have been previously defined for allowing a Cyber-Physical System to be controlled through input event associated with controllable transitions and to be observed thanks to output events issued by the marking values and/or marking changes. The proposed new timed extension, called timed Output Synchronized Petri nets, is obtained by assigning firing durations to transitions. As the state space of such formalism involves dense time variables, we propose a state class graph abstraction called Synchronized State Class Graph.

Keywords: Modeling tools: Petri nets, automata, ...
Abstract: The enumeration of legal transition paths leading to a target state (or set of states) is of paramount importance in the control of discrete event systems, but is hindered by the state explosion problem. A method is proposed in this paper, in the context of Petri nets, to calculate and enumerate firing count vectors for which there exists at least an admissible transition sequence leading to a given target marking. The method is based on the concept of singular complementary transition invariants proposed by Kostin and combines an integer linear programming formulation that finds the shortest minimal solution and a branching procedure that effects a partition of the solution set. The enumeration can be restricted to minimal solutions or extended to non-minimal ones. Some analytical examples are discussed in detail to show the effectiveness of the proposed approach.

Keywords: Performance evaluation, optimization, Modeling tools: Petri nets, automata, ...
Abstract: An optimization formulation is presented for timed Petri nets, based on a recently developed optimization solver where a satisfiability solver is integrated with constraint programming. The solver, called CP-SAT, is a part of Google's OR-Tools. The first optimization formulation includes an arbitrary number of concurrent sequences of operations, with shared, alternative, and local resources. A benchmark shows how much faster CP-SAT is compared to both an alternative SAT optimization solver and an A* implementation. The optimization formulation is then generalized to mixed alternative and concurrent sequences. A comparison with a recent MILP formulation for timed Petri nets is presented, showing the strength of the proposed optimization formulation. Finally, an evaluation of an industrial-sized flexible manufacturing system, including uncontrollable events, demonstrates how efficient and easy to implement the proposed strategy is compared to existing results.

Keywords: Modeling tools: Petri nets, automata, ..., Identification
Abstract: The COVID-19 pandemic has placed unprecedented pressure on hospitals and requires efficient patient management to optimize bed utilization. This paper introduces a formal modeling tool designed to streamline and update clinical pathways, facilitating evaluation of system performance and resource optimization. Emphasizing user-friendliness for medical personnel, we employ Probabilistic Time Petri Nets to represent clinical pathways. These models are constructed using a novel pattern discovery algorithm that efficiently extracts pertinent data from patient treatment databases. This approach significantly improves the management of hospital workflow, particularly critical during health crises.

Keywords: Supervisory Control Theory, Verification, validation, test
Abstract: We present a new algorithm to verify inference observability in supervisory control of decentralized discrete-event systems. The algorithm's success relies on the following idea. An inferencing solution exists only when a language contains no inferencing cycles. When there are no cycles, the algorithm computes the smallest upper bound for an inferencing solution.

Keywords: Supervisory Control Theory, Performance evaluation, optimization, Verification, validation, test
Abstract: This work investigates robust supervisory control problems of discrete event systems modeled as finite state automata equipped with metric functions to measure the distance between states. The system may deviate from its nominal behaviors and fail to achieve the specification under disturbances whose effects are considered to be bounded. Accordingly, the supervisor should be designed to ensure that the controlled system degrades gracefully against such adversary. We formally formulate two problems: robustness bound verification and optimal robust supervisor synthesis. For the special case of verification under constant disturbances, a control Lyapunov function approach is introduced. Then we develop a two player game framework for the general verification and synthesis problems. Specifically, a dynamic programming method is proposed on the game structure, which uniformly tackles both problems.

Keywords: Supervisory Control Theory, Diagnosis, fault tolerance, observability, ...
Abstract: This paper presents an approach towards the synthesis of maximally permissive, safe, controllable, control consistent and nonblocking supervisors where the supervisor is assumed to have partial observation of the events in the plant that is modeled as a discrete event system. In contrast to existing work, the presented approach avoids the use of concepts such as observability and normality and only relies on a transformation of the plant into another discrete event system to which subsequently supervisory control synthesis with full observation is applied.

Keywords: Supervisory Control Theory
Abstract: This paper explores the problem of analysis and control towards model-unknown discrete-event systems. Using data, i.e. partly observed output event sequences and some pre-established knowledge, we apply an event-forcing mechanism to verify an extended concept of controllability, namely forcible-controllability, and develop control strategies with respect to the observed specification language. In particular, for the given data, a property namely forcible-informativity is proposed, representing a criterion for determining the forcible-controllability of the observed specification language. The data-driven supervisory control is also devised accordingly, if feasible.

Keywords: Supervisory Control Theory, Applications
Abstract: This paper presents a novel algorithm that employs the Markov Decision Process approach to efficiently determine sequences that minimize makespan for planning problems. The approach employs local modular supervisors, enhancing flexibility and computational capability. The algorithm achieves optimal makespan values for the evaluated case study, demonstrating its effectiveness. Moreover, the method empowers real-time decision-making, outperforming existing approaches by significantly reducing computation time.