Keywords:Performance evaluation, optimization, Applications Abstract: In a recent work, we introduced a new set of problems in the area of networked robotic systems that concern the time-optimal execution of certain coverage tasks taking place in constricted environments. That work provided the detailed problem definitions, a complete representation of these problems in terms of Mathematical Programming (MP) formulations, and a formal analysis of their worst-case computational complexity. The current work establishes some structural results for the considered problems that are useful for the strengthening of the aforementioned MIP formulations and for the further development of pertinent heuristic solution methods for these problems. We demonstrate the first possibility in this paper, and we defer the second one to future work.

Keywords:Applications, Supervisory Control Theory, Modeling tools: Petri nets, automata, ... Abstract: In this paper, we investigate the problem of optimal multi-robot path planning for a cyclic task represented by a particular type of linear-temporal logic (LTL) formulae. Specifically, the team of robot needs to fulfill a given LTL formula and at the same time, accomplishes some particular tasks infinitely ofte}. To avoid the state-space explosion when the number of robot increases, we use Petri nets to model the team of multi-robot. Our goal is to find an optimal infinite sequence in the prefix-suffix form for each robot such that the average cost per task is minimized. We propose an efficient planning method based on the notion of basis reachability graph (BRG), which is a compact representation of the reachability space of the PN. We demonstrate the computational efficiency of our method through illustrative examples.

Keywords:Supervisory Control Theory, Applications, Modeling tools: Petri nets, automata, ... Abstract: Safe control has recently attracted much attention due to its applications in safety-critical cyber-physical systems. Supervisory control theory (SCT) is a formal control method that provides correct-by-construction safety certificates, but is computationally inefficient when the number of system components is large. On the other hand, deep reinforcement learning (DRL) provides a toolbox of efficient algorithms to compute control decisions even for very large state space, but does not always guarantee safety. In this paper, we propose to synergize SCT and DRL into a new efficient safe control approach. Specifically, we first employ DRL algorithms to efficiently compute sub-optimal solutions which may be unsafe; then we convert the obtained solutions into a standard supervisory control problem with an automaton (plant model) and a set of unsafe states (safety specification); finally we use SCT to synthesize a supervisor with a safety certificate. A case study of multi-robot warehouse logistic automation is conducted to demonstrate the efficiency of this proposed approach.

Keywords:Performance evaluation, optimization, Applications Abstract: The Conflict-Free Electric Vehicle Routing Problem (CF-EVRP) is a combinatorial optimization problem of designing routes for vehicles to visit customers such that a cost function, typically the number of vehicles or the total travelled distance, is minimized. The CF-EVRP involves constraints such as time windows on the delivery to the customers, limited operating range of the vehicles, and limited capacity on the number of vehicles that a road segment can simultaneously accommodate. In previous work, the compositional algorithm ComSat was introduced and that solves the CF-EVRP by breaking it down into sub-problems and iteratively solve them to build an overall solution. Though ComSat showed good performance in general, some problems took significant time to solve due to the high number of iterations required to find solutions that satisfy the road segments' capacity constraints. The bottleneck is the Path Changing Problem, i.e., the sub-problem of finding a new set of shortest paths to connect a subset of the customers, disregarding previously found shortest paths. This paper presents an improved version of the PathsChanger function to solve the Path Changing Problem that exploits the unsatisfiable core, i.e., information on which constraints conflict, to guide the search for feasible solutions. Experiments show faster convergence to feasible solutions compared to the previous version of PathsChanger.

Keywords:Performance evaluation, optimization, Supervisory Control Theory, Modeling tools: Petri nets, automata, ... Abstract: This paper proposes an algorithm to find the time optimal fault-tolerant controllable string for multi-process systems, in which some specifications are enforced to the nonfaulty system, such that the system can recover from faults and satisfy the specifications efficiently through resource sharing. We first derive an algorithm from checking the fault-tolerant property via the abstraction of the system, then a backtracking algorithm is sequentially used to find the optimal fault-tolerant string based on the abstraction of the system. Moreover, the proposed fault-tolerant string synthesis algorithms are tested on a simulated manufacturing system to show their effectiveness.

