Author name cluster

Manfred Broy

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

12 papers

2 author rows

TCS Journal 2023 Journal Article

Specification and verification of concurrent systems by causality and realizability

Manfred Broy

A logical theory for interface specification and verification of distributed, concurrent, interactive, real-time systems is worked out based on a semantic foundation including operational and denotational semantics. It supports a calculus for the specification and verification of concurrent interactive systems by interface assertions. Systems are composed acting concurrently and interacting via streams exchanged over their channels forming feedback loops. A denotational semantics is defined handling feedback communication by recursion and fixpoints based on strong causality and realizability instead of monotonicity. The resulting verification calculus for the specification logic is proved to be sound and relatively complete with respect to an operational semantics in terms of generalized Moore machines. Actually, two models of concurrent systems are defined, a more abstract one with communication and interaction modeled by untimed streams and a more concrete one working with timed streams. The untimed model is an abstraction of the timed model. The timed model allows expressing the laws of causality and realizability. Moreover, the timed model can be used to specify real-time properties.

Details DOI

I&C Journal 2015 Journal Article

Computability and realizability for interactive computations

Manfred Broy

This paper deals with computability of interactive computations. It aims at the characterization and analysis of a general concept of interactive computation as a basis for the extension and generalization of the notion of computability to interactive computations. We extend the notion of computability to interactive computations. Instead of partial functions on natural numbers or on finite strings we work with functions and relations on infinite input and output streams. As part of the computability of such functions and relations on streams we treat the following aspects of interactive computations: • causality between input and output streams • realizability of single output streams for given input streams • the role of non-realizable output • relating non-realizable behaviors to state machines • the concept of interactive computation and computability for interactive systems • the role of time in computability. Finally, we relate our results to established notions of computability.

Details DOI

TCS Journal 2001 Journal Article

Refinement of time

Manfred Broy

We discuss mathematical models of the timed behaviour of system components. We study reactive system components that relate input-to-output streams. We work out a hierarchy of timing concepts. We distinguish non-timed streams, discrete streams with discrete or with continuous time, and dense streams with continuous time. We introduce a notion of a timed system component and formulate requirements for the time flow. We show how to compose timed systems in a modular way. We demonstrate that the introduction of time into a system model as well as the change of the timing model during the system development process can be captured as classical refinement steps.

Details DOI

TCS Journal 2001 Journal Article

The algebra of stream processing functions

Manfred Broy
Gheorghe Ştefănescu

Data flow networks are a model of concurrent computation. They consist of a collection of concurrent asynchronous processes which communicate by sending data over FIFO channels. In this paper we study the algebraic structure of the data flow networks and base their semantics on stream processing functions. Our algebraic theory is based on the calculus of flownomials. With an additive (or cantorian) interpretation the calculus gives a unified presentation of the classical algebraic models for control structures, that is, regular algebra and iteration theories. The kernel of the calculus is an equational axiomatization called basic network algebra (BNA) for flow graphs modulo graph isomorphism. We show that the algebra of stream processing functions called SPF (used for deterministic networks) and the algebra of sets of stream processing functions called P SPF (used for nondeterministic networks) are BNA algebras. Actually they give a multiplicative (or cartesian) interpretation of the calculus of flownomials. As a byproduct this shows that both semantic models are compositional. This means the semantics of a network may be described in terms of the semantics of its components. (As it is well known this is not true for the input–output relational semantics of nondeterministic networks.) We also identify additional axioms satisfied by the branching constants in these two algebraic theories. For the deterministic case we study in addition the coarser equivalence relation on networks given by the input–output behavior and provide a correct and complete axiomatization.

Details DOI

TCS Journal 2000 Journal Article

Algebraic specification of reactive systems

Manfred Broy

We present an algebraic method for the equational specification of reactive distributed systems. We define a mathematical concept of specifications of reactive components in terms of predicates. A component specification is a predicate that describes a set of behaviours. A deterministic component has exactly one behaviour. A component behaviour is represented by a stream processing function. We introduce operations on behaviours and lift them to specifications leading to an algebra of system specifications in analogy to the process algebras that provide algebras of reactive programs. However, in contrast to the purely axiomatic description of process algebras we use algebraic equations to specify components and not to formalise composition operators. We show how algebraic system specifications can be used as an algebraic and logical basis for state automata specifications and state transition diagrams.

Details DOI

TCS Journal 1988 Journal Article

Equational specification of partial higher-order algebras

Manfred Broy

