Specification sketching for Linear Temporal Logic

• URL: http://arxiv.org/abs/2206.06722v1
• Date: Tue, 14 Jun 2022 10:09:23 GMT
• Title: Specification sketching for Linear Temporal Logic
• Authors: Simon Lutz, Daniel Neider and Rajarshi Roy
• Abstract summary: We propose a fundamentally novel approach to writing formal specifications, named specification sketching for Linear Temporal Logic (LTL) The key idea is that an engineer can provide a partial formula, called a sketch, where parts that are hard to formalize can be left out. We show that deciding whether a sketch can be completed falls into the complexity class NP and present two SAT-based sketching algorithms.
• Score: 3.3946853660795893
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: Virtually all verification and synthesis techniques assume that the formal specifications are readily available, functionally correct, and fully match the engineer's understanding of the given system. However, this assumption is often unrealistic in practice: formalizing system requirements is notoriously difficult, error-prone, and requires substantial training. To alleviate this severe hurdle, we propose a fundamentally novel approach to writing formal specifications, named specification sketching for Linear Temporal Logic (LTL). The key idea is that an engineer can provide a partial LTL formula, called an LTL sketch, where parts that are hard to formalize can be left out. Given a set of examples describing system behaviors that the specification should or should not allow, the task of a so-called sketching algorithm is then to complete a given sketch such that the resulting LTL formula is consistent with the examples. We show that deciding whether a sketch can be completed falls into the complexity class NP and present two SAT-based sketching algorithms. We also demonstrate that sketching is a practical approach to writing formal specifications using a prototype implementation.

Related papers

• What is Formal Verification without Specifications? A Survey on mining LTL Specifications [5.655251163654288]
  We list and compare advances in mining specifications in Linear Temporal Logic (LTL), the de facto standard specification language for reactive systems. Several approaches have been designed for learning formulas, which address different aspects and settings of specification design. We survey the current state-of-the-art techniques and compare them for the convenience of the formal methods practitioners.
  arXiv  Detail & Related papers  (2025-01-27T18:06:48Z)
• 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)
• It's All About Your Sketch: Democratising Sketch Control in Diffusion Models [114.73766136068357]
  This paper unravels the potential of sketches for diffusion models, addressing the deceptive promise of direct sketch control in generative AI. We importantly democratise the process, enabling amateur sketches to generate precise images, living up to the commitment of "what you sketch is what you get"
  arXiv  Detail & Related papers  (2024-03-12T01:05:25Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  We consider the problem of automatically synthesizing formal specifications from system executions. Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead.
  arXiv  Detail & Related papers  (2023-10-26T14:13:15Z)
• I Know What You Draw: Learning Grasp Detection Conditioned on a Few Freehand Sketches [74.63313641583602]
  We propose a method to generate a potential grasp configuration relevant to the sketch-depicted objects. Our model is trained and tested in an end-to-end manner which is easy to be implemented in real-world applications.
  arXiv  Detail & Related papers  (2022-05-09T04:23: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)
• From English to Signal Temporal Logic [7.6398837478968025]
  We propose DeepSTL, a tool and technique for the translation of informal requirements, given as free English sentences, into Signal Temporal Logic (STL), a formal specification language for cyber-physical systems. A major challenge to devise such a translator is the lack of publicly available informal requirements and formal specifications. In the second step, we use a state-of-the-art transformer-based neural translation technique, to train an accurate attentional translator of English to STL.
  arXiv  Detail & Related papers  (2021-09-21T16:13:29Z)
• Learning-Augmented Sketches for Hessians [54.97773807211337]
  We show how to design learned sketches for the Hessian in the context of second order methods. We show empirically that learned sketches, compared with their "non-learned" counterparts, improve the approximation accuracy for important problems.
  arXiv  Detail & Related papers  (2021-02-24T14:50:59Z)
• Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods [28.72161643908351]
  This paper presents a technique, named STLCG, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems.
  arXiv  Detail & Related papers  (2020-07-31T22:01:39Z)
• 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.