Talk:Region (model checking)
Latest comment: 1 year ago by Alzeha in topic Subsection Definition->Timed Bisimulation
This article has not yet been rated on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||
|
Subsection Definition->Timed Bisimulation
editI'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)