TY - JOUR
T1 - On behavioural abstraction and behavioural satisfaction in higher-order logic
AU - Hofmann, Martin
AU - Sannella, Donald
PY - 1996
Y1 - 1996
N2 - The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, which is due to Reichel and was recently generalized to the case of first-order logic by Bidoit et al., is further generalized to this case. The fact that higher-order logic is powerful enough to express the indistinguishability relation is used to characterize behavioural satisfaction in terms of ordinary satisfaction, and to develop new methods for reasoning about specifications under behavioural semantics.
AB - The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, which is due to Reichel and was recently generalized to the case of first-order logic by Bidoit et al., is further generalized to this case. The fact that higher-order logic is powerful enough to express the indistinguishability relation is used to characterize behavioural satisfaction in terms of ordinary satisfaction, and to develop new methods for reasoning about specifications under behavioural semantics.
U2 - 10.1016/0304-3975(96)00068-0
DO - 10.1016/0304-3975(96)00068-0
M3 - Article
SN - 0304-3975
VL - 167
SP - 3
EP - 45
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1?2
ER -