Catálogo de publicaciones - libros

Artificial Intelligence techniques have massively been applied for Intelligent Tutor systems (ITS), e.g., user modeling, error diagnosis, user adaptation, knowledge representation, and dialog techniques. In this paper, I will argue in favor of the application of another AI-technique in ITS, namely of proof planning, a methodology from automated theorem proving.

The aim of the MMiSS project is the construction of a multi-media Internet-based adaptive educational system. Its content will initially cover a whole curriculum in the area of Safe and Secure Systems. Traditional teaching materials (slides, handouts, annotated course material, assignments and so on) are to be converted into a new hypermedia format, integrated with tool interactions for formally developing correct software; they will be suitable for learning on campus and distance learning, as well as interactive, supervised, or co-operative self-study. Coherence and consistency are especially emphasised, through extensive semantic linking of teaching elements, and through a process model borrowed from the theory of formal software development, enlarging the knowledge base with the help of version and configuration management, to ensure “sustainable development”, i.e. continuous long-term usability of the contents.

Software construction is essentially a modeling task. The most important decisions in software development are decisions that deal with modeling. The better, the more adequate and more powerful the available modeling paradigms are the easier the program development task is and the better its results are. In the following we describe the role of models in program development and show how closely the issue of modeling is related to the so-called formal methods in program development. We give a number of arguments the usage of mathematical models in software construction and back them up by some detailed examples.

The formal development of industrial-size software is an error-prone and therefore an evolutionary process. Verifying formal specifications usually reveals hidden errors causing the change of parts of the specification. Also adding new functionality will result in changes of the specification which always endangers the verification work already done. In this paper we describe the system which maintains formal developments. The -system supports an evolutionary formal development since it allows users to specify and verify developments in a structured manner, incorporates a uniform mechanism for verification in-the-large to exploit the structure of the specification, and maintains the verification work already done when changing the specification. relies on development graphs as a uniform representation of structured specifications, which enables the use of various (structured) specification languages to formalize the software development. Moreover, allows the integration of different theorem provers to deal with the actual proof obligations arising from the specification, i.e. to perform verification in-the-small.

Analysis of authentication cryptographic protocols, particularly finding flaws in them and determining a sequence of actions that an intruder can take to gain access to the information which a given protocol purports not to reveal, has recently received considerable attention. One effective way of detecting flaws is to hypothesize an insecure state and determine whether it is possible to get to that state by a legal sequence of actions permitted by the protocol from some legal initial state which captures the knowledge of the principals and the assumptions made about an intruder’s behavior. Relations among encryption and decryption functions as well as properties of number theoretic functions used in encryption and decryption can be specified as rewrite rules. This, for example, is the approach used by the NRL Protocol Analyzer, which uses narrowing to reason about such properties of cryptographic and number-theoretic functions.

Following [15], a related approach is proposed here in which equation solving modulo most of these properties of cryptographic and number-theoretic functions is done by developing new unification algorithms for such theories. A new unification algorithm for an equational theory needed to reason about protocols that use the Diffie-Hellman algorithm is developed. In this theory, multiplication forms an abelian group; exponentiation function distributes over multiplication, and exponents can commute. This theory is useful for analyzing protocols which use blinded signatures. It is proved that the unification problem over this equational theory can be reduced to the unification problem modulo the theory of abelian groups with commuting homomorphisms with an additional constraint. Baader’s unification algorithm for the theory of abelian groups with commuting homomorphisms, which reduces the unification problem to solving equations over the polynomial ring over the integers with the commuting homomorphisms serving as indeterminates, is generalized to give a unification algorithm over the theory of abelian groups with commuting homomorphism with a .

It is also shown that the unification problem over a (simple) extension of the equational theory considered here (which is also an extension of the equational theory considered in [15]) is undecidable.

The construction of security models from scratch is a difficult, time consuming, and expensive task. In this article, we demonstrate how to exploit generic concepts, in particular the concept of secure information flow, to simplify the construction of security models. Requirements concerned with confidentiality or integrity can often be expressed nicely as restrictions on the allowed flow of information. For a verification of these restrictions, it is necessary to explicate formally what information flow means. Various information flow properties have been suggested for this purpose and we employ , the “Modular Assembly Kit for Security” [Man00a], for a unified perspective on these properties. How to exploit the generic security models based on secure information flow in practice is described in the context of the VSE system [AHL00].

Formal software development turns out to become one of the key issues in software engineering. Today an enormous variety of methods and tools exist that serve as an aid for the software engineer to formally specify and verify large-scaled systems. This paper reviews some of the most important general notions in formal software engineering and, in particular, gives an overview on VSE (), a tool that supports both hierarchical specification and formal verification.

We present a work-in-progress on distributed planning, which relies on the “planning as satisfiability” paradigm. It allows for multi-agent cooperative planning by joining SAT-based planning and a particular approach to distributed propositional satisfiability. Each agent is thus enabled to plan on its own and communicate with other agents during the planning process, in such a way that synchronized and possibly cooperative plans come out as a result. We discuss in some details both piers of our construction: SAT-based planning techniques and distributed approaches to satisfiability. Then, we propose how to join them by presenting a working example.

In this paper we present an overview of recent developments in the plan-based control of autonomous robots. We identify computational principles that enable autonomous robots to accomplish complex, diverse, and dynamically changing tasks in challenging environments. These principles include plan-based high-level control, probabilistic reasoning, plan transformation, and context and resource-adaptive reasoning. We will argue that the development of comprehensive and integrated computational models of plan-based control requires us to consider different aspects of plan-based control – plan representation, reasoning, execution, and learning – together and not in isolation. This integrated approach enables us to exploit synergies between the different aspects and thereby come up with simpler and more powerful computational models.

In the second part of the paper we describe , our own approach to the development of a comprehensive computational model for the plan-based control of robotic agents. We show how the principles, described in the first part of the paper, are incorporated into the SRCs and summarize results of several long-term experiments that demonstrate the practicality of SRCs.

Computational experiments are reported involving the concept of , an agent’s direct, unmediated and accurate, but possibly incomplete, awareness of its future including states and events involving the agent itself. Foreknowledge is used here as a conceptual tool with which to explore certain issues around time and rationality. We first explain how foreknowledge in this sense may be given to the agents in an agent society on a computer. The generation of a world history is viewed as a process of solving a constraint satisfaction problem. Then we seek to understand the circumstances in which foreknowledge may be either beneficial or detrimental to a society of rational agents. A special case is when agents have foreknowledge of their own “deaths”. An experimental interpretation of this special case has been implemented, and results are presented and discussed. Finally, the work reported is briefly discussed in the context of current theories of time.