OpenRaiser/Intern-Atlas huggingface dataset:
Model Checking Synchronized Products of Infinite Transition Systems
Venue: arXiv cs.LO 2007
Year: 2007

Formal verification using the model checking paradigm has to deal with two aspects: The system models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many (parameterized) synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components. This result is optimal in the following sense: (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of first-order logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.
Social Browsing & Information Filtering in Social Media
Venue: arXiv cs.CY 2007
Year: 2007

Social networks are a prominent feature of many social media sites, a new generation of Web sites that allow users to create and share content. Sites such as Digg, Flickr, and Del.icio.us allow users to designate others as "friends" or "contacts" and provide a single-click interface to track friends' activity. How are these social networks used? Unlike pure social networking sites (e.g., LinkedIn and Facebook), which allow users to articulate their online professional and personal relationships, social media sites are not, for the most part, aimed at helping users create or foster online relationships. Instead, we claim that social media users create social networks to express their tastes and interests, and use them to filter the vast stream of new submissions to find interesting content. Social networks, in fact, facilitate new ways of interacting with information: what we call social browsing. Through an extensive analysis of data from Digg and Flickr, we show that social browsing is one of the primary usage modalities on these social media sites. This finding has implications for how social media sites rate and personalize content.
Convex and linear models of NP-problems
Venue: arXiv cs.DM 2007
Year: 2007

Reducing the NP-problems to the convex/linear analysis on the Birkhoff polytope.
Security Analysis of a Remote User Authentication Scheme with Smart Cards
Venue: arXiv cs.CR 2007
Year: 2007

Yoon et al. proposed a new efficient remote user authentication scheme using smart cards to solve the security problems of W. C. Ku and S. M. Chen scheme. This paper reviews Yoon et al. scheme and then proves that the password change phase of Yoon et al. scheme is still insecure. This paper also proves that the Yoon et al. is still vulnerable to parallel session attack.
Diversification in the Internet Economy:The Role of For-Profit Mediators
Venue: arXiv cs.GT 2007
Year: 2007

We investigate market forces that would lead to the emergence of new classes of players in the sponsored search market. We report a 3-fold diversification triggered by two inherent features of the sponsored search market, namely, capacity constraints and collusion-vulnerability of current mechanisms. In the first scenario, we present a comparative study of two models motivated by capacity constraints - one where the additional capacity is provided by for-profit agents, who compete for slots in the original auction, draw traffic, and run their own sub-auctions, and the other, where the additional capacity is provided by the auctioneer herself, by essentially acting as a mediator and running a single combined auction. This study was initiated by us in \cite{SRGR07}, where the mediator-based model was studied. In the present work, we study the auctioneer-based model and show that this model seems inferior to the mediator-based model in terms of revenue or efficiency guarantee due to added capacity. In the second scenario, we initiate a game theoretic study of current sponsored search auctions, involving incentive driven mediators who exploit the fact that these mechanisms are not collusion-resistant. In particular, we show that advertisers can improve their payoffs by using the services of the mediator compared to directly participating in the auction, and that the mediator can also obtain monetary benefit, without violating incentive constraints from the advertisers who do not use its services. We also point out that the auctioneer can not do very much via mechanism design to avoid such for-profit mediation without losing badly in terms of revenue, and therefore, the mediators are likely to prevail.
Self-Organising management of Grid environments
Venue: arXiv cs.DC 2007
Year: 2007

This paper presents basic concepts, architectural principles and algorithms for efficient resource and security management in cluster computing environments and the Grid. The work presented in this paper is funded by BTExacT and the EPSRC project SO-GRM (GR/S21939).
The Price of Selfish Stackelberg Leadership in a Network Game
Venue: arXiv cs.GT 2007
Year: 2007

We study a class of games in which a finite number of agents each controls a quantity of flow to be routed through a network, and are able to split their own flow between multiple paths through the network. Recent work on this model has contrasted the social cost of Nash equilibria with the best possible social cost. Here we show that additional costs are incurred in situations where a selfish ``leader'' agent allocates his flow, and then commits to that choice so that other agents are compelled to minimise their own cost based on the first agent's choice. We find that even in simple networks, the leader can often improve his own cost at the expense of increased social cost. Focusing on the 2-player case, we give upper and lower bounds on the worst-case additional cost incurred.
On the performance of Golden space-time trellis coded modulation over MIMO block fading channels
Venue: arXiv cs.IT 2007
Year: 2007

The Golden space-time trellis coded modulation (GST-TCM) scheme was proposed in \cite{Hong06} for a high rate $2\times 2$ multiple-input multiple-output (MIMO) system over slow fading channels. In this letter, we present the performance analysis of GST-TCM over block fading channels, where the channel matrix is constant over a fraction of the codeword length and varies from one fraction to another, independently. In practice, it is not useful to design such codes for specific block fading channel parameters and a robust solution is preferable. We then show both analytically and by simulation that the GST-TCM designed for slow fading channels are indeed robust to all block fading channel conditions.
Channel Code Design with Causal Side Information at the Encoder
Venue: arXiv cs.IT 2007
Year: 2007

The problem of channel code design for the $M$-ary input AWGN channel with additive $Q$-ary interference where the sequence of i.i.d. interference symbols is known causally at the encoder is considered. The code design criterion at high SNR is derived by defining a new distance measure between the input symbols of the Shannon's \emph{associated} channel. For the case of binary-input channel, i.e., M=2, it is shown that it is sufficient to use only two (out of $2^Q$) input symbols of the \emph{associated} channel in the encoding as far as the distance spectrum of code is concerned. This reduces the problem of channel code design for the binary-input AWGN channel with known interference at the encoder to design of binary codes for the binary symmetric channel where the Hamming distance among codewords is the major factor in the performance of the code.
Performance bounds and codes design criteria for channel decoding with a-priori information
Venue: arXiv cs.IT 2007
Year: 2007

In this article we focus on the problem of channel decoding in presence of a-priori information. In particular, assuming that the a-priori information reliability is not perfectly estimated at the receiver, we derive a novel analytical framework for evaluating the decoder's performance. It is derived the important result that a "good code", i.e., a code which allows to fully exploit the potential benefit of a-priori information, must associate information sequences with high Hamming weights to codewords with low Hamming weights. Basing on the proposed analysis, we analyze the performance of convolutional codes, random codes, and turbo codes. Moreover, we consider the transmission of correlated binary sources from independent nodes, a problem which has several practical applications, e.g. in the case of sensor networks. In this context, we propose a very simple joint source-channel turbo decoding scheme where each decoder works by exploiting a-priori information given by the other decoder. In the case of block fading channels, it is shown that the inherent correlation between information signals provide a form of non-cooperative diversity, thus allowing joint source-channel decoding to outperform separation-based schemes.
Entropy of capacities on lattices and set systems
Venue: arXiv cs.DM 2007
Year: 2007

We propose a definition for the entropy of capacities defined on lattices. Classical capacities are monotone set functions and can be seen as a generalization of probability measures. Capacities on lattices address the general case where the family of subsets is not necessarily the Boolean lattice of all subsets. Our definition encompasses the classical definition of Shannon for probability measures, as well as the entropy of Marichal defined for classical capacities. Some properties and examples are given.
Derivative of functions over lattices as a basis for the notion of interaction between attributes
Venue: arXiv cs.DM 2007
Year: 2007

The paper proposes a general notion of interaction between attributes, which can be applied to many fields in decision making and data analysis. It generalizes the notion of interaction defined for criteria modelled by capacities, by considering functions defined on lattices. For a given problem, the lattice contains for each attribute the partially ordered set of remarkable points or levels. The interaction is based on the notion of derivative of a function defined on a lattice, and appears as a generalization of the Shapley value or other probabilistic values.
A Biologically Inspired Classifier
Venue: arXiv cs.DB 2007
Year: 2007

We present a method for measuring the distance among records based on the correlations of data stored in the corresponding database entries. The original method (F. Bagnoli, A. Berrones and F. Franci. Physica A 332 (2004) 509-518) was formulated in the context of opinion formation. The opinions expressed over a set of topic originate a ``knowledge network'' among individuals, where two individuals are nearer the more similar their expressed opinions are. Assuming that individuals' opinions are stored in a database, the authors show that it is possible to anticipate an opinion using the correlations in the database. This corresponds to approximating the overlap between the tastes of two individuals with the correlations of their expressed opinions. In this paper we extend this model to nonlinear matching functions, inspired by biological problems such as microarray (probe-sample pairing). We investigate numerically the error between the correlation and the overlap matrix for eight sequences of reference with random probes. Results show that this method is particularly robust for detecting similarities in the presence of translocations.
Première étape vers une navigation référentielle par l'image pour l'assistance à la conception des ambiances lumineuses
Venue: arXiv cs.IR 2007
Year: 2007

In the first design stage, image reference plays a double role of means of formulation and resolution of problems. In our approach, we consider image reference as a support of creation activity to generate ideas and we propose a tool for navigation in references by image in order to assist daylight ambience design. Within this paper, we present, in a first part, the semantic indexation method to be used for the indexation of our image database. In a second part we propose a synthetic analysis of various modes of referential navigation in order to propose a tool implementing all or a part of these modes.
Complexity of the conditional colorability of graphs
Venue: arXiv cs.DM 2007
Year: 2007

For an integer $r>0$, a conditional $(k,r)$-coloring of a graph $G$ is a proper $k$-coloring of the vertices of $G$ such that every vertex $v$ of degree $d(v)$ in $G$ is adjacent to vertices with at least $min\{r, d(v)\}$ different colors. The smallest integer $k$ for which a graph $G$ has a conditional $(k,r)$-coloring is called the $r$th order conditional chromatic number, denoted by $χ_r(G)$. It is easy to see that the conditional coloring is a generalization of the traditional vertex coloring for which $r=1$. In this paper, we consider the complexity of the conditional colorings of graphs. The main result is that the conditional $(3,2)$-colorability is $NP$-complete for triangle-free graphs with maximum degree at most 3, which is different from the old result that the traditional 3-colorability is polynomial solvable for graphs with maximum degree at most 3. This also implies that it is $NP$-complete to determine if a graph of maximum degree 3 is $(3,2)$- or $(4,2)$-colorable. Also we have proved that some old complexity results for traditional colorings still hold for the conditional colorings.
Limited Feedback-based Block Diagonalization for the MIMO Broadcast Channel
Venue: arXiv cs.IT 2007
Year: 2007

Block diagonalization is a linear precoding technique for the multiple antenna broadcast (downlink) channel that involves transmission of multiple data streams to each receiver such that no multi-user interference is experienced at any of the receivers. This low-complexity scheme operates only a few dB away from capacity but requires very accurate channel knowledge at the transmitter. We consider a limited feedback system where each receiver knows its channel perfectly, but the transmitter is only provided with a finite number of channel feedback bits from each receiver. Using a random quantization argument, we quantify the throughput loss due to imperfect channel knowledge as a function of the feedback level. The quality of channel knowledge must improve proportional to the SNR in order to prevent interference-limitations, and we show that scaling the number of feedback bits linearly with the system SNR is sufficient to maintain a bounded rate loss. Finally, we compare our quantization strategy to an analog feedback scheme and show the superiority of quantized feedback.
3-D Self-Assembled Soi Mems: An Example of Multiphysics Simulation
Venue: arXiv cs.OH 2007
Year: 2007

MEMS devices are typical systems where multiphysics simulations are unavoidable. In this work, we present possible applications of 3-D self-assembled SOI (Silicon-on-Insulator) MEMS such as, for instance, thermal actuators and flow sensors. The numerical simulations of these microsystems are presented. Structural and thermal parts have to be strongly coupled for correctly describing the fabrication process and for simulating the behavior of these 3-D SOI MEMS.
Parametric Yield Analysis of Mems via Statistical Methods
Venue: arXiv cs.OH 2007
Year: 2007

This paper considers a developing theory on the effects of inevitable process variations during the fabrication of MEMS and other microsystems. The effects on the performance and design yield of the microsystems devices are analyzed and presented. A novel methodology in the design cycle of MEMS and other microsystems is briefly introduced. This paper describes the initial steps of this methodology that is aimed at counteracting the parametric variations in the product cycle of microsystems. It is based on a concept of worst-case analysis that has proven successful in the parent IC technology. Issues ranging from the level of abstraction of the microsystem models to the availability of such models are addressed
Resolution Limits for Resonant Mems Sensors Based on Discrete Relay Feedback Techniques
Venue: arXiv cs.OH 2007
Year: 2007

This paper is devoted to the analysis of resonant MEMS sensors based on discrete relay feedback techniques. One drawback of such techniques is that some synchronization usually occurs between the discrete part and the continuous part of the system: this results in sensor responses that are very similar to the curves known as devil's staircases, i.e. the frequency does not vary smoothly with the sensor's input. The main contribution of this paper is a theoretical calculation of the resolution of such systems. The resolutions of two existing resonant MEMS architectures are then calculated and these results are discussed.
A Silicon-Based Micro Gas Turbine Engine for Power Generation
Venue: arXiv cs.OH 2007
Year: 2007

This paper reports on our research in developing a micro power generation system based on gas turbine engine and piezoelectric converter. The micro gas turbine engine consists of a micro combustor, a turbine and a centrifugal compressor. Comprehensive simulation has been implemented to optimal the component design. We have successfully demonstrated a silicon-based micro combustor, which consists of seven layers of silicon structures. A hairpin-shaped design is applied to the fuel/air recirculation channel. The micro combustor can sustain a stable combustion with an exit temperature as high as 1600 K. We have also successfully developed a micro turbine device, which is equipped with enhanced micro air-bearings and driven by compressed air. A rotation speed of 15,000 rpm has been demonstrated during lab test. In this paper, we will introduce our research results major in the development of micro combustor and micro turbine test device.
Above Ic Micro-Power Generators for RF-Mems
Venue: arXiv cs.OH 2007
Year: 2007

This work presents recent advances in the development and the integration of an electrochemical (chemicalelectrical energy conversion) micro power generator used as a high voltage energy source for RF-MEMS powering. Autonomous MEMS require similarly miniaturized power sources. Up to day, solid state thin film batteries are realized with mechanical masks. This method doesn't allow dimensions below a few mm^2 active area, and besides the whole process flow is done under controlled atmosphere so as to ensure materials chemical stability (mainly lithiated materials). Within this context, Microelectronics micro-fabrication procedures (photolithography, Reactive Ion Etching...) are used to reach both miniaturisation (100x100 $μ$m^2 targeted unit cell active area) and Above IC technological compatibility. All process steps developed here are realized in clean room environment.
Characterisation of the Etching Quality in Micro-Electro-Mechanical Systems by Thermal Transient Methodology
Venue: arXiv cs.OH 2007
Year: 2007

Our paper presents a non-destructive thermal transient measurement method that is able to reveal differences even in the micron size range of MEMS structures. Devices of the same design can have differences in their sacrificial layers as consequence of the differences in their manufacturing processes e.g. different etching times. We have made simulations examining how the etching quality reflects in the thermal behaviour of devices. These simulations predicted change in the thermal behaviour of MEMS structures having differences in their sacrificial layers. The theory was tested with measurements of similar MEMS devices prepared with different etching times. In the measurements we used the T3Ster thermal transient tester equipment. The results show that deviations in the devices, as consequence of the different etching times, result in different temperature elevations and manifest also as shift in time in the relevant temperature transient curves.
Optimization of Piezoelectric Electrical Generators Powered by Random Vibrations
Venue: arXiv cs.OH 2007
Year: 2007

This paper compares the performances of a vibrationpowered electrical generators using PZT piezoelectric ceramic associated to two different power conditioning circuits. A new approach of the piezoelectric power conversion based on a nonlinear voltage processing is presented and implemented with a particular power conditioning circuit topology. Theoretical predictions and experimental results show that the nonlinear processing technique may increase the power harvested by a factor up to 4 compared to the Standard optimization technique. Properties of this new technique are analyzed in particular in the case of broadband, random vibrations, and compared to those of the Standard interface.
Electrostatic Actuators Operating in Liquid Environment : Suppression of Pull-in Instability and Dynamic Response
Venue: arXiv cs.OH 2007
Year: 2007

This paper presents results about fabrication and operation of electrostatic actuators in liquids with various permittivities. In the static mode, we provide experimental and theoretical demonstration that the pull-in effect can be shifted beyond one third of the initial gap and even be eliminated when electrostatic actuators are operated in liquids. This should benefit to applications in microfluidics requiring either binary state actuation (e.g. pumps, valves) or continuous displacements over the whole gap (e.g. microtweezers). In dynamic mode, actuators like micro-cantilevers present a great interest for Atomic Force Microscopy (AFM) in liquids. As this application requires a good understanding of the cantilever resonance frequency and Q-factor, an analytical modeling in liquid environment has been established. The theoretically derived curves are validated by experimental results using a nitride encapsulated cantilever with integrated electrostatic actuation. Electrode potential screening and undesirable electrochemistry in dielectric liquids are counteracted using AC-voltages. Both experimental and theoretical results should prove useful in micro-cantilever design for AFM in liquids.
Micro-Ball Lens Array Fabrication in Photoresist Using Ptfe Hydrophobic Effect
Venue: arXiv cs.OH 2007
Year: 2007

This paper presents a simple method to fabricate micro-ball lens and its array. The key technology is to use the hydrophobic characteristics of polyterafluoroethylene (PTFE) substrate. High contact angle between melted photoresist pattern and PTFE can generate micro-ball lens and its array. PTFE thin film was spun onto a silicon wafer and dried in oven. Photoresist AZ4620 was used to pattern micro-columns with different diameters 60, 70 and 80 $μ$m. A thermal reflow process then was applied to melt these micro-column patterns resulted in micro-ball lens array. The achieved micro-ball lens array with diameter 98 $μ$m was fabricated using 80 $μ$m in diameter patterns. This method provides a simple fabrication process and low material cost.