On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic

Martin Hofmann, Donald Sannella

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The behavioural semantics of specifications with higher-order formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, due to Reichel and 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.
Original languageEnglish
Title of host publicationTAPSOFT '95: Theory and Practice of Software Development
Subtitle of host publication6th International Joint Conference CAAP/FASE Aarhus, Denmark, May 22–26, 1995 Proceedings
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-540-49233-7
ISBN (Print)978-3-540-59293-8
Publication statusPublished - 1995

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic'. Together they form a unique fingerprint.

Cite this