Showing 1–11 of 11 results for author: Meira-Goes, R

Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems

Authors: Changjian Zhang, Parv Kapoor, Eunsuk Kang, Romulo Meira-Goes, David Garlan, Akila Ganlath, Shatadal Mishra, Nejib Ammar

Abstract: Cyber-physical systems (CPS) with reinforcement learning (RL)-based controllers are increasingly being deployed in complex physical environments such as autonomous vehicles, the Internet-of-Things(IoT), and smart cities. An important property of a CPS is tolerance; i.e., its ability to function safely under possible disturbances and uncertainties in the actual operation. In this paper, we introduc… ▽ More Cyber-physical systems (CPS) with reinforcement learning (RL)-based controllers are increasingly being deployed in complex physical environments such as autonomous vehicles, the Internet-of-Things(IoT), and smart cities. An important property of a CPS is tolerance; i.e., its ability to function safely under possible disturbances and uncertainties in the actual operation. In this paper, we introduce a new, expressive notion of tolerance that describes how well a controller is capable of satisfying a desired system requirement, specified using Signal Temporal Logic (STL), under possible deviations in the system. Based on this definition, we propose a novel analysis problem, called the tolerance falsification problem, which involves finding small deviations that result in a violation of the given requirement. We present a novel, two-layer simulation-based analysis framework and a novel search heuristic for finding small tolerance violations. To evaluate our approach, we construct a set of benchmark problems where system parameters can be configured to represent different types of uncertainties and disturbancesin the system. Our evaluation shows that our falsification approach and heuristic can effectively find small tolerance violations. △ Less

Submitted 24 June, 2024; originally announced June 2024.

Comments: arXiv admin note: text overlap with arXiv:2311.07462

Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications

Authors: Parv Kapoor, Eunsuk Kang, Romulo Meira-Goes

Abstract: Trajectory planning is a critical process that enables autonomous systems to safely navigate complex environments. Signal temporal logic (STL) specifications are an effective way to encode complex temporally extended objectives for trajectory planning in cyber-physical systems (CPS). However, planning from these specifications using existing techniques scale exponentially with the number of nested… ▽ More Trajectory planning is a critical process that enables autonomous systems to safely navigate complex environments. Signal temporal logic (STL) specifications are an effective way to encode complex temporally extended objectives for trajectory planning in cyber-physical systems (CPS). However, planning from these specifications using existing techniques scale exponentially with the number of nested operators and the horizon of specification. Additionally, performance is exacerbated at runtime due to limited computational budgets and compounding modeling errors. Decomposing a complex specification into smaller subtasks and incrementally planning for them can remedy these issues. In this work, we present a way to decompose STL requirements temporally to improve planning efficiency and performance. The key insight in our work is to encode all specifications as a set of reachability and invariance constraints and scheduling these constraints sequentially at runtime. Our proposed technique outperforms the state-of-the-art trajectory synthesis techniques for both linear and non linear dynamical systems. △ Less

Submitted 18 March, 2024; v1 submitted 13 March, 2024; originally announced March 2024.

Comments: Accepted to Nasa Formal Methods (NFM) 2024

Investigating Robustness in Cyber-Physical Systems: Specification-Centric Analysis in the face of System Deviations

Authors: Changjian Zhang, Parv Kapoor, Romulo Meira-Goes, David Garlan, Eunsuk Kang, Akila Ganlath, Shatadal Mishra, Nejib Ammar

Abstract: The adoption of cyber-physical systems (CPS) is on the rise in complex physical environments, encompassing domains such as autonomous vehicles, the Internet of Things (IoT), and smart cities. A critical attribute of CPS is robustness, denoting its capacity to operate safely despite potential disruptions and uncertainties in the operating environment. This paper proposes a novel specification-based… ▽ More The adoption of cyber-physical systems (CPS) is on the rise in complex physical environments, encompassing domains such as autonomous vehicles, the Internet of Things (IoT), and smart cities. A critical attribute of CPS is robustness, denoting its capacity to operate safely despite potential disruptions and uncertainties in the operating environment. This paper proposes a novel specification-based robustness, which characterizes the effectiveness of a controller in meeting a specified system requirement, articulated through Signal Temporal Logic (STL) while accounting for possible deviations in the system. This paper also proposes the robustness falsification problem based on the definition, which involves identifying minor deviations capable of violating the specified requirement. We present an innovative two-layer simulation-based analysis framework designed to identify subtle robustness violations. To assess our methodology, we devise a series of benchmark problems wherein system parameters can be adjusted to emulate various forms of uncertainties and disturbances. Initial evaluations indicate that our falsification approach proficiently identifies robustness violations, providing valuable insights for comparing robustness between conventional and reinforcement learning (RL)-based controllers △ Less

Submitted 25 March, 2024; v1 submitted 13 November, 2023; originally announced November 2023.

Comments: 12 pages

Runtime Resolution of Feature Interactions through Adaptive Requirement Weakening

Authors: Simon Chu, Emma Shedden, Changjian Zhang, Rômulo Meira-Góes, Gabriel A. Moreno, David Garlan, Eunsuk Kang

