A simple, exhaustive implementation of the bisimulation property in Python.

bi.py

"""A simple, exhaustive implementation of the bisimulation property in Python.

In order to more deeply understand the bisimulation property of an LTS,
this code implements two forms of LTS verification. Note, this code is
not intended to be production ready, but rather as a proof of concept
to express the bisimulation property. Further, it is intentionally
computationally slow, hence, there are a large number of slow for loops.

LICENSE
-------
This is free and unencumbered software released into the public domain.

Anyone is free to copy, modify, publish, use, compile, sell, or
distribute this software, either in source code form or as a compiled
binary, for any purpose, commercial or non-commercial, and by any
means.

In jurisdictions that recognize copyright laws, the author or authors
of this software dedicate any and all copyright interest in the
software to the public domain. We make this dedication for the benefit
of the public at large and to the detriment of our heirs and
successors. We intend this dedication to be an overt act of
relinquishment in perpetuity of all present and future rights to this
software under copyright law.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
OTHER DEALINGS IN THE SOFTWARE.

For more information, please refer to <https://unlicense.org/>
"""

import itertools
from typing import Iterable, NamedTuple

from itertools import chain, combinations


class Transition(NamedTuple):
    """Encodes a transition from source via label to sink"""

    source: str
    label: str
    sink: str


class LTS:
    """Non-deterministic, finite Labelled Transition System."""

    def __init__(
        self, states: set[str], labels: set[str], transitions: set[Transition]
    ) -> None:
        self._states = states
        self._labels = labels
        self._transitions = transitions

    @property
    def states(self) -> set[str]:
        return self._states

    @property
    def labels(self) -> set[str]:
        return self._labels

    def transition(self, state: str, label: str) -> Iterable[str]:
        """Generator for each sink state reachable from state, via transition."""
        for transition in self._transitions:
            if transition.source == state and transition.label == label:
                yield transition.sink

    def transition_exists(self, source: str, label: str, sink: str) -> bool:
        """Checks if a transition between two points via  given label exists."""
        return Transition(source, label, sink) in self._transitions


def powerset(iterable: Iterable):
    """Subsequences of the iterable from shortest to longest.

    Taken from the itertools documentation.
    """
    # powerset([1,2,3]) → () (1,) (2,) (3,) (1,2) (1,3) (2,3) (1,2,3)
    s = list(iterable)
    return chain.from_iterable(combinations(s, r) for r in range(len(s) + 1))


class BinaryRelation:
    """Implements a non-symmetric binary relation."""

    def __init__(self, iterable: Iterable[tuple[str, str]]) -> None:
        self._br = set(iterable)

    def __str__(self) -> str:
        return str(self._br)

    def pairs(self) -> Iterable[tuple[str, str]]:
        """Iterates through each tuple in the binary relation."""
        yield from self._br

    def related(self, x, y) -> bool:
        """Checks if a pair exists in the binary relation."""
        return (x, y) in self._br

    def transpose(self) -> "BinaryRelation":
        """Creates a new binary relation with transposed values."""
        return BinaryRelation(transpose(self._br))


def possible_binary_relation_sets(
    iterable: Iterable[str],
) -> Iterable[Iterable[tuple[str, str]]]:
    """Produces every possible relation on each permutation of 2-length pairs."""
    return powerset(itertools.permutations(iterable, 2))


def possible_binary_relations(iterable: Iterable[str]) -> Iterable[BinaryRelation]:
    """Filters the binary relations to only include those of interest (x, y) being bisimilar."""
    return (
        BinaryRelation(iterable)
        for iterable in possible_binary_relation_sets(iterable)
        if ("x", "y") in iterable
    )


def yprime_search(lts: LTS, br: BinaryRelation, y: str, a: str, xprime: str):
    """Checks that there exists at least one transition such that y -{a}> y' and x' R y'.

    ∃{y' ∈ X} ( y {a}{→} y' ∧ x' R y' )
    """
    # Check all possible yprime states
    for yprime in lts.states:
        # A valid y' has: y -a> y' ^ x' R y'
        if lts.transition_exists(y, a, yprime) and br.related(xprime, yprime):
            print(f"     Found Valid: {y} -{a}> {yprime} ^ {xprime} R {yprime}")
            return True

    return False


def binary_relation_is_bisimulation(lts: LTS, br: BinaryRelation) -> bool:
    """Implements the following relation in code (exhaustively):

    ∀{x, x', y ∈ X, a ∈ L} [ ( x {a}{→} x' ∧ x R y )  ∃{y' ∈ X} ( y {a}{→} y' ∧ x' R y' ) ]
    """
    # forall x, x', y in X
    for x, xprime, y in itertools.permutations(lts.states, 3):
        # for a in L
        for a in lts.labels:
            # if x -a> x' ^ x R y
            if lts.transition_exists(x, a, xprime) and br.related(x, y):
                print(f"{x} -{a}> {xprime} ^ {x} R {y}")
                # we must satisfy yprime search - or it will be false
                if not yprime_search(lts, br, y, a, xprime):
                    return False
    return True


def formal_qprime_search(
    pprime: str, q: str, lmbda: str, lts: LTS, br: BinaryRelation
) -> bool:
    """Implements the consequent of the following if statement:

    If p {a}{→}  p', then there is q {a}{→} q' such that (p', q') ∈ R
    """
    for qprime in lts.transition(q, lmbda):
        if br.related(pprime, qprime):
            print(f"{q} -{lmbda}> {qprime} && ({pprime}, {qprime}) in R")
            return True
    return False


