### Refine

#### Year of publication

- 1999 (351) (remove)

#### Document Type

- Preprint (351) (remove)

#### Language

- English (351) (remove)

#### Keywords

- Case-Based Reasoning (5)
- Location Theory (5)
- case-based problem solving (5)
- Abstraction (4)
- Knowledge Acquisition (4)
- Fallbasiertes Schließen (3)
- Internet (3)
- Knowledge acquisition (3)
- Multicriteria Optimization (3)
- case-based reasoning (3)

#### Faculty / Organisational entity

A growing share of all software development project work is being done by geographically distributed teams. To satisfy shorter product design cycles, expert team members for a development project may need to be r ecruited globally. Yet to avoid extensive travelling or r eplacement costs, distributed project work is preferred. Current-generation software engineering tools and ass ociated systems, processes, and methods were for the most part developed to be used within a single enterprise. Major innovations have lately been introduced to enable groupware applications on the Internet to support global collaboration. However, their deployment for distributed software projects requires further research. In partic ular, groupware methods must seamlessly be integrated with project and product management systems to make them attractive for industry. In this position paper we outline the major challenges concerning distributed (virtual) software projects. Based on our experiences with software process modeling and enactment environments, we then propose approaches to solve those challenges.

MOLTKE is a research project dealing with a complex technical application. After describing the domain of CNCmachining centers and the applied KA methods, we summarize the concrete KA problems which we have to handle. Then we describe a KA mechanism which supports an engineer in developing a diagnosis system. In chapter 6 weintroduce learning techniques operating on diagnostic cases and domain knowledge for improving the diagnostic procedure of MOLTKE. In the last section of this chapter we outline some essential aspects of organizationalknowledge which is heavily applied by engineers for analysing such technical systems (Qualitative Engineering). Finally we give a short overview of the actual state of realization and our future plans.

In this paper we will present a design model (in the sense of KADS) for the domain of technical diagnosis. Based on this we will describe the fully implemented expert system shell MOLTKE 3.0, which integrates common knowledge acquisition methods with techniques developed in the fields of Model-Based Diagnosis and Machine Learning, especially Case-Based Reasoning.

Case-based knowledge acquisition, learning and problem solving for diagnostic real world tasks
(1999)

Within this paper we focus on both the solution of real, complex problems using expert system technology and the acquisition of the necessary knowledge from a case-based reasoning point of view. The development of systems which can be applied to real world problems has to meet certain requirements. E.g., all available information sources have to be identified and utilized. Normally, this involves different types of knowledge for which several knowledge representation schemes are needed, because no scheme is equally natural for all sources. Facing empirical knowledge it is important to complement the use of manually compiled, statistic and otherwise induced knowledge by the exploitation of the intuitive understandability of case-based mechanisms. Thus, an integration of case-based and alternative knowledge acquisition and problem solving mechanisms is necessary. For this, the basis is to define the "role" which case-based inference can "play" within a knowledge acquisition workbench. We will discuss a concrete casebased architecture, which has been applied to technical diagnosis problems, and its integration into a knowledge acquisition workbench which includes compiled knowledge and explicit deep models, additionally.

Today, the worlds and terminologies of mechanical engineering and software engineering coexist, but they do not always work together seamlessly. Both worlds have developed their own separate formal vocabulary for expressing their concepts as well as for capturing and communicating their respective domain knowledge. But, these two vocabularies are not unified, interwoven, or at least interconnected in a reasonable manner. Thus, the subject of this paper is a comparison of the vocabularies of the two fields, namely feature technology from the area of mechanical engineering and software design patterns from the software engineering domain. Therefore, a certain amount of definitions, history, examples, etc. is presented for features as well as for design patterns. After this, an analysis is carried out to identify analogies and differences. The main intention of this paper is to inform both worlds - mechanical and software engineering - about the other side's terminology and to start a discussion about potential mutual benefits and possibilities to bridge the gap between these two worlds, e.g. to improve the manageability of CAx product development processes.

PANDA is a run-time package based on a very small operating system kernel which supports distributed applications written in C++. It provides powerful abstractions such as very efficient user-level threads, a uniform global address space, object and thread mobility, garbage collection, and persistent objects. The paper discusses the design ration- ales underlying the PANDA system. The fundamental features of PANDA are surveyed, and their implementation in the current prototype environment is outlined.

