LNCS 4362
Sponsors
Springer LNCS Contributed Papers
Foundations
- Jérémie Chalopin,Emmanuel Godard,Yves Métivier,Gerard Tel:
About the termination detection in the asynchronous message passing model AbstractThe paper presents a complete characterisation of the families of networks in which distributed computations can be performed in a process terminating manner, that is, with explicit termination in the asynchronous message passing model. The characterisation encompasses all criteria that have been formulated in the past that were known to influence explicit termination: topological restriction (tree or complete networks), topological knowledge (size or diameter), and local knowledge to distinguish nodes (identities or a leader). These results are now presented as corollaries of a single generalising theorem. In addition our characterisation covers combinations of these, as well as new criteria. - Sungwook Kim,Sungchun Kim:
Online Service Management Algorithms for Cellular/WALN Multimedia Networks AbstractNew multimedia services over the cellular/WLAN overlay networks require different Quality of Service (QoS). Therefore, efficient network management system is necessary in order to provide QoS sensitive multimedia services while enhancing network performance. In this paper, we propose a new online network management framework that implements bandwidth reservation, congestion and transmission control strategies. Simulation results indicate the superior performance of our proposed framework to strike the appropriate performance balance between contradictory QoS requirements under widely varying diverse traffic loads. - Ivan Lanese:
Concurrent and located synchronizations in pi-calculus AbstractWe present two novel semantics for pi-calculus. The first allows one to observe on which channel a synchronization is performed, while the second allows concurrent actions, provided that they do not compete for resources. We present both a reduction and a labeled semantics and show that they induce the same behavioral equivalence. As main result we show that bisimilarity is a congruence for the concurrent semantics. This important property fails for the standard semantics. - Xiaoxiao Yang,Zhenhua Duan:
Operational Semantics of Framed Temporal Logic Programs AbstractThis paper investigates the operational semantics of framed temporal logic programs. To this end, a framed temporal logic programming language called Framed Tempura is employed. The evaluation rules for both the arithmetic and boolean expressions are defined. The semantic equivalence rules for the reduction of a program within a state is formalized. Furthermore, the congruence and transition rules between configurations for the reduction of programs are also specified. Moreover, some examples are given to illustrate how the rules work. Thus, the executable behavior of framed programs can be captured in an operational way. In addition, the consistency of the operational semantics and the minimal model semantics based on model theory is proved in detail. - Joel Ratsaby:
Information Efficiency AbstractShannon's theory of information stands on a probabilistic representation of events that convey information, e.g., sending messages over a communication channel. Kolmogorov argues that information is a more fundamental concept which exists also in problems with no underlying stochastic model, for instance, the information contained in an algorithm or in the genome. In a classic paper he defines the discrete entropy of a finite set which establishes a combinatorial based definition of the information I(x:\sy) conveyed by a variable \sx (taking a binary string value x) about the unknown value of a variable \sy. The current paper extends Kolmogorov's definition of information to a more general setting where given `\sx=x' there may still be uncertainty about the set of possible values of \sy. It then establishes a combinatorial based description complexity of x and introduces a novel concept termed {\em information width}, similar to n-widths in approximation theory. This forms the basis of new measures of cost and efficiency of information which give rise to a new framework whereby information of any input source, e.g., sample-based, general side-information or a hybrid of both, is represented and computed according to a single common formula. As an application, we consider the space of Boolean functions where input strings x correspond to descriptions of properties of classes of Boolean functions. - Ladislav Vagner,Bořivoj Melichar:
Formal Translation Directed by Parallel LLP Parsing AbstractFormal translation directed by parallel LLP parsing is presented. The translator follows the traditional translation scheme - the input grammar is extended by output symbols that are added into appropriate right-hand sides of grammar rules. The translation algorithm is based on the intermediate results provided by the parallel LLP parser. The correct sequence of output symbols is obtained from the intermediate results using parallel prefix sum, segmented parallel prefix sum, and parallel sorting steps. The presented translation algorithm is suitable for all translations with LLP(q,k) input grammars. The asymptotical parallel time of the translation algorithm is O(log^2(n)). - Costas Iliopoulos,M. Sohel Rahman:
Indexing Factors with Gaps AbstractIndexing of factors is a widely used and useful technique in stringology and can be seen as a tool in solving diverse text algorithmic problems. A gapped-factor is a concatenation of a factor of length k, a gap of length d and another factor of length k'. The problem of indexing the gapped-factors was considered recently by~\cite{PeterlongoAS06}. In this paper, we present a new improved indexing scheme for the gapped-factors. - Dominique Quadri,Eric Soutif,Pierre Tolla:
A branch-and-bound algorithm to solve large scale integer quadratic multi-knapsack problems AbstractThe separable quadratic multi-knapsack problem (QMKP) consists in maximizing a concave separable quadratic integer (non pure binary) function subject to m linear capacity constraints. In this paper we develop a branch-and-bound algorithm to solve (QMKP) to optimality. This method is based on the computation of a tight upper bound for (QMKP) which is derived from a linearization and a surrogate relaxation. Our branch-and-bound also incorporates pre-processing procedures. The computational performance of our branch-and-bound is compared to that of three exact methods: a branch-and-bound algorithm developed by Djerdjour et al. (1988), a 0-1 linearization method originally applied to the separable quadratic knapsack problem with a single constraint that we extend to the case of m constraints, a standard branch-and-bound algorithm (Cplex9.0 quadratic optimization). Our branch-and-bound clearly outperforms other methods for large instances (up to 2000 variables and constraints). - Bala Ravikumar,Nicolae Santean:
Deterministic Simulation of a NFA with k-symbol Lookahead AbstractWe investigate deterministically simulating (i.e., solving the membership problem for) nondeterministic finite automata (NFA), relying solely on the NFA's resources (states and transitions). Unlike the standard NFA simulation, involving an algorithm which stores at each step all the states reached nondeterministically while reading the input, we consider deterministic finite automata (DFA) with lookahead, which choose the ``right'' NFA transitions based on a fixed number of input symbols read ahead. This concept, known as {\it lookahead delegation}, arose in a formal study of web services composition and its subsequent practical applications. Here we answer several related questions, such as {\it ``when is lookahead delegation possible?''} and {\it ``how hard is it to find a delegator with a given lookahead buffer size?''}. In particular, we show that only finite languages have the property that all of their NFA's have delegators. This implies, among others, that delegation is a machine property, rather than a language property. We also prove that the existence of lookahead delegators for unambiguous NFA is decidable, thus partially solving an open problem. Finally, we show that finding delegators (even for a given buffer size) is hard in general, and is efficient for unambiguous NFA, and we give an algorithm and a compact characterization for NFA delegation in general. - Lukas Petru,Jiri Wiedermann:
A Model of an Amorphous Computer and its Communication Protocol AbstractWe design a formal model of an amorphous computer suitable for theoretical investigation of its computational properties. The model consists of a finite set of nodes created by RAMs with restricted memory, which are dispersed uniformly in a given area. Within a limited radius the nodes can communicate with their neighbors via a single-channel radio. The assumptions on low-level communication abilities are among the weakest possible: the nodes work asynchronously, there is no broadcasting collision detection mechanism and no network addresses. For the underlying network we design a randomized auto-configurational communication protocol and analyze its efficiency. The subsequent experiments and combinatorial analysis of random networks show that the expectations under which our protocol was designed are met by the vast majority of the instances of our amorphous computer model. - Shay Solomon,Yefim Dinitz:
On Optimal Solutions for the Bottleneck Tower of Hanoi Problem AbstractWe study two aspects of a generalization of the Tower of Hanoi puzzle. In 1981, D.~Wood suggested its variant, where a bigger disk may be placed \emph{higher than} a smaller one if their size difference is less than k. In 1992, D.~Poole suggested a natural disk-moving strategy for this problem, but only in 2005, the authors proved it be optimal in the general case. We describe the family of all optimal solutions to this problem and present a closed formula for their number, as a function of the number of disks and k. Besides, we prove a tight bound for the diameter of the configuration graph of the problem suggested by Wood. Finally, we prove that the \emph{average} length of shortest sequence of moves, over all pairs of initial and final configurations, is the same as the above diameter, up to a constant factor. - Sang-Wook Kim,Junghoon Lee,Miyung Shin:
Generating High Dimensional Data and Query Sets AbstractPrevious researches on multidimensional indexes typically have used synthetic data sets distributed uniformly or normally over multidimensional space for performance evaluation. However, recent research result has shown that these kinds of data sets hardly reflect the characteristics of multimedia database applications. In this paper, we discuss issues on generating high dimensional data and query sets for resolving the problem. We first identify the features of the data and query sets that are appropriate for fairly evaluating performances of multidimensional indexes, and then propose HDDQ_Gen (High-Dimensional Data and Query Generator) that satisfies such features. HDDQ_Gen supports the following features: (1) clustered distribution, (2) various object distribution in each cluster, (3) various cluster distribution, (4) various correlations among different dimensions, and (5) query distribution depending on data distribution. Using these features, users are able to control the distribution characteristics of data and query sets. Our contribution is fairly important in that HDDQ_Gen provides the benchmark environment evaluating multidimensional indexes correctly. - František Galčík,Gabriel Semanišin:
Maximum finding in the symmetric radio networks with collision detection AbstractWe consider a problem of computing the maximal value associated to the nodes of a network in the model of unknown symmetric radio network with availability of collision detection. We assume that the nodes have no initial knowledge about the network topology, number of nodes and even they have no identifiers. The network contains one distinguished node, called initiator, that starts the process of computing. We design a series of algorithms that result into an asymptotically optimal deterministic algorithm completing the task in Theta(ecc+log Max) rounds, where ecc is the eccentricity of the initiator and Max is the maximal value among the values associated to the nodes. Some other utilisations of the developed algorithm are presented as well. - Mika Hirvensalo:
Improved Undecidability Results on the Emptiness Problem of Probabilistic and Quantum Cut-Point Languages AbstractWe give constructions of small probabilistic and MO-type quantum automata that have undecidable emptiness problem for the cut-point languages. - Hua Wang,Zuquan Ge,Jun Ma:
Self-adaptive Lagrange Relaxtion Algorithm for Aggregated Multicast AbstractMulticast has great advantages in data forwarding. But the number of forwarding states becomes huge in routers when there are large numbers of multicast groups in the network, which may cause explosions of state information and control information. Aggregated multicast is a novel approach to reducing multicast state numbers. It enables multicast groups to share a single distribution tree so that the tree management overhead at core routers can be reduced. Aggregated Multicast can actually be attributed to minimal set cover problem, which is an NP-complete problem. To solve it this paper proposes a self-adaptive Lagrange Relaxation Algorithm, which can achieve best solution. Simulation results show that this algorithm is better than the conventional greedy algorithm in that it improves aggregation degree and reduces multicast state number. - JaeKwon Seo,KyungGeun Lee:
Mobility Management using Virtual Domain in IPv6-based Cellular Networks AbstractHierarchical Mobile IPv6 (HMIPv6) has been proposed by Internet Engineering Task Force (IETF) to compensate for such problems as handover latency and signaling overhead in employing Mobile IPv6 (MIPv6). HMIPv6 supports micro-mobility within a domain and introduces a new entity, namely mobility anchor point (MAP) as a local home agent. However, HMIPv6 causes load concentration at a particular MAP and longer handover latency when inter-domain handover occurs. In order to solve such problems, this paper establishes a virtual domain (VD) of a higher layer MAP and proposes a MAP changing scheme in which the routing path changes between mobile node (MN) and correspondent node (CN) according to the mobile position and the direction of the MN before inter-domain handover occurs. The MAP changing scheme not only enables complete handover binding-update of the on-link care of address (LCoA) only when inter-domain handover occurs, but concentrated load of a particular MAP is distributed as well because the MNs registered with higher layer MAP and lower layer MAP coexist in VD. We simulate the performance of the MAP changing scheme and compare with HMIPv6. From the result, we have confirmed that the MAP changing scheme can reduce handover latency when inter-domain handover occurs and distributes load of higher layer MAP and lower layer MAP. We also analyze the MAP changing scheme through numerical modeling in comparison with other schemes. - Jérôme Monnot,Sophie Toulouse:
The Pk partition problem and related problems in bipartite graphs AbstractIn this paper, we continue the investigation proposed in [MonnotToulouse05] about the approximability of Pk partition problems, but focusing here on their complexity. More precisely, we prove that the problem consisting of deciding if a graph of nk vertices has n vertex disjoint simple paths {P_1,...,P_n} such that each path P_i has k vertices is NP-complete, even in bipartite graphs of maximum degree 3. Note that this result also holds when each path P_i is chordless in G[V(P_i)]. Then, we prove that MaxP3Packing and MaxInducedP3Packing in bipartite graphs of maximum degree 3 are not in PTAS. Finally, we propose a 3/2-approximation for Min3PathPartition in general graphs within O(|V||E|+|V|^2\log |V|) time and a 1/3 (resp., 1/2)-approximation for MaxWP3Packing in general (resp., bipartite) graphs of maximum degree 3 within linear (resp., O(|V|^2\log |V|)) time. - Pok-Son Kim,Arne Kutzner:
A Simple Algorithm for Stable Minimum Storage Merging AbstractWe contribute to the research on stable minimum storage merging by introducing an algorithm that is particularly simply structured compared to its competitors. The presented algorithm performs O(m \log(n/m+1)) comparisons and O((m+n)\log m) assignments, where m and n are the sizes of the input sequences with m\leq n. Hence, according to the lower bounds of merging the algorithm is asymptotically optimal regarding the number of comparisons. As central new idea we present a principle of symmetric splitting, where the start and end point of a rotation are computed by a repeated halving of two search spaces. This principle is structurally simpler than the principle of symmetric comparisons introduced earlier by Kim and Kutzner. It can be transparently implemented by few lines of Pseudocode. We report concrete benchmarks that prove the practical value of our algorithm. - Jiří Šíma,Stanislav Žák:
A Polynomial Time Constructible Hitting Set for Restricted 1-Branching Programs of Width 3 AbstractAn important problem in complexity theory is to find polynomial time constructible hitting sets for Boolean functions in different standard models. This would have consequences for the relationship between deterministic and probabilistic computations in the respective models. Using the result by Alon, Goldreich, Hastad, and Peralta (1992) we provide a polynomial time constructible hitting set for restricted read-once branching programs of width 3. The restriction excludes only one from all patterns of level-to-level transitions in a normalized form of 3-width 1-branching programs. In fact, our technique works for a slightly more general class of such programs. Although this restriction seems to be strong our proof reveals the core of difficulties and thus represents the first step for proving the result for less restricted models. - Orhan Dagdeviren,Kayhan Erciyes:
A Software Architecture for Shared Resource Management in Mobile Ad hoc Networks AbstractWe provide the implementation results of the distributed mutual exclusion algorithm based on Ricart-Agrawala algorithm for mobile ad hoc networks (MANETs) using the ns2 simulator described in \cite{Erciyes04c}. The MANET consists of a ring of clusters and it is partitioned into a number of clusters periodically using the MCA \cite{Dagdeviren06}. Each cluster is represented by a coordinator. We also show a new algorithm to construct a directed ring architecture across coordinators to be able to implement the distributed mutual exclusion algorithm. Coordinators implement various distributed mutual exclusion algorithms on behalf of any member in the cluster they represent. We show experimentally that the protocol designed is scalable and that it provides an order of decrease in message and time complexities when compared with other algorithms. - Qingjun Xiao,Ruonan Rao,Jinyuan You:
A language for reliable service composition AbstractService Composition is one of the pillars under Service Oriented Architecture. BPEL becomes the de-facto standard within this area. A key aspect when aggregating business processes using BPEL is to realize a compensation-based reliable service composition, often referred to as BPEL LRT(Long Running Transaction). But there lacks precise modeling on how to combine BPEL control flow with long running transactions. The paper presents a formal language named BPTX, which is a simplified version of BPEL at syntactic level and offers effective directions to underlying transaction coordinator as semantics. The paper also proposes an optimization not contained in traditional transaction processing: detect the failure destiny of a branch and react to it as early as possible. - David Janin:
On the (high) undecidability of distributed synthesis problems AbstractThe distributed synthesis problem is known to be undecidable [PnuRos90]. Our purpose here is to study further this undecidability. For this, we consider distributed games [MohWal03] , an infinite variant of Peterson and Reif multiplayer games with partial information [PetRei79], where Pnueli and Rosner's distributed synthesis problem can be encoded and, when decidable [PnuRos90,KupVar01,Mad01], uniformly solved [MohWal03]. We first prove that the simple problem of solving two process distributed game with reachability condition is already undecidable (Sigma^0_1-complete). This decision problem, equivalent to two process distributed synthesis with fairly restricted FO-specification was left open [MohWal03]. We prove then that the safety case is Pi^0_1-complete. More generally, we establish a correspondence between two-process distributed game with Mostowski's weak parity conditions [Mos91] and levels of the arithmetical hierarchy. Last, distributed game with general omega-regular infinitary condition are shown to be highly undecidable (Sigma^1_1-complete). - Miroslaw Dynia,Miroslaw Korzeniowski,Jaroslaw Kutylowski:
Competitive Maintenance of Minimum Spanning Trees in Dynamic Graphs AbstractWe present the problem of maintaining a minimum spanning tree within a graph with dynamically changing edge weights. An online algorithm is confronted with an input sequence of edge weight changes and has to choose a minimum spanning tree after each such change in the graph. The task of the algorithm is to perform as few changes in its minimum spanning tree as possible. We compare the number of changes in the minimum spanning tree produced by an online algorithm and that produced by an optimal offline algorithm. The number of changes is counted in the number of edges changed between spanning trees in consecutive rounds. For any graph with n vertices we provide a deterministic algorithm achieving a competitive ratio of O(n^2). We show that this result is optimal up to a constant. Furthermore we give a lower bound for randomized algorithms of Omega(log n). We show a randomized algorithm achieving a competitive ratio of O(n log n) for general graphs and O(log n) for planar graphs. - Raphael Clifford,Benjamin Sach:
Fast Approximate Point Set Matching for Information Retrieval AbstractWe investigate randomised algorithms for subset matching with spatial point sets---given two sets of d-dimensional points: a data set T consisting of n points and a pattern P consisting of m points, find the largest match for a subset of the pattern in the data set. This problem is known to be 3-SUM hard and so unlikely to be solvable exactly in subquadratic time. We present an efficient bit-parallel O(nm) time algorithm and an O(n\log{m}) time solution based on correlation calculations using fast Fourier transforms. Both methods are shown experimentally to give answers within a few percent of the exact solution and provide a considerable practical speedup over existing deterministic algorithms. - Yuichi Asahiro,Eiji Miyano,Shuichi Miyazaki,Takuro Yoshimuta:
Weighted Nearest Neighbor Algorithms for the Graph Exploration Problem on Cycles AbstractIn the graph exploration problem, a searcher explores the whole set of nodes of an unknown graph. The searcher does not aware the existence of an edge until he/she visits one of its endpoints. The searcher's task is to visit all the nodes by traveling as a short tour as possible. It is known that the weighted nearest neighbor algorithm (WNN) with weight three is 16-competitive for planar graphs. In this paper we apply WNN to cycles and prove that the nearest neighbor algorithm (NN), that is, WNN with weight one, can achieve the competitive ratio of 1.5 for cycles. In addition, we show that the analysis for the competitive ratio of NN is tight by providing a matching lower bound, and NN is the best for cycles among WNN with all possible weights. Furthermore, we prove that no online algorithm is better than 1.25-competitive. - Susanne Graf,Gregor Goessler,Mila Majster-Cederbaum,Moritz Martens,Josef Sifakis:
An Approach to Modelling and Verification of Component Based Systems AbstractWe build on a framework for modelling and investigating component-based systems that strictly separates the description of behavior of components from the way they interact. We discuss various properties of system behavior as liveness, local progress, local and global deadlock, and robustness. We present a criterion that ensures liveness and can be tested in polynomial time. - Harald Zankl,Nao Hirokawa,Aart Middeldorp:
Constraints for Argument Filterings AbstractThe dependency pair method is a powerful method for automatically proving termination of rewrite systems. When used with traditional simplification orders like LPO and KBO, argument filterings play a key role. In this paper we propose an encoding of argument filterings in propositional logic. By incorporating propositional encodings of simplification orders, the search for suitable argument filterings is turned into a satisfiability problem. Preliminary experimental results show that our logic-based approach is significantly faster than existing implementations. - Ruben Agadzanyan,Rusins Freivalds:
Size of Quantum Finite State Transducers AbstractSizes of quantum and deterministic finite state transducers are compared in the case when both quantum and deterministic finite state transducers exist. The difference in size may be exponential. - Markus Maier,Steffen Mecke,Dorothea Wagner:
Algorithmic Aspects of Minimum Energy Edge-Disjoint Paths in Wireless Networks AbstractThe problem of finding k minimum energy, edge-disjoint paths in wireless networks (MEEP) arises in the context of routing and belongs to the class of range assignment problems. A polynomial algorithm which guarantees a factor-k-approximation for this problem has been presented before, but its complexity status was open. In this paper we prove that MEEP is NP-hard and give a lower bound on the approximation factor of the k-approximation algorithm. For \MEEP on acyclic graphs we introduce an exact, polynomial algorithm which is then extended to a heuristic for arbitrary graphs. - Sergey Bereg,Markus Völker,Alexander Wolff,Yuanyi Zhang:
Straightening Drawings of Clustered Hierarchical Graphs AbstractIn this paper we deal with making drawings of clustered layered graphs nicer. Given a planar graph G=(V,E) with an assignment of the vertices to horizontal layers, a plane drawing of G (with polygonal or y-monotone edges) can be specified by stating for each layer the order of the vertices lying on and the edges intersecting that layer. Given these orders and a recursive partition of the vertices into clusters, our aim is to draw G such that (i) edges are straight-line segments, (ii) clusters lie in disjoint convex regions, and (iii) no edge intersects a cluster boundary twice. First we investigate fast algorithms that produce drawings of the above type if the clustering fulfills certain conditions. We give two linear-time algorithms with different preconditions. Second we give a linear programming (LP) formulation that always yields a drawing that fulfills the above three requirements---if such a drawing exists. The number of variables and constraints in our LP formulation is linear in the size of the graph. We discuss two different objective functions and compare them visually. - Bastian Katz,Marco Gaertler,Dorothea Wagner:
Maximum Rigid Components as Means for Direction-based Localization in Sensor Networks AbstractMany applications in sensor networks require positional information of the sensors. Recovering node positions is closely related to graph realization problems for geometric graphs. Here, we address the case where nodes have angular information. Whereas Bruck et al. proved that the corresponding realization problem together with unit-disk-graph-constraints is \NP-hard, we focus on rigid components which allow both efficient identification and fast, unique realizations. Our technique allows to identify maximum rigid components in graphs with partially known rigid components using a reduction to maximum flow problems. This approach is analyzed for the two-dimensional case, but can easily be extended to higher dimensions. - Oscar Pedreira,Nieves Brisaboa:
Spatial Selection of Sparse Pivots for Similarity Search in Metric Spaces AbstractSimilarity search is a necessary operation for a great number of applications dealing with retrieval of unstructured data where, in general, a multidimensional Metric Space is assumed to explain the difference/distances among the objects. The number of dimensions and the dimensions themselves are usually unknown, therefore, only a distance function can be used to figure out whether two objects are close to each other. In this paper we present a pivot-based method useful, not only to obtain an insight in the complexity of the metric space, but also to obtain a good pivot selection without specify in advance the number of pivots to extract. Our method, called Sparse Spatial Selection (SSS), adapts itself to the dimensionality of the metric space we are working with. SSS is dynamic, it supports object insertions in the database efficiently, it can work with both continuous and discrete distance functions, and it is suitable for secondary memory storage. In this paper we provide experimental results that confirm the advantages of the method with several vector and metric spaces. Moreover, in this paper we explain how SSS can be easily parallelized. On the other hand, in this paper we conceptualize Nested Metric Spaces, and we prove that, in some applications areas, objects can be grouped in different clusters with different associated metric spaces, all of them nested into the general metric space that explains the distances among clusters. To deal with this complex spaces we propose the extension of SSS becoming Sparse Spatial Selection for Nested Metric Spaces (SSSNMS). - Heiko Stamer,Friedrich Otto:
Restarting Tree Automata AbstractTraditional restarting automata have been introduced to mirror the linguistic concept of the so-called analysis by reduction. In the last years there was a grown effort to investigate formal language classes generated by different variants of these automata. We follow this line of research and generalize the automata model to a more complex data structure, i.e. terms of a free algebra. Unsurprisingly, many of the known results about restarting automata on strings can be transferred to the new model. We consider the expressive power of such restarting tree automata and prove some closure properties. - Martin Furer,Shiva Kasiviswanathan:
Exact MAX 2-SAT: Easier and Faster AbstractPrior algorithms known for exactly solving MAX 2-SAT improve upon the trivial upper bound only for very sparse instances. We present new algorithms for exactly solving (in fact, counting) weighted MAX 2-SAT instances. One of them has a good performance if the underlying constraint graph has a small separator decomposition, another has a slightly improved worst case performance. For a 2-SAT instance F with n variables, the worst case running time is ilde{O}(2^{(1-1/( ilde{d}(F)-1))n}), where ilde{d}(F) is the average degree in the constraint graph defined by F. The algorithms and bounds actually are valid for any MAX 2-CSP, whose clauses are over pairs of binary variables. We use strict \alpha-gadgets introduced by Trevisan, Sorkin, Sudan, and Williamson to get the same upper bounds for problems like MAX 3-SAT and MAX CUT. We also introduce a notion of strict (\alpha,\beta)-gadget to provide a framework that allows composition of gadgets. This framework allows us to obtain the same upper bounds for MAX K-SAT and MAX K-LIN-2. - Vera Kurkova:
Estimates of data complexity in neural-network learning AbstractComplexity of data with respect to a particular class of neural networks is studied. Data complexity can be measured by the magnitudes of certain norms of the regression function induced by a probability measure describing the data or its discrete approximation in the form of a function interpolating a sample of input/output pairs of training data. The norms are tailored to types of computational units. It is shown that for data for which these norms are ``small'', convergence of infima of error functionals over networks with increasing number of hidden units to the global minima is relatively fast. Thus for such data, networks with a reasonable model complexity can achieve good performance during learning. For perceptron networks, the relationship between data complexity, data dimensionality and smoothness is investigated. - O'Neil Delpratt,Naila Rahman,Rajeev Raman:
Compressed Prefix Sums AbstractWe consider the \emph{prefix sums} problem: given a (static) sequence of positive integers ec{x} = (x_1, \ldots, x_n), such that \sum_{i=1}^n x_i = m, we wish to support the operation \Sum( ec{x},j), which returns \sum_{i=1}^{j} x_i. Our interest is in minimising the space required for storing ec{x}, where `minimal space' is defined according to some compressibility criteria, while supporting \Sum as rapidly as possible. There are two main criteria: the \emph{succinct} space bound of B(m-1,n-1), where B(x,y) = \log_2 \lceil{{x}\choose{y}} ceil, applies to any sequence ec{x} whose elements add up to m. So-called \emph{data-aware} measures can be better than the succinct bound when the x_is are distributed in a skewed manner, and appropriate data-aware measures have been studied extensively in the information retrieval (IR) community \cite{WMB-99}. We discuss theoretical solutions that are close to (often within o(n) bits) of the corresponding compressibility measure, and support \Sum in doubly-logarithmic (or better) time, and experimental evaluations of practical variants thereof. We demonstrate a close connection between a particular data-aware measure (in practice, the best for an important IR application) and the succinct bound. The standard data structure that achieves the succinct bound requires a data structure that supports `\Rank{}/\Select{}' on a bit-string, which is a fundamental subroutine in succinct/compressed data structures. We provide a new efficient solution for this subroutine. - Hajo Broersma,Bert Marchal,Daniel Paulusma,A.N.M. Salman:
Improved upper bounds for \lambda-backbone colorings along matchings and stars AbstractWe continue the study on backbone colorings, a variation on classical vertex colorings that was introduced at WG2003. Given a graph G=(V,E) and a spanning subgraph H of G (the backbone of G), a \lambda-backbone coloring for G and H is a proper vertex coloring V ightarrow \{1,2,\ldots\} of G in which the colors assigned to adjacent vertices in H differ by at least\lambda. The main outcome of earlier studies is that the minimum number \ell of colors for which such colorings V ightarrow \{1,2,\ldots ,\ell\} exist in the worst case is a factor times the chromatic number (for all studied types of backbones). We show here that for split graphs and matching or star backbones, \ell is at most a small additive constant (depending on \lambda) higher than the chromatic number. Despite the fact that split graphs have a nice structure, these results are difficult to prove. Our proofs combine algorithmic and combinatorial arguments. We also indicate other graph classes for which our results imply better upper bounds on \ell than the previously known bounds. - Joachim Kneis,Daniel Moelle,Peter Rossmanith:
Partial vs. Complete Domination: t-Dominating Set AbstractWe examine the parameterized complexity of t-Dominating Set, the problem of finding a set of at most~k nodes that dominate at least t nodes of a graph~G=(V,E). The classic NP-complete problem Dominating Set, which can be seen to be t-Dominating Set with the restriction that t=n, has long been known to be W[2]-complete when parameterized in~k. Whereas this implies W[2]-hardness for t-Dominating Set and the parameter~k, we are able to prove fixed-parameter tractability for t-Dominating Set and the parameter~t. More precisely, we obtain a quintic problem kernel and a randomized O((4+\epsilon)^t\poly(n)) algorithm. The algorithm is based on the divide-and-color method introduced to the community earlier this year, rather intuitive and can be derandomized using a standard frameworks. - SU MI LEE,SU YEON LEE,DONG HOON LEE:
Efficient Group Key Agreement for Dynamic TETRA Networks AbstractTerrestrial Trunked Radio (TETRA) is the most frequency-efficient standard for mobile communication and its architecture is fully scalable, from a large high-capacity system to a low-capacity system. In the TETRA Standard, a base station unicasts encrypting messages to each mobile station in a cluster for sharing a group key. This basic key-establishment burdens mobile stations with high computation and Communication costs. Various attacks in TETRA networks, furthermore, have occurred by this lack of proper key-establishment scheme. In the paper, we first propose an efficient group key agreement in TETRA network that guarantees secure communication among light-weight mobile stations. That is, computation cost per a mobile station is very low, only requires XOR operation, and our scheme allows mobile stations and a base station to agree a group key with 1-round complexity.
Multi-Agent Systems
- Xue Xiao,Zeng Zhifeng:
Agent Oriented Methodology Construction and Customization with HDA AbstractThe agent-oriented (AO) methodology is an effective means for constructing complex systems. Despite a great deal of research, a number of challenges still exist before making agent-based computing a widely accepted paradigm in software engineering practice. In order to solve the problem of "a variety in number, difficult to use", the paper presents a hierarchical development architecture (HDA) for customizing a new AO methodology according to the given project. Based on the HDA, the developer can extract meta models from existing AO methods to assemble a new approach, much like developers building applications from third party off-the-shelf components. To exemplify its feasibility and effectiveness, the construction of C4I system is presented as a case study. - Jiri Vokrinek,Jiri Biba,Jiri Hodik,Jaromir Vybihal,Michal Pechoucek:
Competitive Contract Net Protocol AbstractThe proposed Competitive Contract Net Protocol has been designed to facilitate a flexible cooperation in competitive multi-agent environments and to support of automated or semi-automated negotiation in competitive domains. The protocol is based on FIPA standards. The protocol covers not only the phase of contracting the commitments, but also allows for a decommitment negotiation and contract termination. Thus, it consists of three phases: (i) a contracting phase, where conditions of agreement are concluded, (ii) an optional decommitment phase, where contract may be breached, and (iii) a contract termination phase, where the compliance with the concluded contract conditions is evaluated. Both the decommitment and non-compliance are bounded with penalties which measurably ensure a compliance with the commitments, but also allow an opportunistic behaviour of the agents at some price. - Claudio Cubillos,Franco Guidi-Polanco,Ricardo Soto:
Performance Analysis of a Multiagent Architecture for Passenger Transportation AbstractThis work describes the development and results on an agent architecture devoted to the planning and scheduling of passenger trips by using the contract-net protocol as base coordination mechanism. The architecture named MADARP, has been implemented over Jade, and provides a set of base agents that perform the basic interface, planning and support services, which can be extended to tackle specific passenger transport conditions and scenarios. In particular, this paper will focus on the planning agents, their coordination mechanism and its performance in a distributed scenario. The agent use allows easily adapting the architecture to different assigning and scheduling models. This work presents the results of a performance test, analyzing two different rates for the requests’ arrivals under a distributed scenario with diverse number of hosts. - Michal Karpowicz,Krzysztof Malinowski:
On Efficient Resource Allocation in Communication Networks AbstractIn this paper we address the problem of designing distributed mechanisms which efficiently allocate resources in large-scale decentralized systems that are characterized by strategic behavior of agents. Our focus is on allocation and payment rules which lead selfishly competing agents to allocations that maximize their payoffs and at the same time are optimal solutions to the resource allocation problem. We establish conditions that must be satisfied by these rules to guarantee efficiency of Nash equilibria of the induced games. The conditions imply the existence of an infinite number of payment rules which determine efficient allocations and enable the resource manager to obtain the revenue that would be generated by price-taking agents. We also prove the convergence of a dynamical bidding process determined by the proposed class of efficient mechanisms. Since signals reported by agents to the resource manager are one-dimensional, the mechanisms are well-suited to network applications. Possible and interesting implementations include bandwidth-broker based multi-agent systems for network interconnection and QoS management, market-pricing of edge-allocated capacity and congestion control. - Mi-Young Kang,Omar F Hamad,Ji-Seung Nam:
FTTH-Enhanced mTBCP-Based Overlay Construction and Evaluation AbstractFor better performance and to avoid member service annoyance that results due to joining-clients’ waiting durations and time-outs when there are more than one clients wanting to join concurrently for FTTH-based Broadcasting Mini-system’s service, this paper proposes a more efficient and better performing Overlay Tree Building Control Protocol by modifying and extending the basic mechanisms building the conventional TBCP. The modified-TBCP (mTBCP) proposed is performance-effective mechanism since it considers the case of how fast will children, concurrently, find and join new parents when paths to existing parents are broken. Besides utilizing partial topology information, mTBCP also does a LAN-out-degree-check. If the selected child-parent-pair falls under the same LAN, that selected parent does not change the out-degree status. The performance comparison, in terms of Overlay-Connection-Count and Latency against Group-Size-Growth, between the proposed mTBCP and the traditional TBCP is done through simulations and the results conclude in favour of the proposed mTBCP. - Javad Safaei Mehranpour,Gholamreza Ghassem-Sani:
Incremental Learning of Planning Operators in Stochastic Domains AbstractIn this work we assume that there is an agent in an unknown environment (domain). This agent has some predefined actions and when explores the environment, it perceives its current state. The mission of this agent is to fulful the tasks (goals) that often are assigned to it as fast as it can. Acting has lots of cost, and usually planning and simulating the environment can reduce this cost. In this paper we address a new approach for incremental induction of probabilistic planning operators, from this environment while the agent tries to reach to its current goals1. We also address some trade offs such as explorations (for better learning of stochastic operators, acting) and exploitation (for fast discovery of goals, planning), and we explain that a good decision in these trade offs is dependant on the stability and accuracy of the learned planning operators, and the fact that how much the plan is probably successful for the future execution. - Reza Ebrahimpour,Ehsanollah Kabir,Mohammad Reza Yousefi:
Teacher-Directed Learning with Mixture of Experts for View-independent Face Recognition AbstractWe propose two new models for view-independent face recognition, which lies under the category of multi-view based approaches. We use the so-called “mixture of experts” (MOE) in which, the problem space is divided into several subspaces for the experts, and then the outputs of experts are combined by a gating network to form the final output. Basically, our focus is on the way that the face space is partitioned by MOE. In our first model, experts of MOE structure are not biased in any way to prefer one class of faces to another, in other words, the gating network learns a partition of input face space and trusts one expert in each of these partitions; we call this method “self-directed partitioning”. In our second model, we attempt to direct experts to specialize in predetermined areas of face space by developing teacher-direted learning methods for MOE. In this model, by including teacher information about the pose of input face image in the training phase of networks, each expert is directed to learn faces of specific pose class, so referred to as “teacher-directed partitioning”. Thus the face space is quantized according to a number of predetermined views and MOE is trained to adapt to such face space partitioning, instead of allowing the mixture structure to partition it irrespective of view. The experiments’ results support our claim that directing the mixture of experts to a predetermined partitioning of face space is a more beneficial way of using MOE for view-independent face recognition. - byungryong kim:
Protecting Agent from Attack in Grid Computing AbstractP2P networks provide a basic form of anonymity, and the participating nodes exchange information without knowing who is the original sender. Packets are relayed through the adjacent nodes and do not contain identity information about the sender. Since these packets are passed through a dynamically-formed path and since the final destination is not known until the last time, it is impossible to know who has sent it in the beginning and who will be the final recipient. The anonymity, however, breaks down at download/upload time because the IP address of the host from which the data is downloaded (or to which it is uploaded) can be known to the outside. We propose a technique to provide anonymity for both the client and the server node. A random node along the path between the client and the server node is selected as an agent node and works as a proxy: the client will see it as the server and the server looks at it as the client, hence protecting the identity of the client and the server from attacker
Emerging Web Technologies
- José Paulo Leal,Marcos Aurélio Domingues:
Rapid development of web interfaces to heterogeneous systems AbstractThe general problem addressed in this paper is the rapid development of web interfaces to software systems using only their command line interface. This kind of system is frequently developed in environments that greatly differ from those where web interface will be implemented. In this setting it is also important to maintain a loose coupling between the web interface and the system it controls since the latter must be able to continue its normal development independently of the former. We propose a framework to develop web interfaces targeted to these systems whose main feature is the fact that it can be extended without requiring code programming. The hot spots of our framework are XML configuration files to define the interface data, how this data is mapped into the system's commands, and how commands output and the interaction state is mapped into web formatting languages. With this approach the web interface is kept separated from the system it controls, it is easy to define and modify, and is able to capture enough domain knowledge to be a real advantage for the novice or sporadic user. In this paper we present the proposed framework architecture, loosely inspired in the MVC pattern, its implementation on Java servlet containers, and its application to the AGILMAT system, a high-school mathematical problem generator developed using constrained grammars. - Josep Silva:
XML Slicing AbstractProgram slicing is a well-known technique to extract the program statements that (potentially) affect the values computed at some point of interest. In this work, we introduce a novel slicing method for XML documents. Essentially, given an XML document (which is valid w.r.t. some DTD), we produce a new XML document (a slice) that contains the relevant information in the original XML document according to some criterion. Furthermore, we also output a new DTD such that the computed slice is valid w.r.t. this DTD. A prototype implementation of the XML slicer has been undertaken. - Deok-Hwan Kim,Jae-Won Song,Ju-Hong Lee:
A Hybrid Region Weighting Approach for Relevance Feedback in Region-Based Image Search on the Web AbstractIn this paper, a new hybrid weighting method, which learns region importance from the region size and the spatial location of regions in an image, is introduced to re-weight regions optimally and improve the performance of the region-based search system on the Web. Relevant images marked by an user may exhibit very different visual characteristics so that they may be scattered in several clusters in the feature space, since there exists the semantic gap between the low level feature and the high level semantics in user's mind. Our main goal is to find semantically related clusters and their weights to narrow down this semantic gap. To do this, The hybrid region weighting method, which refines the weights of region-clusters through relevance feedback, determines the importance of regions according to the region size and spatial location information of regions in an image. Experimental results demonstrate the efficiency and the effectiveness of the proposed weighting method in comparison with the area percentage method and the region frequency weighted by inverse image frequency method, respectively. - Heung-Nam Kim,Kyung-Jin Oh,In-Kyung Bae,Geun-Sik Jo:
Semantic Web Approach in Designing Collaborative E-Item Bank System AbstractExisting item bank system presents a variety of assessments for data management and integration with individual learning evaluation system. How-ever, as the data in these established item bank systems do not include seman-tics, they cannot analyze the implication and perform the accurate search such as synonymous words. Therefore, both learners and teachers only can access simple text data using the item bank system and often waste their time on checking unnecessary search results and extracting information from data once again. Moreover, since there is no clear definition of the relationship between items and teachers or learners, and between data and units, it is hard to use and share extra-item information. In order to solve these problems, this research de-scribes the definition of conception and organization by constructing Ontology of E-Item Bank system using OWL, which is semantic web technology. Fur-thermore, on the basis of Ontology, OWL metadata, individuals, are built, then extracted semantic factors using OWLJessKB. We do not only used this ex-tracted semantic factors as a fact, but also domain rules using SWRL for JESS inferencing engine, so that we can make it possible to inference and provide reasoning in web data structures. As a result, it is possible to combine all the data of E-Item bank system and make computer understand the meanings of concepts. In addition, a search service with inference can be applied to educa-tion and lead to cooperative study between teachers and students. - Michal Tvarozek,Michal Barla,Maria Bielikova:
Presentation and Personalization in Web-Based Information Systems AbstractLarge information spaces and complex functionality of contemporary systems together with the advent of the Semantic Web are big challenges for the design of simple yet powerful user interfaces. The complex nature of systems thus requires the use of several presentation, personalization and user modeling methods and techniques to address the growing needs and requirements of both users and systems. We present a design of an architecture for the presentation and personalization layer of a web-based information system that employs a set of interconnected software components implemented as autonomous software tools for presentation, personalization and user modeling to support features such as navigation support and different views on the presented data, acquisition and evaluation of user characteristics and user adaptation and personalization. The feasibility of our design is evaluated by its realization in the labor market application domain. - Peter Bartalos,Michal Barla,Gyorgy Frivolt,Michal Tvarozek,Anton Andrejko,Mária Bieliková,Pavol Návrat:
Building Ontological Base for Experimental Evaluation of Semantic Web Applications AbstractThe increasing number of Semantic Web applications that work with ontologies implies an increased need for building ontological knowledge bases. In order to improve ontologies during their development as well as to allow applications to be experimentally evaluated prior to their complete implementation and deployment, ontology bases must be filled with experimental data (i.e., instance ontologies), which can be used to evaluate methods used for information processing. We describe several approaches together with a method of building an ontological knowledge base for purposes of experimentation with Semantic Web applications. We also discuss characteristics and suitability of particular approaches to the development of experimental ontological knowledge bases. - Sun Park,Ju-Hong Lee,Deok-Hwan Kim,Chan-Min Ahn:
Multi-document Summarization Based on Cluster using Non-negative Matrix Factorization AbstractIn this paper, a new summarization method, which uses non-negative matrix factorization (NMF) and K-means clustering, is introduced to extract meaningful sentences from multi-documents. The proposed method can im-prove the quality of document summaries because the inherent semantics of the documents are well reflected by using the semantic features calculated by NMF and the sentences most relevant to the given topic are extracted efficiently by using the semantic variables derived by NMF. Besides, it uses K-means clustering to remove noises so that it can avoid the biased inherent semantics of the documents to be reflected in summaries. We perform detail experiments with the well-known DUC test dataset. The experimental results demonstrate that the proposed method has better performance than other methods using the LSA, the Kmeans, and the NMF. - Jianyin Zhang:
Immune-inspired Online Method for Service Intertion detection AbstractService composition technique aims to integrate several Web services to meet the increasing user demand that a single service can not satisfy.But it also brings the potential of abnormal message interactions among the composed services which lead to the service interactions problem resembling the feature interactions in the telecom. Inspired by the similarities between the immune system and the service interactions detection system, this paper presents an online method to detect the service interactions problem by using ideas from the immune principles. The method overcomes the drawbacks of static methods, and conduces to an effective detection for the detection of not only known feature interactions, but also the previously unknown ones. - Hyunho Lee,Wonsuk Lee:
Runtime-Efficient Approach for Multiple Continuous Filtering in XML Message Brokers AbstractXML message brokers play a key role in exchanging information in ubiquitous environments. One of their core technical issues is difficulty associated with processing a set of XPath queries for multiple continuous filtering over incoming XML streams. This paper proposes a novel system designed to provide an epochal solution to this problem. The proposed system provides efficient data structures and matching algorithm in order to minimize the runtime workload of continuous filtering over XML streams. Also, the performance of proposed approach is verified through a variety of experiments, including comparisons with YFilter. The proposed approach is practically linear-scalable and stable in terms of processing a set of XPath queries in a continuous and timely fashion. Furthermore, this approach consistently outperforms YFilter, particularly under conditions of low selectivity. - Dae Sung Lee,Ki Chang Kim,Year Back Yoo:
IPBio : Embedding Biometric Data in IP Header for Per-Packet Authentication AbstractPer-packet authentication is a powerful way to authenticate the user. Other authentication mechanisms (e.g. password authentication) verify the user at login time only while per-packet authentication verifies all packets coming from that user. Since every packet is authenticated repeatedly, inserting a fake packet or masquerading as a legitimate user is effectively prevented. Existing techniques for per-packet authentication such as IPSec or PLA, however, is either too expensive or not strong enough. We propose to include biometric data of the user in all packets for per-packet authentication. By collecting the user's biometric data periodically and physically from the user during the session and including it in all packets, we believe that we can provide a cheaper and more secure way of per-packet authentica-tion. A random portion of the biometric data is extracted and used to digest the IP datagram. This technique allows us to control the size of the biometric data and to protect its contents from eavesdropper. This paper explains about the technique and provides experimental results. - Yong LI,Fangchun YANG,Sen SU:
A Semantic Peer-to-Peer Overlay for Web Services Discovery AbstractWeb Services with distributed and dynamic characteristics need efficient and decentralized discovery infrastructure supporting the semantic descriptions and discovery. In this paper, a structured peer-to-peer semantic routing system is proposed to support the completely decentralized semantic service discovery. In the presented system, with the semantic service characteristic vector, the semantic service description is distributed on the structured P2P network to allow requesters to routing and locating services according to semantic similarity and relationship. Finally, experimental result shows that the presented system is efficient and scalable. - Wei Shi,Jian Wu,Zhaohui Wu:
Using Improved FOAF to Enhance BPEL-extracted RBAC Capability (withdrawn) - Joe Tekli,Richard Chbeir,Kokou Yetongnon:
A Hybrid Approach for XML Similarity AbstractIn the past few years, XML has been established as an effective means for information management, and has been widely exploited for complex data representation. Owing to an unparalleled increasing use of the XML standard, developing efficient techniques for comparing XML-based documents becomes essential in information retrieval (IR) research. Various algorithms for comparing hierarchically structured data, e.g. XML documents, have been proposed in the literature. However, to our knowledge, all of them focus exclusively on comparing documents based on structural features, overlooking the semantics involved. In this paper, we integrate IR semantic similarity assessment in an edit distance algorithm, seeking to amend similarity judgments when comparing XML-based documents. Our approach comprises of an original edit distance operation cost model, introducing semantic relatedness of XML element/attribute labels, in traditional edit distance computations. A prototype has been developed to evaluate our model’s performance. Experiments yielded notable results.
Dependable Software and Systems
- Tomas Matousek,Filip Zavoral:
Extracting Zing Models from C Source Code AbstractIn the paper, we propose an approach to an automatic extraction of verification models for the C language source code. We primarily focus on the representation of pointers and arrays, which make the extraction from the C language specific. We provide an implementation of the model extractor as a part of our broader effort to develop a verifier of Windows kernel drivers based on the Zing model checker. To demonstrate the feasibility of our approach, we give examples of the extraction results on a practical synchronization problem. - Jai Wug Kim,Jongpil Lee,Heon Y. Yeom:
Experimental Assessment of the Practicality of a Fault-tolerant System AbstractFault-tolerance has gained renewed importance with the proliferation of high-performance clusters. However, fault-tolerant systems have not yet been widely adopted commercially because they are either hard to deploy, hard to use, hard to manage, hard to maintain, or hard to justify. We have developed M3, a practical and easily-deployable multiple fault-tolerant MPI system for Myrinet, to satisfy the demand for a fault-tolerant system. In this paper, we run rigorous tests using real-world applications to verify that M3 can be used in commercial clusters. We also describe improvements made to our system to solve various problems that arose when deploying it on a commercial cluster. This paper models our system’s checkpoint overhead and presents the results of a series of tests using computation- and communication-intensive MPI applications used commercially in various fields of science. The experimental results show that not only does our system conform to various types of running environment well, but that it can also be practically deployed in commercial clusters. - Jaroslav Drazan,Vladimir Mencl:
Improved Processing of Textual Use Cases: Deriving Behavior Specifications AbstractThe requirements for a system are often specified as textual use cases. Although they are specified in natural language, the simple and uniform sentence structure used makes automated processing of use cases feasible. However, the numerous use case approaches vary in the permitted complexity and variations of sentence structure. Frequently, use cases are written in the form of compound sentences describing several actions. While there are methods for analyzing use cases following the very simple SVDPI (subject-verb-direct object ... indirect object) pattern, methods for more complex sentences are still needed. We propose a new method for processing textual requirements based on the conversion scheme earlier described in [13]. The new method allows to process the commonly used complex sentence structures, obtaining more descriptive behavior specifications. Such behavior specifications may be used to verify and validate requirements and to derive the initial design of the system. - Alain Ozanne,Philippe Collet,Nicolas Rivierre:
Towards a Versatile Contract Model to Organize Behavioral Specifications AbstractThe dependability of component-based systems mainly relies on the ability to guarantee components safe collaboration. Many specification formalisms can then be used and we argue that such specifications should be organized through an appropriate contract model so that checking and guarantees can be better exploited. In this paper, we propose a versatile contract model that explicitly reifies the assumptions and guarantees of some behavioral specifications on component assemblies. We briefly illustrate the integration of executable assertions and we detail how Behavior Protocols can be integrated in the contract model. - Mila Majster-Cederbaum,Moritz Martens,Christoph Minnameier:
A Polynomial-Time checkable sufficient Condition for Deadlock-Freedom of Component-Based Systems AbstractInteraction systems are a formal model for component based systems. Combining components via connectors to form more complex systems may give rise to deadlock situations. Testing the existence of deadlocks is NP-hard as it involves global state analysis. We present a parametrized polynomial-time algorithm that is able to confirm deadlock-freedom for a certain class of interaction systems. The discussion includes characteristic examples and displays the role of the parameter of the algorithm. - Xin Chen,Zhiming Liu,Vladimir Mencl:
Separation of Concerns and Consistent Integration in Requirements Modelling AbstractDue to their increasing complexity, design of software systems is not becoming easier. Furthermore, modern applications ranging from enterprise to embedded systems require very high levels of correctness and dependability assurance. The most effective means to handle complexity is separation of concerns and incremental development, and assurance of correctness requires formal modelling and formal analysis. When separation of concerns splits the model into several parts, an important issue is to ensure consistency among these parts. We propose an approach supporting separation of concerns and consistent and incremental modelling of requirements. - Dietmar Schreiner,Karl M. Göschka:
Explicit Connectors in Component Based Software Engineering for Distributed Embedded Systems AbstractThe increasing complexity of today's embedded systems applications imposes the requirements and constraints of distributed, heterogeneous subsystem interaction to software engineers. These requirements are well met by the component based software engineering paradigm: complex software is decomposed into coherent, interacting units of execution, the so called components. Connectors are a commonly used abstraction to model the interaction between them. We propose to use explicit connectors when building distributed embedded systems applications. Explicit connectors encapsulate the logic of distributed interaction, hence they provide well defined contracts regarding properties of inter-component communication. Our approach allows model level validation of component composition and interaction incorporating communication related constraints beyond simple interface matching. In addition, by using explicit connectors, the complexity of application components is reduced without the need for any heavy weight middleware. - Ian Peake,Heinz Schmidt:
Extra-functional prediction of component-based control systems---industrial experience AbstractDelivering and maintaining dependable component-based systems within budget is a significant practical challenge. For example, best practice, even in large organisations, is only just starting to move beyond simple testing for verification of performance and reliability. The eCAP(-CBCS) project, a collaboration between ABB Corporate Research and Monash University, Australia, seeks to extend research in architectural modelling and analysis, and apply it to distributed, embedded control systems. Background theory developed by Monash's Distributed Systems and Software Engineering group includes generic models for composing {\em parameterised} component interaction protocols, behaviours, types and properties such as reliability and execution time. The eCAP project produced for evaluation a prototype to warn about, and diagnose, possible excessive peak load in IEC 61131-3 controllers caused by high task worst-case execution time / interval time ratios. Development incorporated typical business and technical requirements, both functional--- e.g., integration via loose coupling into an existing development platform, and prediction strategy to cope with black-box components (no source, only performance data) ---and extra-functional---e.g., usability and adequate analyser performance. Lessons learned in satisfying these led to: applications for software metrics and profile visualisation techniques; design refinements such as the use of component type parameterisation for accurate, context-sensitive component property analyses, and; new ideas for exploiting underlying theory such as context-sensitive model-driven performance testing. - Yunja Choi:
Checking Interaction Consistency in MARMOT Component Refinements AbstractThe refinement process of component designs is one of the basic building blocks for a systematic component-based development. In this process, identifying inconsistent specifications of interactions among refined and refining components can be a critical issue for system safety and/or reliability. To efficiently identify interaction inconsistencies, we have been developing a consistency checking framework integrated into the component-based development methodology {\sc Marmot}, using model checking as a debugging tool. We introduce our notion of interaction consistency, propose a general framework for integrating the consistency checking mechanism into the refinement process, and demonstrate how the efficiency of identifying inconsistencies can be improved through abstractions. - Harksoo Kim:
A Dialogue-based NLIDB System in a Schedule Management Domain: About the Method to Find Users’ Intentions AbstractTo reduce the complexities of SQL query generation and increase the flexibilities of user interface, we propose a dialogue-based NLIDB system. The system classifies users’ intentions into domain actions (pairs of a speech act and a concept sequence) using a maximum entropy model. Based on the classifica-tion results, the system fills up predefined SQL templates and generates proper SQL queries for natural language interface. In the experiment, the system showed the success rate of 83.4% for SQL generation.