-
Constrained LTL Specification Learning from Examples
Authors:
Changjian Zhang,
Parv Kapoor,
Ian Dardik,
Leyi Cui,
Romulo Meira-Goes,
David Garlan,
Eunsuk Kang
Abstract:
Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime monitoring. Given a set of positive and negative examples, specified as traces, LTL learning is the problem of synthesizing a specification, in linear temporal logic (LTL), that evaluates to true over the positive traces an…
▽ More
Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime monitoring. Given a set of positive and negative examples, specified as traces, LTL learning is the problem of synthesizing a specification, in linear temporal logic (LTL), that evaluates to true over the positive traces and false over the negative ones. In this paper, we propose a new type of LTL learning problem called constrained LTL learning, where the user, in addition to positive and negative examples, is given an option to specify one or more constraints over the properties of the LTL formula to be learned. We demonstrate that the ability to specify these additional constraints significantly increases the range of applications for LTL learning, and also allows efficient generation of LTL formulas that satisfy certain desirable properties (such as minimality). We propose an approach for solving the constrained LTL learning problem through an encoding in first-order relational logic and reduction to an instance of the maximal satisfiability (MaxSAT) problem. An experimental evaluation demonstrates that ATLAS, an implementation of our proposed approach, is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in LTL learning.
△ Less
Submitted 30 December, 2024; v1 submitted 3 December, 2024;
originally announced December 2024.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
