Hybrid Parallel Model Checking of Hybrid LTL on Hybrid State Space Representation

In this paper, we propose a hybrid parallel model checking algorithm for both shared and distributed memory architectures. The model checking is performed simultaneously with a parallel construction of system state space by distributed multi-core machines. The representation of the system's state space is a hybrid graph called Symbolic Observation Graph (SOG), which combines the symbolic representation of its nodes (sets of single states) and the explicit representation of its arcs. The SOG is adapted to allow the preservation of both state and event-based LTL formulae (hybrid LTL), i.e. the atomic propositions involved in the formula to be checked are either state or event-based propositions. We have implemented the proposed model checker within a C++ prototype and compared our preliminary results to the LTSmin model checker.