OpenRaiser/Intern-Atlas huggingface dataset:
Optimal Time-Convex Hull under the Lp Metrics
Venue: arXiv cs.CG 2013
Year: 2013

We consider the problem of computing the time-convex hull of a point set under the general $L_p$ metric in the presence of a straight-line highway in the plane. The traveling speed along the highway is assumed to be faster than that off the highway, and the shortest time-path between a distant pair may involve traveling along the highway. The time-convex hull ${TCH}(P)$ of a point set $P$ is the smallest set containing both $P$ and \emph{all} shortest time-paths between any two points in ${TCH}(P)$. In this paper we give an algorithm that computes the time-convex hull under the $L_p$ metric in optimal $O(n\log n)$ time for a given set of $n$ points and a real number $p$ with $1\le p \le \infty$.
Verification of Building Blocks for Asynchronous Circuits
Venue: arXiv cs.LO 2013
Year: 2013

Scalable formal verification constitutes an important challenge for the design of asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an emergent property that has to be verified monolithically. We present our approach to using ACL2 to verify necessary and sufficient conditions over asynchronous delay-insensitive primitives. These conditions are used to derive SAT/SMT instances from circuits built out of these primitives. These SAT/SMT instances help in establishing absence of deadlocks. Our verification effort consists of building an executable checker in the ACL2 logic tailored for our purpose. We prove that this checker is correct. This approach enables us to prove ACL2 theorems involving defun-sk constructs and free variables fully automatically.
An Improvised Algorithm to Identify The Beauty of A Planar Curve
Venue: arXiv cs.GR 2013
Year: 2013

An improvised algorithm is proposed based on the work of Yoshimoto and Harada. The improvised algorithm results a graph which is called LDGC or Logarithmic Distribution Graph of Curvature. This graph has the capability to identify the beauty of monotonic planar curves with less effort as compared to LDDC by Yoshimoto and Harada.
A Syntactic-Semantic Approach to Incremental Verification
Venue: arXiv cs.SE 2013
Year: 2013

Software verification of evolving systems is challenging mainstream methodologies and tools. Formal verification techniques often conflict with the time constraints imposed by change management practices for evolving systems. Since changes in these systems are often local to restricted parts, an incremental verification approach could be beneficial. This paper introduces SiDECAR, a general framework for the definition of verification procedures, which are made incremental by the framework itself. Verification procedures are driven by the syntactic structure (defined by a grammar) of the system and encoded as semantic attributes associated with the grammar. Incrementality is achieved by coupling the evaluation of semantic attributes with an incremental parsing technique. We show the application of SiDECAR to the definition of two verification procedures: probabilistic verification of reliability requirements and verification of safety properties.
On Discrete Preferences and Coordination
Venue: arXiv cs.GT 2013
Year: 2013

An active line of research has considered games played on networks in which payoffs depend on both a player's individual decision and also the decisions of her neighbors. Such games have been used to model issues including the formation of opinions and the adoption of technology. A basic question that has remained largely open in this area is to consider games where the strategies available to the players come from a fixed, discrete set, and where players may have different intrinsic preferences among the possible strategies. It is natural to model the tension among these different preferences by positing a distance function on the strategy set that determines a notion of "similarity" among strategies; a player's payoff is determined by the distance from her chosen strategy to her preferred strategy and to the strategies chosen by her network neighbors. Even when there are only two strategies available, this framework already leads to natural open questions about a version of the classical Battle of the Sexes problem played on a graph. We develop a set of techniques for analyzing this class of games, which we refer to as discrete preference games. We parametrize the games by the relative extent to which a player takes into account the effect of her preferred strategy and the effect of her neighbors' strategies, allowing us to interpolate between network coordination games and unilateral decision-making. When these two effects are balanced, we show that the price of stability is equal to 1 for any discrete preference game in which the distance function on the strategies is a tree metric; as a special case, this includes the Battle of the Sexes on a graph. We also show that trees form the maximal family of metrics for which the price of stability is 1, and produce a collection of metrics on which the price of stability converges to a tight bound of 2.
Optimal Ternary Cyclic Codes from Monomials
Venue: arXiv cs.IT 2013
Year: 2013

Cyclic codes are a subclass of linear codes and have applications in consumer electronics, data storage systems, and communication systems as they have efficient encoding and decoding algorithms. Perfect nonlinear monomials were employed to construct optimal ternary cyclic codes with parameters $[3^m-1, 3^m-1-2m, 4]$ by Carlet, Ding and Yuan in 2005. In this paper, almost perfect nonlinear monomials, and a number of other monomials over $\gf(3^m)$ are used to construct optimal ternary cyclic codes with the same parameters. Nine open problems on such codes are also presented.
Ordering Metro Lines by Block Crossings
Venue: arXiv cs.DS 2013
Year: 2013

