Model Checking Strategies from Synthesis Over Finite Traces
- URL: http://arxiv.org/abs/2305.08319v3
- Date: Sun, 30 Jul 2023 19:44:20 GMT
- Title: Model Checking Strategies from Synthesis Over Finite Traces
- Authors: Suguman Bansal and Yong Li and Lucas Martinelli Tabajara and Moshe Y.
Vardi and Andrew Wells
- Abstract summary: 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.
- Score: 25.871354900295056
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The innovations in reactive synthesis from {\em Linear Temporal Logics over
finite traces} (LTLf) will be amplified by the ability to verify the
correctness of the strategies generated by LTLf synthesis tools. This motivates
our work on {\em LTLf model checking}. LTLf model checking, however, is not
straightforward. The strategies generated by LTLf synthesis may be represented
using {\em terminating} transducers or {\em non-terminating} transducers where
executions are of finite-but-unbounded length or infinite length, respectively.
For synthesis, there is no evidence that one type of transducer is better than
the other since they both demonstrate the same complexity and similar
algorithms.
In this work, we show that for model checking, the two types of transducers
are fundamentally different. Our central result is that LTLf model checking of
non-terminating transducers is \emph{exponentially harder} than that of
terminating transducers. We show that the problems are EXPSPACE-complete and
PSPACE-complete, respectively. Hence, considering the feasibility of
verification, LTLf synthesis tools should synthesize terminating transducers.
This is, to the best of our knowledge, the \emph{first} evidence to use one
transducer over the other in LTLf synthesis.
Related papers
- 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) - Unlock the Correlation between Supervised Fine-Tuning and Reinforcement Learning in Training Code Large Language Models [12.656574142412484]
We make an attempt to understand the correlation between supervised fine-tuning and reinforcement learning.
We find that both atomic and synthetic functions are indispensable for SFT's generalization.
arXiv Detail & Related papers (2024-06-14T03:39:01Z) - SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
We study the synthesis of six datasets, covering topic classification, sentiment analysis, tone detection, and humor.
We find that SynthesizRR greatly improves lexical and semantic diversity, similarity to human-written text, and distillation performance.
arXiv Detail & Related papers (2024-05-16T12:22:41Z) - 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) - Exposing Attention Glitches with Flip-Flop Language Modeling [55.0688535574859]
This work identifies and analyzes the phenomenon of attention glitches in large language models.
We introduce flip-flop language modeling (FFLM), a family of synthetic benchmarks designed to probe the extrapolative behavior of neural language models.
We find that Transformer FFLMs suffer from a long tail of sporadic reasoning errors, some of which we can eliminate using various regularization techniques.
arXiv Detail & Related papers (2023-06-01T17:44:35Z) - 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) - Learning Bounded Context-Free-Grammar via LSTM and the
Transformer:Difference and Explanations [51.77000472945441]
Long Short-Term Memory (LSTM) and Transformers are two popular neural architectures used for natural language processing tasks.
In practice, it is often observed that Transformer models have better representation power than LSTM.
We study such practical differences between LSTM and Transformer and propose an explanation based on their latent space decomposition patterns.
arXiv Detail & Related papers (2021-12-16T19:56:44Z) - 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) - Synthesizer: Rethinking Self-Attention in Transformer Models [93.08171885200922]
dot product self-attention is central and indispensable to state-of-the-art Transformer models.
This paper investigates the true importance and contribution of the dot product-based self-attention mechanism on the performance of Transformer models.
arXiv Detail & Related papers (2020-05-02T08:16:19Z) - 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)
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.