Keywords:Supervisory Control Theory, Modeling tools: Petri nets, automata, ... Abstract: In supervised discrete event systems under attack, the goal of the supervisor, who has a partial observation of the system evolution, is to prevent the system from reaching a set of unsafe states. An attacker may act in two different ways: it can corrupt the observation of the supervisor by editing the sensor readings, and it can enable events that have been disabled by the supervisor. This is done with the aim of leading the plant to an unsafe state. A special automaton, called attack structure is constructed as the parallel composition of two special structures: an attacker observer and a supervisor under attack. Such an automaton can be used by the attacker to select proper actions (if any) to lead the plant to reach the unsafe state.

Keywords:Modeling tools: Petri nets, automata, ..., Diagnosis, fault tolerance, observability, ... Abstract: This paper addresses the problem of cyber-attacks in discrete-event systems framework. Labeled finite state automata with inputs derived from a particular class of Petri net, called Output Synchronized Petri nets, are used to model a given cyber-physical system along with the information that circulate between controllers and plant. Stealthy cyber-attacks that may alter the control symbols, i.e., the orders sent by the controllers to the actuators, are considered. The objective is to construct an observer that uses both input and output information to provide a state estimation of the system under such stealthy actuators attacks. This observer provides a refined state estimation related to both normal and attack conditions.

Keywords:Diagnosis, fault tolerance, observability, ..., Modeling tools: Petri nets, automata, ..., Verification, validation, test Abstract: This paper discusses fault diagnosis and diagnosability analysis in discrete-event systems modeled with nondeterministic finite automata, {partially observed via} a sensor measuring unit whose measurements (reported observations) may be vitiated by a malicious attacker. The attacks considered in this paper include arbitrary deletions, insertions, or substitutions of observed symbols. Assuming that each deletion, insertion, or substitution bears a positive cost to the attacker, two scenarios are taken into account: (1) a bounded number of attacks or, more generally, a total cost constraint on tampering actions; (2) an infinite number of attacks or, more generally, no constraints on the total cost of tampering actions. Several examples are presented to demonstrate the influence of cost constraints on tamper-tolerant diagnosis and tamper-tolerant system diagnosability.

Keywords:Applications, Tools Abstract: In this paper, we consider Cyber-Physical Systems (CPS) in a Discrete-Event Systems (DES) framework, and consider cyber attacks in the automation network of the CPS, where a malicious agent eavesdrops communication channels with the objective to gather information about the system behavior. We propose a cryptographic scheme to be applied in an automation network which cipher events without altering the size or structure of the transmitted data. In addition, the proposed cryptographic scheme leads to small communication delays, which makes it suitable for application in automation networks. We call this scheme event-based cryptography, where an event is defined as any change in the binary signals transmitted in the network. In order to do so, we propose a method for the codification of events as event vectors, which is suitable for encryption. We also propose the use of a stream cipher called ChaCha20, which is known to have a high resistance to cryptanalysis. A simulated example is used to illustrate the application of the proposed event-based cryptography, and to make a comparison with the RSA cipher, a public-key cipher widely used in Information Technology.

Keywords:Applications, Diagnosis, fault tolerance, observability, ..., Modeling tools: Petri nets, automata, ... Abstract: Software Defined Networking (SDN) is a networking architecture within the control is centralized through a software-based controller. Like Cyber-Physical Systems manager, this centralization eases the support of advances application. Being a single point of attack makes the controller a preferred target in case of attack. To enforce the control plane, an observer is introduce and is in charge of the detection of cyber-attacks on the nominal controller. In this objective, an anomalies detection method in the activity of the control is proposed. This activity is defined as the events at the interface of communication between the controller and the network-plant. In this paper, a non-deterministic control is considered which means that the decisions are stochastics. Hence, a probabilistic approach is proposed which aims to evaluate the deviation of the likelihood of the sequence of decisions taken by the controller. The formalism used to determine the likelihood is the Hidden Markov Model which permits to infer over the internal states of the controller through the observations. This method is discussed on a network case study.

