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
- LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces [44.35335751462176]
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.
arXiv Detail & Related papers (2024-11-14T11:17:06Z) - Training Nonlinear Transformers for Chain-of-Thought Inference: A Theoretical Generalization Analysis [82.51626700527837]
Chain-of-shift (CoT) is an efficient method that enables the reasoning ability of large language models by augmenting the query using examples with multiple intermediate steps.
We show that despite the theoretical success of CoT, it fails to provide an accurate generalization when CoT does.
arXiv Detail & Related papers (2024-10-03T03:12:51Z) - 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) - 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) - 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) - 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.