Search results for: Walter Hussak

Authors: Rafat Alshorman, Walter Hussak

Abstract:

Most of the concurrent transactional protocols consider serializability as a correctness criterion of the transactions execution. Usually, the proof of the serializability relies on mathematical proofs for a fixed finite number of transactions. In this paper, we introduce a protocol to deal with an infinite number of transactions which are iterated infinitely often. We specify serializability of the transactions and the protocol using a specification language based on temporal logics. It is worthwhile using temporal logics such as LTL (Lineartime Temporal Logic) to specify transactions, to gain full automatic verification by using model checkers.

Keywords: Multi-step transactions, LTL specifications, Model Checking.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1380

Authors: Walter Hussak, Heiko Schröder

Abstract:

Star graphs are Cayley graphs of symmetric groups of permutations, with transpositions as the generating sets. A star graph is a preferred interconnection network topology to a hypercube for its ability to connect a greater number of nodes with lower degree. However, an attractive property of the hypercube is that it has a Hamiltonian decomposition, i.e. its edges can be partitioned into disjoint Hamiltonian cycles, and therefore a simple routing can be found in the case of an edge failure. The existence of Hamiltonian cycles in Cayley graphs has been known for some time. So far, there are no published results on the much stronger condition of the existence of Hamiltonian decompositions. In this paper, we give a construction of a Hamiltonian decomposition of the star graph 5-star of degree 4, by defining an automorphism for 5-star and a Hamiltonian cycle which is edge-disjoint with its image under the automorphism.

Keywords: interconnection networks, paths and cycles, graphs andgroups.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1744

Authors: Rafat Alshorman, Walter Hussak

Abstract:

Existing work in temporal logic on representing the execution of infinitely many transactions, uses linear-time temporal logic (LTL) and only models two-step transactions. In this paper, we use the comparatively efficient branching-time computational tree logic CTL and extend the transaction model to a class of multistep transactions, by introducing distinguished propositional variables to represent the read and write steps of n multi-step transactions accessing m data items infinitely many times. We prove that the well known correspondence between acyclicity of conflict graphs and serializability for finite schedules, extends to infinite schedules. Furthermore, in the case of transactions accessing the same set of data items in (possibly) different orders, serializability corresponds to the absence of cycles of length two. This result is used to give an efficient encoding of the serializability condition into CTL.

Keywords: computational tree logic, serializability, multi-step transactions.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1175

Authors: Walter Hussak

Abstract:

We present an operator for a propositional linear temporal logic over infinite schedules of iterated transactions, which, when applied to a formula, asserts that any schedule satisfying the formula is serializable. The resulting logic is suitable for specifying and verifying consistency properties of concurrent transaction management systems, that can be defined in terms of serializability, as well as other general safety and liveness properties. A strict form of serializability is used requiring that, whenever the read and write steps of a transaction occurrence precede the read and write steps of another transaction occurrence in a schedule, the first transaction must precede the second transaction in an equivalent serial schedule. This work improves on previous work in providing a propositional temporal logic with a serializability operator that is of the same PSPACE complete computational complexity as standard propositional linear temporal logic without a serializability operator.

Keywords: Temporal logic, iterated transactions, serializability.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1565

Authors: Rafat Alshorman, Walter Hussak

Abstract:

In mobile environments, unspecified numbers of transactions arrive in continuous streams. To prove correctness of their concurrent execution a method of modelling an infinite number of transactions is needed. Standard database techniques model fixed finite schedules of transactions. Lately, techniques based on temporal logic have been proposed as suitable for modelling infinite schedules. The drawback of these techniques is that proving the basic serializability correctness condition is impractical, as encoding (the absence of) conflict cyclicity within large sets of transactions results in prohibitively large temporal logic formulae. In this paper, we show that, under certain common assumptions on the graph structure of data items accessed by the transactions, conflict cyclicity need only be checked within all possible pairs of transactions. This results in formulae of considerably reduced size in any temporal-logic-based approach to proving serializability, and scales to arbitrary numbers of transactions.

Keywords: multi-step transactions, serializability, directed graph.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1357

Authors: Walter Hussak, John Keane

Abstract:

