4.7 Article

Synthesis of Maximally-Permissive Supervisors for the Range Control Problem

期刊

IEEE TRANSACTIONS ON AUTOMATIC CONTROL
卷 62, 期 8, 页码 3914-3929

出版社

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2016.2644867

关键词

Discrete event systems; maximal permissiveness; partial observation; supervisory control; synthesis

资金

  1. U.S. National Science Foundation [CCF-1138860, CNS-1446298]
  2. Direct For Computer & Info Scie & Enginr
  3. Division Of Computer and Network Systems [1446298] Funding Source: National Science Foundation
  4. Division of Computing and Communication Foundations
  5. Direct For Computer & Info Scie & Enginr [1138860] Funding Source: National Science Foundation

向作者/读者索取更多资源

We investigate the supervisor synthesis problem for centralized partially-observed discrete event systems subject to safety specifications. It is well known that this problem does not have a unique supremal solution in general. Instead, there may be several incomparable locally maximal solutions. One then needs a mechanism to select one locally maximal solution. Our approach in this paper is to consider a lower bound specification on the controlled behavior, in addition to the upper bound for the safety specification. This leads to a generalized supervisory control problem called the range control problem. While the upper bound captures the (prefix-closed) legal behavior, the lower bound captures the (prefix-closed) minimum required behavior. We provide a synthesis algorithm that solves this problem by effectively constructing amaximally-permissive safe supervisor that contains the required lower bound behavior. This is the first algorithm with such properties, as previous works solve either the maximally-permissive safety problem (with no lower bound), or the lower bound containment problem (without maximal permissiveness).

作者

我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。

评论

主要评分

4.7
评分不足

次要评分

新颖性
-
重要性
-
科学严谨性
-
评价这篇论文

推荐

Article Automation & Control Systems

Optimal supervisory control with mean payoff objectives and under partial observation ?

Yiding Ji, Xiang Yin, Stephane Lafortune

Summary: The article explores optimal mean payoff supervisory control problems on partially observed discrete event systems modeled as weighted finite-state automata. Two supervisory control problems are considered, each involving optimization and solution processes. The use of energy information states to capture system state and energy level information is proposed as a way to facilitate decision-making by the supervisor.

AUTOMATICA (2021)

Editorial Material Automation & Control Systems

Editorial-Thirty years of J-DEDS: moving on with new leadership

Christoforos Hadjicostis, Stephane Lafortune

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS (2021)

Article Automation & Control Systems

Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications

Sahar Mohajerani, Robi Malik, Andrew Wintenberg, Stephane Lafortune, Necmiye Ozay

Summary: This paper proposes a method for synthesising controllers for systems with possibly infinite number of states, satisfying a specification given as an LTL\degrees. formula. By using divergent stutter bisimulation to abstract the state space, a faster but coarser abstraction can be obtained, at the expense of not preserving the temporal “next” operator.

AUTOMATICA (2021)

Article Automation & Control Systems

A general language-based framework for specifying and verifying notions of opacity

Andrew Wintenberg, Matthew Blischke, Stephane Lafortune, Necmiye Ozay

Summary: This paper provides a general framework of opacity to unify the existing notions of opacity for discrete event systems. It discusses language-based and state-based notions of opacity and presents verification methods. It also investigates the concept of K-step opacity and provides corresponding language-based verification methods.

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS (2022)

Article Automation & Control Systems

Synthesis of Optimal Multiobjective Attack Strategies for Controlled Systems Modeled by Probabilistic Automata

Romulo Meira-Goes, Raymond H. Kwong, Stephane Lafortune

Summary: This article studies the security of control systems in the supervisory control layer of stochastic discrete-event systems, focusing on cases where communication is partially compromised by a malicious attacker. The author investigates the synthesis of attack strategies from the attacker's viewpoint in systems modeled as probabilistic automata.

IEEE TRANSACTIONS ON AUTOMATIC CONTROL (2022)

Article Automation & Control Systems

Local Mean Payoff Supervisory Control for Discrete Event Systems

Yiding Ji, Xiang Yin, Stephane Lafortune

Summary: This article investigates quantitative supervisory control with local mean payoff objectives on discrete event systems modeled as weighted automata. It focuses on the stability or robustness of weight flows measured by mean weights over a finite number of events. The study addresses qualitative and quantitative requirements through formulating two supervisory control problems and providing a solution based on a two-player game model.

IEEE TRANSACTIONS ON AUTOMATIC CONTROL (2022)

Article Automation & Control Systems

A Compact and Uniform Approach for Synthesizing State-Based Property-Enforcing Supervisors for Discrete-Event Systems

