Refine
Year of publication
- 2007 (37) (remove)
Document Type
- Report (37) (remove)
Has Fulltext
- yes (37)
Keywords
- numerical upscaling (4)
- Dienstgüte (3)
- Darcy’s law (2)
- Formalisierung (2)
- effective heat conductivity (2)
- hub location (2)
- single phase flow (2)
- 3D (1)
- Ad-hoc-Netz (1)
- Asymptotic Expansion (1)
Faculty / Organisational entity
In this article, we present an analytic solution for Jiang's constitutive model of elastoplasticity. It is considered in its stress controlled form for proportional stress loading under the assumptions that the one-to-one coupling of the yield surface radius and the memory surface radius is switched off, that the transient hardening is neglected and that the ratchetting exponents are constant.
Abstraction is intensively used in the verification of large, complex or infinite-state systems. With abstractions getting more complex it is often difficult to see whether they are valid. However, for using abstraction in model checking it has to be ensured that properties are preserved. In this paper, we use a translation validation approach to verify property preservation of system abstractions. We formulate a correctness criterion based on simulation between concrete and abstract system for a property to be verified. For each distinct run of the abstraction procedure the correctness is verified in the theorem prover Isabelle/HOL. This technique is applied in the verification of embedded adaptive systems. This paper is an extended version a previously published work.
On the Complexity of the Uncapacitated Single Allocation p-Hub Median Problem with Equal Weights
(2007)
The Super-Peer Selection Problem is an optimization problem in network topology construction. It may be cast as a special case of a Hub Location Problem, more exactly an Uncapacitated Single Allocation p-Hub Median Problem with equal weights. We show that this problem is still NP-hard by reduction from Max Clique.
In this article we give a sufficient condition that a simply connected flexible body does not penetrate itself, if it is subjected to a continuous deformation. It is shown that the deformation map is automatically injective, if it is just locally injective and injective on the boundary of the body. Thereby, it is very remarkable that no higher regularity assumption than continuity for the deformation map is required. The proof exclusively relies on homotopy methods and the Jordan-Brouwer separation theorem.
Guaranteeing correctness of compilation is a ma jor precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof, one can be sure that the compiler produced correct code. This paper presents a certifying code generation phase for a compiler translating an intermediate language into assembler code. The time spent for checking the proofs is the bottleneck of certifying compilation. We exhibit an improved framework for certifying compilation and considerable advances to overcome this bottleneck. We compare our implementation featuring the Coq theorem prover to an older implementation. Our current implementation is feasible for medium to large sized programs.
This paper deals with the problem of determining the sea surface topography from geostrophic flow of ocean currents on local domains of the spherical Earth. In mathematical context the problem amounts to the solution of a spherical differential equation relating the surface curl gradient of a scalar field (sea surface topography) to a surface divergence-free vector field(geostrophic ocean flow). At first, a continuous solution theory is presented in the framework of an integral formula involving Green’s function of the spherical Beltrami operator. Different criteria derived from spherical vector analysis are given to investigate uniqueness. Second, for practical applications Green’s function is replaced by a regularized counterpart. The solution is obtained by a convolution of the flow field with a scaled version of the regularized Green function. Calculating locally without boundary correction would lead to errors near the boundary. To avoid these Gibbs phenomenona we additionally consider the boundary integral of the corresponding region on the sphere which occurs in the integral formula of the solution. For reasons of simplicity we discuss a spherical cap first, that means we consider a continuously differentiable (regular) boundary curve. In a second step we concentrate on a more complicated domain with a non continuously differentiable boundary curve, namely a rectangular region. It will turn out that the boundary integral provides a major part for stabilizing and reconstructing the approximation of the solution in our multiscale procedure.
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Existing approaches to the specification of network QoS requirements are mainly focused on specific domains or individual system layers. In this paper, we present a holistic, comprehensive formalization of network QoS requirements, across layers. QoS requirements are specified on each layer by defining QoS domain, consisting of QoS performance, reliability, and guarantee, and QoS scalability, with utility and cost functions. Furthermore, we derive preorders on multi-dimensional QoS domains, and present criteria to reduce these domains, leading to a manageable subset of QoS values that is sufficient for system design and implementation. We illustrate our approach by examples from the case study Wireless Video Transmission.
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Since QoS functionalities are integrated across layers and hence QoS specifications exist on different system layers, a QoS mapping technique is needed to translate the specifications into each other. In this paper, we formalize the relationship between layers. Based on a comprehensive and holistic formalization of network QoS requirements, we define two kinds of QoS mappings. QoS domain mappings associate QoS domains of two abstraction levels. QoS scalability mappings associate utility and cost functions of two abstraction levels. We illustrate our approach by examples from the case study Wireless Video Transmission.
The provision of quality-of-service (QoS) on the network layer is a major challenge in communication networks. This applies particularly to mobile ad-hoc networks (MANETs) in the area of Ambient Intelligence (AmI), especially with the increasing use of delay and bandwidth sensitive applications. The focus of this survey lies on the classification and analysis of selected QoS routing protocols in the domain of mobile ad-hoc networks. Each protocol is briefly described and assessed, and the results are summarized in multiple tables.
In this expository article, we give an introduction into the basics of bootstrap tests in general. We discuss the residual-based and the wild bootstrap for regression models suitable for applications in signal and image analysis. As an illustration of the general idea, we consider a particular test for detecting differences between two noisy signals or images which also works for noise with variable variance. The test statistic is essentially the integrated squared difference between the signals after denoising them by local smoothing. Determining its quantile, which marks the boundary between accepting and rejecting the hypothesis of equal signals, is hardly possible by standard asymptotic methods whereas the bootstrap works well. Applied to the rows and columns of images, the resulting algorithm not only allows for the detection of defects but also for the characterization of their location and shape in surface inspection problems.
In this paper we propose a general approach solution method for the single facility ordered median problem in the plane. All types of weights (non-negative, non-positive, and mixed) are considered. The big triangle small triangle approach is used for the solution. Rigorous and heuristic algorithms are proposed and extensively tested on eight different problems with excellent results.
Abstract. The stationary, isothermal rotational spinning process of fibers is considered. The investigations are concerned with the case of large Reynolds (± = 3/Re ¿ 1) and small Rossby numbers (\\\" ¿ 1). Modelling the fibers as a Newtonian fluid and applying slender body approximations, the process is described by a two–point boundary value problem of ODEs. The involved quantities are the coordinates of the fiber’s centerline, the fluid velocity and viscous stress. The inviscid case ± = 0 is discussed as a reference case. For the viscous case ± > 0 numerical simulations are carried out. Transfering some properties of the inviscid limit to the viscous case, analytical bounds for the initial viscous stress of the fiber are obtained. A good agreement with the numerical results is found. These bounds give strong evidence, that for ± > 3\\\"2 no physical relevant solution can exist. A possible interpretation of the above coupling of ± and \\\" related to the die–swell phenomenon is given.
It has been empirically verified that smoother intensity maps can be expected to produce shorter sequences when step-and-shoot collimation is the method of choice. This work studies the length of sequences obtained by the sequencing algorithm by Bortfeld and Boyer using a probabilistic approach. The results of this work build a theoretical foundation for the up to now only empirically validated fact that if smoothness of intensity maps is considered during their calculation, the solutions can be expected to be more easily applied.
An algorithm for automatic parallel generation of three-dimensional unstructured computational meshes based on geometrical domain decomposition is proposed in this paper. Software package build upon proposed algorithm is described. Several practical examples of mesh generation on multiprocessor computational systems are given. It is shown that developed parallel algorithm enables us to reduce mesh generation time significantly (dozens of times). Moreover, it easily produces meshes with number of elements of order 5 · 107, construction of those on a single CPU is problematic. Questions of time consumption, efficiency of computations and quality of generated meshes are also considered.
Abstract — Various advanced two-level iterative methods are studied numerically and compared with each other in conjunction with finite volume discretizations of symmetric 1-D elliptic problems with highly oscillatory discontinuous coefficients. Some of the methods considered rely on the homogenization approach for deriving the coarse grid operator. This approach is considered here as an alternative to the well-known Galerkin approach for deriving coarse grid operators. Different intergrid transfer operators are studied, primary consideration being given to the use of the so-called problemdependent prolongation. The two-grid methods considered are used as both solvers and preconditioners for the Conjugate Gradient method. The recent approaches, such as the hybrid domain decomposition method introduced by Vassilevski and the globallocal iterative procedure proposed by Durlofsky et al. are also discussed. A two-level method converging in one iteration in the case where the right-hand side is only a function of the coarse variable is introduced and discussed. Such a fast convergence for problems with discontinuous coefficients arbitrarily varying on the fine scale is achieved by a problem-dependent selection of the coarse grid combined with problem-dependent prolongation on a dual grid. The results of the numerical experiments are presented to illustrate the performance of the studied approaches.
This work presents a new framework for Gröbner basis computations with Boolean polynomials. Boolean polynomials can be modeled in a rather simple way, with both coefficients and degree per variable lying in {0, 1}. The ring of Boolean polynomials is, however, not a polynomial ring, but rather the quotient ring of the polynomial ring over the field with two elements modulo the field equations x2 = x for each variable x. Therefore, the usual polynomial data structures seem not to be appropriate for fast Gröbner basis computations. We introduce a specialized data structure for Boolean polynomials based on zero-suppressed binary decision diagrams (ZDDs), which is capable of handling these polynomials more efficiently with respect to memory consumption and also computational speed. Furthermore, we concentrate on high-level algorithmic aspects, taking into account the new data structures as well as structural properties of Boolean polynomials. For example, a new useless-pair criterion for Gröbner basis computations in Boolean rings is introduced. One of the motivations for our work is the growing importance of formal hardware and software verification based on Boolean expressions, which suffer – besides from the complexity of the problems – from the lack of an adequate treatment of arithmetic components. We are convinced that algebraic methods are more suited and we believe that our preliminary implementation shows that Gröbner bases on specific data structures can be capable to handle problems of industrial size.
This report reviews selected image binarization and segmentation methods that have been proposed and which are suitable for the processing of volume images. The focus is on thresholding, region growing, and shape–based methods. Rather than trying to give a complete overview of the field, we review the original ideas and concepts of selected methods, because we believe this information to be important for judging when and under what circumstances a segmentation algorithm can be expected to work properly.
In this work, we analyze two important and simple models of short rates, namely Vasicek and CIR models. The models are described and then the sensitivity of the models with respect to changes in the parameters are studied. Finally, we give the results for the estimation of the model parameters by using two different ways.
With the ever-increasing significance of software in our everyday lives, it is vital to afford reliable software quality estimates. Typically, quantitative software quality analyses rely on either statistical fault prediction methods (FPMs) or stochastic software reliability growth models (SRGMs). Adopting solely FPMs or SRGMs, though, may result in biased predictions that do not account for uncertainty in the distinct prediction methods; thus rendering the prediction less reliable. This paper identifies flaws of the individual prediction methods and suggests a hybrid prediction approach that combines FPMs and SRGMs. We adopt FPMs for initially estimating the expected number of failures for fi- nite failure SRGMs. Initial parameter estimates yield more accurate reliability predictions until sufficient failures are observed that enable stable parameter estimates in SRGMs. Being at the equilibrium level of FPM and SRGM pre- dictions we suggest combining the competing prediction methods with respect to the principle of heterogeneous redundancy. That is, we propose using the in- dividual methods separately and combining their predictions. In this paper we suggest Bayesian model averaging (BMA) for combining the different methods. The hybrid approach allows early reliability estimates and encourages higher confidence in software quality predictions.
This paper disscuses the minimal area rectangular packing problem of how to pack a set of specified, non-overlapping rectangels into a rectangular container of minimal area. We investigate different mathematical programming approaches of this and introduce a novel approach based on non-linear optimization and the \\\"tunneling effect\\\" achieved by a relaxation of the non-overlapping constraints.