Forward LTLf Synthesis: DPLL At Work

• URL: http://arxiv.org/abs/2302.13825v2
• Date: Mon, 19 Jun 2023 17:02:21 GMT
• Title: Forward LTLf Synthesis: DPLL At Work
• Authors: Marco Favorito
• Abstract summary: We propose a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (LTLf) Within such framework, we devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves. We also propose a novel equivalence check for search nodes based on syntactic equivalence of state formulas.
• Score: 1.370633147306388
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper proposes a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (\LTLf), that overcomes some limitations of previous approaches. Within such framework, we devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves in a truly depth-first fashion, possibly avoiding exhaustive enumeration or costly compilations. We also propose a novel equivalence check for search nodes based on syntactic equivalence of state formulas. Since the resulting procedure is not guaranteed to terminate, we identify a stopping condition to abort execution and restart the search with state-equivalence checking based on Binary Decision Diagrams (BDD), which we show to be correct. The experimental results show that in many cases the proposed techniques outperform other state-of-the-art approaches. Our implementation Nike competed in the LTLf Realizability Track in the 2023 edition of SYNTCOMP, and won the competition.

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)
• Double-Ended Synthesis Planning with Goal-Constrained Bidirectional Search [27.09693306892583]
  We present a formulation of synthesis planning with starting material constraints. We propose Double-Ended Synthesis Planning (DESP), a novel CASP algorithm under a bidirectional graph search scheme. DESP can make use of existing one-step retrosynthesis models, and we anticipate its performance to scale as these one-step model capabilities improve.
  arXiv  Detail & Related papers  (2024-07-08T18:56:00Z)
• Optimizing NOTEARS Objectives via Topological Swaps [41.18829644248979]
  In this paper, we develop an effective method for a set of candidate algorithms. At the inner level, given a subject, we utilize off-the-the-art constraints. The proposed method significantly improves the score of other algorithms.
  arXiv  Detail & Related papers  (2023-05-26T21:49:37Z)
• 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)
• Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
  Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on networks with extensive branching functions. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with DeepSoI.
  arXiv  Detail & Related papers  (2022-03-19T15:05:09Z)
• Recursive Causal Structure Learning in the Presence of Latent Variables and Selection Bias [27.06618125828978]
  We consider the problem of learning the causal MAG of a system from observational data in the presence of latent variables and selection bias. We propose a novel computationally efficient constraint-based method that is sound and complete. We provide experimental results to compare the proposed approach with the state of the art on both synthetic and real-world structures.
  arXiv  Detail & Related papers  (2021-10-22T19:49:59Z)
• Revisiting the Complexity Analysis of Conflict-Based Search: New Computational Techniques and Improved Bounds [5.158632635415881]
  State-of-the-art approach to computing optimal solutions is Conflict-Based Search (CBS) We revisit the complexity analysis of CBS to provide tighter bounds on the algorithm's run-time in the worst-case.
  arXiv  Detail & Related papers  (2021-04-18T07:46:28Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. We present a novel activation-based branching strategy and a BaB framework, named Branch and Dual Network Bound (BaDNB) BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial properties.
  arXiv  Detail & Related papers  (2021-04-14T09:22:42Z)
• Lower bounds in multiple testing: A framework based on derandomized proxies [107.69746750639584]
  This paper introduces an analysis strategy based on derandomization, illustrated by applications to various concrete models. We provide numerical simulations of some of these lower bounds, and show a close relation to the actual performance of the Benjamini-Hochberg (BH) algorithm.
  arXiv  Detail & Related papers  (2020-05-07T19:59:51Z)
• 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)
• The Simulator: Understanding Adaptive Sampling in the Moderate-Confidence Regime [52.38455827779212]
  We propose a novel technique for analyzing adaptive sampling called the em Simulator. We prove the first instance-based lower bounds the top-k problem which incorporate the appropriate log-factors. Our new analysis inspires a simple and near-optimal for the best-arm and top-k identification, the first em practical of its kind for the latter problem.
  arXiv  Detail & Related papers  (2017-02-16T23:42:02Z)

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.