Search

One of the most important challenges for the application of cyber-physical systems (CPS) in smart industries is ensuring its security against cyber attacks. In this paper, we consider that the CPS is abstracted as a Discrete-Event System (DES), and we consider cyber attacks where the intruder eavesdrops the communication channels from the system to an intended receiver (e.g. a supervisor or diagnoser) to detect the occurrence of a sequence in the secret behavior of the system. In order to prevent the attacker from discovering secret information from the communication channel, a new cryptographic scheme based on events, called event-based cryptography, is introduced. We also define the property of confidentiality of DES with respect to an encryption function and a secret language, which is associated with the fact that only the sender and the intended receiver are able to understand the transmitted secret message. A necessary and sufficient condition for confidentiality is presented, and we propose a test to verify this property. We also present a method to create an encryption function to ensure confidentiality for a CPS, if it exists, when the secret language is formed only of sequences with length bounded by a given number. [ABSTRACT FROM AUTHOR]

Compared with the traditional pulse repetition interval (PRI) parameters, PRI pattern can describe the temporal characteristics of radar more completely, and the method based on PRI pattern is more suitable for tasks of deinterleaving and identification. Therefore, effective reconstruction of PRI pattern is an important task in radar signal processing. However, previous PRI pattern reconstruction methods either set too many subjective parameters or have high requirements for the number of pulses, making it not very practical for analyzing actual radar signals. In this paper, the temporal rule of pulse train is modeled from the perspective of radar timing state switching. Then the pulses of different timing states in the pulse train are clustered based on state merging algorithms in model learning. The transitions between different timing states are established based on the pulse sets obtained by clustering. Finally, the PRI pattern of radar is reconstructed after processing interferential pulses and missing pulses. Based on the above method, this paper further proposes a method to reconstruct PRI patterns of all radars in interleaved pulse trains. Simulation results verify the effectiveness of the proposed PRI pattern reconstruction method. • PRI pattern reconstruction framework based on model learning. • Pulse clustering algorithm based on state merging. • Radar emitter division method for interleaved pulse trains. • Better adaptability to the data noises, PRI pattern order and small pulse number. [ABSTRACT FROM AUTHOR]

Ensuring safety is crucial for the successful deployment of autonomous systems, such as self-driving vehicles, unmanned aerial vehicles, and robots acting close to humans. While there exist many controllers that optimize certain criteria, such as energy consumption, comfort, or low wear, they are usually not able to guarantee safety at all times for constrained nonlinear systems affected by disturbances. Many controllers providing safety guarantees, however, have no optimal performance. The idea of this article is, therefore, to synthesize a formally correct controller that serves as a safety net for an unverified, optimal controller. This way, most of the time, the optimal controller is in charge and leads to a desired, optimal control performance. The safety controller constantly monitors the actions of the optimal controller and takes over if the system would become unsafe. The safety controller utilizes a novel concept of backward reachable set computation, where we avoid the need of computing underapproximations of reachable sets. We have further developed a new approach that analytically describes reachable sets, making it possible to efficiently maximize the size of the backward reachable set. We demonstrate our approach by a numerical example from autonomous driving. [ABSTRACT FROM AUTHOR]

This article is concerned with a compositional approach for the construction of control barrier certificates for large-scale interconnected stochastic systems while synthesizing hybrid controllers against high-level logic properties. Our proposed methodology involves decomposition of interconnected systems into smaller subsystems and leverages the notion of control sub-barrier certificates of subsystems, enabling one to construct control barrier certificates of interconnected systems by employing some $\max$ -type small-gain conditions. The main goal is to synthesize hybrid controllers enforcing complex logic properties, including the ones represented by the accepting language of deterministic finite automata, while providing probabilistic guarantees on the satisfaction of given specifications in bounded-time horizons. To do so, we propose a systematic approach to first decompose high-level specifications into simple reachability tasks by utilizing automata corresponding to the complement of specifications. We then construct control sub-barrier certificates and synthesize local controllers for those simpler tasks and combine them to obtain a hybrid controller that ensures satisfaction of the complex specification with some lower bound on the probability of satisfaction. We finally apply our proposed techniques to a fully-interconnected Kuramoto network composed of 100 nonlinear oscillators. [ABSTRACT FROM AUTHOR]

Opacity is a confidentiality property that holds if certain secret behavior of a system, typically represented by a predicate, cannot be revealed under any system evolution. Among other proposed methodologies, when opacity is violated, it can be enforced using insertion mechanisms, i.e., by inserting symbols before an actual system output (in real time as the system evolves) in order to replace observation sequences that lead to opacity violations with observation sequences that can be generated by system behavior that does not violate opacity. This article focuses on opacity enforcement in discrete-event systems modeled with finite-state automata and proposes an extended insertion mechanism that can enforce opacity in a practical manner to a wide class of systems by inserting symbols before and after an actual system output. This article also introduces event insertion constraints that require only certain specific symbols to be inserted before and after an actual system output. For each case, we obtain a necessary and sufficient condition (based on the construction of an appropriate verifier) for opacity enforceability using the proposed extended insertion mechanism and devise a pertinent extended insertion strategy. [ABSTRACT FROM AUTHOR]

