A Process Algebra for Hybrid Systems
Jan Joris Vereijken · 1999
ing from the synchronization actions we get the system HT # : HT # = # T(0) = 0 # dT dt = 1 # # off(22) HT # warm (22) HT # warm (u) = # T(u) = 22 # dT dt =-1 # # on(u+ 4) HT # cold (u + 4) HT # cold (u) = # T(u) = 18 # dT dt = 1 # # off(u + 4) HT # warm (u + 4) So HT starts in a state where the temperature is 0 # C, rising by 1 # C per hour. After 22 hours (when it is 22 # C), the heater turns off, after which the temperature starts to fall. Four hours 5 later, (when it is 18 # C), the heater turns on, the temperature starts to rise, and another four hours later the temperature is 22 # C again. This cycle repeats ad infinitum. This completes the absolute time version of our small example. Note that we have not given any correctness criterion. One such criterion could for example be "eventually the temperature stays within the interval 18 # T(t) # 22". This is not necessarily a bad thing; we are more focused on transforming large, conc...