Distributed systems are an alternative to shared-memorymultiprocessors for the execution of parallel applications.PANDA is a runtime system which provides architecturalsupport for efficient parallel and distributed program-ming. PANDA supplies means for fast user-level threads,and for a transparent and coordinated sharing of objectsacross a homogeneous network. The paper motivates themajor architectural choices that guided our design. Theproblem of sharing data in a distributed environment isdiscussed, and the performance of appropriate mecha-nisms provided by the PANDA prototype implementation isassessed.

As the properties of components have gradually become clearer, attention has started to turn to the architectural issues which govern their interaction and composition. In this paper we identify some of the major architectural questions affecting component-based software develop-ment and describe the predominant architectural dimensions. Of these, the most interesting is the "architecture hierarchy" which we believe is needed to address the "interface vicissitude" problem that arises whenever interaction refinement is explicitly documented within a component-based system. We present a solution to this problem based on the concept of stratified architectures and object metamorphosis Finally, we describe how these concepts may assist in increasing the tailorability of component-based frameworks.

This paper presents a new kind of abstraction, which has been developed for the purpose of proofplanning. The basic idea of this paper is to abstract a given theorem and to find an abstractproof of it. Once an abstract proof has been found, this proof has to be refined to a real proofof the original theorem. We present a goal oriented abstraction for the purpose of equality proofplanning, which is parameterized by common parts of the left- and right-hand sides of the givenequality. Therefore, this abstraction technique provides an abstract equality problem which ismore adequate than those generated by the abstractions known so far. The presented abstractionalso supports the heuristic search process based on the difference reduction paradigm. We give aformal definition of the abstract space including the objects and their manipulation. Furthermore,we prove some properties in order to allow an efficient implementation of the presented abstraction.

In this paper we show that distributing the theorem proving task to several experts is a promising idea. We describe the team work method which allows the experts to compete for a while and then to cooperate. In the cooperation phase the best results derived in the competition phase are collected and the less important results are forgotten. We describe some useful experts and explain in detail how they work together. We establish fairness criteria and so prove the distributed system to be both, complete and correct. We have implementedour system and show by non-trivial examples that drastical time speed-ups are possible for a cooperating team of experts compared to the time needed by the best expert in the team.

We investigate one of the classical problems of the theory ofterm rewriting, namely termination. We present an ordering for compar-ing higher-order terms that can be utilized for testing termination anddecreasingness of higher-order conditional term rewriting systems. Theordering relies on a first-order interpretation of higher-order terms anda suitable extension of the RPO.

In this paper we are interested in an algebraic specification language that (1) allowsfor sufficient expessiveness, (2) admits a well-defined semantics, and (3) allows for formalproofs. To that end we study clausal specifications over built-in algebras. To keep thingssimple, we consider built-in algebras only that are given as the initial model of a Hornclause specification. On top of this Horn clause specification new operators are (partially)defined by positive/negative conditional equations. In the first part of the paper wedefine three types of semantics for such a hierarchical specification: model-theoretic,operational, and rewrite-based semantics. We show that all these semantics coincide,provided some restrictions are met. We associate a distinguished algebra A spec to ahierachical specification spec. This algebra is initial in the class of all models of spec.In the second part of the paper we study how to prove a theorem (a clause) valid in thedistinguished algebra A spec . We first present an abstract framework for inductive theoremprovers. Then we instantiate this framework for proving inductive validity. Finally wegive some examples to show how concrete proofs are carried out.This report was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)

Chains of Recurrences (CRs) are a tool for expediting the evaluation of elementary expressions over regular grids. CR based evaluations of elementaryexpressions consist of 3 major stages: CR construction, simplification, and evaluation. This paper addresses CR simplifications. The goal of CRsimplifications is to manipulate a CR such that the resulting expression is more efficiently to evaluate. We develop CR simplification strategies which takethe computational context of CR evaluations into account. Realizing that it is infeasible to always optimally simplify a CR expression, we give heuristicstrategies which, in most cases, result in a optimal, or close-to-optimal expressions. The motivations behind our proposed strategies are discussed and theresults are illustrated by various examples.

