TIC: a tImed calculus (Q1261314)

The calculus TIC (timed and upward compatible extension of basic LOTOS) is presented. Time is introduced by assigning explicit time restrictions to events, the domain is the discrete one. Semantics is given operationally via LTS. Strong/weak timed bisimulations are defined and some of their properties are analysed (e.g., weak timed bisimulation is proven to be a congruence w.r.t. prefix, time-choice, parallel composition, hiding and relabelling). TIC applications are illustrated by two standard examples (stop and wait protocol, railroad crossing).