This thesis is about coalgebraic methods in software specification and verification. It extends known techniques of coalgebraic specification to a more general level to pave the way for real world applications of software verification. There are two main contributions of the present thesis: 1. Chapter 3 proposes a generalisation of the familiar notion of coalgebra such that classes containing methods with arbitrary types (including binary methods) can be modelled with these generalised coalgebras. 2. Chapter 4 presents the specification language CCSL (short for Coalgebraic Class Specification Language), its syntax, its semantics, and a prototype compiler that translates CCSL into higher-order logic. / Die Dissertation beschreibt coalgebraische Mittel und Methoden zur Softwarespezifikation und -verifikation. Die Ergebnisse dieser Dissertation vereinfachen die Anwendung coalgebraischer Spezifikations- und Verifikationstechniken und erweitern deren Anwendbarkeit. Damit werden Softwareverifikation im Allgemeinen und im Besonderen coalgebraische Methoden zur Softwareverifikation der praktischen Anwendbarkeit ein Stück nähergebracht. Diese Dissertation enthält zwei wesentliche Beiträge: 1. Im Kapitel 3 wird eine Erweiterung des klassischen Begriffs der Coalgebra vorgestellt. Diese Erweiterung erlaubt die coalgebraische Modellierung von Klassenschnittstellen mit beliebigen Methodentypen (insbesondere mit binären Methoden). 2. Im Kapitel 4 wird die coalgebraische Spezifikationssprache CCSL (Coalgebraic Class Specification Language) vorgestellt. Die Bescheibung umfasst Syntax, Semantik und einen Prototypcompiler, der CCSL Spezifikationen in Logik höherer Ordnung (passend für die Theorembeweiser PVS und Isabelle/HOL) übersetzt.

This thesis describes a probabilistic model for optimum information retrieval in a distributed heterogeneous environment. The model assumes the collection of documents offered by the environment to be hierarchically partitioned into subcollections. Documents as well as subcollections have to be indexed. At this indexing methods using different indexing vocabularies can be employed. A query provided by a user is answered in terms of a ranked list of documents. The model determines a procedure for ranking the documents that stems from the Probability Ranking Principle: For each subcollection the subcollection´s elements are ranked; the resulting ranked lists are combined into a final ranked list of documents where the ordering is determined by the documents´ probabilities of being relevant with respect to the user´s query. Various probabilistic ranking methods may be involved in the distributed ranking process. The underlying data volume is arbitrarily scalable. A criterion for effectively limiting the ranking process to a subset of subcollections extends the model. The model´s applicability is experimentally confirmed. When exploiting the degrees of freedom provided by the model experiments showed evidence that the model even outperforms comparable models for the non-distributed case with respect to retrieval effectiveness. An architecture for a distributed information retrieval system is presented that realizes the probabilistic model. The system provides access to an arbitrary number of dynamic multimedia databases.

Besonders in Call Centern spielt die unter dem Begriff CTI (Computer Telephony Integration) zusammengefasste Integration von IT-Systemen und Telefonanlagen eine wichtige Rolle. Wenn auch diese Integration auf technischer Ebene in der Regel zufriedenstellend gelöst wird, zeigt ein Blick auf die Softwareentwicklung in diesem Bereich noch Nachholbedarf. Die vorliegende Arbeit greift dieses Problem auf und versucht, den Ansatz CTI auf die Ebene der Entwicklung verteilter Anwendungen abzubilden. Ziel dabei ist es, Erkenntnisse darüber zu erzielen, inwieweit ein allgemeines Basismodell als Framework für die Entwicklung von CTI-Anwendungen definiert werden kann und welchen Mehrwert es mit sich bringt. Parallel dazu wird die Frage untersucht, inwieweit bewährte Methoden und Technologien verteilter Systeme auf diesem Spezialgebiet ihre Anwendung finden können. Dazu wird ein allgemeines Anwendungsmodell für CTI-Lösungen und darauf aufbauend ein objektorientiertes, verteiltes Framework entworfen. Das Framework selbst wird als Prototyp implementiert und diversen Leistungsmessungen unterzogen. / Computer Telephony Integration (CTI) plays an important role wherever computer and telecommunication systems have to interact. Applications in a call center are typical examples. This integration has been studied widely from a technical viewpoint only, but not at the level of application development. Since telecommunication systems are naturally distributed systems, CTI eventually leads to distributed applications. This thesis presents an example of a general, object-oriented framework for CTI applications and examines the use of proven technologies and methodologies for distributed applications. Based on a prototype implementation the practicability of the concept is being examined and verified.