Abstract: The feature interaction problem occurs when two or more independently developed components interact with each other in unanticipated ways, resulting in undesirable system behaviors. Feature interaction problems remain a challenge for emerging domains in cyber-physical systems (CPS), such as the Internet of Things and autonomous drones. Existing techniques for resolving feature interactions take a… ▽ More The feature interaction problem occurs when two or more independently developed components interact with each other in unanticipated ways, resulting in undesirable system behaviors. Feature interaction problems remain a challenge for emerging domains in cyber-physical systems (CPS), such as the Internet of Things and autonomous drones. Existing techniques for resolving feature interactions take a "winner-takes-all" approach, where one out of the conflicting features is selected as the most desirable one, and the rest are disabled. However, when multiple of the conflicting features fulfill important system requirements, being forced to select one of them can result in an undesirable system outcome. In this paper, we propose a new resolution approach that allows all of the conflicting features to continue to partially fulfill their requirements during the resolution process. In particular, our approach leverages the idea of adaptive requirement weakening, which involves one or more features temporarily weakening their level of performance in order to co-exist with the other features in a consistent manner. Given feature requirements specified in Signal Temporal Logic (STL), we propose an automated method and a runtime architecture for automatically weakening the requirements to resolve a conflict. We demonstrate our approach through case studies on feature interactions in autonomous drones. △ Less

Submitted 27 October, 2023; originally announced October 2023.

Comments: 10 pages, submitted to SEAMS conference

Safe Environmental Envelopes of Discrete Systems

Authors: Rômulo Meira-Góes, Ian Dardik, Eunsuk Kang, Stéphane Lafortune, Stavros Tripakis

Abstract: A safety verification task involves verifying a system against a desired safety property under certain assumptions about the environment. However, these environmental assumptions may occasionally be violated due to modeling errors or faults. Ideally, the system guarantees its critical properties even under some of these violations, i.e., the system is \emph{robust} against environmental deviations… ▽ More A safety verification task involves verifying a system against a desired safety property under certain assumptions about the environment. However, these environmental assumptions may occasionally be violated due to modeling errors or faults. Ideally, the system guarantees its critical properties even under some of these violations, i.e., the system is \emph{robust} against environmental deviations. This paper proposes a notion of \emph{robustness} as an explicit, first-class property of a transition system that captures how robust it is against possible \emph{deviations} in the environment. We modeled deviations as a set of \emph{transitions} that may be added to the original environment. Our robustness notion then describes the safety envelope of this system, i.e., it captures all sets of extra environment transitions for which the system still guarantees a desired property. We show that being able to explicitly reason about robustness enables new types of system analysis and design tasks beyond the common verification problem stated above. We demonstrate the application of our framework on case studies involving a radiation therapy interface, an electronic voting machine, a fare collection protocol, and a medical pump device. △ Less

Submitted 1 June, 2023; originally announced June 2023.

Comments: Full version of CAV23 paper

A Model Predictive Control Framework for Improving Risk-Tolerance of Manufacturing Systems

Authors: Mostafa Tavakkoli Anbarani, Efe C. Balta, Rômulo Meira-Góes, Ilya Kovalenko

Abstract: The need for control strategies that can address dynamic system uncertainty is becoming increasingly important. In this work, we propose a Model Predictive Control by quantifying the risk of failure in our system model. The proposed control scheme uses a Priced Timed Automata representation of the manufacturing system to promote the fail-safe operation of systems under uncertainties. The proposed… ▽ More The need for control strategies that can address dynamic system uncertainty is becoming increasingly important. In this work, we propose a Model Predictive Control by quantifying the risk of failure in our system model. The proposed control scheme uses a Priced Timed Automata representation of the manufacturing system to promote the fail-safe operation of systems under uncertainties. The proposed method ensures that in case of unforeseen failure(s), the optimization-based control strategy can still achieve the manufacturing system objective. In addition, the proposed strategy establishes a trade-off between minimizing the cost and reducing failure risk to allow the manufacturing system to function effectively in the presence of uncertainties. An example from manufacturing systems is presented to show the application of the proposed control strategy. △ Less

Submitted 15 February, 2023; originally announced February 2023.

Comments: 7 pages

Risk-Averse Model Predictive Control for Priced Timed Automata

Authors: Mostafa Tavakkoli Anbarani, Efe C. Balta, Rômulo Meira-Góes, Ilya Kovalenko

Abstract: In this paper, we propose a Risk-Averse Priced Timed Automata (PTA) Model Predictive Control (MPC) framework to increase flexibility of cyber-physical systems. To improve flexibility in these systems, our risk-averse framework solves a multi-objective optimization problem to minimize the cost and risk, simultaneously. While minimizing cost ensures the least effort to achieve a task, minimizing ris… ▽ More In this paper, we propose a Risk-Averse Priced Timed Automata (PTA) Model Predictive Control (MPC) framework to increase flexibility of cyber-physical systems. To improve flexibility in these systems, our risk-averse framework solves a multi-objective optimization problem to minimize the cost and risk, simultaneously. While minimizing cost ensures the least effort to achieve a task, minimizing risk provides guarantees on the feasibility of the task even during uncertainty. Our framework explores the trade-off between these two qualities to obtain risk-averse control actions. The solution of risk-averse PTA MPC dynamic decision-making algorithm reacts relatively better to PTA changes compared to PTA MPC without risk-averse feature. An example from manufacturing systems is presented to show the application of the proposed control strategy. △ Less

