Logiche modali e temporali per sistemi concorrenti

E' stato provato che le logiche modali e temporali sono appropriate per descrivere interessanti proprietà temporali di sistemi di processi comunicanti e concorrenti [Pnu 81, Man 81, Lam 83] che non possono essere espresse direttamente per mezzo di logiche tradizionali (calcolo proposizionale, logica del primo ordine). Tra queste proprietà si possono citare le classi delle proprietà di "safety" e quelle di "liveness". Una proprietà di safety esprime il fatto che "niente di negativo accadrà" in un sistema, mentre una proprietà di liveness esprime il fatto che "qualcosa di buono accadrà". Proprietà rilevanti del primo tipo sono l'assenza di deadlock, correttezza parziale, etc., mentre del secondo sono la terminazione, la fairness, etc. Un'altra classe di proprietà esprimibili con la logica temporale include quelle relative a comportamenti ciclici cioè quelli che si hanno in un sistema che deve compiere ciclicamente una sequenza di azioni.