Equivalencia de tartamudeo

En la ciencia teórica de la computación , la equivalencia de tartamudeo , ^{[ 1 ]} una relación escrita como

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

puede verse como una partición de caminos${\displaystyle \pi }$y${\displaystyle \pi '}$en bloques, de modo que los estados en el${\displaystyle k^{\mathrm {th} }}$Los bloques de una ruta están etiquetados (${\displaystyle L(\cdot )}$) lo mismo que los estados en el${\displaystyle k^{\mathrm {th} }}$bloque del otro camino. Los bloques correspondientes pueden tener longitudes diferentes.

Formalmente, esto se puede expresar como dos caminos infinitos.${\displaystyle \pi =s_{0},s_{1},\ldots }$y${\displaystyle \pi '=r_{0},r_{1},\ldots }$ser tartamudo equivalente (${\displaystyle \pi \sim _{st}\pi '}$) si hay dos secuencias infinitas de enteros${\displaystyle 0=i_{0}<i_{1}<i_{2}<\ldots }$y${\displaystyle 0=j_{0}<j_{1}<j_{2}<\ldots }$de tal manera que para cada bloque${\displaystyle k\geq 0}$sostiene${\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 de tartamudeo no es lo mismo que la bisimulación , ya que esta última no puede capturar la semántica del operador «eventualmente» (o «finalmente») presente en la lógica de árbol temporal lineal / de computación (lógica temporal ramificada) ( lógica modal ). Por lo tanto , debe utilizarse la denominada bisimulación ramificada .