Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I tried to define a translation from LTL to ω-regular languages. I built it inductively on the structure of LTL formulae. No problem except with the 'until' operator where I came up with the expression:

$$ L_\omega(f \mathbf{U} g) = \bigcup_{k\ge 0} \biggl( \bigl(\bigcap_{0\le j\le k-1} \Sigma^j L_\omega(f)\bigr) \cap \Sigma^k L_\omega(g) \biggr) $$

where $L_\omega(f)$, $L_\omega(g)$ are $\omega$-regular, $\Sigma^j$ is a symbol from $\Sigma$ repeated $j$ times (where $\Sigma$ is the set of language symbols). The problem with this expression is that it is a countable union of $\omega$-regular languages. Are $\omega$-regular languages closed under countable union? (reference to a proof). Otherwise, can somebody suggest another expression (I tried also a recursive expression based on the identity $f \cup g = g \vee (f \wedge O(f \cup g))$ but then the same question with respect to recursive expressions?

share|improve this question
    
Note that for computer science questions, you may have better luck on Computer Science. –  Gilles Dec 25 '13 at 21:40

1 Answer 1

Given a word $u \in \Sigma^\omega$, write $u_n$ for its $n$th symbol and $\bar u_n$ for its prefix of length $n$. Let $u \in \Sigma^\omega$ be an arbitrary word. $$ \bigcap_{n\in\mathbb{N}} \{\bar u_n\}\Sigma^\omega = \{v \mid \forall i \le n, v_i = u_i\} = \{u\} $$ Thus an arbitrary word can be expressed as a countable intersection of $\omega$-regular languages. (This is similar to expressing a real number as the limit of its expansion in base $|\Sigma|$.) There are uncountably many words in $\Sigma^\omega$, but only countably many $\omega$-regular languages since there are only countably many Büchi automata to recognize them. Therefore countable intersections of $\omega$-regular are not always (indeed almost never) $\omega$-regular. Since $\omega$-regular languages are closed under complementation, the same goes for countable unions.

In any case, you won't be able to find such a translation, because LTL is not quite as expressive as Büchi automata: there are $\omega$-regular properties that cannot be defined in LTL. Extensions of LTL have been proposed that can express all $\omega$-regular properties. See Temporal Logic can be more expressive, Pierre Wolper, Information and Computation, 1983. (via Vijay D in Equivalence of Büchi automata and linear μ\mu-calculus on Computer Science Stack Exchange)

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.