Transforming structures by set interpretations

Abstract

We consider a new kind of interpretation over relational structures: finite sets interpretations. Those interpretations are defined by weak monadic second-order (WMSO) formulas with free set variables. They transform a given structure into a structure with a domain consisting of finite sets of elements of the orignal structure. The definition of these interpretations directly implies that they send structures with a decidable WMSO theory to structures with a decidable first-order theory. In this paper, we investigate the expressive power of such interpretations applied to infinite deterministic trees. The results can be used in the study of automatic and tree-automatic structures.

36 pages

Cited by in corpus (12)

• MontiArc - Architectural Modeling of Interactive Distributed and Cyber-Physical Systems
• A Myhill-Nerode theorem for automata with advice
• Regular Abstractions for Array Systems
• Generating collection transformations from proofs
• Boundedness in languages of infinite words
• Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
• Compatibility of Shelah and Stupp's and Muchnik's iteration with fragments of monadic second order logic
• Unfolding of Finite Concurrent Automata
• Automatic structures of bounded degree revisited
• Regular Model Checking Revisited (Technical Report)
• Probabilistic Bisimulation for Parameterized Systems (Technical Report)
• Complexity Analysis of Tree Share Structure