Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
В теоретической информатике бисимуляция — это бинарное отношение между системами переходов состояний, связывающее системы, которые ведут себя одинаково, в том смысле, что одна система моделирует поведение другой и наоборот. Интуитивно, две системы бисимилярны, если, рассматривая их как игру по определенным правилам, они соответствуют ходам друг друга. В этом смысле ни одна из систем не может быть различима для наблюдателя.
Relation between transition systems in computer science
In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa. Intuitively two systems are bisimilar if they, assuming we view them as playing a game according to some rules, match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer.
Варианты бисимуляции
В особых контекстах понятие бисимуляции иногда уточняется добавлением дополнительных требований или ограничений. Примером является бисимуляция с повторами, при которой один переход одной системы может соответствовать нескольким переходам другой, при условии, что промежуточные состояния эквивалентны начальному состоянию ("повторы"). Другой вариант применяется, если система переходов состояний включает понятие невидимого (или внутреннего) действия, часто обозначаемого как , то есть действия, которые не наблюдаются внешними наблюдателями, тогда бисимуляцию можно ослабить до слабой бисимуляции, в которой, если два состояния и являются бисимильными, и существует некоторое количество внутренних действий, ведущих из в некоторое состояние , то должно существовать состояние , такое что существует некоторое количество (возможно, нулевое) внутренних действий, ведущих из в . Отношение на процессах является слабой бисимуляцией, если выполняется следующее (где и являются наблюдаемым и невидимым переходом соответственно):
In special contexts the notion of bisimulation is sometimes refined by adding additional requirements or constraints. An example is that of stutter bisimulation, in which one transition of one system may be matched with multiple transitions of the other, provided that the intermediate states are equivalent to the starting state ("stutters"). A different variant applies if the state transition system includes a notion of silent (or internal) action, often denoted with , i. e. actions that are not visible by external observers, then bisimulation can be relaxed to be weak bisimulation, in which if two states and are bisimilar and there is some number of internal actions leading from to some state then there must exist state such that there is some number (possibly zero) of internal actions leading from to A relation on processes is a weak bisimulation if the following holds (with , and being an observable and mute transition respectively):
Это тесно связано с понятием бисимуляции "с точностью до" отношения. Как правило, если система переходов состояний задает операционную семантику языка программирования, то точное определение бисимуляции будет специфично для ограничений этого языка программирования. Поэтому, в общем случае, может существовать более одного типа отношения бисимуляции (соответственно, бисимилярности) в зависимости от контекста.
This is closely related to the notion of bisimulation "up to" a relation. Typically, if the state transition system gives the operational semantics of a programming language, then the precise definition of bisimulation will be specific to the restrictions of the programming language. Therefore, in general, there may be more than one kind of bisimulation (respectively bisimilarity) relationship depending on the context.
Бисимуляция и модальная логика
Поскольку модели Крипке являются частным случаем (обозначенных) систем переходов состояний, бисимуляция также является темой, изучаемой в модальной логике. Фактически, модальная логика – это фрагмент логики первого порядка, инвариантный относительно бисимуляции (теорема ван Бентема).
Since Kripke models are a special case of (labelled) state transition systems, bisimulation is also a topic in modal logic. In fact, modal logic is the fragment of first order logic invariant under bisimulation (van Benthem's theorem).
Алгоритм
Проверка бисимилярности двух конечных систем переходов может быть выполнена за полиномиальное время. Наиболее быстрые алгоритмы имеют квазилинейную временную сложность, используя уточнение разбиения посредством сведения к задаче о самом грубом разбиении.
Checking that two finite transition systems are bisimilar can be done in polynomial time. The fastest algorithms are quasilinear time using partition refinement through a reduction to the coarsest partition problem.