def formal_pprime_search(
    qprime: str, p: str, lmbda: str, lts: LTS, br: BinaryRelation
) -> bool:
    """Implements the consequent of the following if statement:

    If q {a}{→}  q', then there is p {a}{→} p' such that (p', q') ∈ R
    """

    for pprime in lts.transition(p, lmbda):
        if br.related(pprime, qprime):
            print(f"{p} -{lmbda}> {pprime} && ({pprime}, {qprime}) in R")
            return True
    return False


def formal_definition_one_directional_simulation(lts: LTS, br: BinaryRelation) -> bool:
    """Implements the wikipedia definition of bisimulation in a single direction (simulation).

    R is a simulation if for every pair of states (p, q) ∈ R and all labels a ∈ L:
     - If p {a}{→}  p', then there is q {a}{→} q' such that (p', q') ∈ R
    """

    # for every pair of states (p, q) in R
    for p, q in br.pairs():
        # for all labels lambda in L
        for lmbda in lts.labels:
            # if p lambda trans to p'
            for pprime in lts.transition(p, lmbda):
                if not formal_qprime_search(pprime, q, lmbda, lts, br):
                    return False
    return True


def formal_definition_trans_directional_simulation(
    lts: LTS, br: BinaryRelation
) -> bool:
    """Implements the wikipedia definition of bisimulation in a single direction (simulation).

    R is a simulation if for every pair of states (p, q) ∈ R and all labels a ∈ L:
     - If q {a}{→}  q', then there is p {a}{→} p' such that (p', q') ∈ R
    """
    # for every pair of states (p, q) in R
    for p, q in br.pairs():
        # for all labels lambda in L
        for lmbda in lts.labels:
            # if q lambda trans to q'
            for qprime in lts.transition(q, lmbda):
                if not formal_pprime_search(qprime, p, lmbda, lts, br):
                    return False
    return True


def formal_definition_bisimulation(lts: LTS, br: BinaryRelation) -> bool:
    """Implements the wikipedia definition of bisimulation in a single direction (simulation).

    R is a bisimulation if and only if for every pair of states (p, q) ∈ R and all labels a ∈ L:
     - If p {a}{→}  p', then there is q {a}{→} q' such that (p', q') ∈ R
     - If q {a}{→}  q', then there is p {a}{→} p' such that (p', q') ∈ R
    """
    return formal_definition_one_directional_simulation(
        lts, br
    ) and formal_definition_trans_directional_simulation(lts, br)


def transpose(iterable: Iterable[tuple[str, str]]) -> Iterable[tuple[str, str]]:
    return ((y, x) for x, y in iterable)


def test_binary_relation(lts: LTS, br: BinaryRelation):
    if binary_relation_is_bisimulation(lts, br):
        print(f"{br} is a bisimulation")
    if formal_definition_one_directional_simulation(lts, br):
        print("works in the p -> p' direction")
    if formal_definition_trans_directional_simulation(lts, br):
        print("works in the q -> q' direction")
    if formal_definition_one_directional_simulation(lts, br.transpose()):
        print("works in the q -> q' direction (via transpose)")
    if formal_definition_trans_directional_simulation(lts, br.transpose()):
        print("works in the p -> p' direction (via transpose)")
    if formal_definition_bisimulation(lts, br.transpose()):
        print(f"{br} is a bisimulation (via wikipedia def.)")
    if binary_relation_is_bisimulation(lts, br.transpose()):
        print(f"{br} is a bisimulation (via transpose)")


def main() -> None:
    # LTS without a bisimulation x <-> y

    lts = LTS(
        {"x", "x1", "x2", "x3", "y", "y1", "y2"},
        {"a", "b"},
        {
            Transition("x", "a", "x1"),
            Transition("x", "a", "x2"),
            Transition("x1", "b", "x3"),
            Transition("y", "a", "y1"),
            Transition("y1", "b", "y2"),
        },
    )

    possible_binary_relation = {("x2", "y1"), ("x", "y"), ("x3", "y2"), ("x1", "y1")}
    print(possible_binary_relation)
    test_binary_relation(lts, BinaryRelation(possible_binary_relation))

    symmetric_binary_relation = possible_binary_relation.union(
        transpose(possible_binary_relation)
    )
    print(symmetric_binary_relation)
    print(symmetric_binary_relation == set(transpose(symmetric_binary_relation)))
    test_binary_relation(lts, BinaryRelation(symmetric_binary_relation))

    # LTS with a bisimulation x <-> y

    lts2 = LTS(
        {"x", "x1", "x3", "y", "y1", "y2"},
        {"a", "b"},
        {
            Transition("x", "a", "x1"),
            # Transition("x", "a", "x2"),
            Transition("x1", "b", "x3"),
            Transition("y", "a", "y1"),
            Transition("y1", "b", "y2"),
        },
    )

    possible_binary_relation = {("x", "y"), ("x3", "y2"), ("x1", "y1")}
    symmetric_binary_relation = possible_binary_relation.union(
        transpose(possible_binary_relation)
    )
    print(symmetric_binary_relation)
    print(symmetric_binary_relation == set(transpose(symmetric_binary_relation)))
    test_binary_relation(lts2, BinaryRelation(symmetric_binary_relation))

    for possible_binary_relation in possible_binary_relations(lts.states):
        test_binary_relation(lts, possible_binary_relation)


if __name__ == "__main__":
    main()