vault backup: 2025-04-14 08:34:56

This commit is contained in:
Marco Realacci 2025-04-14 08:34:56 +02:00
parent 16a89a0328
commit 493d36cf07

View file

@ -60,4 +60,4 @@ If S contained one among (p1,q1) or (p1,q2), then it would not be a simulation:
p0 is simulated by q0: $$S = {(p0, q0), (p1, q2), (p2, q3)}$$
q0 is simulated by p0: $$S ={(q0,p0),(q1,p1),(q2,p1),(q3,p2)}$$
However, p0 and q0 are not bisimilar: the transition q0 -> a -> q1 is not bisimulable by any transition from p0
However, p0 and q0 are not bisimilar: the transition q0 -> a -> q1 is not bisimulable by any transition from p0 (ndeed, p0 a> p1 does not suffice, because p1 can perform a b and so cannot be bisimilar to q1).