Бисимуляция заикания

В теоретической информатике бисимуляция заикания — это связь между двумя переходными системами , абстрактными машинами, моделирующими вычисления. Оно определяется коиндуктивно и обобщает идею бисимуляций . Бисимуляция сопоставляет состояния машины так, чтобы переходы соответствовали друг другу; бисимуляция заикания позволяет сопоставить переходы с конечными фрагментами пути. ^[1]

Определение

В «Принципах проверки моделей » Байер и Катоен определяют бисимуляцию заикания для одной системы переходов, а затем адаптируют ее к отношению в двух системах переходов. Бисимуляция заикания для ${\text{TS}}=(S,{\text{Act}},\to ,I,{\text{AP}},L)$ — это бинарное отношение R на S всех ( s1 _{что для} , s2 _{такое ,} ) в R :

$s_{1},s_{2}$ имеют одинаковые этикетки
Если $s_{1}\to s_{1}'$ является допустимым переходом и $(s_{1}',s_{2})\not \in R$ тогда существует конечный фрагмент пути $s_{2}u_{1}\cdots u_{n}s_{2}'$ ( $n\geq 0$ ) такой, что каждая пара $(s_{1},u_{i})$ находится в R и $(s_{1}',s_{2}')$ находится в Р
Если $s_{2}\to s_{2}'$ является допустимым переходом и $(s_{1},s_{2}')\not \in R$ нет, то существует конечный фрагмент пути $s_{1}v_{1}\cdots v_{n}s_{1}'$ ( $n\geq 0$ ) такой, что каждая пара $(v_{i},s_{2})$ находится в R и $(s_{1}',s_{2}')$ находится в Р

Обобщения

Обобщение, бисимуляция дивергентного заикания, может использоваться для упрощения пространства состояний системы с компромиссом, заключающимся в том, что утверждения, использующие оператор линейной временной логики «следующий», могут изменить значение истинности. ^[2] Надежная бисимуляция заикания допускает неопределенность в отношении переходов в системе. ^[3]

Ссылки

^ Принципы проверки моделей (страницы 536–580), Кристель Байер и Йост-Питер Катоен , MIT Press, Кембридж, Массачусетс.
^ «Абстракция бисимуляции дивергентного заикания для синтеза контроллера со спецификациями линейной временной логики». Автоматика . 130 . 2021. doi : 10.1016/j.automatica.2021.109723 . hdl : 10289/14366 .
^ «Надежная бисимуляция заикания для абстракции и синтеза контроллера с возмущениями» . Автоматика . 160 . 2024. дои : 10.1016/j.automatica.2023.111394 .

Эта по информатике статья незавершена . Вы можете помочь Википедии, расширив ее .

[1] Принципы проверки моделей (страницы 536–580), Кристель Байер и Йост-Питер Катоен , MIT Press, Кембридж, Массачусетс.

[2] «Абстракция бисимуляции дивергентного заикания для синтеза контроллера со спецификациями линейной временной логики». Автоматика . 130 . 2021. doi : 10.1016/j.automatica.2021.109723 . hdl : 10289/14366 .

[3] «Надежная бисимуляция заикания для абстракции и синтеза контроллера с возмущениями» . Автоматика . 160 . 2024. дои : 10.1016/j.automatica.2023.111394 .

[1]

[2]

[3]