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:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
