Parallel Model Checking and the FMICS-jETI Platform
Jǐŕı Barnat, Luboš Brim, Martin Leucker · 2007
In this paper we summarize parallel algorithms for enumerative model checking of properties formulated in linear time temporal logic (LTL) as well as a fragment of the \mu- calculus which naturally subsumes the branching time logic CTL (computation tree logic). We also indicate how to provide parallel model checking applications as services for integrated modelling, analysis, and verification using the FMICS-jETI platform.