Model checking for combined logics with an application to mobile systems
| Authors |
|
|---|---|
| Publication date | 2004 |
| Journal | Automated Software Engineering |
| Volume | Issue number | 11 |
| Pages (from-to) | 289-321 |
| Organisations |
|
| 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. |
| Document type | Article |
| Permalink to this page | |
