Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Computability of Measures of Regular Sets of Infinite Trees

Damian Niwiński, Paweł Parys, Michał Skrzypczak

TL;DR

This work shows how to compute the probability that a randomly chosen tree satisfies a given formula, and additionally shows that this probability is an algebraic number.

Abstract

The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where similar results were shown for formalisms weaker than the full monadic second-order logic.

On the Computability of Measures of Regular Sets of Infinite Trees

TL;DR

This work shows how to compute the probability that a randomly chosen tree satisfies a given formula, and additionally shows that this probability is an algebraic number.

Abstract

The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where similar results were shown for formalisms weaker than the full monadic second-order logic.
Paper Structure (32 sections, 51 theorems, 125 equations, 1 figure)

This paper contains 32 sections, 51 theorems, 125 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Basic concepts
  3. Fixed-point approach
  4. Non-emptiness for nondeterministic automata
  5. Unary mu-calculus
  6. Computing measure
  7. Profiles
  8. Alternating automata
  9. Unary mu-calculus
  10. Intensional definition
  11. Computing limits
  12. A type system
  13. Basic functions
  14. Functions in Vd
  15. Invariants
  16. ...and 17 more sections

Key Result

Theorem 1.2

There is an algorithm that inputs a nondeterministic parity tree automaton $\mathcal{A}\xspace$ and computes the coin/̄flipping measure of the language of trees recognised by $\mathcal{A}\xspace$. Moreover, this measure is an algebraic number.

Figures (1)

  • Figure 13.1: An illustration of the function $F_r$, for $r\in R$. The first subtree, denoted $t'$, is used to determine $(a,r_1,\dots,r_s)$ as $e_{\theta(r)}(t')$. This $a$ goes to the label of the root, while states $s_i$ together with subtrees denoted $t_i$ are used to recursively define subtrees attached below the root. Labels in the remaining part of the input tree $t$ are irrelevant for the construction of $F_r(t)$.

Theorems & Definitions (106)

  • Theorem 1.2
  • Corollary 1.3
  • Lemma 4.1
  • proof
  • Proposition 4.2
  • Remark 4.4
  • Lemma 5.1
  • Definition 5.2
  • Lemma 5.3
  • proof
  • ...and 96 more