Constrained LTL Specification Learning from Examples

• URL: http://arxiv.org/abs/2412.02905v3
• Date: Mon, 30 Dec 2024 18:51:21 GMT
• Title: Constrained LTL Specification Learning from Examples
• Authors: Changjian Zhang, Parv Kapoor, Ian Dardik, Leyi Cui, Romulo Meira-Goes, David Garlan, Eunsuk Kang,
• Abstract summary: We propose a new type of learning problem called constrained learning. In addition to positive and negative examples, the user can specify one or more constraints over the properties of the formula. An experimental evaluation demonstrates that ATLAS is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in learning.
• Score: 8.544277223210894
• License:
• 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 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.

Related papers

• Regret-Free Reinforcement Learning for LTL Specifications [6.342676126028222]
  Reinforcement learning is a promising method to learn optimal control policies for systems with unknown dynamics. Current RL-based methods offer only guarantees, which provide no insight into the transient performance during the learning phase. We present the first regret-free online algorithm for learning a controller that addresses the general class of specifications over Markov decision processes.
  arXiv  Detail & Related papers  (2024-11-18T20:01:45Z)
• CoT-TL: Low-Resource Temporal Knowledge Representation of Planning Instructions Using Chain-of-Thought Reasoning [0.0]
  CoT-TL is a data-efficient in-context learning framework for translating natural language specifications into representations. CoT-TL achieves state-of-the-art accuracy across three diverse datasets in low-data scenarios.
  arXiv  Detail & Related papers  (2024-10-21T17:10:43Z)
• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications [59.01527054553122]
  Linear temporal logic (LTL) has recently been adopted as a powerful formalism for specifying complex, temporally extended tasks in reinforcement learning (RL) Existing approaches suffer from several shortcomings: they are often only applicable to finite-horizon fragments, are restricted to suboptimal solutions, and do not adequately handle safety constraints. In this work, we propose a novel learning approach to address these concerns. Our method leverages the structure of B"uchia, which explicitly represent the semantics of automat- specifications, to learn policies conditioned on sequences of truth assignments that lead to satisfying the desired formulae.
  arXiv  Detail & Related papers  (2024-10-06T21:30:38Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  Linear temporal logic (LTL) is a powerful language for task specification in reinforcement learning. We show that the synthesized reward signal remains fundamentally sparse, making exploration challenging. We show how better exploration can be achieved by further leveraging the specification and casting its corresponding Limit Deterministic B"uchi Automaton (LDBA) as a Markov reward process.
  arXiv  Detail & Related papers  (2024-08-18T14:25:44Z)
• Instruction Tuning for Large Language Models: A Survey [52.86322823501338]
  We make a systematic review of the literature, including the general methodology of supervised fine-tuning (SFT) We also review the potential pitfalls of SFT along with criticism against it, along with efforts pointing out current deficiencies of existing strategies.
  arXiv  Detail & Related papers  (2023-08-21T15:35:16Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)
• Policy Optimization with Linear Temporal Logic Constraints [37.27882290236194]
  We study the problem of policy optimization with linear temporal logic constraints. We develop a model-based approach that enjoys a sample complexity analysis for guaranteeing both task satisfaction and cost optimality.
  arXiv  Detail & Related papers  (2022-06-20T02:58:02Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Computing unsatisfiable cores for LTLf specifications [3.251765107970636]
  Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains. We provide four algorithms for extracting an unsatisfiable core using state-of-the-art approaches to satisfiability checking. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools.
  arXiv  Detail & Related papers  (2022-03-09T16:08:43Z)
• Learning Interpretable Models in the Property Specification Language [6.875312133832079]
  We develop a learning algorithm for formulas in the IEEE standard temporal logic PSL. Our work is motivated by the fact that many natural properties, such as an event happening at every n-th point in time, cannot be expressed in speak.
  arXiv  Detail & Related papers  (2020-02-10T11:42:50Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.