The usual correctness condition for a schedule of concurrent database transactions is some form of serializability of the transactions. For general forms, the problem of deciding whether a schedule is serializable is NP-complete. In those cases other approaches to proving correctness, using proof rules that allow the steps of the proof of serializability to be guided manually, are desirable. Such an approach is possible in the case of conflict serializability which is proved algebraically by deriving serial schedules using commutativity of non-conflicting operations. However, conflict serializability can be an unnecessarily strong form of serializability restricting concurrency and thereby reducing performance. In practice, weaker, more general, forms of serializability for extended models of transactions are used. Currently, there are no known methods using proof rules for proving those general forms of serializability. In this paper, we define serializability for an extended model of partitioned transactions, which we show to be as expressive as serializability for general partitioned transactions. An algebraic method for proving general serializability is obtained by giving an initial-algebra specification of serializable schedules of concurrent transactions in the model. This demonstrates that it is possible to conduct algebraic proofs of correctness of concurrent transactions in general cases.

Keywords: Algebraic Specification, Partitioned Transactions, Serializability.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1226

Authors: A.Memari

Abstract:

In this article, a simulation method called the Homotopy Perturbation Method (HPM) is employed in the steady flow of a Walter's B' fluid in a vertical channel with porous wall. We employed Homotopy Perturbation Method to derive solution of a nonlinear form of equation obtained from exerting similarity transforming to the ordinary differential equation gained from continuity and momentum equations of this kind of flow. The results obtained from the Homotopy Perturbation Method are then compared with those from the Runge–Kutta method in order to verify the accuracy of the proposed method. The results show that the Homotopy Perturbation Method can achieve good results in predicting the solution of such problems. Ultimately we use this solution to obtain the other terms of velocities and physical discussion about it.

Keywords: Steady flow; Walter's B' Fluid;, vertical channel;porous media, Homotopy Perturbation Method (HPM), Numerical Solution (NS).

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1977

Authors: Marcus Walter, Norbert Nitzsche, Dirk Odenthal, Steffen M¨uller

Abstract:

This contribution presents a friction estimator for industrial purposes which identifies Coulomb friction in a steering system. The estimator only needs a few, usually known, steering system parameters. Friction occurs on almost every mechanical system and has a negative influence on high-precision position control. This is demonstrated on a steering angle controller for highly automated driving. In this steering system the friction induces limit cycles which cause oscillating vehicle movement when the vehicle follows a given reference trajectory. When compensating the friction with the introduced estimator, limit cycles can be suppressed. This is demonstrated by measurements in a series vehicle.

Keywords: Friction estimation, friction compensation, steering system, lateral vehicle guidance.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3054

Authors: Anthony E. Ohazulike, Georg Still, Walter Kern, Eric C. van Berkum

Abstract:

A road pricing game is a game where various stakeholders and/or regions with different (and usually conflicting) objectives compete for toll setting in a given transportation network to satisfy their individual objectives. We investigate some classical game theoretical solution concepts for the road pricing game. We establish results for the road pricing game so that stakeholders and/or regions playing such a game will beforehand know what is obtainable. This will save time and argument, and above all, get rid of the feelings of unfairness among the competing actors and road users. Among the classical solution concepts we investigate is Nash equilibrium. In particular, we show that no pure Nash equilibrium exists among the actors, and further illustrate that even “mixed Nash equilibrium" may not be achievable in the road pricing game. The paper also demonstrates the type of coalitions that are not only reachable, but also stable and profitable for the actors involved.

Keywords: Road pricing game, Equilibrium problem with equilibrium constraint (EPEC), Nash equilibrium, Game stability.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1479

Authors: Suparat Niwitpong

Abstract:

Motivated by the recent work of Herbert, Hayen, Macaskill and Walter [Interval estimation for the difference of two independent variances. Communications in Statistics, Simulation and Computation, 40: 744-758, 2011.], we investigate, in this paper, new confidence intervals for the difference between two normal population variances based on the generalized confidence interval of Weerahandi [Generalized Confidence Intervals. Journal of the American Statistical Association, 88(423): 899-905, 1993.] and the closed form method of variance estimation of Zou, Huo and Taleban [Simple confidence intervals for lognormal means and their differences with environmental applications. Environmetrics 20: 172-180, 2009]. Monte Carlo simulation results indicate that our proposed confidence intervals give a better coverage probability than that of the existing confidence interval. Also two new confidence intervals perform similarly based on their coverage probabilities and their average length widths.

Keywords: Confidence interval, generalized confidence interval, the closed form method of variance estimation, variance.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2778

Authors: Stefanie Rukavina, Sascha Gruss, Steffen Walter, Holger Hoffmann, Harald C. Traue

Abstract:

OPEN_EmoRec_II is an open multimodal corpus with experimentally induced emotions. In the first half of the experiment, emotions were induced with standardized picture material and in the second half during a human-computer interaction (HCI), realized with a wizard-of-oz design. The induced emotions are based on the dimensional theory of emotions (valence, arousal and dominance). These emotional sequences - recorded with multimodal data (facial reactions, speech, audio and physiological reactions) during a naturalistic-like HCI-environment one can improve classification methods on a multimodal level. This database is the result of an HCI-experiment, for which 30 subjects in total agreed to a publication of their data including the video material for research purposes*. The now available open corpus contains sensory signal of: video, audio, physiology (SCL, respiration, BVP, EMG Corrugator supercilii, EMG Zygomaticus Major) and facial reactions annotations.