We propose algorithms for performing model checking and control synthesis for discrete-time uncertain systems under linear temporal logic (LTL) specifications. We construct temporal logic trees (TLTs) from LTL formulae via reachability analysis. In contrast to automaton-based methods, the construction of the TLT is abstraction-free for infinite systems; that is, we do not construct discrete abstractions of the infinite systems. Moreover, for a given transition system and an LTL formula, we prove that there exist both a universal TLT and an existential TLT via minimal and maximal reachability analysis, respectively. We show that the universal TLT is an underapproximation for the LTL formula and the existential TLT is an overapproximation. We provide sufficient conditions and necessary conditions to verify whether a transition system satisfies an LTL formula by using the TLT approximations. As a major contribution of this work, for a controlled transition system and an LTL formula, we prove that a controlled TLT can be constructed from the LTL formula via a control-dependent reachability analysis. Based on the controlled TLT, we design an online control synthesis algorithm, under which a set of feasible control inputs can be generated at each time step. We also prove that this algorithm is recursively feasible. We illustrate the proposed methods for both finite and infinite systems and highlight the generality and online scalability with two simulated examples. [ABSTRACT FROM AUTHOR]

The deployment of autonomous systems in uncertain and dynamic environments has raised fundamental questions. Addressing these is pivotal to build fully autonomous systems and requires a systematic integration of planning and control. We first propose reactive risk signal interval temporal logic (ReRiSITL) as an extension of signal temporal logic (STL) to formulate complex spatiotemporal specifications. Unlike STL, ReRiSITL allows to consider uncontrollable propositions that may model humans as well as random environmental events such as sensor failures. Additionally, ReRiSITL allows to incorporate risk measures, such as (but not limited to) the conditional value-at-risk, to measure the risk of violating certain spatial specifications. Second, we propose an algorithm to check if an ReRiSITL specification is satisfiable. For this purpose, we abstract the ReRiSITL specification into a timed signal transducer and devise a game-based approach. Third, we propose a reactive planning and control framework for dynamical control systems under ReRiSITL specifications. [ABSTRACT FROM AUTHOR]

This article studies the prognosis of failure, i.e., its prediction prior to its occurrence, in stochastic discrete event systems. Prior work has focused on the definition and offline verification of $m$ -steps stochastic-prognosability, or $S_m$ -prognosability, which allows the prediction of a fault at least $m$ -steps in advance. This article complements the existing work by proposing an algorithm for the computation of online failure prognoser. The proposed algorithm reduces the condition for issuing an affirmative prognostic decision to verification condition of a safety property of a Markov chain. We discuss how such a verification condition can be computed using a finitely terminating algorithm. [ABSTRACT FROM AUTHOR]

Reinforcement learning (RL) algorithms have been used to learn how to implement tasks in uncertain and partially unknown environments. In practice, environments are usually uncontrolled and may affect task performance in an adversarial way. In this article, we model the interaction between an RL agent and its potentially adversarial environment as a turn-based zero-sum stochastic game. The task requirements are represented both qualitatively as a subset of linear temporal logic (LTL) specifications, and quantitatively as a reward function. For each case in which the LTL specification is realizable and can be equivalently transformed into a deterministic Büchi automaton, we show that there always exists a memoryless almost-sure winning strategy that is $\varepsilon$ -optimal for the discounted-sum objective for any arbitrary positive $\varepsilon$. We propose a probably approximately correct (PAC) learning algorithm that learns such a strategy efficiently in an online manner with a priori unknown reward functions and unknown transition distributions. To the best of our knowledge, this is the first result on PAC learning in stochastic games with independent quantitative and qualitative objectives. [ABSTRACT FROM AUTHOR]

This article studies the state estimation for probabilistic Boolean networks via observing output sequences. Detectability describes the ability of an observer to uniquely estimate system states. By defining the probability of an observed output sequence, a new concept called detectability measure is proposed. The detectability measure is defined as the limit of the sum of probabilities of all detectable output sequences when the length of output sequences goes to infinity, and it can be regarded as a quantitative assessment of state estimation. A stochastic state estimator is designed by defining a corresponding nondeterministic stochastic finite automaton, which combines the information of state estimation and probability of output sequences. The proposed concept of detectability measure further performs the quantitative analysis on detectability. Furthermore, by defining a Markov chain, the calculation of detectability measure is converted to the calculation of the sum of probabilities of certain specific states in Markov chain. Finally, numerical examples are given to illustrate the obtained theoretical results. [ABSTRACT FROM AUTHOR]

We address, in this article, the problem of codiagnosability of networked discrete event systems with timing structure (NDESWTS) subject to delays and loss of observations of events between the measurement sites (MS) and local diagnosers (LD). To this end, we first introduce a new timed model that represents the dynamic behavior of the plant based on the, a priori, knowledge of the minimal activation time for each transition of the plant and on the maximal delays in the communication channels that connect MS and LD. We then convert this timed model into an equivalent untimed one, and add possible intermittent packet loss in the communication network. Based on this untimed model, we present necessary and sufficient conditions for NDESWTS codiagnosability and propose two tests for its verification: one that deploys diagnosers and another one that uses verifiers. [ABSTRACT FROM AUTHOR]