The theory of algebraic abstract types specified by positive conditional formulas formed of equations and a definedness predicate is outlined and extended to hierarchical types with “noustrict” operations, partial and even infinite objects. Its model theory is based on the concept of partial interpretations. Deduction rules are given, too. Models of types are studied where all explicit equations have solutions. The inclusion of nigher-order types, i. e. , types comprising higher-order functions leads to an algebraic (“equational”) specification of algebras including sorts with “infinite” objects and higher-order functions (“functionals”).

Details DOI

TCS Journal 1986 Journal Article

A theory for nondeterminism, parallelism, communication, and concurrency

Manfred Broy

An applicative language is introduced for representing concurrent programs and communicating systems in the form of mutually recursive systems of nondeterministic equations for functions and streams. Mathematical semantics is defined by associating particular fixed points with such systems. These fixed points are chosen using a combination of several complete partial orderings. Operational semantics is described in the form of term rewriting rules, consistent with the mathematical semantics. It represents data-driven reduction semantics for usual expressions and data-driven data flow semantics in the case of recursive stream equations. So the language allows to treat the basic semantic notions of nondeterminism, parallelism, communication, and concurrency for multiprogramming in a completely formal, applicative framework. In particular, it provides a semantic theory for networks of loosely coupled, nondeterministic, communicating, stream processing functions. Finally, the relationship of the presented language to partial recursive functions and nonconventional computational models such as data flow and reduction machines is shown.

Details DOI

MFCS Conference 1986 Invited Paper

Partial Interpretations of Higher Order Algebraic Types (Extended Abstract)

Manfred Broy

Abstract The theory of algebraic abstract types specified by conditional equations is extended to types with “nonstrict” operations, partial and even infinite objects based on the concept of partial interpretations. Models of such types are studied where all explicit equations have solutions. Higher order types, i. e. types comprising higher order functions are treated, too. This allows an algebraic (“equational”) specification of algebras including sorts with “infinite” objects and higher order functions (“functionals”).

Details

TCS Journal 1985 Journal Article

On the Herbrand-Kleene universe for nondeterministic computations

Manfred Broy

For nondeterministic recursive equations over an arbitrary signature of function symbols including the nondeterministic choice operator “or” the interpretation is factorized according to the techniques developed by the present author (1982). It is shown that one can either associate an infinite tree with the equations, then interpret the function symbol “or” as a nondeterministic choice operator and so mapping the tree onto a set of infinite trees and then interpret these trees. Or one can interpret the recursive equation directly yielding a set-valued function. Both possibilities lead to the same result, i. e. , one obtains a commuting diagram. However, one has to use more refined techniques than just powerdomains. This explains and solves a problem posed by Nivat (1980). Basically, the construction gives a generalization of the powerdomain approach applicable to arbitrary nonflat (nondiscrete) algebraic domains.

Details DOI

MFCS Conference 1984 Conference Paper

On the Herbrand Kleene Universe for Nondeterministic Computations

Manfred Broy

Abstract For nondeterministic recursive equations over an arbitrary signature of function symbols including the nondeterministic choice operator "or" the interpretation is factorized. It is shown that one can either associate an infinite tree with the equations, then interprete the function symbol "or" as a nondeterministic choice operator and so mapping the tree onto a set of infinite trees and then interprete these trees. Or one can interprete the recursive equation directly yielding a set-valued function. Both possibilities lead to the same result, i. e. we obtain a commuting diagram. This explains and solves a problem posed in [Nivat 80]. Basically the construction gives a generalisation of the powerdomain approach applicable to arbitrary nonflat (nondiscrete) algebraic domains.

Details

MFCS Conference 1981 Conference Paper

On the Power of Algebraic Specifications

Jan A. Bergstra
Manfred Broy
John V. Tucker
Martin Wirsing

Abstract We study the expressive power of different algebraic specification methods. In contrast to (nonhierarchical) initial and terminal algebra specifications which correspond to semicomputable and cosemicomputable algebras, hierarchical specifications — as e. g. in the specification language CLEAR — allow to specify hyperarithmetical algebras and are characterized by them. For partial abstract types we prove that every computable partial algebra has an equational hidden enrichment specification and discuss the power of hierarchical partial algebras. Finally we give an example of the specification of a simple nondeterministic programming language.

Details

MFCS Conference 1980 Conference Paper

Abstract Data Types as Lattices of Finitely Generated Models

Martin Wirsing
Manfred Broy

Abstract For abstract data types with arbitrary first order formulas properties of the equations in the axioms are studied which allow to decide whether an abstract type has initial or terminal algebras or whether it forms a complete lattice. An example of an equationally defined abstract type forming a complete lattice with nonrecursive initial and terminal models is given.

Details