Заикающаяся эквивалентность

В информатике теоретической заикающаяся эквивалентность , отношение , записанное как

Пути $\pi$ и $\pi '$ эквивалентны заиканию.

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

можно рассматривать как разделение путей $\pi$ и $\pi '$ на блоки, так что состояния в $k^{\mathrm {th} }$ блок одного пути помечен ( $L(\cdot )$) то же, что и состояния в $k^{\mathrm {th} }$ блок другого пути. Соответствующие блоки могут иметь разную длину.

Формально это можно выразить как два бесконечных пути $\pi =s_{0},s_{1},\ldots$ и $\pi '=r_{0},r_{1},\ldots$ эквивалент заикания ( $\pi \sim _{st}\pi '$), если существуют две бесконечные последовательности целых чисел $0=i_{0}<i_{1}<i_{2}<\ldots$ и $0=j_{0}<j_{1}<j_{2}<\ldots$ такой, что для каждого блока $k\geq 0$ держит $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})$.

Заикающаяся эквивалентность — это не то же самое, что бисимуляция , поскольку бисимуляция не может уловить семантику оператора «в конечном итоге» (или «наконец»), обнаруженного в линейной логике временного / вычислительного дерева (логика времени ветвления) ( модальная логика ). так называемую ветвящуюся бисимуляцию . Необходимо использовать