In this article, we are interested in the problem of synthesizing a partial observation supervisor for a discrete-event system such that it enforces a desired property. We introduce a compact and uniform approach to the problem of synthesizing state-based property-enforcing supervisors. A state-based property is a property that only depends on the current estimate of the past behavior of the system and does not depend on its future behavior. Previous work has introduced a uniform methodology to solve this problem through the construction of a finite structure called the all enforcement structure (AES), which captures a game between the supervisor and the environment. Although the AES is a powerful structure that includes all possible property-enforcing supervisors, its construction is computationally challenging since the number of states grows exponentially in the number of states and the number of events of the system. Our contribution is the definition of a compact AES that is equivalent to but computationally more efficient than the original AES. Specifically, the compact AES enjoys the same properties as the original AES with respect to synthesizing maximally permissive supervisors under the assumption of incomparable sets of controllable and observable events. We also provide experimental results to show the benefits of the compact AES over the original AES. [ABSTRACT FROM AUTHOR]

In this article, we study the security of control systems in the context of the supervisory control layer of stochastic discrete-event systems. Control systems heavily rely on correct communication between the plant and the controller. In this article, we consider that such communication is partially compromised by a malicious attacker. The attacker has the ability to modify a subset of the sensor readings and mislead the supervisor, with the goal of inducing the system into an unsafe state. We consider this problem from the attacker’s viewpoint and investigate the synthesis of an attack strategy for systems modeled as probabilistic automata. Specifically, we investigate the synthesis of attack functions constrained by multiple objectives. We proceed in two steps. First, we quantify each attack strategy based on the likelihood of successfully reaching an unsafe state. Based on this quantification, we study the problem of synthesizing attack functions with the maximum likelihood of successfully reaching an unsafe state. Second, we consider the problem of synthesizing attack functions that have the maximum likelihood of successfully reaching an unsafe state while minimizing a cost function, i.e., the synthesis of attack functions is constrained by multiple objectives. Our solution methodology is based on mapping these problems to optimal control problems for Markov decision processes, specifically, a probabilistic reachability problem and a stochastic shortest path problem. [ABSTRACT FROM AUTHOR]

A novel framework is introduced for the supervisory control (SC) of timed discrete event systems based on Time Petri nets. The method encompasses both logical (markings to reach or avoid) and temporal specifications (arrival and departure times in specific markings). It relies on the construction of a partial forward reachability graph of the modified state class graph type and the formulation of integer linear programming problems to establish suitable firing time intervals (FTIs) for the controllable transitions. For each enabled controllable transition, the SC algorithm provides the largest FTI that that the specifications are met, irrespectively of the firing times of the uncontrollable transitions. [ABSTRACT FROM AUTHOR]

In this article, we study a security problem of protecting secrets in discrete-event systems modeled by deterministic finite automata. In the system, some states are defined as secrets, each of which is associated with a security level. The problem is to design an event-protecting policy such that any event sequence from the initial state that reaches a secret state contains a number of protected events no less than the required level of security. To solve this secret securing problem, we first develop a layered structure called the security automaton. Then, we show that the problem is transformed to a supervisory control problem in the security automaton. We consider two criteria of optimality on protecting policies: 1) disruptiveness, i.e., protecting policies with a minimum degree of disturbance to legal users’ normal operations; and 2) cost, i.e., protecting policies with a minimal cost. For the optimality on disruptiveness, we prove that a minimally disruptive protecting policy is obtained by using the classical supervisory control theory in the security automaton. For the optimality on cost, we develop a method to obtain a protecting policy with minimal cost by finding a min-cut in the security automaton. [ABSTRACT FROM AUTHOR]

Various nonclassical approaches of distributed information processing, such as neural networks, reservoir computing (RC), vector symbolic architectures (VSAs), and others, employ the principle of collective-state computing. In this type of computing, the variables relevant in computation are superimposed into a single high-dimensional state vector, the collective state. The variable encoding uses a fixed set of random patterns, which has to be stored and kept available during the computation. In this article, we show that an elementary cellular automaton with rule 90 (CA90) enables the space–time tradeoff for collective-state computing models that use random dense binary representations, i.e., memory requirements can be traded off with computation running CA90. We investigate the randomization behavior of CA90, in particular, the relation between the length of the randomization period and the size of the grid, and how CA90 preserves similarity in the presence of the initialization noise. Based on these analyses, we discuss how to optimize a collective-state computing model, in which CA90 expands representations on the fly from short seed patterns—rather than storing the full set of random patterns. The CA90 expansion is applied and tested in concrete scenarios using RC and VSAs. Our experimental results show that collective-state computing with CA90 expansion performs similarly compared to traditional collective-state models, in which random patterns are generated initially by a pseudorandom number generator and then stored in a large memory. [ABSTRACT FROM AUTHOR]

