Towards the one-tiered design of data types and transition systems

Abstract

States build up hidden sorts. Consequently, labelled transition systems can be specified as ternary predicates within many-sorted specifications with visible (static, constructor-based) as well as hidden (dynamic, state-based) components. In modal logic, transition systems determine the equality of states, usually called bisimilarity. In manysorted type logic, the equality of hidden data usually comes as contextual or behavioural equivalence. We integrate both concepts and specify transition systems in terms of functional, relational and/or transitional actions. We introduce standard specifications, which, on the one hand, specialize many-sorted specifications insofar as visible domains are axiomatized by particular Horn clauses that can be regarded as constructor-based functional-logic programs for defined functions and safety predicates. On the other hand, hidden domains are axiomatized by co-Horn clauses for liveness predicates such as bisimilarity, fairness and properties concerned with infinite state sequences. The formal reasoning about a standard specification is based on a hierarchical model construction that starts out from the initial model (for inductive reasoning), interprets liveness predicates (including bisimilarity) as the greatest solutions of their co-Horn axioms and becomes a final model by factoring the initial one through bisimilarity. This model construction, which is quite natural because it combines standard semantics of logic programs, data types and modal logic, relies upon certain constraints, namely functionality (existence and uniqueness of visible normal forms), behavioural congruence (compatibility of bisimilarity with defined functions and safety predicates) and behavioural consistency (closedness of the model class under factoring through bisimilarity). We introduce the notions of a factorizable goal and a coinductive Horn clause for obtaining syntactical criteria for behavioural congruence and consistency, respectively.