On-Line Synthesis of Permissive Supervisors for Partially Observed Discrete Event Systems under scLTL Constraints

带事件强制的监督控制理论

Supervisory Control Theory with Event Forcing

针对传统Ramadge-Wonham监督控制理论交互机制单一的问题，本文引入可强制事件以抢占不可控事件，定义可强制可控性概念，证明最大允许非阻塞监督器的存在性并给出计算算法，通过案例验证了方法有效性。

确定性规范的双模拟强制监督控制

Bisimilarity Enforcing Supervisory Control for Deterministic Specifications

本文研究非确定性离散事件系统的监督控制，通过引入基于同步模拟的可控性概念，提出存在双模拟强制监督器的充要条件及多项式验证算法，并给出规范不满足时的最大许可子规范合成方法。

Bounded Synthesis and Reinforcement Learning of Supervisors for Stochastic Discrete Event Systems with LTL Specifications

In this paper, we consider supervisory control of stochastic discrete event systems (SDESs) under linear temporal logic specifications. Applying the bounded synthesis, we reduce the supervisor synthesis into a problem of satisfying a safety condition. First, we consider a synthesis problem of a directed controller using the safety condition. We assign a negative reward to the unsafe states and introduce an expected return with a state-dependent discount factor. We compute a winning region and a directed controller with the maximum satisfaction probability using a dynamic programming method, wh…

Supervisory Control of Multi-Agent Discrete-Event Systems with Partial Observation

In this paper we investigate multi-agent discrete-event systems with partial observation. The agents can be divided into several groups in each of which the agents have similar (isomorphic) state transition structures, and thus can be relabeled into the same template. Based on the template a scalable supervisor whose state size and computational cost are independent of the number of agents is designed for the case of partial observation. The scalable supervisor under partial observation does not need to be recomputed regardless of how many agents are added to or removed from the system. We gen…

Supervisory Control Synthesis of Timed Automata Using Forcible Events

Considering real-valued clocks in timed automata (TA) makes it a practical modeling framework for discrete-event systems. However, the infinite state space brings challenges to the control of TA. To synthesize a supervisor for TA using the conventional supervisory control theory, existing methods abstract TA to finite automata (FA). For many applications, the abstraction of real-time values results in an explosion in the state space of FA. This paper presents a supervisory control synthesis algorithm directly applicable to the TA without any abstraction. The plant is given as a TA with a set o…

编排与编排合成的桥梁：弥合监督控制与服务协调之间的鸿沟

Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services

本文通过修改监督控制理论中的合成算法，引入新颖可控性概念，提出抽象参数化合成算法，统一了经典合成与编排、编排合成，并证明其细化关系，以服务领域示例验证。

Networked Supervisory Control Synthesis of Timed Discrete-Event Systems

Conventional supervisory control theory assumes full synchronization between the supervisor and the plant. This assumption is violated in a networked-based communication setting due to the presence of delays, and this may result in incorrect behavior of a supervisor obtained from conventional supervisory control theory. This paper presents a technique to synthesize a networked supervisor handling communication delays. For this purpose, first, a networked supervisory control framework is provided, where the supervisor interacts with the plant through control and observation channels, both of wh…

基于状态树结构的离散事件系统监督器定位

Supervisor Localization of Discrete-Event Systems based on State Tree Structures

本文在状态树结构框架下提出监督器定位理论，引入局部状态跟踪器、局部控制函数等概念，提出更高效的定位算法，并在半导体制造系统模型中验证了方法的有效性。

受限的鲁棒监督器合成

Bounded Synthesis of Resilient Supervisors

本文研究了针对联合执行器和传感器攻击的鲁棒监督器合成问题，针对可以建模为离散事件系统的一类网络物理系统。我们假设攻击者可以执行执行器启用和禁用攻击以及传感器替换攻击。在考虑风险攻击者和隐蔽攻击者的情况下，攻击者可能或可能不窃听监督器发出的控制命令。通过将问题转化为量化布尔公式（QBF）问题，开发了一种基于约束的受限鲁棒监督器合成方法，可以使用QBF求解器或通过多次调用命题满足（SAT）求解器来解决受限合成问题，利用最大宽容攻击者，这些攻击者可以通过现有的部分观察监督器合成过程生成，作为反例引导归纳合成循环中的反例。

时间离散事件系统的有界时间非阻塞监控控制

Bounded-Time Nonblocking Supervisory Control of Timed Discrete-Event Systems

本文将定量非阻塞性扩展至时间离散事件系统，提出有界时间非阻塞性概念，要求任务在有限滴答时间内完成，并构建有界时间非阻塞监控控制问题（BTNSCP），给出其可解性条件及最大宽容解的计算方法。

基于马尔可夫聚类的大规模离散事件系统全自动非阻塞分层监督控制

Markov Clustering based Fully Automated Nonblocking Hierarchical Supervisory Control of Large-Scale Discrete-Event Systems

本文提出基于马尔可夫聚类的全自动分层监督控制方法，解决大规模离散事件系统非阻塞控制中组件分组难题，并证明其可实现全局非阻塞且最大许可行为。

离散事件系统的定量非阻塞监督控制

Quantitatively Nonblocking Supervisory Control of Discrete-Event Systems

针对离散事件系统的非阻塞监督控制需求，本文提出两种定量非阻塞性质与对应控制问题，通过语言可完备性刻画可解性，证明极大可完备子语言的存在唯一性并给出计算最大允许控制解的算法。

Modeling and Control of Discrete Event Systems under Joint Sensor-Actuator Cyber Attacks

In this paper, we investigate joint sensor-actuator cyber attacks in discrete event systems. We assume that attackers can attack some sensors and actuators at the same time by altering observations and control commands. Because of the nondeterminism in observation and control caused by cyber attacks, the behavior of the supervised system becomes nondeterministic and may deviate from the safety specification. We define the upper-bound on all possible languages that can be generated by the supervised system to investigate the safety supervisory control problem under cyber attacks. After introduc…

离散事件系统基于预测的性质研究：概念、应用与监控器综合

On Prediction-Based Properties of Discrete-Event Systems: Notions, Applications and Supervisor Synthesis

针对部分可观测离散事件系统，提出基于预测的性质概念以建模依赖未来行为的性质，通过新型信息结构将监控器综合转化为信息空间安全博弈，得到可靠完备且最大允许的监控器综合算法。

多智能体离散事件系统中重标记观测一致性的判定

Deciding Relabeling Observation Consistency in Multi-Agent Discrete-Event Systems

本文证明多智能体离散事件系统的重标记观测一致性（ROC）是PSPACE完全问题，给出易处理情形的多项式时间算法与充分条件，修正了文献中相关错误结论并证明ROC的组合性。