A domain equation for refinement of partial systems

Abstract

A reactive system can be specified by a labelled transition system, which indicates static structure, along with temporal-logic formulas, which assert dynamic behaviour. But refining the former while preserving the latter can be difficult, because:

(i) Labelled transition systems are ‘total’ – characterised up to bisimulation – meaning that no new transition structure can appear in a refinement.

(ii) Alternatively, a refinement criterion not based on bisimulation might generate a refined transition system that violates the temporal properties.

In response, Larsen and Thomson proposed modal transition systems, which are ‘partial’, and defined a refinement criterion that preserved formulas in Hennessy–Milner logic. We show that modal transition systems are, up to a saturation condition, exactly the mixed transition systems of Dams that meet a mix condition, and we extend such systems to non-flat state sets. We then solve a domain equation over the mixed powerdomain whose solution is a bifinite domain that is universal for all saturated modal transition systems and is itself fully abstract when considered as a modal transition system. We demonstrate that many frameworks of partial systems can be translated into the domain: partial Kripke structures, partial bisimulation structures, Kripke modal transition systems, and pointer-shape-analysis graphs.