Romulo Meira-Goes, Jack Weitze, Stephane Lafortune

Summary: This article focuses on synthesizing a partial observation supervisor for a discrete-event system and introduces a compact and uniform approach. By defining a compact all enforcement structure (AES), it is possible to efficiently synthesize property-enforcing supervisors, as demonstrated by the experimental results.

IEEE TRANSACTIONS ON AUTOMATIC CONTROL (2022)

Article Automation & Control Systems

Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies

Shoma Matsui, Stephane Lafortune

Summary: This research focuses on the vulnerability of communication protocols in distributed systems and proposes a formal synthesis methodology for successful attacks against two well-known protocols. The approach considers the attacker's partial observability and controllability of system events and employs supervisory control theory for discrete event systems. The study presents several scenarios of person-in-the-middle attacks and showcases the results of attack synthesis using the proposed methodology.

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS (2022)

Article Automation & Control Systems

Dealing with sensor and actuator deception attacks in supervisory control

Romulo Meira-Goes, Herve Marchand, Stephane Lafortune

Summary: This study focuses on feedback control systems in which sensor readings and actuator commands may be compromised by attackers. The problem is studied at the supervisory layer of the control system using discrete event systems techniques. The goal is to synthesize a supervisor that can withstand a wide range of edit attacks and ensure system safety.

AUTOMATICA (2023)

Article Automation & Control Systems

On tolerance of discrete systems with respect to transition perturbations

Romulo Meira-Goes, Eunsuk Kang, Stephane Lafortune, Stavros Tripakis

Summary: This paper proposes an approach for analyzing the tolerance of discrete-state control systems to environmental perturbations and investigates the behavior of the system when the environment is disturbed. The study reveals an inherent trade-off between permissiveness and tolerance.

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS (2023)

Article Automation & Control Systems

Opacity From Observers With a Bounded Memory

Andrew Wintenberg, Stephane Lafortune, Necmiye Ozay

Summary: Opacity is a property that protects privacy by preventing observers from inferring a system's dynamics. We propose a new notion called bounded memory opacity, which addresses the challenge of verifying opacity when an observer has limited memory. We show that verifying this weaker notion has reduced computational complexity compared to general opacity. Additionally, we present a verification algorithm using Boolean satisfiability problem encoding, and demonstrate its effectiveness on randomly generated automata and a Web server load-hiding example.

IEEE CONTROL SYSTEMS LETTERS (2023)

Proceedings Paper Automation & Control Systems

Cybersecurity and Supervisory Control: A Tutorial on Robust State Estimation, Attack Synthesis, and Resilient Control

Christoforos N. Hadjicostis, Stephane Lafortune, Feng Lin, Rong Su

Summary: This tutorial paper investigates the impact of deception attacks on compromised sensors and actuators at the supervisory control layer. It analyzes robust estimation and diagnosis in the presence of sensor attacks, formulates the problem of synthesizing covert attacks, discusses resilient supervisors in a general attack model, and studies supervisors resilient to covert attacks on sensors and actuators.

2022 IEEE 61ST CONFERENCE ON DECISION AND CONTROL (CDC) (2022)

Proceedings Paper Automation & Control Systems

On synthesizing tolerable and permissive controllers for labeled transition systems

Romulo Meira-Goes, Eunsuk Kang, Stephane Lafortune, Stavros Tripakis

Summary: We propose an approach for analyzing discrete-state systems with respect to their permissiveness and tolerance against environmental perturbations using Pareto optimality conditions. We investigate the trade-off between permissiveness and tolerance by defining Pareto optimality and show that memoryless controllers are sufficient for capturing the Pareto front. We also study the synthesis of Pareto optimal controllers that achieve a minimum level of tolerance and permissiveness.

IFAC PAPERSONLINE (2022)

Proceedings Paper Computer Science, Information Systems

A Dynamic Obfuscation Framework for Security and Utility

Andrew Wintenberg, Matthew Blischke, Stephane Lafortune, Necmiye Ozay

Summary: Obfuscation is a technique used in dynamic systems to ensure private and secure communication in networks vulnerable to eavesdroppers. This article proposes a new framework for obfuscation that includes an inference interface for intended recipients to interpret the obfuscated information. The security of the obfuscation is modeled using opacity, a formal notion of plausible deniability. The article demonstrates the application of this approach in enforcing privacy while maintaining utility in a contact tracing model.

2022 13TH ACM/IEEE INTERNATIONAL CONFERENCE ON CYBER-PHYSICAL SYSTEMS (ICCPS 2022) (2022)

暂无数据