What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints

• URL: http://arxiv.org/abs/2008.01926v1
• Date: Wed, 5 Aug 2020 04:18:59 GMT
• Title: What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints
• Authors: Hazhar Rahmani, Jason M. O'Kane
• Abstract summary: 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.
• Score: 28.072597424460472
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this paper, 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 expressed in linear temporal logic (LTL) while nevertheless satisfying a hard specification expressed in LTL. Our previous work considered a similar problem in which linear dynamic logic for finite traces (LDLf), rather than LTL, was used to express the soft constraints. In that work, LDLf was used to impose constraints on finite prefixes of the infinite trajectory. By using LTL, one is able not only to impose constraints on the finite prefixes of the trajectory, but also to set `soft' goals across the entirety of the infinite trajectory. Our algorithm first constructs a product automaton, on which the planning problem is reduced to computing a lasso with minimum cost. Among all such lassos, it is desirable to compute a shortest one. Though we prove that computing such a shortest lasso is computationally hard, we also introduce an efficient greedy approach to synthesize short lassos nonetheless. We present two case studies describing an implementation of this approach, and report results of our experiment comparing our greedy algorithm with an optimal baseline.

Related papers

• 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)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  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.
  arXiv  Detail & Related papers  (2023-07-31T17:02:23Z)
• Accelerated First-Order Optimization under Nonlinear Constraints [73.2273449996098]
  We exploit between first-order algorithms for constrained optimization and non-smooth systems to design a new class of accelerated first-order algorithms. An important property of these algorithms is that constraints are expressed in terms of velocities instead of sparse variables.
  arXiv  Detail & Related papers  (2023-02-01T08:50:48Z)
• 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)
• Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic [2.631744051718347]
  We consider the problem of learning formulas for classifying traces. Existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime.
  arXiv  Detail & Related papers  (2021-10-13T13:57:31Z)
• Efficient Temporal Piecewise-Linear Numeric Planning with Lazy Consistency Checking [4.834203844100679]
  We propose a set of techniques that allow the planner to compute LP consistency checks lazily where possible. We also propose an algorithm to perform duration-dependent goal checking more selectively. The resultant planner is not only more efficient, but outperforms most state-of-the-art temporal-numeric and hybrid planners.
  arXiv  Detail & Related papers  (2021-05-21T07:36:54Z)
• Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach [22.46055650237819]
  We devise two algorithms for inferring concise formulas even in the presence of noise. Our first algorithm infers minimal formulas by reducing the inference problem to a problem in satisfiability. Our second learning algorithm relies on the first algorithm to derive a decision tree over formulas based on a decision tree learning algorithm.
  arXiv  Detail & Related papers  (2021-04-30T16:06:03Z)
• 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)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  A fundamental component of neural network verification is the computation of bounds on the values their outputs can take. We propose a novel approach based on Lagrangian Decomposition. We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
  arXiv  Detail & Related papers  (2020-02-24T17:55:10Z)

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.