Talk:Region (model checking)

Subsection Definition->Timed Bisimulation

I'm pretty sure, this is wrong. Given a set of clocks C = {x}, the clock assignments u, u': C -> R with u(x)=0.3 and u'(x)=0.6 are in the same region. Nevertheless, the state (l, u) might has an outgoing delay transition with d=0.6, which means that the target state is in the same region, but the state (l, u') might not has such an outgoing transition, since we are changing region here, right?

I also did not find this at Bengtsson and Yi and I highly recommend to remove this subsection. Alzeha (talk) 15:17, 2 August 2023 (UTC)