Model checking for action abstraction

We endow action sets of transition systems with a partial order that expresses the degree of specialization of actions, and with an intuitive but flexible consistency predicate that constrains the extension of such orders with more specialized actions. We develop a satisfaction relation for such models and the p-calculus. We prove that this satisfaction relation is sound for Thomsen's extended bisimulation as our refinement notion for models, even for consistent extensions of ordered action sets. We then demonstrate how this satisfaction relation can be reduced, fairly efficiently, to classical p-calculus model checking. These results provide formal support for change management of models and their validation (e.g. in model-centric software development), and enable verification of concrete systems with respect to properties specified for abstract actions.