Keywords:Modeling tools: Petri nets, automata, ... Abstract: This work achieves parallel movements and collision free paths for a team of identical robots evolving in a known environment while satisfying a global Boolean-based formula over a set of regions of interest. The movement capabilities of the robots within the grid-based environment are modeled as a Petri net system. The solution starts from initially known robot paths given by the approach in (Mahulea et al., 2020b). The main advantages of this work are two-folded: (i) it reduces the number of waiting states of the robots throughout their paths, (ii) it considers path rerouting action solved by a MILP problem, without generating new observations along their paths. The rerouting is triggered when the number of robots that are waiting is greater than a threshold, or when some stopped robots inhibit the movement of others. Thus, the proposed method yields parallel movement of robots and path rerouting when needed. The algorithm is integrated in the open-source toolbox RMTool (Gonz´alez et al., 2015)

Keywords:Supervisory Control Theory, Verification, validation, test, Discrete approaches for hybrid systems Abstract: A third of the Dutch highways is monitored and controlled by roadside units. These RSUs are safety-critical systems, as they safeguard roadworks and accidents. Therefore, it is essential to have guarantees on the correctness of the roadside unit controller. Using supervisory control theory, a correct-by-construction supervisor is obtained from a model of the system and its requirements. From the supervisor model, a controller implementation can be obtained automatically.

There are many roadside units sharing the same basic components, but in different numbers and configurations. To take advantage of this, parametric models are used. Subsequently, these models can be used to create different models for different configurations of an roadside unit.

The purpose of this paper is to show the applicability of supervisory control theory to roadside units. To this end, parametrized models of the components of an roadside unit are presented. The models are used to synthesize a supervisor for a specific roadside unit, which is validated using simulation. After validation, a controller implementation is generated from the supervisor model. The implementation is then validated using hardware-in-the-loop simulation.

Keywords:Discrete approaches for hybrid systems, Supervisory Control Theory, Modeling tools: Petri nets, automata, ... Abstract: The paper contributes with a hybrid controller for multiple mobile robot systems (MMRS) that ensures the correct accomplishment of its mission by each robot. We capitalize on earlier results concerning the supervision of the robot flow, in particular the concept of partitioning the motion area into cells. Then the system comprises three control levels: DES (Discrete Event System) based cell-transition controller, APF (Artificial Potential Field) based cell-traverse controller, and CTS (Continuous Time System) based robot motion controller. The breakdown of the coordination concept into two control levels allows the optimal solution of the system liveness problem, and the holistic approach to the control of MMRS provides for its direct implementation in both a simulator and a real-robot test-bed.

Keywords:Applications, Supervisory Control Theory Abstract: The Maeslantkering is a key flood defense infrastructural system in the Netherlands. This movable barrier protects the city and harbor of Rotterdam, without impacting ship traffic under normal circumstances. Its control system, which operates completely autonomously, must be guaranteed to work correctly even under extreme weather conditions, although it closes only sporadically. During its development in the 1990's, the formal methods Z and Spin were used to increase reliability. As the availability of industrial expert knowledge on these formal methods declines, maintaining the specifications defined back then has become cumbersome. In the quest for an alternative mathematically rigorous approach, this paper reports on an experience in applying supervisory control synthesis. This formal method was recently applied successfully to other types of infrastructural systems like waterway locks, bridges, and tunnels, with the purpose to ensure safe behavior by coordinating hardware components. Here, we show that it can also be used to coordinate several (controller) software systems. Additionally, we compare the lessons learned from the originally used formal methods and link Z to supervisory control synthesis.

