Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
- URL: http://arxiv.org/abs/2310.17410v1
- Date: Thu, 26 Oct 2023 14:13:15 GMT
- Title: Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
- Authors: Ritam Raha, Rajarshi Roy, Nathanael Fijalkow, Daniel Neider and
Guillermo A. Perez
- Abstract summary: 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.
- Score: 4.60607942851373
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In runtime verification, manually formalizing a specification for monitoring
system executions is a tedious and error-prone process. To address this issue,
we consider the problem of automatically synthesizing formal specifications
from system executions. To demonstrate our approach, we consider the popular
specification language Metric Temporal Logic (MTL), which is particularly
tailored towards specifying temporal properties for cyber-physical systems
(CPS). Most of the classical approaches for synthesizing temporal logic
formulas aim at minimizing the size of the formula. However, for efficiency in
monitoring, along with the size, the amount of "lookahead" required for the
specification becomes relevant, especially for safety-critical applications. We
formalize this notion and devise a learning algorithm that synthesizes concise
formulas having bounded lookahead. To do so, our algorithm reduces the
synthesis task to a series of satisfiability problems in Linear Real Arithmetic
(LRA) and generates MTL formulas from their satisfying assignments. The
reduction uses a novel encoding of a popular MTL monitoring procedure using
LRA. Finally, we implement our algorithm in a tool called TEAL and demonstrate
its ability to synthesize efficiently monitorable MTL formulas in a CPS
application.
Related papers
- Smoothing Methods for Automatic Differentiation Across Conditional
Branches [0.0]
Smooth interpretation (SI) approximates the convolution of a program's output with a Gaussian kernel, thus smoothing its output in a principled manner.
We combine SI with automatic differentiation (AD) to efficiently compute gradients of smoothed programs.
We propose a novel Monte Carlo estimator that avoids the underlying assumptions by estimating the smoothed programs' gradients through a combination of AD and sampling.
arXiv Detail & Related papers (2023-10-05T15:08:37Z) - Large Language Models as General Pattern Machines [64.75501424160748]
We show that pre-trained large language models (LLMs) are capable of autoregressively completing complex token sequences.
Surprisingly, pattern completion proficiency can be partially retained even when the sequences are expressed using tokens randomly sampled from the vocabulary.
In this work, we investigate how these zero-shot capabilities may be applied to problems in robotics.
arXiv Detail & Related papers (2023-07-10T17:32:13Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
We propose a method for synthesising controllers for Markov jump linear systems.
Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS.
We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
arXiv Detail & Related papers (2022-12-01T17:36:30Z) - 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) - Activation Relaxation: A Local Dynamical Approximation to
Backpropagation in the Brain [62.997667081978825]
Activation Relaxation (AR) is motivated by constructing the backpropagation gradient as the equilibrium point of a dynamical system.
Our algorithm converges rapidly and robustly to the correct backpropagation gradients, requires only a single type of computational unit, and can operate on arbitrary computation graphs.
arXiv Detail & Related papers (2020-09-11T11:56:34Z) - 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) - Iterative Algorithm Induced Deep-Unfolding Neural Networks: Precoding
Design for Multiuser MIMO Systems [59.804810122136345]
We propose a framework for deep-unfolding, where a general form of iterative algorithm induced deep-unfolding neural network (IAIDNN) is developed.
An efficient IAIDNN based on the structure of the classic weighted minimum mean-square error (WMMSE) iterative algorithm is developed.
We show that the proposed IAIDNN efficiently achieves the performance of the iterative WMMSE algorithm with reduced computational complexity.
arXiv Detail & Related papers (2020-06-15T02:57:57Z) - 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.