Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: concurrency

Topic: Partial order on NFA up to bisimilarity

Robin Piedeleu (Dec 14 2022 at 17:01):

Not sure where to ask this, but here we go.

We can define a monoid operation over the set of nondeterministic finite-state automata (NFA) up to bisimilarity (reminiscent of the sum of regular expressions/automata up to language equivalence): given two automata $A_1,A_2$, let $A_1+A_2$ be the automata whose (final) states are the disjoint sum of the (final) states of $A_1$ and $A_2$, with the two initial states identified, and whose transition relation is also the disjoint union of the two transition relations, except on the initial state, where it behaves as you'd expect. This operation is a congruence for bisimilarity, so we can lift it to equivalence classes.

Moreover, because $A+A\cong A$, we can define a partial order on NFA up to bisimilarity: $A\leq B$ iff $A +B\cong B$.

The sum is the join for this partial order, but does it also have meets? An obvious candidate for $A_1\land A_2$ is the automata that behaves like both $A_1$ and $A_2$ whenever possible: let $A_1\land A_2$ be the NFA whose states are pairs of states of the two NFA, whose transition relation $R(a)$ for each letter $a$ is given by $((q_1,q_2),(q_1',q_2'))\in R(a)$ iff $(q_1,q_1')\in R_1(a)$ and $(q_2,q_2')\in R_2(a)$ (where I'm writing $R_i$ for the transition relation of $A_i$), and whose final states are pairs of final states of the two NFA. I have not checked this carefully, but the operation seems to lift to bisimilarity classes and to define a valid meet, making automata up to bisimilarity a lattice.

If it is correct (I'm half expecting it not to be) someone must have done this before, given the volume of work on bisimilarity etc. Have you seen something like this before? Do you know of a reference?

Ralph Sarkis (Dec 14 2022 at 18:00):

Not an answer (but maybe a helpful discussion). Just to make sure I understand, we have $A \leq B$ implies the language recognized by $A$ (denoted by $L(A)$) is included in $L(B)$, but not necessarily the converse. That is, we might have $L(A) \subseteq L(B)$ but not $A\leq B$.

So we know the language recognized by the meet of $A_1$ and $A_2$ (if it exists) is included in the intersection of the languages. This suggests your construction, but the failure of the converse above does not help confirming your construction is the right one.

Robin Piedeleu (Dec 14 2022 at 18:15):

Hmm... I had not thought about the relationship of this order with language inclusion. My intuition is the same as yours (that the relationship between this order and language inclusion is the same as that between language equivalence and bisimilarity, namely that the latter is finer than the former). I suppose the construction I describe also the one that constructs an automaton for the intersection of the languages recognised by two automata, so in that sense it is well-known!

Todd Schmid (he/they) (May 16 2023 at 14:10):

Robin Piedeleu said:

Not sure where to ask this, but here we go.

We can define a monoid operation over the set of nondeterministic finite-state automata (NFA) up to bisimilarity (reminiscent of the sum of regular expressions/automata up to language equivalence): given two automata $A_1,A_2$, let $A_1+A_2$ be the automata whose (final) states are the disjoint sum of the (final) states of $A_1$ and $A_2$, with the two initial states identified, and whose transition relation is also the disjoint union of the two transition relations, except on the initial state, where it behaves as you'd expect. This operation is a congruence for bisimilarity, so we can lift it to equivalence classes.

Moreover, because $A+A\cong A$, we can define a partial order on NFA up to bisimilarity: $A\leq B$ iff $A +B\cong B$.

The sum is the join for this partial order, but does it also have meets? An obvious candidate for $A_1\land A_2$ is the automata that behaves like both $A_1$ and $A_2$ whenever possible: let $A_1\land A_2$ be the NFA whose states are pairs of states of the two NFA, whose transition relation $R(a)$ for each letter $a$ is given by $((q_1,q_2),(q_1',q_2'))\in R(a)$ iff $(q_1,q_1')\in R_1(a)$ and $(q_2,q_2')\in R_2(a)$ (where I'm writing $R_i$ for the transition relation of $A_i$), and whose final states are pairs of final states of the two NFA. I have not checked this carefully, but the operation seems to lift to bisimilarity classes and to define a valid meet, making automata up to bisimilarity a lattice.

If it is correct (I'm half expecting it not to be) someone must have done this before, given the volume of work on bisimilarity etc. Have you seen something like this before? Do you know of a reference?

I know I'm late to the party (hello again, Zulip!), but I suspect this has to do with the fact that $\mathcal P(A \times (-))$ weakly preserves pullbacks. If $B$ weakly preserves pullbacks, then $\text{Coalg}(B)$ has pullbacks. You can't define your join operation in terms of a pushforward (in $\text{Coalg}(B)$), but maybe in the category with functional simulations this is possible?

Robin Piedeleu (May 27 2023 at 13:11):

Sorry @Todd Schmid (he/they) , only saw this recently. I was asking about the meet, as $+$ is the join by construction, since we define the order from it ($A\leq B$ iff $A+B\sim B$). But I am now convinced that the construction I gave above does not give a meet.

I am still curious about whether anyone has ever seen this order before though. It seems like a fairly natural order to consider on bisimilarity classes of NFA since, unlike the simulation pre-order, it is anti-symmetric. I'm now looking for a nice characterisation of it. If we reason on unfoldings of automata instead (or rather elements of the final coalgebra for the relevant functor), it looks like $A\leq B$ requires that the unfolding of $A$ be a subtree (modulo bisimilarity) of the unfolding of $B$. But I'd prefer a nice coinductive definition rather than working with equivalence classes of automata or trees, neither of which I feel like I ever really get. Could it be a gsos-style rule of the form: if $x\leq y$ and $x\xrightarrow{a} x'$ then $x'\leq y$?

Todd Schmid (he/they) (May 29 2023 at 19:15):

It took me a bit to realize which precise order you mean! You literally mean the sum operator in classic process algebra (nondeterministic choice). If you are in need of a meet operation for this join that is defined on the final coalgebra, you can use Lambek's lemma: the final $\mathcal P_f$-coalgebra (or final $\mathcal P_f(A\times-)$-coalgebra, if you want labels) is a free semilattice with bottom, so you can indeed take finite intersections.

Todd Schmid (he/they) (May 29 2023 at 19:17):

If you think about unfoldings (strongly extensional/up to bisimilarity, I mean), then the intersection of two trees is obtained by identifying the roots, and then identifying the pairs of children between the two trees that are bisimilar

Todd Schmid (he/they) (May 29 2023 at 19:18):

(and deleting the rest of the children :grimacing:)

Todd Schmid (he/they) (May 29 2023 at 19:40):

OK, I think these are the rules you want:
$x \xrightarrow{a} z$ and $y \xrightarrow{a} z'$ and $z \sim z'$ implies $x \wedge y \xrightarrow{a} z$
$x \to \checkmark$ and $y \to \checkmark$ implies $x \wedge y \to \checkmark$
All I'm doing here is mimicking the intersection in the final coalgebra, seeing it as a free semilattice with bottom

Robin Piedeleu (May 30 2023 at 10:32):

Thanks! If I unpack what you said a bit more: Lambek's lemma tells us that $Z$, the final $\mathcal{P}_f$-coalgebra, is isomorphic to $\mathcal{P}_f(Z)$, which gives me both finite meets and joins by pushing intersection and union through the isomorphism. I guess I would still need to check that these coincide with the joins as I've defined them above (via the sum operation of classic process algebra)? Because nothing guarantees that they're the same, unless I'm missing something.

Robin Piedeleu (May 30 2023 at 10:33):

And the rules you gave for the meet look convincing to me!

Todd Schmid (he/they) (May 30 2023 at 17:17):

Now I'm wondering if there's a nice axiomatization of this join operation :thinking:
Edit: meet operation!

Robin Piedeleu (May 30 2023 at 20:35):

Do you mean the meet? The join is the usual sum of process algebra, for which there are several axiomatisations with fixed-point, prefixing etc. Or perhaps you mean something else by "axiomatisation" in this context?

Todd Schmid (he/they) (May 30 2023 at 20:39):

I meant meet! I can never remember which is which :sweat_smile:

Todd Schmid (he/they) (May 30 2023 at 20:43):

I suspect we would need some pretty interesting equations. Thinking about expressions like
$(\mu v.(a+bv)) \wedge \mu v.(b + bv)$
which I think should be bisimilar to $\mu v.bv$...?

Todd Schmid (he/they) (May 30 2023 at 20:45):

No, that's not quite right.
$(a+\mu v.bv) \wedge (b + \mu v.bv) \sim \mu v.bv$