LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces

• URL: http://arxiv.org/abs/2411.09366v1
• Date: Thu, 14 Nov 2024 11:17:06 GMT
• Title: LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
• Authors: Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Moshe Y. Vardi,
• Abstract summary: DFA-based synthesis techniques for automatf+/PPLTL+ are presented. We show that the full expressive power of PPLTL+ is EXPTIME-complete instead of 2EXPTIME-complete.
• Score: 44.35335751462176
• License:
• Abstract: We introduce LTLf+ and PPLTL+, two logics to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli's LTL safety-progress hierarchy, and thus have the same expressive power as LTL. However, they also retain a crucial characteristic of the reactive synthesis problem for the base logics: the game arena for strategy extraction can be derived from deterministic finite automata (DFA). Consequently, these logics circumvent the notorious difficulties associated with determinizing infinite trace automata, typical of LTL reactive synthesis. We present DFA-based synthesis techniques for LTLf+/PPLTL+, and show that synthesis is 2EXPTIME-complete for LTLf+ (matching LTLf) and EXPTIME-complete for PPLTL+ (matching PPLTL). Notably, while PPLTL+ retains the full expressive power of LTL, reactive synthesis is EXPTIME-complete instead of 2EXPTIME-complete. The techniques are also adapted to optimally solve satisfiability, validity, and model-checking, to get EXPSPACE-complete for LTLf+ (extending a recent result for the guarantee level using LTLf), and PSPACE-complete for PPLTL+.

Related papers

• On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts [20.14001970300658]
  We present an on-the-fly framework for Linear Temporal Logic over finite traces (LTLf) based on top-down deterministic automata construction.
  arXiv  Detail & Related papers  (2024-08-14T06:52:58Z)
• Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis [1.1797787239802762]
  We show how to generate correct controllers from temporal logic specifications using classical reactive handles (propositional) as a specification language. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to always provide the smallest safe values.
  arXiv  Detail & Related papers  (2024-07-12T15:23:27Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• 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)
• Model Checking Strategies from Synthesis Over Finite Traces [25.871354900295056]
  For model checking, two types of transducers are fundamentally different. We show that for model checking of non-terminating transducers is emphexponentially harder than that of terminating transducers.
  arXiv  Detail & Related papers  (2023-05-15T03:09:20Z)
• A first-order logic characterization of safety and co-safety languages [63.29821624186913]
  Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to a language, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis. This paper introduces a fragment of FO-TLO, called SafetyFO, and of its dual coSafety, which are expressively complete with respect to the safety and co-safety languages.
  arXiv  Detail & Related papers  (2022-09-06T09:00:38Z)
• 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)
• 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)
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications [26.547133495699093]
  We use a neural network to learn a Q-function that is then used to guide search, and to construct programs that are subsequently verified for correctness. Our method is unique in combining search with deep learning to realize synthesis.
  arXiv  Detail & Related papers  (2019-12-31T17:09:49Z)
• 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.