Property information

x simultaneous with y iff ω(x) = ω(y) and ω(α ) = ω(α), where α is a function that maps a process to a start point, and ω is a function that maps a process to an end point and '=' indicates the same instance in time.

comment

t1 simultaneous_with t2 iff:= t1 before_or_simultaneous_with t2 and not (t1 before t2)

Property relations