Keywords: Open multimodal emotion corpus, annotated labels.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1820

Authors: Stefanie Rukavina, Sascha Gruss, Steffen Walter, Holger Hoffmann, Harald C. Traue

Abstract:

OPEN_EmoRec_II is an open multimodal corpus with experimentally induced emotions. In the first half of the experiment, emotions were induced with standardized picture material and in the second half during a human-computer interaction (HCI), realized with a wizard-of-oz design. The induced emotions are based on the dimensional theory of emotions (valence, arousal and dominance). These emotional sequences - recorded with multimodal data (facial reactions, speech, audio and physiological reactions) during a naturalistic-like HCI-environment one can improve classification methods on a multimodal level. This database is the result of an HCI-experiment, for which 30 subjects in total agreed to a publication of their data including the video material for research purposes*. The now available open corpus contains sensory signal of: video, audio, physiology (SCL, respiration, BVP, EMG Corrugator supercilii, EMG Zygomaticus Major) and facial reactions annotations.

Keywords: Open multimodal emotion corpus, annotated labels.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 389

Authors: Florian Gschösser, Walter Purrer

Abstract:

The paper shows examples for the (environmental) optimization of production processes for asphalt mixtures applied for typical road pavements in Austria and Switzerland. The conducted “from-cradle-to-gate” LCA firstly analyzes the production one cubic meter of asphalt and secondly all material production processes for exemplary highway pavements applied in Austria and Switzerland. It is shown that environmental impacts can be reduced by the application of reclaimed asphalt pavement (RAP) and by the optimization of specific production characteristics, e.g. the reduction of the initial moisture of the mineral aggregate and the reduction of the mixing temperature by the application of low-viscosity and foam bitumen. The results of the LCA study demonstrate reduction potentials per cubic meter asphalt of up to 57 % (Global Warming Potential–GWP) and 77 % (Ozone depletion–ODP). The analysis per square meter of asphalt pavement determined environmental potentials of up to 40 % (GWP) and 56 % (ODP).

Keywords: Asphalt mixtures, environmental potentials, life cycle assessment, material production.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1092

Authors: Stephan Rupp, Matthias Elter, Michael Breitung, Walter Zink, Christian Küblbeck

Abstract:

Camera calibration is an indispensable step for augmented reality or image guided applications where quantitative information should be derived from the images. Usually, a camera calibration is obtained by taking images of a special calibration object and extracting the image coordinates of projected calibration marks enabling the calculation of the projection from the 3d world coordinates to the 2d image coordinates. Thus such a procedure exhibits typical steps, including feature point localization in the acquired images, camera model fitting, correction of distortion introduced by the optics and finally an optimization of the model-s parameters. In this paper we propose to extend this list by further step concerning the identification of the optimal subset of images yielding the smallest overall calibration error. For this, we present a Monte Carlo based algorithm along with a deterministic extension that automatically determines the images yielding an optimal calibration. Finally, we present results proving that the calibration can be significantly improved by automated image selection.

Keywords: Camera Calibration, Discrete Optimization, Monte Carlo Method.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1813

Authors: Camilla G. Goncalves, Benedito Christ, Walter Miyakawa, Antonio J. Abdalla

Abstract:

This work aims to investigate the properties and microstructure of diamond-like carbon film deposited by pulsed laser deposition by ablation of a graphite target in a vacuum chamber on a steel substrate. The equipment was mounted to provide one laser beam. The target of high purity graphite and the steel substrate were polished. The mechanical and tribological properties of the film were characterized using Raman spectroscopy, nanoindentation test, scratch test, roughness profile, tribometer, optical microscopy and SEM images. It was concluded that the pulsed laser deposition (PLD) technique associated with the low-pressure chamber and a graphite target provides a good fraction of sp3 bonding, that the process variable as surface polishing and laser parameter have great influence in tribological properties and in adherence tests performance. The optical microscopy images are efficient to identify the metallurgical bond.

Keywords: Characterization, diamond-like carbon, DLC, mechanical properties, pulsed laser deposition.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 703

Authors: Walter Beck

Abstract:

