Decidable Fragments of LTLf Modulo Theories (Extended Version)

• URL: http://arxiv.org/abs/2307.16840v1
• Date: Mon, 31 Jul 2023 17:02:23 GMT
• Title: Decidable Fragments of LTLf Modulo Theories (Extended Version)
• Authors: Luca Geatti and Alessandro Gianola and Nicola Gigante and Sarah Winkler
• Abstract summary: In general,fMT was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics) with a tableau-based semi-decision procedure. We show that for anyfMT formula satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with a new rule is also guaranteed to terminate.
• Score: 66.25779635347122
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLfMT), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by first-order formulas and where first-order variables referring to different time points can be compared. In general, LTLfMT was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics), with a tableau-based semi-decision procedure. In this paper we present a sound and complete pruning rule for the LTLfMT tableau. We show that for any LTLfMT formula that satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with the new rule is also guaranteed to terminate. Last but not least, this technique allows us to establish novel decidability results for the satisfiability of several fragments of LTLfMT, as well as to give new decidability proofs for classes that are already known.

Related papers

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation. For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• 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)
• Independent Component Alignment for Multi-Task Learning [2.5234156040689237]
  In a multi-task learning (MTL) setting, a single model is trained to tackle a diverse set of tasks jointly. We propose using a condition number of a linear system of gradients as a stability criterion of an MTL optimization. We present Aligned-MTL, a novel MTL optimization approach based on the proposed criterion.
  arXiv  Detail & Related papers  (2023-05-30T12:56:36Z)
• 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)
• LTL-Constrained Steady-State Policy Synthesis [0.0]
  We study Markov decision processes (MDP) with the specification combining all these types. We provide a unified solution reducing the multi-type specification to a multi-dimensional long-run average reward. The algorithm also extends to the general $omega$-regular properties and runs in time in the sizes of the MDP as well as the LDBA.
  arXiv  Detail & Related papers  (2021-05-31T11:35:42Z)
• LTLf Synthesis on Probabilistic Systems [0.0]
  synthesis is used to find a policy that maximizes the probability of achieving this behavior. No tools exist to solve policy synthesis for behaviors given finite-trace properties. We present two algorithms for solving this problem: the first via reduction of Markov Processes and the second native tools for automatonf.
  arXiv  Detail & Related papers  (2020-09-23T01:26:47Z)
• What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints [28.072597424460472]
  We consider a temporal logic planning problem in which the objective is to find an infinite trajectory that satisfies an optimal selection from a set of soft specifications. Our algorithm first constructs a product, on which the planning problem is reduced to computing a lasso with minimum cost. Though we prove that computing such a shortest lasso is hard, we also introduce an efficient greedy approach to synthesize short lassos.
  arXiv  Detail & Related papers  (2020-08-05T04:18:59Z)
• A Generic First-Order Algorithmic Framework for Bi-Level Programming Beyond Lower-Level Singleton [49.23948907229656]
  Bi-level Descent Aggregation is a flexible and modularized algorithmic framework for generic bi-level optimization. We derive a new methodology to prove the convergence of BDA without the LLS condition. Our investigations also demonstrate that BDA is indeed compatible to a verify of particular first-order computation modules.
  arXiv  Detail & Related papers  (2020-06-07T05:18:50Z)

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.