A problem that arises in drawings of transportation networks is to minimize the number of crossings between different transportation lines. While this can be done efficiently under specific constraints, not all solutions are visually equivalent. We suggest merging crossings into block crossings, that is, crossings of two neighboring groups of consecutive lines. Unfortunately, minimizing the total number of block crossings is NP-hard even for very simple graphs. We give approximation algorithms for special classes of graphs and an asymptotically worst-case optimal algorithm for block crossings on general graphs. That is, we bound the number of block crossings that our algorithm needs and construct worst-case instances on which the number of block crossings that is necessary in any solution is asymptotically the same as our bound.
Combinatorial Pair Testing: Distinguishing Workers from Slackers
Venue: arXiv cs.DS 2013
Year: 2013

We formalize a problem we call combinatorial pair testing (CPT), which has applications to the identification of uncooperative or unproductive participants in pair programming, massively distributed computing, and crowdsourcing environments. We give efficient adaptive and nonadaptive CPT algorithms and we show that our methods use an optimal number of testing rounds to within constant factors. We also provide an empirical evaluation of some of our methods.
Translating cities: the use of digital technologies in urban environments
Venue: arXiv cs.CY 2013
Year: 2013

Computer models and information systems have been used for urban planning and design since the 1950s. Their capacity for analysis and problem-solving has increased substantially since then with hardware and software being able to manage large amounts of data. The beginning of the 2000s brought better technologies for data visualisation and intuitive software products and nowadays they are being used to design and manipulate highly complex urban systems. However, ontological and epistemological questions remain about the nature of urban environments. What do we know about cities - and what is a city exactly? What theoretical models can be applied to the study of cities? How do we translate a city into data? What type of information really matters and what do we want to communicate with them? What are the implications of computer modelling for urban planning and design? This paper reviews how digital technologies have been used to shape our understanding of cities and how they impact the design and planning of cities. The point of depart is a scrutiny of the emergence of modern planning in the nineteenth century when cities became a scientific subject. A range of theories and concepts of the urban form and urban growth developed during the twentieth century will be presented and then linked to the first investigations involving the use of the computer for modelling and planning. The paper concludes with some discussions around the interaction of computing and urban theories.
Topological Properties of Web Services Similarity Networks
Venue: arXiv cs.IR 2013
Year: 2013

The number of publicly available Web services (WS) is continuously growing. To perform efficient WS discovery, it is desirable to organize the WS space. Works in this direction propose to group WS according to certain shared properties. Such groups commonly called communities are based either on similarity or on interaction between WS. In this paper we focus on the former, and propose a new network-based approach to extract communities from a WS collection. This process is three-stepped: first we define several similarity functions able to compare WS operations, second we use them to build so-called similarity networks, and third we identify communities under the form of specific structures in these networks. We apply our method on a collection of real-world WS and comment the resulting communities. Finally, we additionally provide an analysis and an interpretation of our similarity networks with a complex networks perspective.
Finitely generated ideal languages and synchronizing automata
Venue: arXiv cs.FL 2013
Year: 2013

We study representations of ideal languages by means of strongly connected synchronizing automata. For every finitely generated ideal language L we construct such an automaton with at most 2^n states, where n is the maximal length of words in L. Our constructions are based on the De Bruijn graph.
Advanced Caching for Distributing Sensor Data through Programmable Nodes
Venue: arXiv cs.NI 2013
Year: 2013

This paper shows an innovative solution for distributing dynamic sensor data by using distributed caches. Our proposal is based on the concepts of service modularization and virtualization of network nodes made available by the NetServ hosting environment, which has been defined and implemented with the aim of extending the functions of the network nodes. Through a lab experiment involving tens of nodes, we have demonstrated a significant performance improvements in term of traffic saving and download time in comparison with a legacy, Internet-based, approach. Beyond this performance improvements, the proposed solution holds also functional improvements, in terms of dynamic deployment and easy integration with services making use of sensor data.
Does Criticisms Overcome the Praises of Journal Impact Factor?
Venue: arXiv cs.DL 2013
Year: 2013

Journal impact factor (IF) as a gauge of influence and impact of a particular journal comparing with other journals in the same area of research, reports the mean number of citations to the published articles in particular journal. Although, IF attracts more attention and being used more frequently than other measures, it has been subjected to criticisms, which overcome the advantages of IF. Critically, extensive use of IF may result in destroying editorial and researchers behaviour, which could compromise the quality of scientific articles. Therefore, it is the time of the timeliness and importance of a new invention of journal ranking techniques beyond the journal impact factor.
Community Structure in Interaction Web Service Networks
Venue: arXiv cs.SI 2013
Year: 2013