Jharkhand is newly constituted 28th State in the eastern part of India which is known for the oldest settlement of the indigenous people. In the State of Jharkhand in which broadly three language family are found namely, Austric, Dravidian, and Indo-European. Ex-Mundari, kharia, Ho Santali come from the Austric Language family. Kurukh, Malto under Dravidian language family and Nagpuri Khorta etc. under Indo-European language family. There are 32 Indigenous Communities identified as Scheduled Tribe in the State of Jharkhand. Santhal, Munda, Kahria, Ho and Oraons are some of the major Tribe of the Jharkhand state. Jharkhand has a Rich Cultural heritage which includes Folk art, folklore, Folk Dance, Folk Music, Folk Songs for which diversity can been seen from place to place, season to season and all traditional Culture and practices. The languages as well as the songs are vulnerable to dominant culture and hence needed to be protected. The collection and documentation of these songs in their natural setting adds significant contribution to the conservation and propagation of the cultural elements. This paper reflects to bring out the Originality of the Collected Songs from remote areas of the plateau of Sothern Jharkhand as a rich intangible Cultural heritage of the Country. The research was done through participatory observation. In this research project more than 100 songs which were never documented before.

Keywords: Cultural heritage, India, Indigenous people, songs.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2193

Authors: Cameron Hamilton, Walter Potter, Gerrit Hoogenboom, Ronald McClendon, Will Hobbs

Abstract:

A model was constructed to predict the amount of solar radiation that will make contact with the surface of the earth in a given location an hour into the future. This project was supported by the Southern Company to determine at what specific times during a given day of the year solar panels could be relied upon to produce energy in sufficient quantities. Due to their ability as universal function approximators, an artificial neural network was used to estimate the nonlinear pattern of solar radiation, which utilized measurements of weather conditions collected at the Griffin, Georgia weather station as inputs. A number of network configurations and training strategies were utilized, though a multilayer perceptron with a variety of hidden nodes trained with the resilient propagation algorithm consistently yielded the most accurate predictions. In addition, a modeled direct normal irradiance field and adjacent weather station data were used to bolster prediction accuracy. In later trials, the solar radiation field was preprocessed with a discrete wavelet transform with the aim of removing noise from the measurements. The current model provides predictions of solar radiation with a mean square error of 0.0042, though ongoing efforts are being made to further improve the model’s accuracy.

Keywords: Artificial Neural Networks, Resilient Propagation, Solar Radiation, Time Series Forecasting.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2761

Authors: Alexander Wachtel, Michael T. Franzen, Walter F. Tichy

Abstract:

Programming requires years of training. With natural language and end user development methods, programming could become available to everyone. It enables end users to program their own devices and extend the functionality of the existing system without any knowledge of programming languages. In this paper, we describe an Interactive Spreadsheet Processing Module (ISPM), a natural language interface to spreadsheets that allows users to address ranges within the spreadsheet based on inferred table schema. Using the ISPM, end users are able to search for values in the schema of the table and to address the data in spreadsheets implicitly. Furthermore, it enables them to select and sort the spreadsheet data by using natural language. ISPM uses a machine learning technique to automatically infer areas within a spreadsheet, including different kinds of headers and data ranges. Since ranges can be identified from natural language queries, the end users can query the data using natural language. During the evaluation 12 undergraduate students were asked to perform operations (sum, sort, group and select) using the system and also Excel without ISPM interface, and the time taken for task completion was compared across the two systems. Only for the selection task did users take less time in Excel (since they directly selected the cells using the mouse) than in ISPM, by using natural language for end user software engineering, to overcome the present bottleneck of professional developers.

Keywords: Natural language processing, end user development; natural language interfaces, human computer interaction, data recognition, dialog systems, spreadsheet.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1122

Authors: Md. Shafiqul Islam, Abdullah Khan, Sharon Kao-Walter, Li Jian

Abstract:

Shear testing is one of the most complex testing areas where available methods and specimen geometries are different from each other. Therefore, a modified shear test specimen (MSTS) combining the simple uniaxial test with a zone of interest (ZOI) is tested which gives almost the pure shear. In this study, material parameters of polypropylene (PP) and high density polyethylene (HDPE) are first measured by tensile tests with a dogbone shaped specimen. These parameters are then used as an input for the finite element analysis. Secondly, a specially designed specimen (MSTS) is used to perform the shear stress tests in a tensile testing machine to get the results in terms of forces and extension, crack initiation etc. Scanning Electron Microscopy (SEM) is also performed on the shear fracture surface to find material behavior. These experiments are then simulated by finite element method and compared with the experimental results in order to confirm the simulation model. Shear stress state is inspected to find the usability of the proposed shear specimen. Finally, a geometry correction factor can be established for these two materials in this specific loading and geometry with notch using Linear Elastic Fracture Mechanics (LEFM). By these results, strain energy of shear failure and stress intensity factor (SIF) of shear of these two polymers are discussed in the special application of the screw cap opening of the medical or food packages with a temper evidence safety solution.

