Abductive Reasoning over Temporal Specifications of Objects

: In the context of reactive system specification, the certification task usually consists in ensuring that some envisaged property of the system behaviour follows from the specification. Considering, in particular, object-oriented system specification based on temporal logic, we have that, in general, the object specifications can only include certain kinds of formulae (e.g. constraints on action ocurrences and changes in attribute values) and the formulae expressing the intended properties of the system behaviour can be different. Therefore, whenever a property is not inferred from the specification, we can not just add it as a new specification axiom and traditional certification approaches do not use to provide help on how the specification could be enriched. Finding how to enrich a specification with suitable new axioms is an important issue that has not been explored. This task has an abuctive flavour and in this paper we address the problem of certification of temporal object sp..