PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Laneve C. Verification of partial properties - temporal semantics. Internal note IEI-B4-36, 1990.
 
 
Abstract
(English)
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.
Subject LOTOS


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional