Model Checking for Combined Logics with an Application to Mobile Systems

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.

• Type: Journal
• Year: 2004
• Where: ASE
• Authors: Massimo Franceschet, Angelo Montanari, Maarten de Rijke
• Keywords: ASE 2004, Independent Combination, Model Checking, Model Checking Framework