On the consistency, expressiveness, and precision of partial modeling formalisms

Partial transition systems support abstract model checking of complex temporal propercombining both over- and under-approximatingabstractions into a single model. Over the years, three families of such modeling formalisms have emerged, represented by (1) Kripke Modal Transition Systems (KMTSs), with restrictions on necessary and possible behaviors; (2) Mixed Transition Systems (MixTSs), with relaxation on these restrictions; and (3) Generalized Kripke MTSs (GKMTSs), with hyper-transitions, respectively. In this paper, we investigate these formalisms based on two fundamental using partial transition systems (PTSs) – as objects for abstracting concrete (and thus, a PTS is semantically consistent if it abstracts at least one concrete system) and as models for checking temporal properties (and thus, a PTS is logically consistent if it gives consistent interpretation to all temporal logic formulas). We study the connection between semantic and logical consistency of PTSs, compare the thr...

• Type: Journal
• Year: 2011
• Where: IANDC
• Authors: Ou Wei, Arie Gurfinkel, Marsha Chechik
• Keywords: Checking, IANDC 2011, Model, Transition Systems