Fork Algebras as a Formalism to Reason Across Behavioral Specifications (Extended Abstract)

Abstract. Describing systems through the specification of different views is a well accepted practice in modern software engineering. In this paper we show how to reason across behavioral specifications within a relational framework. We consider views specifying behavioral information using linear temporal logic or dynamic logic. The main result is that independently generated specifications can be amalgamated within a common relational framework to which different analysis techniques can be applied. The paper also presents a realistic problem for which behavioral specifications in dyamic logic and linear temporal logic are jointly employed in the proof of a non trivial property.