Tiempo para construir un GNBA para la fórmula LTL

Question

Tengo un problema con la prueba para la construcción de un GNBA ( generalizada no determinista Büchi autómata ) para un LTL fórmula :

Teorema: Para cualquier fórmula LTL $ \ varphi $ existe una GNBA $ G _ {\ varphi} $ sobre alfabeto $ 2 ^ {AP} $ tal que:

1. $ \ operatorname {Palabra} (\ varphi) = L _ {\ omega} (G _ {\ varphi}) $.

2. $ G _ {\ varphi} $ se puede costructed en el tiempo y en el espacio $ 2 ^ {O (| \ phi |)} $, donde $ | \ phi |. $ Es el tamaño de $ \ phi $

3. El número de estados de aceptación de $ G _ {\ varphi} $ está acotado superiormente por $ O (| \ phi |). $

Mi problema radica en la demostración de (2), es decir, en la prueba que dice que el número de estados en $ G _ {\ varphi} $ está delimitada por $ 2 ^ {| \ operatorname {Subf} (\ varphi ) |} $ pero desde $ | \ operatorname {Subf} (\ varphi) | \ Leq 2 \ cdot | \ phi | $ (donde $ \ operatorname {Subf} (\ varphi) $ es el conjunto de todas las fórmulas parciales) el número de estados es limitado por $ 2 ^ {O (| \ phi |)} $.

Pero ¿por qué $ | \ operatorname {Subf} (\ varphi) | \ Leq 2 \ cdot | \ phi | $ bodega?

Answer 1

En, fórmulas lógicas generales puede ser pensado como árboles; nodos internos son los operadores y las hojas son proposiciones atómicas. Por lo tanto, cada fórmula consta de como subfórmulas directa muchos (que está en el primer nivel) como su parte superior-más aridad del operador. Por ejemplo,

$ \ qquad \ phi \ tierra \ psi $

tiene dos fórmulas parciales directa $ \ phi $ y $ \ psi $. Esto se puede continuar de forma recursiva y vemos que

$ \ qquad \ displaystyle | \ operatorname {Subf} (\ varphi) | \ Leq \ sum _ {\ circ \ en \ operatorname {op} (\ phi)} \ operatorname {aridad} (\ circ) $,

donde $ \ operatorname {op} (\ varphi) $ es el multi-conjunto de operadores que ocurren en $ \ phi $. Informalmente hablando, todos los operadores de sus operandos contribuye al conjunto de fórmulas parciales. Tenga en cuenta que tenemos $ \ leq $ no $ = $ debido a que una subfórmula puede aparecer varias veces.

En LTL, todos los operadores tienen como máximo aridad dos, por lo que $ | \ operatorname {Subf} (\ varphi) | \ Leq 2 | \ phi | $ $, siempre que |. |. $ Recuentos (por lo menos) ocurrencias operador