In this thesis we see deductive systems for classical propositional and predicate logic which use deep inference, i.e. inference rules apply arbitrarily deep inside formulas, and a certain symmetry, which provides an involution on derivations. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they enjoy various new interesting properties. Not only the identity axiom, but also cut, weakening and even contraction are reducible to atomic form. This leads to inference rules that are local, meaning that the effort of applying them is bounded, and finitary, meaning that, given a conclusion, there is only a finite number of premises to choose from. The systems also enjoy new normal forms for derivations and, in the propositional case, a cut elimination procedure that is drastically simpler than the ones for sequent systems.

This thesis is about coalgebraic methods in software specification and verification. It extends known techniques of coalgebraic specification to a more general level to pave the way for real world applications of software verification. There are two main contributions of the present thesis: 1. Chapter 3 proposes a generalisation of the familiar notion of coalgebra such that classes containing methods with arbitrary types (including binary methods) can be modelled with these generalised coalgebras. 2. Chapter 4 presents the specification language CCSL (short for Coalgebraic Class Specification Language), its syntax, its semantics, and a prototype compiler that translates CCSL into higher-order logic. / Die Dissertation beschreibt coalgebraische Mittel und Methoden zur Softwarespezifikation und -verifikation. Die Ergebnisse dieser Dissertation vereinfachen die Anwendung coalgebraischer Spezifikations- und Verifikationstechniken und erweitern deren Anwendbarkeit. Damit werden Softwareverifikation im Allgemeinen und im Besonderen coalgebraische Methoden zur Softwareverifikation der praktischen Anwendbarkeit ein Stück nähergebracht. Diese Dissertation enthält zwei wesentliche Beiträge: 1. Im Kapitel 3 wird eine Erweiterung des klassischen Begriffs der Coalgebra vorgestellt. Diese Erweiterung erlaubt die coalgebraische Modellierung von Klassenschnittstellen mit beliebigen Methodentypen (insbesondere mit binären Methoden). 2. Im Kapitel 4 wird die coalgebraische Spezifikationssprache CCSL (Coalgebraic Class Specification Language) vorgestellt. Die Bescheibung umfasst Syntax, Semantik und einen Prototypcompiler, der CCSL Spezifikationen in Logik höherer Ordnung (passend für die Theorembeweiser PVS und Isabelle/HOL) übersetzt.

Gescannte und vektorisierte technische Zeichnungen werden automatisch unter Nutzung eines Netzes von Modellen in eine hochwertige Datenstruktur migriert. Die Modelle beschreiben die Inhalte der Zeichnungen hierarchisch und deklarativ. Modelle für einzelne Bestandteile der Zeichnungen können paarweise unabhängig entwickelt werden. Dadurch werden auch sehr komplexe Zeichnungsklassen wie Elektroleitungsnetze oder Gebäudepläne zugänglich. Die Modelle verwendet der neue, sogenannte Y-Algorithmus: Hypothesen über die Deutung lokaler Zeichnungsinhalte werden hierarchisch generiert. Treten bei der Nutzung konkurrierender Modelle Konflikte auf, werden diese protokolliert. Mittels des Konfliktbegriffes können konsistente Interpretationen einer kompletten Zeichnung abstrakt definiert und während der Analyse einer konkreten Zeichnung bestimmt werden. Ein wahrscheinlichkeitsbasiertes Gütemaß bewertet jede dieser alternativen, globalen Interpretationen. Das Suchen einer bzgl. dieses Maßes optimalen Interpretation ist ein NP-hartes Problem. Ein Branch and Bound-Algorithmus stellt die adäquate Lösung dar.

In this thesis I study several deductive systems for linear logic, its fragments, and some noncommutative extensions. All systems will be designed within the calculus of structures, which is a proof theoretical formalism for specifying logical systems, in the tradition of Hilbert's formalism, natural deduction, and the sequent calculus. Systems in the calculus of structures are based on two simple principles: deep inference and top-down symmetry. Together they have remarkable consequences for the properties of the logical systems. For example, for linear logic it is possible to design a deductive system, in which all rules are local. In particular, the contraction rule is reduced to an atomic version, and there is no global promotion rule. I will also show an extension of multiplicative exponential linear logic by a noncommutative, self-dual connective which is not representable in the sequent calculus. All systems enjoy the cut elimination property. Moreover, this can be proved independently from the sequent calculus via techniques that are based on the new top-down symmetry. Furthermore, for all systems, I will present several decomposition theorems which constitute a new type of normal form for derivations.

