scholarly journals Verified decision procedures for MSO on words based on derivatives of regular expressions

2015 ◽  
Vol 25 ◽  
Author(s):  
DMITRIY TRAYTEL ◽  
TOBIAS NIPKOW
Keyword(s):  
Code Generation ◽  
Decision Procedures ◽  
Theorem Prover ◽  
Regular Expressions ◽  
Data Types ◽  
Regular Structures ◽  
Derivatives Of ◽  
Second Order Logic ◽  
Generation Facility ◽  
Monadic Second Order Logic

AbstractMonadic second-order logic on finite words is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of some regular structures (e.g., automata). This paper presents a verified functional decision procedure for MSO formulas that is not based on automata but on regular expressions. Functional languages are ideally suited for this task: regular expressions are data types and functions on them are defined by pattern matching and recursion and are verified by structural induction. Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions, an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO. Our results have been formalized and verified in the theorem prover Isabelle. Using Isabelle's code generation facility, this yields purely functional, formally verified programs that decide equivalence of MSO formulas.

scholarly journals Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications

2019 ◽  
Author(s):  
Jakub Michaliszyn ◽  
Piotr Witkowski
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Order Logic ◽  
Regular Expressions ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Interval Temporal Logic ◽  
Multi Agent ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Epistemic Halpern-Shoham logic (EHS) is an interval temporal logic defined to verify properties of Multi-Agent Systems. In this paper we show that the model checking Multi-Agent Systems with regular expressions against the EHS specifications is decidable. We achieve this by reducing the model checking problem to the satisfiability problem of Monadic Second-Order Logic on trees.

scholarly journals Symbolic WS1S

10.29007/t28j ◽  
2018 ◽  
Author(s):  
Loris D'Antoni ◽  
Margus Veanes
Keyword(s):  
Blow Up ◽  
Finite Automata ◽  
Decision Procedures ◽  
Second Order ◽  
Order Logic ◽  
Symbolic Logic ◽  
First Order ◽  
Symbolic Automata ◽  
Second Order Logic ◽  
Monadic Second Order Logic

We extend weak monadic second-order logic of one successor (WS1S) to symbolic alphabets byallowing character predicates to range over decidable first order theories and not just finite alphabets.We call this extension symbolic WS1S (s-WS1S). We then propose two decision procedures for such alogic: 1) we use symbolic automata to extend the classic reduction from WS1S to finite automata toour symbolic logic setting; 2) we show that every s-WS1S formula can be reduced to a WS1S formulathat preserves satisfiability, at the price of an exponential blow-up.

scholarly journals HEINRICH BEHMANN’S 1921 LECTURE ON THE DECISION PROBLEM AND THE ALGEBRA OF LOGIC

2015 ◽  
Vol 21 (2) ◽  
pp. 164-187 ◽  
Author(s):  
PAOLO MANCOSU ◽  
RICHARD ZACH
Keyword(s):  
English Translation ◽  
Decision Problem ◽  
Axiomatic Approach ◽  
Decision Procedures ◽  
Second Order ◽  
Order Logic ◽  
David Hilbert ◽  
Second Order Logic ◽  
Monadic Second Order Logic

AbstractHeinrich Behmann (1891–1970) obtained his Habilitation under David Hilbert in Göttingen in 1921 with a thesis on the decision problem. In his thesis, he solved—independently of Löwenheim and Skolem’s earlier work—the decision problem for monadic second-order logic in a framework that combined elements of the algebra of logic and the newer axiomatic approach to logic then being developed in Göttingen. In a talk given in 1921, he outlined this solution, but also presented important programmatic remarks on the significance of the decision problem and of decision procedures more generally. The text of this talk as well as a partial English translation are included.

scholarly journals Verification of Pointers

1994 ◽  
Vol 23 (470) ◽  
Author(s):  
Nils Klarlund ◽  
Michael I. Schwartzbach
Keyword(s):  
Programming Languages ◽  
Future Research ◽  
Hoare Logic ◽  
Data Types ◽  
Type Checking ◽  
State Spaces ◽  
Global Properties ◽  
Finite State ◽  
Second Order Logic ◽  
Monadic Second Order Logic

<p>Our recent work links type checking in programming languages to verification based on automata. In this survey, we give an overview of our methods and suggest directions for future research.</p><p> </p><p>In our approach, we view data types as invariants and devise a logical and decidable framework for expressing global properties of a store consisting of records and pointers.</p><p>We can express common properties, for example about doubly-linked lists and their algorithms. Such properties seemed to have called for a full Hoare logic beyond the reach of type checking and decidability.</p><p> </p><p>Our work is based on monadic second-order logic. Thus verification boils down to calculations on finite-state automata. This raises specific questions about combinatorial techniques for representing state spaces if these calculations are ever to be carried out on more than simple examples.</p>

scholarly journals The Lean 4 Theorem Prover and Programming Language

2021 ◽  
pp. 625-635
Author(s):  
Leonardo de Moura ◽  
Sebastian Ullrich
Keyword(s):  
Programming Language ◽  
Code Generation ◽  
Decision Procedures ◽  
Theorem Prover ◽  
Code Generator ◽  
Proof Automation ◽  
Significant Performance ◽  
Efficient Code ◽  
Tabled Resolution ◽  
New System

AbstractLean 4 is a reimplementation of the Lean interactive theorem prover (ITP) in Lean itself. It addresses many shortcomings of the previous versions and contains many new features. Lean 4 is fully extensible: users can modify and extend the parser, elaborator, tactics, decision procedures, pretty printer, and code generator. The new system has a hygienic macro system custom-built for ITPs. It contains a new typeclass resolution procedure based on tabled resolution, addressing significant performance problems reported by the growing user base. Lean 4 is also an efficient functional programming language based on a novel programming paradigm called functional but in-place. Efficient code generation is crucial for Lean users because many write custom proof automation procedures in Lean itself.

The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

2021 ◽  
Vol 178 (1-2) ◽  
pp. 1-30
Author(s):  
Florian Bruse ◽  
Martin Lange ◽  
Etienne Lozes
Keyword(s):  
Model Checking ◽  
Lower Bounds ◽  
Expressive Power ◽  
Higher Order ◽  
Order Logic ◽  
High Complexity ◽  
Transition Systems ◽  
Recursive Formulas ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal μ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most k < 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k − 1)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

scholarly journals Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

2021 ◽  
Vol 22 (2) ◽  
pp. 1-37
Author(s):  
Christopher H. Broadbent ◽  
Arnaud Carayol ◽  
C.-H. Luke Ong ◽  
Olivier Serre
Keyword(s):  
Model Checking ◽  
Free Variable ◽  
Higher Order ◽  
Second Order ◽  
Effective Solution ◽  
Parity Games ◽  
Transition Graphs ◽  
Second Order Logic ◽  
Pushdown Automata ◽  
Monadic Second Order Logic

This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

Sign in / Sign up

Export Citation Format

Share Document