Keywords: Shear test specimen, Stress intensity factor, Finite Element simulation, Scanning electron microscopy, Screw cap opening.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2924

Authors: Anthony Ikechukwu Agboeze, Walter Timo de Vries, Pamela Durán-Díaz

Abstract:

Since attaining urban status, the population of Enugu, Nigeria, has continued to grow rapidly, leading to growing demands for housing by the teeming population which is predominantly low income. Several government dispensations have developed various affordable housing projects to help deliver decent housing to the Enugu populace. However, over a long period of usage, some of those housing projects in Enugu are unabatedly deteriorating into slums alongside rising housing deficits which has remained problematic for most Nigerian urban centers to address. Emerging from a literature review, this research posits that the link between slum and affordable housing is that both the seekers of affordable housing and slum housing are the low-income earners. This research further investigated the possible causalities of slum emergence from decently built affordable housing projects in Enugu, Nigeria. To do so, we first analyzed the Nigerian housing policy to examine how the policy addresses slum prevention. We further conducted semi-structured expert interviews (qualitative) to sample the views of private housing developers on the degeneration of government housing projects into slums in Enugu, Nigeria. Findings from the housing policy analysis suggest that the housing policy itself is not legally binding on anybody to implement. Sequel to this non-compulsory nature of the housing policy is the poor/non-implementation of the Nigerian housing policy, leading to a constant tendency by the government developers (contractors) to deliver potential slums. The expert respondents corroborated this viewpoint by suggesting that poor planning (including designs of the housing units and the master plan) and poor management (including non-maintenance, poor documentation, and inaccurate housing inventory) are germane to the emergence of slums from affordable housings. This research recommends periodic auditing of delivered housing projects to evaluate the developers’ adherence to the housing policy guidelines – it proposes incentives to policy adherents since the housing policy is not legally binding. We also recommend a participatory management to engage the occupants in the monitoring and reporting of breakdowns in the housing properties – to help improve the quality of management and maintenance to have slum-free settlements.

Keywords: Affordable housing, Enugu, low income, Nigeria, slum.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 352

Authors: Walter Sebron, Hans Tschürtz, Peter Krebs

Abstract:

The choice of applicable analysis methods in safety or systems engineering depends on the depth of knowledge about a system, and on the respective lifecycle phase. However, the analysis method chain still shows gaps as it should support system analysis during the lifecycle of a system from a rough concept in pre-project phase until end-of-life. This paper’s goal is to discuss an analysis method, the VISSE Shell Model Analysis (VISMA) method, which aims at closing the gap in the early system lifecycle phases, like the conceptual or pre-project phase, or the project start phase. It was originally developed to aid in the definition of the system boundary of electronic system parts, like e.g. a control unit for a pump motor. Furthermore, it can be also applied to non-electronic system parts. The VISMA method is a graphical sketch-like method that stratifies a system and its parts in inner and outer shells, like the layers of an onion. It analyses a system in a two-step approach, from the innermost to the outermost components followed by the reverse direction. To ensure a complete view of a system and its environment, the VISMA should be performed by (multifunctional) development teams. To introduce the method, a set of rules and guidelines has been defined in order to enable a proper shell build-up. In the first step, the innermost system, named system under consideration (SUC), is selected, which is the focus of the subsequent analysis. Then, its directly adjacent components, responsible for providing input to and receiving output from the SUC, are identified. These components are the content of the first shell around the SUC. Next, the input and output components to the components in the first shell are identified and form the second shell around the first one. Continuing this way, shell by shell is added with its respective parts until the border of the complete system (external border) is reached. Last, two external shells are added to complete the system view, the environment and the use case shell. This system view is also stored for future use. In the second step, the shells are examined in the reverse direction (outside to inside) in order to remove superfluous components or subsystems. Input chains to the SUC, as well as output chains from the SUC are described graphically via arrows, to highlight functional chains through the system. As a result, this method offers a clear and graphical description and overview of a system, its main parts and environment; however, the focus still remains on a specific SUC. It helps to identify the interfaces and interfacing components of the SUC, as well as important external interfaces of the overall system. It supports the identification of the first internal and external hazard causes and causal chains. Additionally, the method promotes a holistic picture and cross-functional understanding of a system, its contributing parts, internal relationships and possible dangers within a multidisciplinary development team.

Keywords: Analysis methods, functional safety, hazard identification, system and safety engineering, system boundary definition, system safety.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1135