This thesis describes a probabilistic model for optimum information retrieval in a distributed heterogeneous environment. The model assumes the collection of documents offered by the environment to be hierarchically partitioned into subcollections. Documents as well as subcollections have to be indexed. At this indexing methods using different indexing vocabularies can be employed. A query provided by a user is answered in terms of a ranked list of documents. The model determines a procedure for ranking the documents that stems from the Probability Ranking Principle: For each subcollection the subcollection´s elements are ranked; the resulting ranked lists are combined into a final ranked list of documents where the ordering is determined by the documents´ probabilities of being relevant with respect to the user´s query. Various probabilistic ranking methods may be involved in the distributed ranking process. The underlying data volume is arbitrarily scalable. A criterion for effectively limiting the ranking process to a subset of subcollections extends the model. The model´s applicability is experimentally confirmed. When exploiting the degrees of freedom provided by the model experiments showed evidence that the model even outperforms comparable models for the non-distributed case with respect to retrieval effectiveness. An architecture for a distributed information retrieval system is presented that realizes the probabilistic model. The system provides access to an arbitrary number of dynamic multimedia databases.

Besonders in Call Centern spielt die unter dem Begriff CTI (Computer Telephony Integration) zusammengefasste Integration von IT-Systemen und Telefonanlagen eine wichtige Rolle. Wenn auch diese Integration auf technischer Ebene in der Regel zufriedenstellend gelöst wird, zeigt ein Blick auf die Softwareentwicklung in diesem Bereich noch Nachholbedarf. Die vorliegende Arbeit greift dieses Problem auf und versucht, den Ansatz CTI auf die Ebene der Entwicklung verteilter Anwendungen abzubilden. Ziel dabei ist es, Erkenntnisse darüber zu erzielen, inwieweit ein allgemeines Basismodell als Framework für die Entwicklung von CTI-Anwendungen definiert werden kann und welchen Mehrwert es mit sich bringt. Parallel dazu wird die Frage untersucht, inwieweit bewährte Methoden und Technologien verteilter Systeme auf diesem Spezialgebiet ihre Anwendung finden können. Dazu wird ein allgemeines Anwendungsmodell für CTI-Lösungen und darauf aufbauend ein objektorientiertes, verteiltes Framework entworfen. Das Framework selbst wird als Prototyp implementiert und diversen Leistungsmessungen unterzogen. / Computer Telephony Integration (CTI) plays an important role wherever computer and telecommunication systems have to interact. Applications in a call center are typical examples. This integration has been studied widely from a technical viewpoint only, but not at the level of application development. Since telecommunication systems are naturally distributed systems, CTI eventually leads to distributed applications. This thesis presents an example of a general, object-oriented framework for CTI applications and examines the use of proven technologies and methodologies for distributed applications. Based on a prototype implementation the practicability of the concept is being examined and verified.

Gescannte und vektorisierte technische Zeichnungen werden automatisch unter Nutzung eines Netzes von Modellen in eine hochwertige Datenstruktur migriert. Die Modelle beschreiben die Inhalte der Zeichnungen hierarchisch und deklarativ. Modelle für einzelne Bestandteile der Zeichnungen können paarweise unabhängig entwickelt werden. Dadurch werden auch sehr komplexe Zeichnungsklassen wie Elektroleitungsnetze oder Gebäudepläne zugänglich. Die Modelle verwendet der neue, sogenannte Y-Algorithmus: Hypothesen über die Deutung lokaler Zeichnungsinhalte werden hierarchisch generiert. Treten bei der Nutzung konkurrierender Modelle Konflikte auf, werden diese protokolliert. Mittels des Konfliktbegriffes können konsistente Interpretationen einer kompletten Zeichnung abstrakt definiert und während der Analyse einer konkreten Zeichnung bestimmt werden. Ein wahrscheinlichkeitsbasiertes Gütemaß bewertet jede dieser alternativen, globalen Interpretationen. Das Suchen einer bzgl. dieses Maßes optimalen Interpretation ist ein NP-hartes Problem. Ein Branch and Bound-Algorithmus stellt die adäquate Lösung dar.