The problem of providing connectivity for a collection of applications is largely one of data integration: the communicating parties must agree on thesemantics and syntax of the data being exchanged. In earlier papers [#!mp:jsc1!#,#!sg:BSG1!#], it was proposed that dictionaries of definitions foroperators, functions, and symbolic constants can effectively address the problem of semantic data integration. In this paper we extend that earlier work todiscuss the important issues in data integration at the syntactic level and propose a set of solutions that are both general, supporting a wide range of dataobjects with typing information, and efficient, supporting fast transmission and parsing.

We report results of the switching properties of Stoner-like magnetic particles subject to short magnetic field pulses, obtained by numerical investigations. We discuss the switching properties as a function of the external field pulse strength and direction, the pulse length and the pulse shape. For field pulses long compared to the ferromagnetic resonance precession time the switching behavior is governed by the magnetic damping term, whereas in the limit of short field pulses the switching properties are dominated by the details of the precession of the magnetic moment. In the latter case, by choosing the right field pulse parameters, the magnetic damping term is of minor importance and ultrafast switching can be achieved. Switching can be obtained in an enlarged angular range of the direction of the applied field compared to the case of long pulses.

A multiscale method is introduced using spherical (vector) wavelets for the computation of the earth's magnetic field within source regions of ionospheric and magnetospheric currents. The considerations are essentially based on two geomathematical keystones, namely (i) the Mie representation of solenoidal vector fields in terms of toroidal and poloidal parts and (ii) the Helmholtz decomposition of spherical (tangential) vector fields. Vector wavelets are shown to provide adequate tools for multiscale geomagnetic modelling in form of a multiresolution analysis, thereby completely circumventing the numerical obstacles caused by vector spherical harmonics. The applicability and efficiency of the multiresolution technique is tested with real satellite data.

We show how to prove ground confluence of term rewrite relations that areinduced by reductive systems of clausal rewrite rules. According to a well-knowncritical pair criterion it suffices for such systems to prove ground joinability ofa suitable set of 'critical clauses'. We outline how the latter can be done in asystematic fashion, using mathematical induction as a key concept of reasoning.

We describe a technique to make application programs fault tolerant. This techADnique is based on the concept of checkpointing from an active program to one ormore passive backup copies which serve as an abstraction of stable memory. Ifthe primary copy fails, one of the backup copies takes over and resumes processADing service requests. After each failure a new backup copy is created in order torestore the replication degree of the service. All mechanisms necessary to achieveand maintain fault tolerance can be added automatically to the code of a nonADfaulttolerant server, thus making fault tolerance completely transparent for the applicaADtion programmer.

We present a new software architecture in which all concepts necessary to achieve fault tolerance can be added to an appli- cation automatically without any source code changes. As a case study, we consider the problem of providing a reliable service despite node failures by executing a group of replicat- ed servers. Replica creation and management as well as fail- ure detection and recovery are performed automatically by a separate fault tolerance layer (ft-layer) which is inserted be- tween the server application and the operating system kernel. The layer is invisible for the application since it provides the same functional interface as the operating system kernel, thus making the fault tolerance property of the service completely transparent for the application. A major advantage of our ar- chitecture is that the layer encapsulates both fault tolerance mechanisms and policies. This allows for maximum flexibility in the choice of appropriate methods for fault tolerance with- out any changes in the application code.

This paper presents a completely systematic design procedure for asynchronous controllers.The initial step is the construction of a signal transition graph (STG, an interpreted Petri net) ofthe dialog between data path and controller: a formal representation without reference to timeor internal states. To implement concurrently operating control structures, and also to reducedesign effort and circuit cost, this STG can be decomposed into overlapping subnets. A univer-sal initial solution is then obtained by algorithmically constructing a primitive flow table fromeach component net. This step links the procedure to classical asynchronous design, in particu-lar to its proven optimization methods, without restricting the set of solutions. In contrast toother approaches, there is no need to extend the original STG intuitively.

Coordinating distributed processes, especially engineering and software design processes, has been a research topic for some time now. Several approaches have been published that aim at coordinating large projects in general, and large software development processes in specific. However, most of these approaches focus on the technical part of the design process and omit management activities like planning and scheduling the project, or monitoring it during execution. In this paper, we focus on coordinating the management activities that accompany the technical software design process. We state the requirements for a Software Engineering Environm ent (SEE) accommodating management, and we describe a possible architecture for such an SEE.

This paper describes the architecture and concept of operation of a Framework for Adaptive Process Modeling and Execution (FAME). The research addresses the absence of robust methods for supporting the software process management life cycle. FAME employs a novel, model-based approach in providing automated support for different activities in the software development life cycle including project definition, process design, process analysis, process enactment, process execution status monitoring, and execution status-triggered process redesign. FAME applications extend beyond the software development domain to areas such as agile manufacturing, project management, logistics planning, and business process reengineering.

In this paper we present an extensional higher-order resolution calculus that iscomplete relative to Henkin model semantics. The treatment of the extensionality princi-ples - necessary for the completeness result - by specialized (goal-directed) inference rulesis of practical applicability, as an implentation of the calculus in the Leo-System shows.Furthermore, we prove the long-standing conjecture, that it is sufficient to restrict the orderof primitive substitutions to the order of input formulae.

Abstract: Random matrix theory (RMT) is a powerful statistical tool to model spectral fluctuations. In addition, RMT provides efficient means to separate different scales in spectra. Recently RMT has found application in quantum chromodynamics (QCD). In mesoscopic physics, the Thouless energy sets the universal scale for which RMT applies. We try to identify the equivalent of a Thouless energy in complete spectra of the QCD Dirac operator with staggered fermions and SU_(2) lattice gauge fields. Comparing lattice data with RMT predictions we find deviations which allow us to give an estimate for this scale.

Beyond the Thouless energy
(1999)

Abstract: The distribution and the correlations of the small eigenvalues of the Dirac operator are described by random matrix theory (RMT) up to the Thouless energy E_= 1 / sqrt (V), where V is the physical volume. For somewhat larger energies, the same quantities can be described by chiral perturbation theory (chPT). For most quantities there is an intermediate energy regime, roughly 1/V < E < 1/sqrt (V), where the results of RMT and chPT agree with each other. We test these predictions by constructing the connected and disconnected scalar susceptibilities from Dirac spectra obtained in quenched SU(2) and SU(3) simulations with staggered fermions for a variety of lattice sizes and coupling constants. In deriving the predictions of chPT, it is important totake into account only those symmetries which are exactly realized on the lattice.

Abstract: Recently, the chiral logarithms predicted by quenched chiral perturbation theory have been extracted from lattice calculations of hadron masses. We argue that the deviations of lattice results from random matrix theory starting around the so-called Thouless energy can be understood in terms of chiral perturbation theory as well. Comparison of lattice data with chiral perturbation theory formulae allows us to compute the pion decay constant. We present results from a calculation for quenched SU(2) with Kogut-Susskind fermions at ß = 2.0 and 2.2.

Abstract: Recently, the contributions of chiral logarithms predicted by quenched chiral perturbation theory have been extracted from lattice calculations of hadron masses. We argue that a detailed comparison of random matrix theory and lattice calculations allows for a precise determination of such corrections. We estimate the relative size of the m log(m), m, and m^2 corrections to the chiral condensate for quenched SU(2).

We present results from a study of the coherence properties of a system involving three discrete states coupled to each other by two-photon processes via a common continuum. This tripod linkage is an extension of the standard laser-induced continuum structure (LICS) which involves two discrete states and two lasers. We show that in the tripod scheme, there exist two population trapping conditions; in some cases these conditions are easier to satisfy than the single trapping condition in two-state LICS. Depending on the pulse timing, various effects can be observed. We derive some basic properties of the tripod scheme, such as the solution for coincident pulses, the behaviour of the system in the adiabatic limit for delayed pulses, the conditions for no ionization and for maximal ionization, and the optimal conditions for population transfer between the discrete states via the continuum. In the case when one of the discrete states is strongly coupled to the continuum, the population dynamics reduces to a standard two-state LICS problem (involving the other two states) with modified parameters; this provides the opportunity to customize the parameters of a given two-state LICS system.

Abstract: We propose a simple method for measuring the populations and the relative phase in a coherent superposition of two atomic states. The method is based on coupling the two states to a third common (excited) state by means of two laser pulses, and measuring the total fluorescence from the third state for several choices of the excitation pulses.

Collecting Experience on the Systematic Development of CBR Applications using the INRECA Methodology
(1999)

This paper presents an overview of the INRECA methodology for building and maintaining CBR applications. This methodology supports the collection and reuse of experience on the systematic development of CBR applications. It is based on the experience factory and the software process modeling approach from software engineering. CBR development experience is documented using software process models and stored in different levels of generality in a three-layered experience base. Up to now, experience from 9 industrial projects enacted by all INRECA II partners has been collected.

Complex problem solving can be substantially improved by the reuse of experience from previously solved problems. This requires that case libraries of successful problem solutions are transformed into problem solving knowledge with high utility, i.e. knowledge which causes high savings in search time, high application probability and low matching costs in a respective performance component. Planning can be improved by explanation-based learning (EBL) of abstract plans from detailed, successfully solved planning problems. Abstract plans, expressed in well-established terms of the domain, serve as useful problem decompositions which can drastically reduce the planning complexity. Abstractions which are valid for a class of planning cases rather than for a single case, ensure a successful application in a larger spectrum of new situations. The hierarchical organization of the learned shared abstractions causes low matching costs. The presented S-PABS procedure is an EBL-procedure in which abstraction, learning from multiple examples and hierarchical clustering are combined to automatically construct a hierarchy of shared abstract plans by analyzing concrete planning cases. A specific planning procedure has been designed to solve new planning problems guided by the knowledge learned by S-PABS. By allowing a feedback from this planning procedure to the learning component, the integrated system shows an increase in performance through past problem solving.

Although skeletal plan refinement is used in several planning systems, a procedure for the automatic acquisition of such high-level plans has not yet been developed. The proposed explanation- based knowledge acquisition procedure constructs a skeletal plan automatically from a sophisticated concrete planning case. The classification of that case into a well-described class of problems serves as an instrument for adjusting the applicability of the acquired skeletal plans to that class. The four phases of the proposed procedure are constituted as follows: In the first phase, the execution of the source plan is simulated, and explanations for the effects of the occurred operators are constructed. In the second phase, the generalization of these explanations is performed with respect to a criterion of operationality which specifies the vocabulary for defining abstract operators for the skeletal plan. The third phase, a dependency analysis of the resulting operator effects, unveils the interactions of the concrete plan which are substantial for the specified class. In the forth phase, the concept descriptions for the abstract operators of the skeletal plan are formed by collecting and normalizing the important constraints for each operation that were indicated by the dependencies. With this procedure sophisticated planning solutions from human experts can be generalized into skeletal plans and consequently be reused by a planning system in novel situations.

Abstraction is one of the most promising approaches to improve the performance of problem solvers. Abstraction by dropping sentences of a domain description - as used in most hierarchical planners - is known to be very representation dependent. To overcome these drawbacks, we propose a more general view of abstraction involving the change of representation language. We have developed a new abstraction methodology and a related sound and complete learning algorithm that allows the complete change of representation language of planning cases from concrete to abstract.

Recently, the use of abstraction in case-based reasoning (CBR) is getting more and more popular. The basic idea is to supply a CBR system with cases at many different levels of abstraction. When a new problem must be solved, one (or several) 'appropriate' concrete or abstract case are retrieved from the case base and the solution that the case contains is reused to derive a solution for the current problem, e.g. by filling in the details that a retrieved case at some higher level of abstraction does not contain. A major problem that occurs when using this approach is, that for a given new problem, usually several cases, e.g., from different levels of abstraction could be reused to solve the new problem. Choosing a wrong abstract case can slow down the problem solving process or even prevents the problem from being solved.

Hierachical planning can be improved by explanation-based learning (EBL) of abstract plans from detailed, successfully solved planning problems. Abstract plans, expressed in well-established terms of the domain, serve as useful problem decompositions which can drastically reduce the planning complexity. The learned plan abstraction must be valid for a class of planning cases rather than for a single case, to ensure their successful application in a larger spectrum of new situations. A hierarchical organization of the newly learned knowledge must be archieved to overcome the utility problem in EBL. This paper presents a new formal model of shared plan abstraction and the closely related explanation-based procedure S-PABS. Unlike other apporaches to plan abstraction, our model allows a total different terminology to be introduced at the abstract level. Finally, an unsupervised incremental procedure for constructing a hierachy of shared abstract plans is proposed, as a kind of concept formation over explanations.

Planning means constructing a course of actions to achieve a specified set of goals when starting from an initial situation. For example, determining a sequence of actions (a plan) for transporting goods from an initial location to some destination is a typical planning problem in the transportation domain. Many planning problems are of practical interest.

In this paper, we propose the PARIS approach for improving complex problem solving by learning from previous cases. In this approach, abstract planning cases are learned from given concrete cases. For this purpose, we have developed a new abstraction methodology that allows to completely change the representation language of a planning case, when the concrete and abstract languages are given by the user. Furthermore, we present a learning algorithm which is correct and complete with respect to the introduced model. An empirical study in the domain of process planning in mechanical engineering shows significant improvements in planning efficiency through learning abstract cases while an explanation-based learning method only causes a very slight improvement.

Abstraction is one of the most promising approaches to improve the performance of problem solvers. In several domains abstraction by dropping sentences of a domain description - as used in most hierarchical planners - has proven useful. In this paper we present examples which illustrate significant drawbacks of abstraction by dropping sentences. To overcome these drawbacks, we propose a more general view of abstraction involving the change of representation language. We have developed a new abstraction methodology and a related sound and complete learning algorithm that allows the complete change of representation language of planning cases from concrete to abstract. However, to achieve a powerful change of the representation language, the abstract language itself as well as rules which describe admissible ways of abstracting states must be provided in the domain model. This new abstraction approach is the core of PARIS (Plan Abstraction and Refinement in an Integrated System), a system in which abstract planning cases are automatically learned from given concrete cases. An empirical study in the domain of process planning in mechanical engineering shows significant advantages of the proposed reasoning from abstract cases over classical hierarchical planning.^

Case-based problem solving can be significantly improved by applying domain knowledge (in opposition to problem solving knowledge), which can be acquired with reasonable effort, to derive explanations of the correctness of a case. Such explanations, constructed on several levels of abstraction, can be employed as the basis for similarity assessment as well as for adaptation by solution refinement. The general approach for explanation-based similarity can be applied to different real world problem solving tasks such as diagnosis and planning in technical areas. This paper presents the general idea as well as the two specific, completely implemented realizations for a diagnosis and a planning task.

In this paper we deal with an NP-hard combinatorial optimization problem, the k-cardinality tree problem in node weighted graphs. This problem has several applications , which justify the need for efficient methods to obtain good solutions. We review existing literature on the problem. Then we prove that under the condition that the graph contains exactly one trough, the problem can be solved in ploynomial time. For the general NP-hard problem we implemented several local search methods to obtain heuristics solutions, which are qualitatively better than solutions found by constructive heuristics and which require significantly less time than needed to obtain optimal solutions. We used the well known concepts of genetic algorithms and tabu search with useful extensions. We show that all the methods find optimal solutions for the class of graphs containing exactly one trough. The general performance of our methods as compared to other heuristics is illustrated by numerical results.

Moment inequalities for the Boltzmann equation and applications to spatially homogeneous problems
(1999)

Some inequalities for the Boltzmann collision integral are proved. These inequalities can be considered as a generalization of the well-known Povzner inequality. The inequalities are used to obtain estimates of moments of solution to the spatially homogeneous Boltzmann equation for a wide class of intermolecular forces. We obtained simple necessary and sufficient conditions (on the potential) for the uniform boundedness of all moments. For potentials with compact support the following statement is proved. .....

Complete presentations provide a natural solution to the word problem in monoids and groups. Here we give a simple way to construct complete presentations for the direct product of groups, when such presentations are available for the factors. Actually, the construction we are referring to is just the classical construction for direct products of groups, which has been known for a long time, but whose completeness-preserving properties had not been detected. Using this result and some known facts about Coxeter groups, we sketch an algorithm to obtain the complete presentation of any finite Coxeter group. A similar application to Abelian and Hamiltonian groups is mentioned.

To present the decision maker's (DM) preferences in multicriteria decision problems as a partially ordered set is an effective method to catch the DM's purpose and avoid misleading results. Since our paper is focused on minimal path problems, we regard the ordered set of edges (E,=). Minimal paths are defined in repect to power-ordered sets which provides an essential tool to solve such problems. An algorithm to detect minimal paths on a multicriteria minimal path problem is presented

The feature interaction problem in telecommunications systems increasingly obstructsthe evolution of such systems. We develop formal detection criteria which render anecessary (but less than sufficient) condition for feature interactions. It can be checkedmechanically and points out all potentially critical spots. These have to be analyzedmanually. The resulting resolution decisions are incorporated formally. Some prototypetool support is already available. A prerequisite for formal criteria is a formal definitionof the problem. Since the notions of feature and feature interaction are often used in arather fuzzy way, we attempt a formal definition first and discuss which aspects can beincluded in a formalization (and therefore in a detection method). This paper describeson-going work.