Action refinement and property inheritance in systems of sequential agents

Abstract

For systems of sequential agents the fundamental relations between events-causality and conflict-are naturally connected to a global dependency relation on the system’s alphabet. Action refinement as a strictly hierarchical approach to system design should preserve this connection. Then it can be guaranteed that also more complex temporal properties of the refined system are inherited from the abstract level. The behaviour of a system of sequential agents is given in terms of synchronisations structures, a location-based subclass of prime event structures. The action refinement operator inherits causality and conflict according to the dependency relation. To express temporal properties of the systems we use νTrPTL, a linear time temporal logic for Mazurkiewicz traces. The logical framework, based on local modalities and fixpoints, allows to define refinement transformation on formulae. Under certain constraints on the refinement function, satisfaction of a formula for the abstract system turns out to be equivalent to satisfaction of the transformed formula for the refined system.