In this paper, we study the problem of simultaneous public event information release and private event information hiding in discrete event systems modeled by partially observed non-deterministic finite automata, where the public and private event information is respectively defined as unobservable fault and secret events. The notion of D-C-compossibility is introduced to characterize whether a system simultaneously conceals the occurrences of secret events while releasing the occurrences of fault events. When such a property does not hold, we investigate its enforcement through a defensive function. This function takes each observable event of a system as input and generates a suitably modified event sequence at the system's output using event deletion, insertion, or substitution. Specifically, our focus is on prioritizing the concealment of the secret events while maximizing the detection of the fault events through the use of defensive functions. The notion of D-C-enforceability that refers to the capability of a defensive function to employ a strategy for manipulating observations of a system to enforce D - C -compossibility is proposed. That is, a D - C -enforcing defensive function ensures that all occurrences of fault events can be revealed while concealing all occurrences of secret events. A D - C -diagnoser construction is proposed to enumerate all feasible defensive actions following system behavior. By taking advantage of the D - C -diagnoser, we obtain a necessary and sufficient condition for D - C -enforceability, along with a corresponding obfuscation strategy for defensive functions. [ABSTRACT FROM AUTHOR]

This article investigates quantitative supervisory control with local mean payoff objectives on discrete event systems modeled as weighted automata. Weight flows are generated as new events occur, which are required to satisfy some quantitative conditions. We focus on mean weights (payoffs) over a finite number of events, which serve as a measure for the stability or robustness of weight flows. The range of events to evaluate the mean payoff is termed a window, which slides as new events occur. Qualitative requirements such as safety and liveness are also necessary along with quantitative requirements. Supervisory control is employed to manipulate the operation of the system so that the requirements are satisfied. We consider two different scenarios based on whether the window size is fixed or not. Correspondingly, we formulate two supervisory control problems, both of which are solved sequentially by first tackling the qualitative issues and then the quantitative ones. The automaton model is then transformed to a two-player game between the supervisor and the environment, where safety and liveness are enforced. Based on the intermediate results, several quantitative objectives are defined to formulate two games, which correspond to the two proposed supervisory control problems. Finally, we synthesize provably correct supervisors by solving the games and completely resolve both problems. [ABSTRACT FROM AUTHOR]

In this article, we deal with state estimation of timed discrete event systems that are modeled by max-plus automata (MPAs), where only some events are observable. For a given MPA, a formal procedure is first proposed for constructing its observer by extending our previous concept of observer for unambiguous MPAs to polynomially ambiguous MPAs. As an application, we present a necessary and sufficient condition based on the constructed observer to check the critical observability of MPAs. The state set of an MPA is divided into two disjoint subsets, i.e., the set of critical states and the set of noncritical states. A system is critically observable if the set of all states that are consistent with any observation is either a subset of the critical states set or a subset of the noncritical states set. [ABSTRACT FROM AUTHOR]

This article addresses the robust control problem of discrete event systems assuming that replacement attacks may occur, thus making it appear that an event that has occurred looks like another event. In particular, we assume that this is done by tampering with the sensor-readings in the sensor communication channel. Specifically, we use Petri nets as the reference formalism to model the plant and assume a control specification in terms of a generalized mutual exclusion constraint. We propose three different methods to derive a control policy that is robust to the possible replacement attacks. The first two methods lead to an optimal (i.e., maximally permissive) policy but are computationally inefficient when applied to large-size systems. On the contrary, the third method computes a policy more efficiently and reveals more easily implementable in practice. However, this is done at the expense of optimality. [ABSTRACT FROM AUTHOR]

A key challenge in the synthesis and subsequent analysis of supervisory controllers is the impact of state-space explosion caused by concurrency. The main bottleneck is often the memory needed to store the composition of plant and requirement automata and the resulting supervisor. Partial-order reduction (POR) is a well-established technique that alleviates this issue in the field of model checking. It does so by exploiting redundancy in the model with respect to the properties of interest. For controller synthesis, the functional properties of interest are nonblockingness, controllability, and least-restrictiveness, but also performance properties, such as throughput and latency are of interest. We propose an on-the-fly POR on the input model that preserves both functional and performance properties in the synthesized supervisory controller. This improves the scalability of the synthesis (and any subsequent performance analysis). Synthesis experiments show the effectiveness of the POR on a set of realistic manufacturing system models. [ABSTRACT FROM AUTHOR]

Many safety-critical systems, such as autonomous vehicles and service robots, must achieve high-level task specifications with performance guarantees. Much recent progress toward this goal has been made through an automatic controller synthesis from temporal logic specifications. Existing approaches, however, have been limited to relatively short and simple specifications. Furthermore, existing methods either consider some prior discretization of the state space, deal only with a convex fragment of temporal logic, or are not provably complete. We propose a scalable, provably complete algorithm that synthesizes continuous trajectories to satisfy nonconvex temporal logic over reals (RTL) specifications. We separate discrete task planning and continuous motion planning on-the-fly and harness highly efficient Boolean satisfiability and linear programming solvers to find dynamically feasible trajectories that satisfy nonconvex RTL specifications for high-dimensional systems. The proposed design algorithms are proven sound and complete, and simulation results demonstrate our approach's scalability. [ABSTRACT FROM AUTHOR]

This article develops a novel design principle for the observer of timed discrete event systems behaving under specific time semantics. Observers devoted to discrete event systems usually ignore the timing aspects of underlying systems but this can have implications to many applications, in particular, for refinement of estimation and inference tasks. The techniques of this article use the time stamps of observations to refine the state estimation process for a class of labeled and timed automata where events occur based on constant time values. The resulting timed observer is beneficial for refining privacy and security issues. Current-state opacity is discussed as a promising application of the timed observer. [ABSTRACT FROM AUTHOR]