Keywords:Diagnosis, fault tolerance, observability, ..., Modeling tools: Petri nets, automata, ..., Tools Abstract: Flexible Manufacturing Systems (FMSs) are designed to execute parallel processes simultaneously by using flexible resources (e.g. robots, re-configurable machines) alongside a supervisor allocating the resources to the different processes. In these systems, deadlocks are defined as blocking states where no resource allocation decision can be taken. They originate from resources characteristics (i.e. mutual exclusion condition, non-preemptive), processes interactions (i.e. shared resources, circular wait of resources) and an inappropriate sequence of allocation decisions. In modern FMSs, the use of open and interconnected control components for resource allocation control and productivity enhancement makes FMSs vulnerable to cyber-attacks. Hence, although FMSs are designed to deal with known natural deadlocks, new malicious ones can originate from sophisticated cyber-attacks. In this paper, malicious deadlocks are defined and contextualized regarding the existing literature on deadlocks management and on cyber-attacks targeting Discrete-Event Systems (DES). Then, a model representative of deadlock attacks is proposed based on the S^3PR theory and DES attacks modeling. Finally, the deadlock attack model is simulated and new malicious deadlocks are exhibited and discussed.

Keywords:Modeling tools: Petri nets, automata, ..., Verification, validation, test Abstract: Opacity is an important property asking whether a passive observer (an intruder), who knows the structure of the system but has only a limited observation of its behavior, may reveal the secret of the system. Several notions of opacity have been studied in the literature, including current-state opacity, k-step opacity, and infinite-step opacity. We investigate weak and strong k-step opacity, the notions that generalize both current-state opacity and infinite-step opacity, and ask whether the intruder is not able to decide, at any instant, when respectively whether the system was in a secret state during the last k observable steps. We design a new algorithm to verify weak k-step opacity, the complexity of which is lower than that of existing algorithms and that does not depend on the parameter k. Then, we show how to use this algorithm to verify strong k-step opacity by reducing the verification of strong k-step opacity to the verification of weak k-step opacity. The complexity of the resulting approach is again better than that of existing algorithms, and does not depend on the parameter k.

Keywords:Supervisory Control Theory Abstract: We investigate opacity, an information-flow privacy property, in a setting where there are two competing agents or adversaries whose objective is to hide their secrets and expose the secrets of the other agent. Each agent has only partial information about the state of the system. The agents can achieve their objective by enabling or disabling events from their set of controllable events. We examine two different scenarios. In the first problem, the agents are passive with no control capabilities, and we seek a global controller to enforce their mutual opacity. In the second problem, the formerly passive agents are autonomous and have control capabilities. We seek the plausibility of two controllers, one for each agent, to see if we can synthesize a winning control strategy so that one adversary can always discover the secrets of the other without revealing its own.

Keywords:Modeling tools: Petri nets, automata, ..., Diagnosis, fault tolerance, observability, ... Abstract: This paper focuses on the problem of the detectability in the setting of partially-observed discrete event systems subject to sensor attackers. We assume the attacker can arbitrarily alter sensor readings after intercepting them from a target system, aiming to trick a given supervisor to issue improper control commands, which may lead the system not be strongly or weakly detectable. The definitions of attackable strong detectability and attackable weak detectability are presented. Necessary and sufficient conditions for two types of detectability are then presented respectively based on the observer construction.

Keywords:Applications, Supervisory Control Theory, Verification, validation, test Abstract: In this paper we present an implementation scheme for a networked control system where the coordination between devices is done by supervisory control theory. The system is intended to be used as a testbed for DES security-related techniques. We provide some examples of attacks whose effect can be evaluated using the proposed setup. The hardware and software are based on low-cost devices and can be modified to suit different control systems. The details of the implementation are available on a free online repository.

Keywords:Diagnosis, fault tolerance, observability, ..., Verification, validation, test, Applications Abstract: In this paper, we investigate a class of information-flow security properties called opacity in partial-observed discrete-event systems. Roughly speaking, a system is said to be opaque if the intruder, which is modeled by a passive observer, can never determine the ``secret" of the system for sure. Most of the existing notions of opacity consider secrets related to the actual behaviors of the system. In this paper, we consider a new type of secret related to the knowledge of the system user. Specifically, we assume that the system user also only has partial observation of the system and has to reason the actual behavior of the system. We say a system is high-order opaque if the intruder can never determine that the system user knows some information of importance based on its own incomparable information. We provide the formal definition of high-order opacity. Two algorithms are provided for the verification of this new notion: one with doubly-exponential complexity for the worst case and the other with single-exponential complexity. Illustrative examples are provided for the new notion of high-order opacity.