A logic for the specification of continuous systems

Abstract

The paper proposes a first-order logic for the specification of continuous components of hybrid systems. The particularity of the approach lies in its interpretation of individual variables not as functions over time or as point-based values, but as environment-based values. An environment-based value closely models the local behavior of a function defined on a continuous time domain. The advantage of the approach is that it enables us to consider the derivation operator as an ordinary unary logical function. Thus, the logic is free from any built-in operators; they can all be defined on the elements of the carrier set of environment-based values.

To facilitate the definition of additional logical functions and predicates like limit, derivation of arbitrary order or continuity, the user is allowed to specify them in the intuitive notation of functions defined on time. The semantics of the logic provides two lifting operators, which lift the functions and the predicates to the appropriate semantic spaces. These lifting operators do not violate the intuitive meaning of the introduced constructs. An outline of the proof of this fact is given.

This work is being funded as part of the KONDISK program of the German Research Foundation (DFG).