In industry, the performance has to be optimized to allow its competitiveness. The goal then is to use the resources at their maximal capacity, reduce the production time, and be flexible to adapt to the customers requests. The closed-loop behavior of a system under the supervisory control theory (SCT) guarantees nonblockingness and safety requirements and, thus, it can be used as the search universe for a planning problem. SCT suffers with the “curse of dimensionality” when systems become bigger and more complex. This article presents a set of sufficient conditions that allow to work with abstractions of the closed-loop behavior (supremal controllable sublanguage), instead of the closed-loop behavior itself, as the search universe to solve a planning problem. Such abstraction is the natural projection of the supervisor into the set of controllable events satisfying the observer property. This process leads to a reduction of the search space. [ABSTRACT FROM AUTHOR]

This article proposes a formal framework based on discrete event systems in order to analyze the democratic progress and regression in a society controlled by networked agents. For this purpose, we construct a simple model using a finite state automaton that describes the dynamic behavior of progress and regression in a democracy. We represent a network of agents as a directed graph where each agent has its own objective. Each agent may be a citizen or a group of people sharing a common objective, and it makes decisions on enabling or disabling events upon the observation of states of a system. Agents may have different decisions on the same event, and the final decision follows the majority rule. Upon this framework, we derive the necessary and sufficient conditions for a democratic system controlled by networked agents to be progressive or regressive, where a progressive one implies that it reaches a more equal state at which a larger number of agents meet their objectives. Finally, we obtain some convergence results for special graph topologies. [ABSTRACT FROM AUTHOR]

We consider the problem of synthesizing controllers for real-time systems where some timing features are not known with precision. We model the plant as a parametric timed automaton (PTA), i.e., a finite automaton equipped with real-valued clocks constraining its behavior, in which the timing constraints on these clocks can make use of parameters. The most general problem we study then consists in synthesizing both a controller and values for the parameters such that some control location of the automaton is reachable. It is, however, well-known that most nontrivial problems on parametric timed automata are undecidable and the classical techniques for the verification (and a fortiori for the control) of timed systems do not terminate in that setting. We, therefore, provide a restriction on the use of parameters to ensure the decidability of the control problems. Since in classical timed automata, real-valued clocks are always compared to integers for all practical purposes, we search for parameter values as bounded integers. Hence, we solve undecidability and termination issues, we provide terminating symbolic synthesis procedures, and our method retains most of the practical usefulness of PTA for the modeling of real-time systems. [ABSTRACT FROM AUTHOR]

In this article, we consider a finite-elementapproximation of the Bellman equation for the optimal control of switched systems. We show that the problem belongs to a special class that we studied in a previous work, for which we developed an efficient solution algorithm. As an application, we present the problem of generating parking maneuvers for self-driving vehicles on two typical urban parking scenarios. The vehicle is described by four different switched systems in which every switching is associated to a penalization term. In this way, we obtain parking paths that have a small number of direction changes and have a simple structure. [ABSTRACT FROM AUTHOR]

On the emerging development of SiC MOSFET, the switching frequency of power converters has been pushed to the order of hundreds of kilohertz or even megahertz to improve power density. However, the state-of-the-art simulations for such high-frequency power electronics circuits are usually time-consuming, blocking the studies of long dynamics such as several seconds. What’s worse, adopting physical models to simulate the turn-on and turn-off transients leads to high stiffness and therefore convergence problems. In this paper, an event-driven approach is proposed to improve the solving speed and simulation stability of SiC based high-frequency converters. A time-scale hierarchical automaton is proposed to model the system, where piecewise analytical transient model for SiC MOSFET is established as the second layer in the automaton to simulate the switching transients with improved numerical stability. Simulation of the system is driven by discrete events in the automaton. A 3.3 kW 79.1 kHz wireless power transfer system for the wireless charging of electric vehicle is studied. Compared with ideal switch model in Simulink and physical switch model in LTspice, 60-fold and 400-fold increases in terms of simulation speed with same level of accuracy are achieved respectively. The simulated results are also attested to by experimental verifications. [ABSTRACT FROM AUTHOR]

This article investigates the enforcement of generalized mutual exclusion constraints (GMECs) and deadlock-freeness on a time Petri net (TPN) system with uncontrollable transitions, motivated by the fact that the existing methods enforcing GMECs may degrade the performance of a closed-loop system and lead to deadlock states. A supervisor enforcing a set of GMECs and deadlock-freeness on an underlying untimed Petri net system is assumed to be available. By exploiting timing information and mathematical programming, a control function is designed to restrict the firing intervals of transitions such that a TPN system can avoid entering forbidden states. The key idea behind the proposed approach is the online computation of a graph, called reduced modified state class graph (RMSCG), that is an extension of the partial modified state class graph recently introduced by the authors. Based on the RMSCG, an online control synthesis procedure is developed, which can enforce the originally given GMECs and deadlock-freeness in a maximally permissive way. [ABSTRACT FROM AUTHOR]

