Computing unsatisfiable cores for LTLf specifications

• URL: http://arxiv.org/abs/2203.04834v1
• Date: Wed, 9 Mar 2022 16:08:43 GMT
• Title: Computing unsatisfiable cores for LTLf specifications
• Authors: Marco Roveri and Claudio Di Ciccio and Chiara Di Francescomarino and Chiara Ghidini
• Abstract summary: 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.
• Score: 3.251765107970636
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several studies approached the respective satisfiability problem. In this paper, we investigate the problem of extracting the unsatisfiable core in LTLf specifications. We provide four algorithms for extracting an unsatisfiable core leveraging the adaptation of state-of-the-art approaches to LTLf satisfiability checking. We implement the different approaches within the respective tools and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable ones. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools.

Related papers

• Benchmarking Agentic Workflow Generation [80.74757493266057]
  We introduce WorFBench, a unified workflow generation benchmark with multi-faceted scenarios and intricate graph workflow structures. We also present WorFEval, a systemic evaluation protocol utilizing subsequence and subgraph matching algorithms. We observe that the generated can enhance downstream tasks, enabling them to achieve superior performance with less time during inference.
  arXiv  Detail & Related papers  (2024-10-10T12:41:19Z)
• 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)
• TSI-Bench: Benchmarking Time Series Imputation [52.27004336123575]
  TSI-Bench is a comprehensive benchmark suite for time series imputation utilizing deep learning techniques. The TSI-Bench pipeline standardizes experimental settings to enable fair evaluation of imputation algorithms. TSI-Bench innovatively provides a systematic paradigm to tailor time series forecasting algorithms for imputation purposes.
  arXiv  Detail & Related papers  (2024-06-18T16:07:33Z)
• When Dataflow Analysis Meets Large Language Models [9.458251511218817]
  This paper introduces LLMDFA, an LLM-powered dataflow analysis framework that analyzes arbitrary code snippets without requiring a compilation infrastructure. Inspired by summary-based dataflow analysis, LLMDFA decomposes the problem into three sub-problems, which are effectively resolved by several essential strategies. Our evaluation has shown that the design can mitigate the hallucination and improve the reasoning ability, obtaining high precision and recall in detecting dataflow-related bugs.
  arXiv  Detail & Related papers  (2024-02-16T15:21:35Z)
• 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)
• Exploring Viable Algorithmic Options for Learning from Demonstration (LfD): A Parameterized Complexity Approach [0.0]
  In this paper, we show how such a systematic exploration of algorithmic options can be done using parameterized complexity analysis. We show that none of our problems can be solved efficiently either in general or relative to a number of (often simultaneous) restrictions on environments, demonstrations, and policies.
  arXiv  Detail & Related papers  (2022-05-10T15:54:06Z)
• 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)
• 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.