Verification of partial properties - temporal semantics

In this section we propose giving LOTOS programs a temporal semantics, i.e. the temporal logic formula expressing the properties of their execution sequences. The advantages of the temporal semantics approach when providing the semantics for concurrent programs can be summed up in the following observations: i) verifying that a program satisfies a given property (expressed by a temporal logic formula) is reduced to verifying that the formula expressing the temporal meaning of the program logically implies the given property formula. ii) verifying the equivalence of programs is reduced to verifying logic equivalence. These observations make it possible to unify these two verification problems, as they amount to checking the validity of a logic formula. Here mechanic tools can help, such as decision procedures and theorem provers.