The environment in which a software system operates is as important to the correct operation of the system as the software itself. Most software development involves making assumptions about the environment in which the resulting system will operate. These assumptions may cease to be valid if the environment changes, causing the system to fail to operate correctly. One solution to this problem is to use run-time requirements monitoring to deter mine, as a system operates, whether it is satisfying the requirements specified for it and to take action to rectify these problems. This thesis describes work that has been carried out in the area of run-time requirements monitoring. A framework has been developed for monitoring requirements which are formally specified using temporal logic and the KAOS goal-oriented requirements specification language. The framework uses AspecU to instrument the monitored system so that events are emitted which are used to determine whether the monitored system satisfies the requirements specification. The framework also provides a language which can specify a mapping between requirements and implementation which can be used to generate instrumentation code. The monitoring framework supports monitoring of soft goals by allowing the formal specification of metrics which can be used to determine whether soft goals are in fact being satisfied. These contributions are validated using a workforce scheduling system as a case study. This is a real world system and the requirements monitored were those considered useful by the developers of the system. The case study shows that the monitoring framework can be used to instrument a system to monitor hard and soft goals and that those goals can be monitored with reasonable performance overhead. Goal failures due to changes in the environment can be detected using the information supplied by the monitoring framework.

No description available.

No description available.

No description available.

Using Constraint Logic Programming and a data model approach, we provide an agent with a flexible way to plan and direct its actions and to manipulate and represent its knowledge. We use constraint solving techniques developed in the KRAFT project to provide the agent with a sophisticated reasoning and deliberation process. We explore the declarative use of constraints within a BDI Agent framework to represent knowledge as complex quantified constraints and apply these techniques to a courier scenario where cooperating agents communicate, delegate and exchange desires and information using Generalised Partial Global Planning mechanisms to solve a given set of tasks.

The aim of this thesis is to provide techniques for the abstraction of floating-point expressions into the polyhedra domain as well as into the finite powerset of polyhedra domain. Moreover, this thesis aims at presenting a forward and a backward analysis for the detection and inference of floating-point errors such as overflow and division by zero. These techniques are based on abstract interpretation, which is a theory for the sound approximation of the semantics of programs. These abstractions and analyses have important applications for instance in engineering, mechanics and computer aided graphics design. The abstraction of floating-point expressions into polyhedra includes two stages. the first, we present an approximation of floating-point expression by a polynomial with interval coefficients that includes the possible floating-point errors. In the second stage we present techniques for abstracting polynomials with interval coefficients into polyhedra and polyhedra powersets. Moreover, we present a technique for abstracting expressions in which a division by zero may occur. A forward analysis for the detection of overflow and division by zero is then presented. This analysis is particular in that it always reaches the output of a programs. This an important requirement since the backward analysis needs information on the output to infer which input to a program could cause an overflow or a division by zero. Such analyses are important especially in the design of systems with high contents of nonlinear floating-point expressions. Experimental results show the usability of these analyses.

This thesis presents two novel inductive logic programming (ILP) approaches, based on the notion of a connected theory. A connected theory contains clauses that depend on one another, either directly or via clauses in the background knowledge. Generalisation of such a theory is proved to be a sound and complete method for learning definite ILP hypotheses. The Induction on Failure (IOF) proof procedure, based on the connected theory generalisation method, adds secondary examples into the hypothesis, and generates auxiliary clauses to explain them. These concepts, novel to IOF, address the issues of incompleteness present in previous definite ILP methods. The concept of the connected theory is also applied to the non-monotonic, normal program setting. Thus, the method of generalisation of a normal connected theory is presented. Fundamental to this is the assertion that a partial non-monotonic hypothesis must include both positive and negative information, which the general hypothesis should preserve. This has resulted in, as far as the author is aware, the most complete semantic characterisation available of non-monotonic ILP using a bridge formula. It is proved that generalisation of such a formula to a set of completed definitions is a sound method of generating normal program hypotheses. In the course of establishing a completeness result for this latter approach, the semantics of the supported consequences of a normal program are defined, and the support tree method is presented and shown to be a sound and complete proof procedure for supported consequences. Using these results, it is shown that, for function-free programs, any correct hypothesis for which the examples are supported consequences of the learned program can be derived via a normal connected theory.

Inductive Logic Programming (ILP) is a machine learning technique that relies on logic programs as a representation language. Most of the effort in the field of ILP has concentrated on a restricted class of problems, providing solutions that do not fully support negation. On the other hand, integration of negation and nonmonotonic reasoning in logic programming is common and important for a number of problems. This thesis presents an approach to nonmonotonic ILP that is based on a transformation of the original problem to a problem that can be solved by employing abductive reasoning. In particular we present a general framework for the transformation that can be used as reference for concrete implementations. We instantiate the transformation to derive two alternative implementations that are rooted in the two dominant computational logic paradigms: Prolog and Answer Set Programming (ASP). In the first case, we derive an implementation, called TAL, that is based on the abductive proof procedure SLDNFA and uses a customisable best-first search on the space of abductive solutions. In the second case the transformation is further refined in order to exploit the computational properties of available ASP solvers. In the proposed system called ASPAL, a theory is constructed from a set of mode declarations and used to extend the search of the underlying solver, so enabling the derivation of inductive hypotheses. We provide completeness and soundness results for the framework and the ILP systems presented and show how, as a consequence of this, it is possible to induce complex multi-predicate hypotheses involving negation, recursion and the definition of elements of the domain that are not directly observed. We validate the framework on established ILP benchmark problems, on some nonmonotonic ILP problems proposed in the literature. Furthermore we demonstrate the approach on a novel application of nonmonotonic ILP to the revision of normative frameworks.

This thesis provides a model-theoretic semantic analysis of aspects of the LF logical framework

Σε αυτήν την εργασία μελετάται ο Επαγωγικός Λογικός Προγραμματισμός μέσα απο το πρίσμα της μάθησης της Γραμματικής της αγγλικής γλώσσας. Ο λόγος που επιλέχθηκε αυτό το πρόβλημα είναι ότι εξομοιώνει, μέχρι ενός σγημείου, τον τρόπο που τα παιδιά μαθαίνουν να μιλούν κάποια γλώσσα, υπό την έννοια ότι μαθαίνουν να μιλάνε χωρίς να έρθουν σε επαφή με τους κανόνες – τη γραμματική – της γλώσσας, αλλά από την επαφή τους με τα με τα ερεθίσματα – τα παραδείγματα – που έχουν από τον περίγυρό τους. / This paper is about Inductive Logic Programming through the prism of a problem. In our case Grammar Learning.