Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 9 of 9 for “"monadic second-order logic"”.
-
Weighted Logics and Weighted Simple Automata for Context-Free Languages of Infinite Words
… provided a seminal connection between monadic second-order logic and finite automata for both finite and infinite words. This BET- Theorem has been extended by Lautemann, Schwentick and Thérien to context-free languages by introducing a monadic second-order logic with an additional …
-
Easy instances for model checking
… intimately related to the expressibility of the logical language in question. We investigate the parameterized complexity of queries expressible in monadic second order logic over tree-like structures (structures with bounded tree-width) and first order logic over locally tree-like structures. …
-
Modular data structure verification
… write Jahob specifications in classical higher-order logic (HOL); Jahob reduces the verification problem to deciding the validity of HOL formulas. I present a new method for proving HOL formulas by combining automated reasoning techniques. My method consists of 1) splitting formulas into …
-
Expressiveness and Decidability of Weighted Automata and Weighted Logics
… regular grammars, regular expressions, and monadic second order (MSO) logic. To increase expressiveness, the fundamental idea underlying finite automata and regular languages was also extended to describe not only languages of strings, or words, but also of infinite words by Büchi and …
-
Finite automata on unranked trees : extensions by arithmetical and equality constraints
… documents. In particular, several automata and logic formalisms on unranked trees have been considered (again) in the literature, and many results that had previously been shown for the ranked-tree setting have turned out to hold for the unranked-tree setting as well. In this thesis, we study …
-
Automata-based decision procedures for weak arithmetics
… <br>arithmetic. A prominent example is the weak monadic second-order logic <br>of one successor, WS1S for short, which is tightly connected to <br>automata over finite words. Nowadays, automata have also emerged as a <br>tool for effectively mechanizing decision procedures for such logical …
-
Structures of bounded partition width
… present thesis we study the question of which monadic theories are simple. In particular, we are looking for theories that are decidable or at least simple enough that we are able to derive structure theorems. We propose to draw the line between simple and complicated theories by defining that …
-
Logic and games on automatic structures
The evaluation of a logical formula can be viewed as a game played by two opponents, one trying to show that the formula is true and the other trying to prove it false. This correspondence is exploited algorithmically to evaluate formulas of first and second-order logic on finite structures. We …
-
Automatic techniques for proving correctness of heap-manipulating programs
… verification. This dissertation presents two logic-based automatic software verification systems, namely Strand and Dryad, that help in the task of verification of heap-manipulating programs, which is one of the most complex aspects of modern software that eludes automatic verification. Strand …