Golog is a high-level action programming language for controlling autonomous agents such as mobile robots. It is defined on top of a logic-based action theory expressed in the Situation Calculus. Before a program is deployed onto an actual robot and executed in the physical world, it is desirable, if not crucial, to verify that it meets certain requirements (typically expressed through temporal formulas) and thus indeed exhibits the desired behaviour. However, due to the high (first-order) expressiveness of the language, the corresponding verification problem is in general undecidable. In this paper, we extend earlier results to identify a large, non-trivial fragment of the formalism where verification is decidable. In particular, we consider properties expressed in a first-order variant of the branching-time temporal logic CTL*. Decidability is obtained by (1) resorting to the decidable first-order fragment C² as underlying base logic, (2) using a fragment of Golog with ground actions only, and (3) requiring the action theory to only admit local effects. / In this extended version we extend the decidability result for the verification problem to the temporal logic CTL* over C2-axioms.

Chemnitz, Techn. Univ., Studienarb., 2007.

Ulm, Univ., Diss., 2007.

Zugl.: Stuttgart, Univ., Diss., 2008

Techn. University, Diss., 2005--Darmstadt.

pyAXL ist eine Programmierschnittstelle (API) zur Steuerung des "Cisco Call Manager", eine enterprise-VoIP-Verwaltung. Der Vortrag zeigt, wie pyAXL aufgebaut ist. An ein paar Beispielen wird die Verwendung von pyAXL demonstriert.

Die Zope Object Database, kurz ZODB, ist eine Open-Source-Datenbank für Python. Im Gegensatz zu den meisten relationalen Datenbanken verfügt die ZODB allerdings nicht über eine Anfragesprache zur gezielten Selektion von Objekten. <br /> Aufgabe dieser Diplomarbeit ist es, effiziente Ad-Hoc-Anfragemöglichkeiten zu evaluieren und eine geeignete als Zusatzprodukt in Python zu implementieren. <br /> Folgende Themen sind zu bearbeiten: <ul> <li>Vergleich und Auswahl einer Anfragesprache für Objektgraphen</li> <li>Auswahl von Indexstrukturen zur Unterstützung der gewählten Anfragesprache</li> <li>Implementation eines Zusatzprodukts zur ZODB, die eine Anfragesprache sowie unterstützende Indizes bereitstellt</li> <li>Testen und Bewerten der Implementierung</li> </ul>

Ist die Reduktion von Quellcoderedundanz ein Motivator für die Evolution von Programmiersprachen? Das ist die Ausgangsfrage der Untersuchung, die exemplarisch an Sprachfeatures von Java 8 beleuchtet wird. Code Clones und Boilerplate Code werden als Formen von Quellcoderedundanz aufgefasst, beschrieben und definiert. Quellcoderedundanz wird als das Verhältnis der Komplexität des Ausdrucks und der durch diesen transportierte Information definiert und operationalisiert. Zur Messung der Änderung der Quellcoderedundanz durch Java 8 werden Codesegmente von Java 7 auf Java 8 migriert. Bei konstantem Informationsgehalt wird die Ausdruckskomplexität durch Maße der statischen Codeanalyse verglichen. Die Untersuchung zeigt für alle betrachteten Sprachfeatures eine Abnahme der Quellcoderedundanz, die aus einer Reduktion von Boilerplate Code oder dem Wegfall von Code Clones resultiert. Die Ergebnisse deuten darauf hin, dass die Reduktion von Quellcoderedundanz für die mit Java 8 in die Sprache eingeführten Neuerungen zumindest eine notwendige Eigenschaft ist. Um im Ökosystem der Programmiersprachen weiter bestehen zu können, müssen sich Sprachen weiterentwickeln, da ihr technologisches Umfeld stets im Wandel ist. Um seinen Nutzern die Möglichkeit zu geben, qualitativ hochwertigen Quellcode zu verfassen, müssen Sprachmittel zur Verfügung gestellt werden, die eine elegante Ausdrucksform komplexer Sachverhalte erlauben. Eine geringe Quellcoderedundanz kann also als Qualitätsmerkmal für Quellcode gelten und deren Ermöglichung als Evolutionsvorteil für Programmiersprachen angesehen werden.:1 Einleitung 2 Programmiersprachen und Quellcoderedundanz 2.1 Code Clones 2.2 Boilerplate Code 2.3 Quellcoderedundanz 3 Paradigmenwechsel mit Java 8 3.1 Streams API 3.2 Lambda-Ausdrücke 3.3 Die Klasse Optional<T> 3.4 default-Methoden in Interfaces 4 Schluss

Um das Fließverhalten von Granulaten in dünnwandigen Metallsilos auch mikroskopisch detailliert beschreiben zu können, ist es wichtig, beide Kontaktpartner (Granulat und elastische Wand) detailliert abbilden zu können. Granulate können vereinfacht als Kugeln betrachtet werden, weswegen die Diskrete-Elemente-Methode (DEM) hierfür geeignet ist. Die elastische Verformung der Metallwand kann mit Hilfe der Finiten-Elemente-Methode (FEM) berechnet werden. Ziel dieser Arbeit ist es, eine Simulation zu entwickeln, welche für beide Kontaktpartner eine gemeinsame Simulationsumgebung schafft. Dabei sollen zu Beginn einfache Beispiele für den Kontakt von Granulat und Festkörperstrukturen erarbeitet werden, die verschiedene Lastfälle abdecken. Um die Simulationsergebnisse bewerten zu können, sollen die Beispiele so gewählt werden, dass die Simulationen analytisch oder numerisch validiert werden können.

The Golog action programming language is a powerful means to express high-level behaviours in terms of programs over actions defined in a Situation Calculus theory. In particular for physical systems, verifying that the program satisfies certain desired temporal properties is often crucial, but undecidable in general, the latter being due to the language’s high expressiveness in terms of first-order quantification and program constructs. So far, approaches to achieve decidability involved restrictions where action effects either had to be contextfree (i.e. not depend on the current state), local (i.e. only affect objects mentioned in the action’s parameters), or at least bounded (i.e. only affect a finite number of objects). In this paper, we present a new, more general class of action theories (called acyclic) that allows for context-sensitive, non-local, unbounded effects, i.e. actions that may affect an unbounded number of possibly unnamed objects in a state-dependent fashion. We contribute to the further exploration of the boundary between decidability and undecidability for Golog, showing that for acyclic theories in the two-variable fragment of first-order logic, verification of CTL properties of programs over ground actions is decidable.