Many real-world complex systems such as social, biological, information as well as technological systems results of a decentralized and unplanned evolution which leads to a common structuration. Irrespective of their origin, these so-called complex networks typically exhibit small-world and scale-free properties. Another common feature is their organisation into communities. In this paper, we introduce models of interaction networks based on the composition process of syntactic and semantic Web services. An extensive experimental study conducted on a benchmark of real Web services shows that these networks possess the typical properties of complex networks (small-world, scale-free). Unlike most social networks, they are not transitive. Using a representative sample of community detection algorithms, a community structuration is revealed. The comparative evaluation of the discovered community structures shows that they are very similar in terms of content. Furthermore, the analysis performed on the community structures and on the communities themselves, leads us to conclude that their topological properties are consistent.
Fixed-Parameter and Approximation Algorithms for Maximum Agreement Forests of Multifurcating Trees
Venue: arXiv cs.DS 2013
Year: 2013

We present efficient algorithms for computing a maximum agreement forest (MAF) of a pair of multifurcating (nonbinary) rooted trees. Our algorithms match the running times of the currently best algorithms for the binary case. The size of an MAF corresponds to the subtree prune-and-regraft (SPR) distance of the two trees and is intimately connected to their hybridization number. These distance measures are essential tools for understanding reticulate evolution, such as lateral gene transfer, recombination, and hybridization. Multifurcating trees arise naturally as a result of statistical uncertainty in current tree construction methods.
A Companion of "Relating Strong Behavioral Equivalences for Processes with Nondeterminism and Probabilities"
Venue: arXiv cs.LO 2013
Year: 2013

In the paper "Relating Strong Behavioral Equivalences for Processes with Nondeterminism and Probabilities" to appear in TCS, we present a comparison of behavioral equivalences for nondeterministic and probabilistic processes. In particular, we consider strong trace, failure, testing, and bisimulation equivalences. For each of these groups of equivalences, we examine the discriminating power of three variants stemming from three approaches that differ for the way probabilities of events are compared when nondeterministic choices are resolved via deterministic schedulers. The established relationships are summarized in a so-called spectrum. However, the equivalences we consider in that paper are only a small subset of those considered in the original spectrum of equivalences for nondeterministic systems introduced by Rob van Glabbeek. In this companion paper we we enlarge the spectrum by considering variants of trace equivalences (completed-trace equivalences), additional decorated-trace equivalences (failure-trace, readiness, and ready-trace equivalences), and variants of bisimulation equivalences (kernels of simulation, completed-simulation, failure-simulation, and ready-simulation preorders). Moreover, we study how the spectrum changes when randomized schedulers are used instead of deterministic ones.
Design and Stability of Load-Side Primary Frequency Control in Power Systems
Venue: arXiv cs.SY 2013
Year: 2013

We present a systematic method to design ubiquitous continuous fast-acting distributed load control for primary frequency regulation in power networks, by formulating an optimal load control (OLC) problem where the objective is to minimize the aggregate cost of tracking an operating point subject to power balance over the network. We prove that the swing dynamics and the branch power flows, coupled with frequency-based load control, serve as a distributed primal-dual algorithm to solve OLC. We establish the global asymptotic stability of a multimachine network under such type of load-side primary frequency control. These results imply that the local frequency deviations at each bus convey exactly the right information about the global power imbalance for the loads to make individual decisions that turn out to be globally optimal. Simulations confirm that the proposed algorithm can rebalance power and resynchronize bus frequencies after a disturbance with significantly improved transient performance.
Prior-Independent Mechanisms for Scheduling
Venue: arXiv cs.GT 2013
Year: 2013

We study the makespan minimization problem with unrelated selfish machines under the assumption that job sizes are stochastic. We design simple truthful mechanisms that under various distributional assumptions provide constant and sublogarithmic approximations to expected makespan. Our mechanisms are prior-independent in that they do not rely on knowledge of the job size distributions. Prior-independent approximation mechanisms have been previously studied for the objective of revenue maximization [Dhangwatnotai, Roughgarden and Yan'10, Devanur, Hartline, Karlin and Nguyen'11, Roughgarden, Talgam-Cohen and Yan'12]. In contrast to our results, in prior-free settings no truthful anonymous deterministic mechanism for the makespan objective can provide a sublinear approximation [Ashlagi, Dobzinski and Lavi'09].
Resource Allocation for Downlink Channel Transmission Based on Superposition Coding
Venue: arXiv cs.IT 2013
Year: 2013

