Name
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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1023/B:AUSE.0000028537.84347.9c | Autom. Softw. Eng. |
Keywords | Field | DocType |
temporal logic,model checking,combined logics,mobile systems | Abstraction model checking,Model checking,Computer science,Theoretical computer science,Implementation,Normalization property,Temporal logic,Computational complexity theory | Journal |
Volume | Issue | ISSN |
11 | 3 | 1573-7535 |
Citations | PageRank | References |
21 | 0.82 | 35 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Massimo Franceschet | 1 | 658 | 39.91 |
| Angelo Montanari | 2 | 1535 | 135.04 |
| Maarten de Rijke | 3 | 6516 | 509.76 |