scholarly journals “Most of” leads to undecidability: Failure of adding frequencies to LTL

2021 ◽  
pp. 82-101
Author(s):  
Bartosz Bednarczyk ◽  
Jakub Michaliszyn
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Statistical Reasoning ◽  
First Order ◽  
High Interest ◽  
The Past ◽  
Influence Networks

AbstractLinear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that $$\sigma $$ σ is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and discuss how the undecidability results transfer to first-order logic on words.

scholarly journals First-Order Logic with Two Variables and Unary Temporal Logic

1997 ◽  
Vol 4 (5) ◽  
Author(s):  
Kousha Etessami ◽  
Moshe Y. Vardi ◽  
Thomas Wilke
Keyword(s):  
Computational Complexity ◽  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Model Property ◽  
First Order ◽  
The Past ◽  
Small Model ◽  
Input Formula

We investigate the power of first-order logic with only two variables over<br />omega-words and finite words, a logic denoted by FO2. We prove that FO2 can<br />express precisely the same properties as linear temporal logic with only the unary temporal operators: “next”, “previously”, “sometime in the future”, and “sometime in the past”, a logic we denote by unary-TL. Moreover, our translation from FO2 to unary-TL converts every FO2 formula to an equivalent unary-TL formula that is at most exponentially larger, and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is optimal.<br />While satisfiability for full linear temporal logic, as well as for<br />unary-TL, is known to be PSPACE-complete, we prove that satisfiability<br />for FO2 is NEXP-complete, in sharp contrast to the fact that satisfiability<br />for FO3 has non-elementary computational complexity. Our NEXP time<br />upper bound for FO2 satisfiability has the advantage of being in terms of<br />the quantifier depth of the input formula. It is obtained using a small model property for FO2 of independent interest, namely: a satisfiable FO2 formula has a model whose “size” is at most exponential in the quantifier depth of the formula. Using our translation from FO2 to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.

A review of temporal logics

1989 ◽  
Vol 4 (2) ◽  
pp. 141-162 ◽  
Author(s):  
Derek Long
Keyword(s):  
Artificial Intelligence ◽  
Temporal Logic ◽  
Temporal Reasoning ◽  
Order Logic ◽  
First Order Logic ◽  
Temporal Logics ◽  
Detailed Review ◽  
First Order ◽  
Reasoning Tasks

AbstractA series of temporal reasoning tasks are identified which motivate the consideration and application of temporal logics in artificial intelligence. There follows a discussion of the broad issues involved in modelling time and constructing a temporal logic. The paper then presents a detailed review of the major approaches to temporal logics: first-order logic approaches, modal temporal logics and reified temporal logics. The review considers the most significant exemplars within the various approaches, including logics due to Russell, Hayes and McCarthy, Prior, McDermott, Allen, Kowalski and Sergot. The logics are compared and contrasted, particularly in their treatments of change and action, the roles they seek to fulfil and the underlying models of time on which they rest. The paper concludes with a brief consideration of the problem of granularity—a problem of considerable significance in temporal reasoning, which has yet to be satisfactorily treated in a temporal logic.

Model Checking Software with First Order Logic Specifications Using AIG Solvers

2016 ◽  
Vol 42 (8) ◽  
pp. 741-763 ◽  
Author(s):  
Mohammad A. Noureddine ◽  
Fadi A. Zaraket
Keyword(s):  
Model Checking ◽  
Order Logic ◽  
First Order Logic ◽  
First Order

scholarly journals Modular specification and verification of closures in Rust

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Fabian Wolff ◽  
Aurel Bílý ◽  
Christoph Matheja ◽  
Peter Müller ◽  
Alexander J. Summers
Keyword(s):  
Formal Verification ◽  
Functional Properties ◽  
Type System ◽  
Order Logic ◽  
First Order Logic ◽  
Formal Reasoning ◽  
First Order ◽  
Novel Technique ◽  
Smt Solvers ◽  
Specification And Verification

Closures are a language feature supported by many mainstream languages, combining the ability to package up references to code blocks with the possibility of capturing state from the environment of the closure's declaration. Closures are powerful, but complicate understanding and formal reasoning, especially when closure invocations may mutate objects reachable from the captured state or from closure arguments. This paper presents a novel technique for the modular specification and verification of closure-manipulating code in Rust. Our technique combines Rust's type system guarantees and novel specification features to enable formal verification of rich functional properties. It encodes higher-order concerns into a first-order logic, which enables automation via SMT solvers. Our technique is implemented as an extension of the deductive verifier Prusti, with which we have successfully verified many common idioms of closure usage.

An Overview of VV&A Methods for Conceptual Model

2013 ◽  
Vol 444-445 ◽  
pp. 860-864
Author(s):  
Xiao Jian Ding ◽  
Feng Xin Sun
Keyword(s):  
Petri Nets ◽  
Formal Verification ◽  
Conceptual Model ◽  
Conceptual Modeling ◽  
Order Logic ◽  
Model Verification ◽  
First Order Logic ◽  
Verification Method ◽  
First Order ◽  
Formal Techniques

This paper summarizes the literature and presents important concepts related to conceptual model verification. Different approaches have been proposed in the literature. These approaches have been introduced as two parts with emphasis on formal techniques. First order logic for structural views and Petri nets for behavioral views are investigated in the search of a practical verification method for conceptual modeling in UML. Then a short assessment of formal verification work for UML will be presented.

scholarly journals First-Order Logic with Two Variables and Unary Temporal Logic

2002 ◽  
Vol 179 (2) ◽  
pp. 279-295 ◽  
Author(s):  
Kousha Etessami ◽  
Moshe Y. Vardi ◽  
Thomas Wilke
Keyword(s):  
Temporal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order

AUTOMATED TERMINATION IN MODEL-CHECKING MODULO THEORIES

2013 ◽  
Vol 24 (02) ◽  
pp. 211-232 ◽  
Author(s):  
ALESSANDRO CARIONI ◽  
SILVIO GHILARDI ◽  
SILVIO RANISE
Keyword(s):  
Model Checking ◽  
Sufficient Conditions ◽  
Order Logic ◽  
Satisfiability Modulo Theories ◽  
First Order Logic ◽  
Reachability Problem ◽  
First Order ◽  
Recent Advances ◽  
Infinite State Systems ◽  
Infinite State

We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic.

scholarly journals Approximate Model Checking Using a Subset of First-order Logic

2010 ◽  
Vol 3 ◽  
pp. 268-282 ◽  
Author(s):  
Kiyoharu Hamaguchi ◽  
Kazuya Masuda ◽  
Toshinobu Kashiwabara
Keyword(s):  
Model Checking ◽  
Approximate Model ◽  
Order Logic ◽  
First Order Logic ◽  
First Order
Sign in / Sign up

Export Citation Format

Share Document