We consider feedback control systems where sensor readings may be compromised by a malicious attacker intending on causing damage to the system. We study this problem at the supervisory layer of the control system, using discrete event systems techniques. We assume that the attacker can edit the outputs from the sensors of the system before they reach the supervisory controller. In this context, we formulate the problem of synthesizing a supervisor that is robust against the class of edit attacks on the sensor readings and present a solution methodology for this problem. This methodology blends techniques from games on automata with imperfect information with results from supervisory control theory of partially observed discrete event systems. Necessary and sufficient conditions are provided for the investigated problem. [ABSTRACT FROM AUTHOR]

We investigate the enforcement of opacity, an information-flow privacy property, using insertion sequences that modify the output of the system by event insertions. Previous work considered the problem of enforcing the opacity under the assumption that the insertion functions were based on the observed system strings. Now, we investigate the more powerful method of insertion sequences based on the exact system states and events. In this case, the insertion function would be embedded into the system itself, rather than being an output interface. In this article, we develop methods that verify if a valid insertion function exists in this setting; if one exists, synthesize one using a computationally effective algorithm; and investigate a special case where it is possible to verify and synthesize a valid embedded insertion function with polynomial complexity in the size of the system. [ABSTRACT FROM AUTHOR]

This article studies the constrained switching (linear) system which is a discrete-time switched linear system whose switching sequences are constrained by a deterministic finite automaton. The stability of a constrained switching system is characterized by its constrained joint spectral radius that is known to be difficult to compute or approximate. Using the semitensor product of matrices, the matrix-form expression of a constrained switching system is shown to be equivalent to that of a lifted arbitrary switching system. Then, the constrained joint/generalized spectral radius of a constrained switching system is proven to be equal to the joint/generalized spectral radius of its lifted arbitrary switching system which can be approximated by off-the-shelf algorithms. [ABSTRACT FROM AUTHOR]

In this article, we investigate controllability of hybrid systems. We use hybrid machines to model such hybrid systems. The model consists of an automaton and a linear time-invariant system. The control goal is to drive the continuous state from any initial state to any final state. To achieve this goal, controls at both the discrete-event level and the continuous-variable level are used. Control at the discrete-event level can force some forcible events, and disable some controllable events. For the case that all events are controllable and forcible, and the graph of the automaton is strongly connected, a necessary and sufficient condition for controllability is obtained, using some existing results on controllability of switched linear systems. For three other cases, sufficient conditions are derived. If a hybrid system is not controllable, we design a supervisor to control the discrete-event part to ensure that the system becomes controllable after some finite transitions if possible. We find a necessary and sufficient condition for such a discrete-event control to exist. [ABSTRACT FROM AUTHOR]

This article addresses the problem of verifying discrete-time stochastic systems against omega-regular specifications using finite-state abstractions. Omega-regular properties allow specifying complex behavior and encompass, for example, linear temporal logic. We focus on a class of systems with mixed monotone dynamics. This class is shown to be amenable to efficient reachable set computation and models a wide range of physically relevant systems. In general, finite-state abstractions of continuous state stochastic systems give rise to augmented Markov chains wherein the probabilities of transition between states are restricted to an interval. We present a procedure to compute a finite-state interval-valued Markov chain (IMC) abstraction of discrete-time, mixed monotone stochastic systems subject to affine disturbances given a rectangular partition of the state space. Then, we suggest an algorithm for performing verification against omega-regular properties in IMCs. Specifically, we aim to compute bounds on the probability of satisfying a specification from any initial state in the IMC. This is achieved by solving a reachability problem on the sets of so-called winning and losing components in the Cartesian product between the IMC and a Rabin automaton representing the specification. Next, the verification of IMCs may yield a set of states whose acceptance status is undecided with respect to the specification, requiring a refinement of the abstraction. We describe a specification-guided approach that compares the best and worst case behaviors of accepting paths in the IMC and targets the appropriate states accordingly. Finally, we show a case study. [ABSTRACT FROM AUTHOR]

In this article, we consider the problem of synthesizing a nondeterministic supervisor for the plant and the specification modeled as nondeterministic automata. A similarity control problem requires us to synthesize a supervisor such that the supervised plant is simulated by the specification. Ideally, the synthesized supervisor should be as permissive as possible. We develop a method for synthesizing a maximally permissive supervisor that solves the similarity control problem. [ABSTRACT FROM AUTHOR]

This article focuses on synthesizing control policies for discrete-time stochastic control systems together with a lower bound on the probability that the systems satisfy the complex temporal properties. The desired properties of the system are expressed as linear temporal logic specifications over finite traces. In particular, our approach decomposes the given specification into simpler reachability tasks based on its automata representation. We, then, propose the use of so-called control barrier certificate to solve those simpler reachability tasks along with computing the corresponding controllers and probability bounds. Finally, we combine those controllers to obtain a hybrid control policy solving the considered problem. Under some assumptions, we also provide two systematic approaches for uncountable and finite input sets to search for control barrier certificates. We demonstrate the effectiveness of the proposed approach on a room temperature control and lane keeping of a vehicle modeled as a four-dimensional single-track kinematic model. We compare our results with the discretization-based methods in the literature. [ABSTRACT FROM AUTHOR]

