Equivalencia de tartamudeo

En informática teórica , equivalencia de tartamudeo , ^[1] una relación escrita como

Los caminos y son tartamudeando equivalentemente. ${\displaystyle \pi }$ ${\displaystyle \pi '}$

${\displaystyle \pi \sim _{st}\pi '}$,

puede verse como una partición de rutas y bloques, de modo que los estados en el bloque de una ruta se etiquetan ( ) de la misma manera que los estados en el bloque de la otra ruta. Los bloques correspondientes pueden tener longitudes diferentes. ${\displaystyle \pi }$ ${\displaystyle \pi '}$ ${\displaystyle k^{\mathrm {th} }}$ ${\displaystyle L(\cdot )}$ ${\displaystyle k^{\mathrm {th} }}$

Formalmente, esto se puede expresar como dos caminos infinitos y siendo tartamudeantemente equivalente ( ) si hay dos secuencias infinitas de números enteros y tales que para cada bloque se cumple . ${\displaystyle \pi =s_{0},s_{1},\ldots }$ ${\displaystyle \pi '=r_{0},r_{1},\ldots }$ ${\displaystyle \pi \sim _{st}\pi '}$ ${\displaystyle 0=i_{0}<i_{1}<i_{2}<\ldots }$ ${\displaystyle 0=j_{0}<j_{1}<j_{2}<\ldots }$ ${\displaystyle k\geq 0}$ ${\displaystyle L(s_{i_{k}})=L(s_{i_{k}+1})=\ldots =L(s_{i_{k+1}-1})=L(r_{j_{k}})=L(r_{j_{k}+1})=\ldots =L(r_{j_{k+1}-1})}$

La equivalencia por tartamudeo no es lo mismo que la bisimulación , ya que la bisimulación no puede capturar la semántica del operador 'eventualmente' (o 'finalmente') que se encuentra en la lógica de árbol de cálculo / temporal lineal (lógica de tiempo ramificado) ( lógica modal ). Se debe utilizar la denominada bisimulación ramificada . ^{[ cita requerida ]}

Referencias

1. Groote, Jan Friso; Vaandrager, Frits W. (1990). "Un algoritmo eficiente para la bisimulación de ramificación y la equivalencia entre parpadeos" . En Paterson, Michael S. (ed.). Actas del 17.º Coloquio Internacional sobre Autómatas, Lenguajes y Programación. Lecture Notes in Computer Science . Vol. 443. Springer-Verlag . págs. 626–638. doi :10.1007/BFb0032063. ISBN. 0-387-52826-1.