Liyong Lin

Yuting Zhu, Liyong Lin, Rong Su

In this paper, we propose and address the problem of supervisor obfuscation against actuator enablement attack, in a common setting where the actuator attacker can eavesdrop the control commands issued by the supervisor. We propose a method to obfuscate an (insecure) supervisor to make it resilient against actuator enablement attack in such a way that the behavior of the original closed-loop system is preserved. An additional feature of the obfuscated supervisor, if it exists, is that it has exactly the minimum number of states among the set of all the resilient and behavior-preserving supervisors. Our approach involves a simple combination of two basic ideas: 1) a formulation of the problem of computing behavior-preserving supervisors as the problem of computing separating finite state automata under controllability and observability constraints, which can be efficiently tackled by using modern SAT solvers, and 2) the use of a recently proposed technique for the verification of attackability in our setting, with a normality assumption imposed on both the actuator attackers and supervisors.

Liyong Lin, Rong Su

In this paper, we investigate the problem of synthesizing resilient supervisors against combined actuator and sensor attacks, for the subclass of cyber-physical systems that can be modelled as discrete-event systems. We assume that the attackers can carry out actuator enablement and disablement attacks as well as sensor replacement attacks. We consider both risky attackers and covert attackers in the setup where the (partial-observation) attackers may or may not eavesdrop the control commands (issued by the supervisor). A constraint-based approach for the bounded synthesis of resilient supervisors is developed, by reducing the problem to the Quantified Boolean Formulas (QBF) problem. The bounded synthesis problem can then be solved either with a QBF solver or with repeated calls to a propositional satisfiability (SAT) solver, by employing maximally permissive attackers, which can be synthesized with the existing partial-observation supervisor synthesis procedures, as counter examples in the counter example guided inductive synthesis loop.

Liyong Lin, Tomáš Masopust, W. Murray Wonham et al.

A reduction of a source distribution is a collection of smaller sized distributions that are collectively equivalent to the source distribution with respect to the property of decomposability. That is, an arbitrary language is decomposable with respect to the source distribution if and only if it is decomposable with respect to each smaller sized distribution (in the reduction). The notion of reduction of distributions has previously been proposed to improve the complexity of decomposability verification. In this work, we address the problem of generating (optimal) reductions of distributions automatically. A (partial) solution to this problem is provided, which consists of 1) an incremental algorithm for the production of candidate reductions and 2) a reduction validation procedure. In the incremental production stage, backtracking is applied whenever a candidate reduction that cannot be validated is produced. A strengthened substitution-based proof technique is used for reduction validation, while a fixed template of candidate counter examples is used for reduction refutation; put together, they constitute our (partial) solution to the reduction verification problem. In addition, we show that a recursive approach for the generation of (small) reductions is easily supported.

Liyong Lin, Sander Thuijsman, Yuting Zhu et al.

In this work, we propose and develop a new discrete-event based actuator attack model on the closed-loop system formed by the plant and the supervisor. We assume the actuator attacker partially observes the execution of the closed-loop system and eavesdrops the control commands issued by the supervisor. The attacker can modify each control command on a specified subset of attackable events. The attack principle of the actuator attacker is to remain covert until it can establish a successful attack and lead the attacked closed-loop system into generating certain damaging strings. We present a characterization for the existence of a successful attacker, via a new notion of attackability, and prove the existence of the supremal successful actuator attacker, when both the supervisor and the attacker are normal (that is, unobservable events to the supervisor cannot be disabled by the supervisor and unobservable events to the attacker cannot be attacked by the attacker). Finally, we present an algorithm to synthesize the supremal successful attackers that are represented by Moore automata.

Liyong Lin, Yuting Zhu, Rong Su

In this paper, we shall formulate and address a problem of covert actuator attacker synthesis for cyber-physical systems that are modelled by discrete-event systems. We assume the actuator attacker partially observes the execution of the closed-loop system and is able to modify each control command issued by the supervisor on a specified attackable subset of controllable events. We provide straightforward but in general exponential-time reductions, due to the use of subset construction procedure, from the covert actuator attacker synthesis problems to the Ramadge-Wonham supervisor synthesis problems. It then follows that it is possible to use the many techniques and tools already developed for solving the supervisor synthesis problem to solve the covert actuator attacker synthesis problem for free. In particular, we show that, if the attacker cannot attack unobservable events to the supervisor, then the reductions can be carried out in polynomial time. We also provide a brief discussion on some other conditions under which the exponential blowup in state size can be avoided. Finally, we show how the reduction based synthesis procedure can be extended for the synthesis of successful covert actuator attackers that also eavesdrop the control commands issued by the supervisor.

Ahmad Reza Shehabinia, Liyong Lin, Rong Su

In this paper, we model an operational planning and scheduling problem under multiple job deadlines in a time-weighted automaton framework. We first present a method to determine whether all given job specifications and deadlines can be met by computing a supremal controllable job satisfaction sublanguage. When this supremal sublanguage is not empty, we compute one of its controllable sublanguages that ensures the minimum total job earliness by adding proper delays. When this supremal sublanguage is empty, we will determine the minimal sets of job deadlines that need to be relaxed.

Lele Li, Liyong Lin

Highly automated assembly lines enable significant productivity gains in the manufacturing industry, particularly in mass production condition. Nonetheless, challenges persist in job scheduling for make-to-job and mass customization, necessitating further investigation to improve efficiency, reduce tardiness, promote safety and reliability. In this contribution, an advantage actor-critic based reinforcement learning method is proposed to address scheduling problems of distributed flexible assembly lines in a real-time manner. To enhance the performance, a more condensed environment representation approach is proposed, which is designed to work with the masks made by priority dispatching rules to generate fixed and advantageous action space. Moreover, a Monte-Carlo tree search based soft shielding component is developed to help address long-sequence dependent unsafe behaviors and monitor the risk of overdue scheduling. Finally, the proposed algorithm and its soft shielding component are validated in performance evaluation.