Partial models support abstract model-checking of complex temporalproperties by combining both over- and under-approximating abstractions into asingle model. Over the years, three families of such modeling formalisms haveemerged, represented by Kripke Modal Transition Systems (KMTSs), with restric-tions on necessary and possible behaviors, Mixed Transition Systems (MixTSs),with relaxation on these restrictions, and Generalized Kripke MTSs (GKMTSs),with hyper-transitions, respectively. In this paper, we compare the three fami-lies w.r.t. their expressive power (i.e., what can be modeled, what abstractioncan be captured), and the cost and precision of model-checking. We show thatthese families have the same expressive power (but do differ in succinctness),whereas GKMTSs are more precise (i.e, can establish more properties) for model-checking than the other two families. However, the use of GKMTSs in practice hasbeen hampered by the difficulty of encoding them symbolically. We address thisproblem by developing a new semantics for temporal logic of partial models thatmakes the MixTS family as precise for model-checking as the GKMTS family.The outcome is a symbolic model-checking algorithm that combines the efficientsymbolic encoding of MixTSs with the model-checking precision of GKMTSs.Our preliminary experiments indicate that the new algorithm is a good match forpredicate-abstraction-based model-checkers.
展开▼