In this article, we study the supervisory control problem of networked discrete event systems with timing structure assuming bounded communication delays and intermittent loss of observations. The communication between the plant and the supervisor is through a network that can have several channels, and so communication delays may change the order of event observations by the supervisor. We assume a priori knowledge of the minimal activation time of the plant transitions and the maximum communication delays, and propose an equivalent untimed model that takes into account all possible observation delays and also loss of observations. Based on this model, we formulate a networked supervisory control problem and show that it can be converted into an equivalent range control problem. We also address implementation, and, to this end, we present a representation for networked supervisors that is able to deal with possible loss of synchronization between event occurrence and its observation. [ABSTRACT FROM AUTHOR]

This article investigates the lossless event compression problem of discrete event systems which is, given a discrete event system and a source string generated by it, to find a minimal recoverable compressed string by removing as many events as possible. In order for the problem to be well post, two compression protocols are introduced. One requires that the last event is always kept. The other requires that, for any loop substring, at least one event is kept. We say a compressed string is recoverable if we can uniquely determine the source string based on the knowledge of the given discrete event system. We first construct an automaton to present all the possible source strings for a given compressed string. Based on the automaton, an algorithm is proposed to check whether the given compressed string is recoverable or not. We then propose an algorithm to calculate a minimal recoverable compressed string for a source string. The compressed string satisfies monotonicity which can significantly reduce the computational complexity of the algorithm. Finally, we use a practical example to illustrate these results. [ABSTRACT FROM AUTHOR]

In this article, we deal with the detectability problem for unambiguous weighted automata (UWAs). The problem is to determine if, after a finite number of observations, the set of possible states is reduced to a singleton. Four types of detectabilities, namely, strong detectability, detectability, strong periodic detectability, and periodic detectability are defined in terms of different requirements for current state estimation. We first construct a deterministic finite state automaton (called observer) over a weighted alphabet and prove that it can be used as the current-state estimator of the studied UWA. Finally, necessary and sufficient conditions based on the observer are proposed to verify detectabilities of a UWA. [ABSTRACT FROM AUTHOR]

The hybrid minimum principle is presented for the optimal control of deterministic hybrid systems with both autonomous and controlled switchings and jumps where state jumps at the switching instants are permitted to be accompanied by changes in the dimension of the state space. A feature of particular importance is the explicit presentation of the boundary conditions on the Hamiltonians and the adjoint processes before and after switchings and jumps. The numerical benefit of these expressions are demonstrated on a modified version of the multiple autonomous switchings algorithm. The results are illustrated for the hybrid model of an electric vehicle powertrain with a two-speed transmission. [ABSTRACT FROM AUTHOR]

In this article, we present a novel control approach for formally solving reach-avoid problems for constrained and disturbed nonlinear systems by optimizing over reachable sets. Reach-avoid problems arise in many modern control applications of safety-critical systems, such as autonomous driving and human-robot collaboration. They require us to control all states from a set of initial states in finite time into a final set while guaranteeing the satisfaction of state and input constraints despite the presence of disturbances and uncertain measurements. We optimize over reachable sets, thereby, simultaneously improving the control performance and guaranteeing constraint satisfaction for all solutions. Moreover, our new approach involves a novel combination of state-dependent feedforward and feedback control, which leads to better control performance compared to the existing approaches as demonstrated in several numerical examples. Our algorithm is particularly suited for computing motion primitives used in maneuver automata, which realizes fast and efficient online planning. The online applicability is supported by the simple structure of the resulting controller, which is a time-varying linear tracking controller. [ABSTRACT FROM AUTHOR]

Temporal logic provides a rigorous and expressive way to model specifications for cyber-physical systems (CPS). Such systems, which are playing increasingly important roles in various domains, are also subject to malicious attacks initiated by intelligent adversaries. Malicious attacks may prevent the system from satisfying the desired specification. In this article, we introduce a control synthesis method to minimize deviations from the desired specification due to adversaries. We consider the scenario where the adversary has limited capability of observing the controller's strategy. We synthesize a minimum violation control strategy for a finite-state stochastic game under cosafe linear temporal logic constraints. We formulate a mixed-integer nonlinear program for computing the optimal controller strategy and present two algorithms. First, we propose an exact algorithm that computes the optimal control strategy with probability one but without guarantees on the convergence rate. Second, we present an approximate algorithm that computes a suboptimal control strategy. The approximate algorithm converges faster compared to the exact algorithm; however, it only returns an optimal solution when the adversary has full observation over the controller's strategy. A numerical case study is presented to evaluate the proposed framework. [ABSTRACT FROM AUTHOR]

In this article, we formulate the problem of satisfying a linear temporal logic formula on a linear plant with output feedback, through a recent hybrid systems formalism. We relate this problem to the notion of recurrence introduced for the considered formalism, and we then extend Lyapunov-like conditions for recurrence of an open, unbounded set. One of the proposed relaxed conditions allows certifying recurrence of a suitable set, and this guarantees that the high-level evolution of the plant satisfies the formula, without relying on discretizations of the plant. Simulations illustrate the proposed approach. [ABSTRACT FROM AUTHOR]