We analyze the problem of transmitting information to multiple users over a shared wireless channel. The problem of resource allocation (RA) for the users with the knowledge of their channel state information has been treated extensively in the literature where various approaches trading off the users' throughput and fairness were proposed. The emphasis was mostly on the time-sharing (TS) approach, where the resource allocated to the user is equivalent to its time share of the channel access. In this work, we propose to take advantage of the broadcast nature of the channel and we adopt superposition coding (SC)-known to outperform TS in multiple users broadcasting scenarios. In SC, users' messages are simultaneously transmitted by superposing their codewords with different power fractions under a total power constraint. The main challenge is to find a simple way to allocate these power fractions to all users taking into account the fairness/throughput tradeoff. We present an algorithm with this purpose and we apply it in the case of popular proportional fairness (PF). The obtained results using SC are illustrated with various numerical examples where, comparing to TS, a rate increase between 20% and 300% is observed.
Minimum Common String Partition Parameterized by Partition Size is Fixed-Parameter Tractable
Venue: arXiv cs.DS 2013
Year: 2013

The NP-hard Minimum Common String Partition problem asks whether two strings $x$ and $y$ can each be partitioned into at most $k$ substrings, called blocks, such that both partitions use exactly the same blocks in a different order. We present the first fixed-parameter algorithm for Minimum Common String Partition using only parameter $k$.
Practical Implementation of Spatial Modulation
Venue: arXiv cs.IT 2013
Year: 2013

In this work we seek to characterise the performance of spatial modulation (SM) and spatial multiplexing (SMX) with an experimental test bed. Two National Instruments (NI)-PXIe devices are used for the system testing, one for the transmitter and one for the receiver. The digital signal processing that formats the information data in preparation of transmission is described along with the digital signal processing that recovers the information data. In addition, the hardware limitations of the system are also analysed. The average bit error ratio (ABER) of the system is validated through both theoretical analysis and simulation results for SM and SMX under line of sight (LoS) channel conditions.
Optimal Productivity of Succoring Patients System using Mobile GIS Based on WCF Technology
Venue: arXiv cs.CY 2013
Year: 2013

Depending on references of the World Health Organization there is large numbers of sick persons with different diseases worldwide, and without succor at a suitable time this could lead to fatality of the patients. This paper offers a succoring system controlled by the patient based on the location of patients. The proposed system is the first tracking system using mobile GIS based on WCF technology to offer online succoring (24 hour a day), but really works only when the patient sends request for succoring. The patients will send a request (SMS by click one button) contains his ID, Longitude and Latitude via GPRS network to a web server containing a database, which the patient was registered previously on it. Then the server will locate the patient on Google map and retrieve the patient's information from the database. This information will be used by the server to send succoring facility and notify the nearest and most suitable ESC; moreover, the server will send SMS over IP to inform the patient emergency contacts and emergency hospital. The optimal productivity for proposed succoring system appears in handling a large number of requests within short period at rate of one request/need succoring per sec as result of using mobile GIS based on WCF technology. Furthermore, the process of request and reply for emergency cases of the patients achieved in costeffective way due to this technology, which allow sending data (SMS over IP) via Internet using GPRS network. The proposed system can be implemented in a minimum configuration (hardware and software) to minimize the overall cost of operation and manufacturing. Keywords- WCF; WPF; Build-in GPS; GPRS; Mobile GIS; SoIP; Tracking System; Google Maps API.
Quantifying the Impact of Parameter Tuning on Nature-Inspired Algorithms
Venue: arXiv cs.NE 2013
Year: 2013

The problem of parameterization is often central to the effective deployment of nature-inspired algorithms. However, finding the optimal set of parameter values for a combination of problem instance and solution method is highly challenging, and few concrete guidelines exist on how and when such tuning may be performed. Previous work tends to either focus on a specific algorithm or use benchmark problems, and both of these restrictions limit the applicability of any findings. Here, we examine a number of different algorithms, and study them in a "problem agnostic" fashion (i.e., one that is not tied to specific instances) by considering their performance on fitness landscapes with varying characteristics. Using this approach, we make a number of observations on which algorithms may (or may not) benefit from tuning, and in which specific circumstances.
Knowledge and Security
Venue: arXiv cs.CR 2013
Year: 2013

Epistemic concepts, and in some cases epistemic logic, have been used in security research to formalize security properties of systems. This survey illustrates some of these uses by focusing on confidentiality in the context of cryptographic protocols, and in the context of multi-level security systems.