In this paper, we develop model checking procedures for three ways of combining (temporal) logics: temporalization, independent combination, and join.We prove that they are terminating, sound, and complete, we analyze their computational complexity, and we report on experiments with implementations.We take a close look at mobile systems and show how the proposed combined model checking framework can be successfully applied to the specification and verification of their properties.
Model checking for combined logics with an application to mobile systems
FRANCESCHET, Massimo;MONTANARI, Angelo;
2004-01-01
Abstract
In this paper, we develop model checking procedures for three ways of combining (temporal) logics: temporalization, independent combination, and join.We prove that they are terminating, sound, and complete, we analyze their computational complexity, and we report on experiments with implementations.We take a close look at mobile systems and show how the proposed combined model checking framework can be successfully applied to the specification and verification of their properties.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
ASE.pdf
non disponibili
Tipologia:
Altro materiale allegato
Licenza:
Non pubblico
Dimensione
227.49 kB
Formato
Adobe PDF
|
227.49 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