Submitted 27 October, 2022; originally announced October 2022.

Comments: 7 pages

Using Subobservers to Synthesize Opacity-Enforcing Supervisors

Authors: Richard Hugh Moulton, Behnam Behinaein Hamgini, Zahra Abedi Khouzani, Rômulo Meira-Góes, Fei Wang, Karen Rudie

Abstract: In discrete-event system control, the worst-case time complexity for computing a system's observer is exponential in the number of that system's states. This results in practical difficulties since some problems require calculating multiple observers for a changing system, e.g., synthesizing an opacity-enforcing supervisor. Although calculating these observers in an iterative manner allows us to s… ▽ More In discrete-event system control, the worst-case time complexity for computing a system's observer is exponential in the number of that system's states. This results in practical difficulties since some problems require calculating multiple observers for a changing system, e.g., synthesizing an opacity-enforcing supervisor. Although calculating these observers in an iterative manner allows us to synthesize an opacity-enforcing supervisor and although methods have been proposed to reduce the computational demands, room exists for a practical and intuitive solution. Here we extend the subautomaton relationship to the notion of a subobserver and demonstrate its use in reducing the computations required for iterated observer calculations. We then demonstrate the subobserver relationship's power by simplifying state-of-the-art synthesis approaches for opacity-enforcing supervisors under realistic assumptions. △ Less

Submitted 8 August, 2022; v1 submitted 8 October, 2021; originally announced October 2021.

Comments: 26 pages, 7 figures, to be published in Discrete Event Dynamic Systems

On tolerance of discrete systems with respect to transition perturbations

Authors: Rômulo Meira-Góes, Eunsuk Kang, Stéphane Lafortune, Stavros Tripakis

Abstract: Control systems should enforce a desired property for both expected modeled situations as well as unexpected unmodeled environmental situations. Existing methods focus on designing controllers to enforce the desired property only when the environment behaves as expected. However, these methods lack discussion on how the system behaves when the environment is perturbed. In this paper, we propose an… ▽ More Control systems should enforce a desired property for both expected modeled situations as well as unexpected unmodeled environmental situations. Existing methods focus on designing controllers to enforce the desired property only when the environment behaves as expected. However, these methods lack discussion on how the system behaves when the environment is perturbed. In this paper, we propose an approach for analyzing control systems with respect to their tolerance against environmental perturbations. A control system tolerates certain environmental perturbations when it remains capable of guaranteeing the desired property despite the perturbations. Each controller inherently has a level of tolerance against environmental perturbations. We formally define this notion of tolerance and describe a general technique to compute it, for any given regular property. We also present a more efficient method to compute tolerance with respect to invariance properties. Moreover, we introduce a new controller synthesis problem based on our notion of tolerance. We demonstrate the application of our framework on an autonomous surveillance example. △ Less

Submitted 18 October, 2021; v1 submitted 8 October, 2021; originally announced October 2021.

Comments: Full version of TACAS'22 submission

Synthesis of Supervisors Robust Against Sensor Deception Attacks

Authors: Rômulo Meira-Góes, Stéphane Lafortune, Hervé Marchand

Abstract: 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, w… ▽ More 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. △ Less

Submitted 23 December, 2020; originally announced December 2020.

Comments: Full version of preprint accepted at IEEE Transactions on Automatic Control

Synthesis of Sensor Deception Attacks at the Supervisory Layer of Cyber-Physical Systems

Authors: Romulo Meira-Goes, Eunsuk Kang, Raymond H. Kwong, Stephane Lafortune

Abstract: We study the security of Cyber-Physical Systems (CPS) in the context of the supervisory control layer. Specifically, we propose a general model of a CPS attacker in the framework of discrete event systems and investigate the problem of synthesizing an attack strategy for a given feedback control system. Our model captures a class of deception attacks, where the attacker has the ability to hijack a… ▽ More We study the security of Cyber-Physical Systems (CPS) in the context of the supervisory control layer. Specifically, we propose a general model of a CPS attacker in the framework of discrete event systems and investigate the problem of synthesizing an attack strategy for a given feedback control system. Our model captures a class of deception attacks, where the attacker has the ability to hijack a subset of sensor readings and mislead the supervisor, with the goal of inducing the system into an undesirable state. We utilize a game-like discrete transition structure, called Insertion-Deletion Attack structure (IDA), to capture the interaction between the supervisor and the environment (which includes the system and the attacker). We show how to use IDAs to synthesize three different types of successful stealthy attacks, i.e., attacks that avoid detection from the supervisor and cause damage to the system. △ Less

Submitted 4 August, 2020; originally announced August 2020.

Comments: Full version of preprint accepted at Automatica