• We give the necessary and sufficient conditions of three opacities for networked discrete event systems. • We present verification algorithms of four kinds of opacity for networked discrete event systems. • We define new notions to extend the notions of opacity in classical discrete systems. Opacity is an important information-flow property, which is used to characterize whether or not the secrets of system have been leaked to the intruders. Over the past ten years, opacity of discrete event systems (DESs) modeled as automata and Petri nets have been well investigated under the assumption that the communication channels between systems and intruders are perfect. However, in networked discrete event systems (NDESs), the DESs run in a shared network, and the communication delays and losses are inevitable usually. In this paper, we investigate the problems of opacity in the framework of NDESs. We formulate four kinds of opacity for NDESs, including current-state opacity, initial-state opacity, initial-final-state opacity, and K -step opacity. We also present the verification algorithms for these notions. We extend the notions of opacity in classical DESs, that is, if the communication delays and losses disappear, then these new notions would reduce to their classical counterparts. A number of examples are provided to illustrate the results obtained. [ABSTRACT FROM AUTHOR]

As an important hardware security primitive, the true random number generator (TRNG) has been widely utilized in many critical applications. The performance and security of TRNGs are always dominant features that determine the usability of a TRNG scheme. In this article, we propose a novel TRNG design method based on a self-timed ring structure. Different from most existing self-timed circuit-based TRNGs that use ring oscillators, the basic circuit component of the proposed TRNG is a digital realization of a chaotic cellular automata topology. We utilize three different methods to validate the proposed TRNG method, including HSpice simulation, FPGA prototype, and ASIC test chips. As the proposed TRNG structure is pure digital, thus it is synthesizable with standard all-digital components. The test chips of the proposed TRNG structure are fabricated with 40nm TSMC technology node, with a hardware footprint equals to 75 NAND gates and a die area of $270\mu m^{2}$. With a PCIe setup connecting the testchip and computer, the TRNGs achieves high throughput as 1600Mb/s. The FPGA implementation is built on a Virtex-6 family FPGA from Xilinx, which also achieves lightweight overhead: 53 look-up-table (LUT) and 22 D Flip-flops (DFF). The collected random numbers from FPGA implementations and ASIC testchips are comprehensively tested with three test suites, including NIST SP800–22, NIST SP800–90B, and AIS-31 with a high pass-rate. Further, the security of the TRNG testchips and FPGA implementations are validated by applying three different attacks, including frequency injection attacks, power attacks, and thermal attacks. The experimental results demonstrate that the proposed TRNG structure is immune to these attacks with trivial entropy loss [ABSTRACT FROM AUTHOR]

In this article, we investigate the synthesis of a (possibly nondeterministic) supervisor, with partial information, such that the controlled nondeterministic plant is bisimulation equivalent to a nondeterministic specification. We derive a new necessary and sufficient condition for the existence of a supervisor and provide an algorithm for the supervisor construction when one exists. The algorithm is exponential in the size of the plant and specification, a substantial improvement over the double exponential cost from exhaustive search. We show that the cases of complete information and deterministic control are special cases of the presented theory. [ABSTRACT FROM AUTHOR]

In this article, we present an active diagnosis method to enhance diagnosability of a plant modeled by a finite-state automaton. Some properties of active diagnosis and silent blocking are studied. To avoid silent blocking, the notion of stop-free event set is proposed, and a stop-free control policy that does not introduce silent blocking is formulated. We develop a heuristic method based on the verifier of the plant to compute a feasible stop-free event set that guarantees the existence of a valid control policy. With the stop-free event set, the set of disabled edges is computed, and an online control policy that is based on the current diagnostic state is computed, which guarantees that the closed-loop system is diagnosable. The structural complexity of the proposed control structure is polynomial with respect to the number of states of the plant. [ABSTRACT FROM AUTHOR]

Controller design for continuous systems with linear temporal logic (LTL) specifications is a computationally intensive task. Abstracting a discrete transition system from a real-world continuous-state system often results in a state machine with a large number of states and nondeterministic transitions. This makes controller synthesis for LTL specifications difficult specially when the design specification is lengthy. To reduce the complexity, we consider the specifications that are in the conjunctive form of practical LTL patterns. We use auditor product to incrementally restrict the system to satisfy the safety part of each subspecification. The control strategy, that satisfies the liveness part is then calculated by solving a generalized Buchi game on the result of the auditor product of the discrete transition system with all subspecifications. This approach has the same worst case computational complexity as GR(1) synthesis, but avoids some of the fundamental limitations involved with Assumption → Guarantee formulation of the problem. [ABSTRACT FROM AUTHOR]

In order to control a discrete-event system (DES), the supervisory controller observes event sequences. Observability, together with controllability, is required for obtaining the exact specification language via supervisory control. By extending observability, relative observability was recently investigated. In this article, relative network observability, which accommodates observation incompleteness and delay in relative observability, is defined. An algorithm is proposed to transform relative network observability to network observability. This leverages existing solutions to problems concerning network observability to solve problems concerning relative network observability. In particular, we propose techniques for checking relative network observability and calculating supremal controllable and relatively network observable sublanguage. [ABSTRACT FROM AUTHOR]

We show how reactive synthesis and automated planning can be leveraged effectively to find nonmaximal solutions to deterministic supervisory control problems of discrete event systems. To do so, we propose efficient translations of the supervisory control problem into the reactive synthesis and planning frameworks. Notably, our translation methods capture the compositional and reactive nature of control specifications, avoiding a potential exponential explosion found in alternative translation approaches. Additionally, we report on experimental results comparing the efficacy of different tools from the three disciplines, for a particular supervisory control benchmark. [ABSTRACT FROM AUTHOR]