waashk/dblp huggingface dataset:
cl_matcont: a continuation toolbox in matlab. cl_matcont is a matlab continuation package for the numerical study of a range of parameterized nonlinear problems. in the case of odes it allows to compute curves of equilibria, limit point, hopf points, limit cycles and period doubling bifurcation points of limit cycles. all curves are computed by the same function that implements a prediction-correction continuation algorithm based on the moore - penrose matrix pseudo-inverse. the continuation of bifurcation points of equilibria and limit cycles is based on bordering methods and minimally extended systems. hence no additional unknowns such as singular vectors and eigenvectors are used and no artificial sparsity in the systems is created.the inherent sparsity of the discretized systems for the computation of limit cycles and their bifurcation points is exploited by using the standard matlab sparse matrix methods.cl_matcont furthermore allows to compute solution branches to underdetermined systems of nonlinear equations and parameterized boundary value problems.
automatic verification of the tls handshake protocol. e-commerce is based on transactions between client and server agents. these transactions require a protocol that provides privacy and reliability between these two agents. a widely used protocol on e-commerce is transport layer security (tls). in this paper we present a way to use formal methods to ensure the e-commerce properties of this protocol. specifically we use a known tool for model checking (uppaal) to describe and analyze the behaviour of the protocol (by means of timed automata). thus, with this tool we can make an automatic verification of tls.
an approach to handle real time and probabilistic behaviors in e-commerce: validating the set protocol. in this work we describe an approach to deal with systems having at the same time probabilistic and real-time behaviors. the main goal in the paper is to show the automatic translation from a real time model based on uppaal tool, which makes automatic verification of real time systems, to the rapture tool, which makes verification of probabilistic systems.furthermore, this approach allows us to use the best techniques developed in both tools (abstraction, refinement, state space reduction, etc). finally, this translation is applied to verify a case study, the set internet protocol.
inter-organizational document exchange: facing the conversion problem with xml. information exchange processes are often characterized by the need of translating from one data format into another in order to achieve compatibility between information systems. a conversion problem often arises when exchanging files between applications of different software vendors or when incorporating legacy business data into new standard software. in this paper we want to survey the conversion problem in the field of multi-organizational networks, since participants often use different data formats. we examine, to what extent xml is able to support the inter-organizational exchange of business documents. thereby, we concentrate on the problem of converting different data and examine different approaches for solving the transformation problem. we show how xml can actually be implemented for a web-based integration in multi-organizational networks. moreover, we present a java-based prototype that enables document exchange over the internet using xml business vocabularies for document representation, xslt for document conversion and presentation, and both dom and sax for processing and integrating documents into in-house-systems.
blomind-protein property prediction by property proximity profiles. we present the infrastructure of a bioinformation system called biomind, which exploits the close relationship between the structural and functional properties of proteins. the scheme presented here views proteins as composite entities with structural and functional properties, and searches are based on distances along each property axis. explicitly, this allows one to frame complex queries using quantitative criteria that confer more discerning power than systems based on a text-matching approach. implicitly, and more importantly, this has the potential to reveal patterns of convergence in properties of proteins and improve our ability to approximate the unknown properties of a protein, given a set of known properties.
computational analysis of microwave heating patterns in resonant multimode cavities. computational results for the microwave heating patterns in singlefed multimode empty and loaded cavities are presented in this paper. combined finite difference time domain (fdtd) and finite volume (fv) methods are used to solve the equations that describe the electromagnetic field and heat transfer in the processed samples. the coupling between the two schemes is through a change in dielectric properties which are assumed to be temperature dependent. the model takes into account the changing effect of the load's properties on the electric field and modal patterns. a study of the modes and their corresponding field pattern inside a resonant cavity is presented computationally using the fdtd solver. the coupled algorithm is then used to investigate heat distribution by observing the occurrence of resonant conditions which are responsible for achieving high heating levels.
assisted verification of elementary functions using gappa. the implementation of a correctly rounded or interval elementary function needs to be proven carefully in the very last details. the proof requires a tight bound on the overall error of the implementation with respect to the mathematical function. such work is function specific, concerns tens of lines of code for each function, and will usually be broken by the smallest change to the code (e.g. for maintenance or optimization purpose). therefore, it is very tedious and error-prone if done by hand. this article discusses the use of the gappa proof assistant in this context. gappa has two main advantages over previous approaches: its input format is very close to the actual c code to validate, and it automates error evaluation and propagation using interval arithmetic. besides, it can be used to incrementally prove complex mathematical properties pertaining to the c code. yet it does not require any specific knowledge about automatic theorem proving, and thus is accessible to a wider community. moreover, gappa may generate a formal proof of the results that can be checked independently by a lower-level proof assistant like coq, hence providing an even higher confidence in the certification of the numerical code.
decision tree classification of spatial data streams using peano count trees. many organizations have large quantities of spatial data collected in various application areas, including remote sensing, geographical information systems (gis), astronomy, computer cartography, environmental assessment and planning, etc. these data collections are growing rapidly and can therefore be considered as spatial data streams. for data stream classification, time is a major issue. however, these spatial data sets are too large to be classified effectively in a reasonable amount of time using existing methods. in this paper, we developed a new method for decision tree classification on spatial data streams using a data structure called peano count tree (p-tree). the peano count tree is a spatial data organization that provides a lossless compressed representation of a spatial data set and facilitates efficient classification and other data mining techniques. using p-tree structure, fast calculation of measurements, such as information gain, can be achieved. we compare p-tree based decision tree induction classification and a classical decision tree induction method with respect to the speed at which the classifier can be built (and rebuilt when substantial amounts of new data arrive). experimental results show that the p-tree method is significantly faster than existing classification methods, making it the preferred method for mining on spatial data streams.
k-nearest-neighbor consistency in data clustering: incorporating local information into global optimization. nearest neighbor consistency is a central concept in statistical pattern recognition, especially the knn classification methods and its strong theoretical foundation. in this paper, we extend this concept to data clustering, requiring that for any data point in a cluster, its k-nearest neighbors and mutual nearest neighbors should also be in the same cluster. we study properties of the cluster k-nearest neighbor consistency and propose knn and kmn consistency enforcing and improving algorithms. extensive experiments on internet newsgroup datasets using the k-means clustering algorithm with knn consistency enhancement show that knn / kmn consistency can be improved significantly (about 100% for 1mn and 1nn consistencies) while the clustering accuracy is improved simultaneously. this indicates the local consistency information helps the global cluster objective function optimization.
the p-tree algebra. the peano count tree (p-tree) is a quadrant-based lossless tree representation of the original spatial data. the idea of p-tree is to recursively divide the entire spatial data, such as remotely sensed imagery data, into quadrants and record the count of 1-bits for each quadrant, thus forming a quadrant count tree. using p-tree structure, all the count information can be calculated quickly. this facilitates efficient ways for data mining. in this paper, we will focus on the algebra and properties of p-tree structure and its variations. we have implemented fast algorithms for p-tree generation and p-tree operations. our performance analysis shows p-tree has small space and time costs compared to the original data. we have also implemented some data mining algorithms using p-trees, such as association rule mining, decision tree classification and k-clustering.
ubicollab: collaboration support for mobile users. shared workspaces have emerged as one of the most successful applications of computer supported cooperative work (cscw). important aspects of shared workspaces are presence and awareness information, flexible sharing of work material, and support for communication among group members. one of the shortcomings of existing shared workspaces is their lack of support for mobility. in this paper we will discuss the need for mobile shared workspaces as well as an experimental platform for ubiquitous collaboration and a number of shared workspace implementations for both formal and informal collaboration.
solving first-order constraints in the theory of finite or infinite trees: introduction to the decomposable theories. we present in this paper an algorithm in the theory t of possibly infinite trees for solving general constraints represented by full first-order formulas, with equality as the only relation and functional symbols taken from an infinite set f. the algorithm consists of a set of 11 rewriting rules. it transforms a first-order formula p in a conjunction q of solved formulas, equivalent in t, such that: (1) the conjunction q is the formula true if p is always true in t, and the formula &not;true if p is always false in t. moreeover, if p or its negation has a finite base of solutions in a model of t, then these solutions or non-solutions have to be explicit in q. (2) each solved formula of q has not new free variables and can be transformed immediately in a boolean combination of basic formulas whose length does not exceed twice the length of the solved formula. the basic formulas are particular cases of existentially quantified conjunctions of equations. the correctness of the algorithm gives another proof of the completeness of t demonstrated by michael maher. we test our algorithm on benchmarks realized by an implementation, solving formulas on two-partners games in t with more than 160 nested alternated quantifiers.finally, we show then that we can generalize this algorithm by introducing a new class of theories that we call decomposable. we show that t is decomposable and give a general algorithm for solving first-order constraint in any decomposable theory. the correctness of our algorithm shows the completeness of the decomposable theories.
co-evolving an effective fitness sample: experiments in symbolic regression and distributed robot control. we investigate two techniques for co-evolving and sampling from a population of fitness cases, and compare these with a random sampling technique. we design three symbolic regression problems on which to test these techniques, and also measure their relative performance on a modular robot control problem. the methods have varying relative performance, but in all of our experiments, at least one of the co-evolutionary methods outperforms the random sampling method by guiding evolution, with substantially fewer fitness evaluations, toward solutions that generalize best on an out-of-sample test set.
representing the applications and compositions of design patterns in uml. design patterns capture the distilled experience of expert designers. the compositions of design patterns may reuse design experience and solve a set of problems. design patterns and their compositions are usually modeled using uml. when a design pattern is applied or composed with other patterns, the pattern-related information may be lost because uml does not track this information. thus, it is hard for a designer to identify a design pattern when it is applied or composed. the benefits of design patterns are compromised because the designers cannot communicate with each other in terms of the design patterns they use when the design patterns are applied or composed. in this paper, we present notations to explicitly represent each pattern in the applications and compositions of design patterns. the notations allow us to maintain pattern-related information. thus, a design pattern is identifiable and traceable from its application and composition with others.
text classification based on data partitioning and parameter varying ensembles. support vector machines (svm) are among the best text classifiers so far. meantimes, ensembles of classifiers are proven to be effective on many domains. it is expected that ensembles of svm classifiers could achieve better performance. in this paper two types of ensembles on svm classifiers, the data partitioning ensembles and heterogeneous ensembles, have been proposed and experimentally evaluated on three well-accepted collections. major conclusions are that disjunct partitioning ensembles with stacking could achieve the best performance, and that the parameter varying ensembles are proven to be effective, meanwhile have the advantage of being deterministic.
embedded predictive modeling in a parallel relational database. a methodology for embedding predictive modeling algorithms in a commercial parallel database is described; specifically, the parallel editions of ibm db2 universal database, although many aspects of the overall approach can be used with other commercial parallel databases. this parallelization approach was implemented in the version 8.2 release of db2 intelligent miner modeling to support a new predictive modeling algorithm called transform regression. this database-embedded mining algorithm provides all the usual benefits, including easier integration into large enterprise applications, the ability to perform entire data mining workflows directly from an sql-based programming interface, reduced data transfer costs between the database and the data mining application, and faster, parallel data access during query processing. however, in addition to the these benefits, a significant part of the data mining computations are also parallelized without the use of any sophisticated parallel programming constructs, or any specialized message passing and parallel synchronization libraries.
ontology-based integration for relational databases. in this paper, we show that representation and reasoning techniques used in traditional knowledge engineering and the emerging semantic web can play an important role for heterogeneous database integration. our ontograte architecture combines ontology-based schema representation, first order logic inference, and some sql wrappers to integrate two sample relational databases. we define inferential data integration as the theoretical framework for our approach. the performance evaluation for query answering shows that ontograte reformulates conjunctive queries and retrieves over 100,000 answers from a target database in under 30 seconds. in addition to query answering, the system translates 40,000 database facts from source to target in under 30 seconds.
synthesis of c++ software for automated teller from cspm specifications. csp++ is an object-oriented application framework for execution of csp specifications that have been automatically translated into c++ source code by a tool called cspt. this approach makes csp specifications directly executable, and extensible via the ability to incorporate user-coded functions. designers can exploit "selective formalism" to code some system functionality in csp for formal verification purposes, and other functionality directly in c++. the translator has now been enhanced to accept input in cspm syntax, the same dialect processed by the commercial verification tool, fdr2, and we demonstrate this with a new atm case study.
combining speech and pen input for effective interaction in mobile geospatial environments. relatively little research has been conducted into designing interfaces that allow gis users to interact effectively with geospatial data in mobile environments. users on the move are faced with limited interaction modalities. the standard mode of input on mobile devices is the pen or stylus, which some users may find difficult or too time-consuming to use. voice commands, combined with pen input, can provide an attractive alternative for interacting with mobile gis, as speech is a natural form of interaction. however, the idea of combining speech and pen input in mobile gis is relatively unexplored. to this effect, we have developed a multimodal interface to a mobile gis, providing users with the ability to freely switch between modalities to suit current tasks or environments.
enhancing network intrusion detection systems with interval methods. two main approaches for network intrusion detection are misuse detection [6] and anomaly detection [11]. the limitation of the misuse approach is that cannot effectively detect new patterns of intrusions that are not precisely encoded in the system [11]. the anomaly detection approach usually produces a large number of false alarms [1, 7]. in addition, anomaly detection requires intensive computations on a large amount of training data to characterize normal behavior patterns.in this paper, we try to apply interval technology to enhance network intrusion detection systems (ids). by storing network state data into interval valued bi-temporal database, we better sample the stream of network states. we represent the likelihood of intrusions associated with an m x n interval valued rule matrix that can be obtained from the database with relatively low computational complexity. by grouping nearby patterns with intervals, we may significantly reduce false alarms. the o(n) computational cost of maintaining the rules makes it possible to integrate the ids with network management systems for almost real-time automatic network control. our probabilistic approach with the rule matrix model can be further applied to study the pattern evolution of network intrusions.
a treecode algorithm for computing ewald summation of dipolar systems. we present a treecode algorithm for efficiently computing the real space part of ewald summation in periodic dipolar systems. the algorithm uses multipole expansion in cartesian coordinates to approximate the real space interaction between a dipole and a distant cluster of dipoles. the necessary taylor coefficients are computed efficiently using recurrence relations. two divide-and-conquer evaluation procedures are described. test results are presented for systems of randomly generated dipoles.
conformational statistics of the nitrogen linkage in glycopeptides using umbrella sampling. the conformational statistics of the glycosylated dipeptide n - acetyl - &delta; - n - (2 - acetamido - &beta; - d - glucopyranosyl) - l - asparaginyl - n' - methyl amide (glcnac-asn), a model of n-linked glycopeptides, was determined using umbrella sampling. the use of umbrella sampling allowed the importance sampling algorithm to accept new conformations with probabilities exceeding 40%. the satisfactory acceptance rate generated a chain of conformations and a set of properties suitable for comparison with available experimental results. comparison of calculated structures for glcnac-asn with those determined experimentally by nmr, circular dichroism spectroscopy, and x-ray crystallography showed that the momany-scheraga conformation energy (ecepp) over-emphasized non-bonded repulsions. based on the experimentally determined structures, an effective two-fold potential barrier was imposed on the anomeric linkage. predictions based on conformational statistics were sensitive to the choice of a three-fold or two-fold torsional barrier at the anomeric linkage.
a deterministic technique for extracting keyword based grammar rules from programs. this paper presents a technique for extracting grammar rules, given a set of programs and an approximate grammar. grammar is an important artifact used in the generation of tools for program analysis, modification, etc. current grammar extraction techniques are heuristic in nature. this work proposes a deterministic technique for extracting keyword based grammar rules. the technique uses cyk-parser and lr-parser to build a set of possible rules. for each rule it checks whether the grammar after including that rule is able to parse all the programs or not. as this results in a large set of possible rules, a set of optimizations are proposed to reduce the search space of possible rules. the proposed optimizations utilize the knowledge from multiple programs and exploit the abundance of unit productions in the grammar of programming languages. the proposed approach and optimizations are experimentally checked on a set of input programs.
security status display and browser interframe communication. we argue that current www protocols are anticompetitive and favor larger www retailers and service providers. consumer confidence has been recognized as an impediment to the development of smaller www based businesses and the growth of online transactions. consumers are understandably concerned about using their credit card number to make www purchases.our assertion is that the development of standards which would allow payment providers to interface with vendors and consumers to interface with vendors with confidence has been made difficult by current browser standards. we suggest that changes can reasonably be made which would make the task of developing such interface protocols easier while enhancing consumer confidence. changes in the direction we suggest could assist in enhancing competition, consumer security and privacy, as well as confidence. in addition, it would be easier to develop protocols to allow consumer choice of payment providers, shippers, and other services ancillary to an online transaction.
the effects of two replacement strategies on a genetic algorithm for scheduling jobs on computational grids. computational grid (cg) represents a new computational framework whose efficient use requires schedulers that allocate user's tasks to the grid resources in an acceptable amount of time. in this paper, we study the effects of two replacement strategies on a ga for job scheduling on computational grids, namely steady-state ga (ssga) and struggle ga (sga). considering the makespan, the experimental results show the improvement obtained by sga over ssga for moderate size instances. however, the time needed by the sga to reach makespan values obtained by the ssga rapidly increases as more jobs and machines are added to the cg.