OpenRaiser/Intern-Atlas huggingface dataset:
On the security of the Yen-Guo's domino signal encryption algorithm (DSEA)
Venue: arXiv cs.CR 2006
Year: 2006

Recently, a new domino signal encryption algorithm (DSEA) was proposed for digital signal transmission, especially for digital images and videos. This paper analyzes the security of DSEA, and points out the following weaknesses: 1) its security against the brute-force attack was overestimated; 2) it is not sufficiently secure against ciphertext-only attacks, and only one ciphertext is enough to get some information about the plaintext and to break the value of a sub-key; 3) it is insecure against known/chosen-plaintext attacks, in the sense that the secret key can be recovered from a number of continuous bytes of only one known/chosen plaintext and the corresponding ciphertext. Experimental results are given to show the performance of the proposed attacks, and some countermeasures are discussed to improve DSEA.
The succinctness of first-order logic on linear orders
Venue: arXiv cs.LO 2006
Year: 2006

Succinctness is a natural measure for comparing the strength of different logics. Intuitively, a logic L_1 is more succinct than another logic L_2 if all properties that can be expressed in L_2 can be expressed in L_1 by formulas of (approximately) the same size, but some properties can be expressed in L_1 by (significantly) smaller formulas. We study the succinctness of logics on linear orders. Our first theorem is concerned with the finite variable fragments of first-order logic. We prove that: (i) Up to a polynomial factor, the 2- and the 3-variable fragments of first-order logic on linear orders have the same succinctness. (ii) The 4-variable fragment is exponentially more succinct than the 3-variable fragment. Our second main result compares the succinctness of first-order logic on linear orders with that of monadic second-order logic. We prove that the fragment of monadic second-order logic that has the same expressiveness as first-order logic on linear orders is non-elementarily more succinct than first-order logic.
Essential Incompleteness of Arithmetic Verified by Coq
Venue: arXiv cs.LO 2006
Year: 2006

A constructive proof of the Goedel-Rosser incompleteness theorem has been completed using the Coq proof assistant. Some theory of classical first-order logic over an arbitrary language is formalized. A development of primitive recursive functions is given, and all primitive recursive functions are proved to be representable in a weak axiom system. Formulas and proofs are encoded as natural numbers, and functions operating on these codes are proved to be primitive recursive. The weak axiom system is proved to be essentially incomplete. In particular, Peano arithmetic is proved to be consistent in Coq's type theory and therefore is incomplete.
Iterative Soft Input Soft Output Decoding of Reed-Solomon Codes by Adapting the Parity Check Matrix
Venue: arXiv cs.IT 2006
Year: 2006

An iterative algorithm is presented for soft-input-soft-output (SISO) decoding of Reed-Solomon (RS) codes. The proposed iterative algorithm uses the sum product algorithm (SPA) in conjunction with a binary parity check matrix of the RS code. The novelty is in reducing a submatrix of the binary parity check matrix that corresponds to less reliable bits to a sparse nature before the SPA is applied at each iteration. The proposed algorithm can be geometrically interpreted as a two-stage gradient descent with an adaptive potential function. This adaptive procedure is crucial to the convergence behavior of the gradient descent algorithm and, therefore, significantly improves the performance. Simulation results show that the proposed decoding algorithm and its variations provide significant gain over hard decision decoding (HDD) and compare favorably with other popular soft decision decoding methods.
Primal-dual distance bounds of linear codes with application to cryptography
Venue: arXiv cs.IT 2006
Year: 2006

Let $N(d,d^\perp)$ denote the minimum length $n$ of a linear code $C$ with $d$ and $d^{\bot}$, where $d$ is the minimum Hamming distance of $C$ and $d^{\bot}$ is the minimum Hamming distance of $C^{\bot}$. In this paper, we show a lower bound and an upper bound on $N(d,d^\perp)$. Further, for small values of $d$ and $d^\perp$, we determine $N(d,d^\perp)$ and give a generator matrix of the optimum linear code. This problem is directly related to the design method of cryptographic Boolean functions suggested by Kurosawa et al.
Proof rules for purely quantum programs
Venue: arXiv cs.PL 2006
Year: 2006

We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a purely quantum language fragment which describes the quantum part of a future quantum computer in Knill's architecture. The denotational semantics, weakest precondition semantics, and weakest liberal precondition semantics of this language fragment are introduced. To help reasoning about quantum programs involving quantum loops, we extend proof rules for classical probabilistic programs to our purely quantum programs.
Source Coding for Quasiarithmetic Penalties
Venue: arXiv cs.IT 2006
Year: 2006

Huffman coding finds a prefix code that minimizes mean codeword length for a given probability distribution over a finite number of items. Campbell generalized the Huffman problem to a family of problems in which the goal is to minimize not mean codeword length but rather a generalized mean known as a quasiarithmetic or quasilinear mean. Such generalized means have a number of diverse applications, including applications in queueing. Several quasiarithmetic-mean problems have novel simple redundancy bounds in terms of a generalized entropy. A related property involves the existence of optimal codes: For ``well-behaved'' cost functions, optimal codes always exist for (possibly infinite-alphabet) sources having finite generalized entropy. Solving finite instances of such problems is done by generalizing an algorithm for finding length-limited binary codes to a new algorithm for finding optimal binary codes for any quasiarithmetic mean with a convex cost function. This algorithm can be performed using quadratic time and linear space, and can be extended to other penalty functions, some of which are solvable with similar space and time complexity, and others of which are solvable with slightly greater complexity. This reduces the computational complexity of a problem involving minimum delay in a queue, allows combinations of previously considered problems to be optimized, and greatly expands the space of problems solvable in quadratic time and linear space. The algorithm can be extended for purposes such as breaking ties among possibly different optimal codes, as with bottom-merge Huffman coding.
Belief Propagation Based Multi--User Detection
Venue: arXiv cs.IT 2006
Year: 2006

We apply belief propagation (BP) to multi--user detection in a spread spectrum system, under the assumption of Gaussian symbols. We prove that BP is both convergent and allows to estimate the correct conditional expectation of the input symbols. It is therefore an optimal --minimum mean square error-- detection algorithm. This suggests the possibility of designing BP detection algorithms for more general systems. As a byproduct we rederive the Tse-Hanly formula for minimum mean square error without any recourse to random matrix theory.
The monadic second-order logic of graphs XVI : Canonical graph<br> decompositions
Venue: arXiv cs.LO 2006
Year: 2006

This article establishes that the split decomposition of graphs introduced by Cunnigham, is definable in Monadic Second-Order Logic.This result is actually an instance of a more general result covering canonical graph decompositions like the modular decomposition and the Tutte decomposition of 2-connected graphs into 3-connected components. As an application, we prove that the set of graphs having the same cycle matroid as a given 2-connected graph can be defined from this graph by Monadic Second-Order formulas.
Evidence with Uncertain Likelihoods
Venue: arXiv cs.AI 2006
Year: 2006

An agent often has a number of hypotheses, and must choose among them based on observations, or outcomes of experiments. Each of these observations can be viewed as providing evidence for or against various hypotheses. All the attempts to formalize this intuition up to now have assumed that associated with each hypothesis h there is a likelihood function μ_h, which is a probability measure that intuitively describes how likely each observation is, conditional on h being the correct hypothesis. We consider an extension of this framework where there is uncertainty as to which of a number of likelihood functions is appropriate, and discuss how one formal approach to defining evidence, which views evidence as a function from priors to posteriors, can be generalized to accommodate this uncertainty.
Integration of Declarative and Constraint Programming
Venue: arXiv cs.PL 2006
Year: 2006

Combining a set of existing constraint solvers into an integrated system of cooperating solvers is a useful and economic principle to solve hybrid constraint problems. In this paper we show that this approach can also be used to integrate different language paradigms into a unified framework. Furthermore, we study the syntactic, semantic and operational impacts of this idea for the amalgamation of declarative and constraint programming.
Carbon Copying Onto Dirty Paper
Venue: arXiv cs.IT 2006
Year: 2006

A generalization of the problem of writing on dirty paper is considered in which one transmitter sends a common message to multiple receivers. Each receiver experiences on its link an additive interference (in addition to the additive noise), which is known noncausally to the transmitter but not to any of the receivers. Applications range from wireless multi-antenna multicasting to robust dirty paper coding. We develop results for memoryless channels in Gaussian and binary special cases. In most cases, we observe that the availability of side information at the transmitter increases capacity relative to systems without such side information, and that the lack of side information at the receivers decreases capacity relative to systems with such side information. For the noiseless binary case, we establish the capacity when there are two receivers. When there are many receivers, we show that the transmitter side information provides a vanishingly small benefit. When the interference is large and independent across the users, we show that time sharing is optimal. For the Gaussian case we present a coding scheme and establish its optimality in the high signal-to-interference-plus-noise limit when there are two receivers. When the interference is large and independent across users we show that time-sharing is again optimal. Connections to the problem of robust dirty paper coding are also discussed.
Chinese Internet AS-level Topology
Venue: arXiv cs.NI 2006
Year: 2006

We present the first complete measurement of the Chinese Internet topology at the autonomous systems (AS) level based on traceroute data probed from servers of major ISPs in mainland China. We show that both the Chinese Internet AS graph and the global Internet AS graph can be accurately reproduced by the Positive-Feedback Preference (PFP) model with the same parameters. This result suggests that the Chinese Internet preserves well the topological characteristics of the global Internet. This is the first demonstration of the Internet's topological fractality, or self-similarity, performed at the level of topology evolution modeling.
Extending the theory of Owicki and Gries with a logic of progress
Venue: arXiv cs.LO 2006
Year: 2006

This paper describes a logic of progress for concurrent programs. The logic is based on that of UNITY, molded to fit a sequential programming model. Integration of the two is achieved by using auxiliary variables in a systematic way that incorporates program counters into the program text. The rules for progress in UNITY are then modified to suit this new system. This modification is however subtle enough to allow the theory of Owicki and Gries to be used without change.
The logic of interactive Turing reduction
Venue: arXiv cs.LO 2006
Year: 2006

The paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic reduction. This concept -- more precisely, the associated concept of reducibility -- is a generalization of Turing reducibility from the traditional, input/output sorts of problems to computational tasks of arbitrary degrees of interactivity. See http://www.cis.upenn.edu/~giorgi/cl.html for a comprehensive online source on computability logic.
The Evolution of Cyberinsurance
Venue: arXiv cs.CR 2006
Year: 2006

Cyberinsurance is a powerful tool to align market incentives toward improving Internet security. We trace the evolution of cyberinsurance from traditional insurance policies to early cyber-risk insurance policies to current comprehensive cyberinsurance products. We find that increasing Internet security risk in combination with the need for compliance with recent corporate legislation has contributed significantly to the demand for cyberinsurance. Cyberinsurance policies have become more comprehensive as insurers better understand the risk landscape and specific business needs. More specifically, cyberinsurers are addressing what used to be considered insurmountable problems (e.g., adverse selection/asymmetric information, moral hazard, etc.) that could lead to a failure of this market solution. Although some implementation issues remain, we suggest the future development of cyberinsurance will resolve these issues as evidenced by insurance solutions in other risk domains.
Constraint-based automatic verification of abstract models of multithreaded programs
Venue: arXiv cs.LO 2006
Year: 2006

We present a technique for the automated verification of abstract models of multithreaded programs providing fresh name generation, name mobility, and unbounded control. As high level specification language we adopt here an extension of communication finite-state machines with local variables ranging over an infinite name domain, called TDL programs. Communication machines have been proved very effective for representing communication protocols as well as for representing abstractions of multithreaded software. The verification method that we propose is based on the encoding of TDL programs into a low level language based on multiset rewriting and constraints that can be viewed as an extension of Petri Nets. By means of this encoding, the symbolic verification procedure developed for the low level language in our previous work can now be applied to TDL programs. Furthermore, the encoding allows us to isolate a decidable class of verification problems for TDL programs that still provide fresh name generation, name mobility, and unbounded control. Our syntactic restrictions are in fact defined on the internal structure of threads: In order to obtain a complete and terminating method, threads are only allowed to have at most one local variable (ranging over an infinite domain of names).
LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)
Venue: arXiv cs.AI 2006
Year: 2006

This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and highly interactive setting for discussions around the following four topics. Implementation and development of proof assistants based on any notion of impredicativity, automated theorem proving tools for higher-order logic reasoning systems, logical framework technology for the representation of proofs in higher-order logic, formal digital libraries for storing, maintaining and querying databases of proofs. We envision attendees that are interested in fostering the development and visibility of reasoning systems for higher-order logics. We are particularly interested in a discusssion on the development of a higher-order version of the TPTP and in comparisons of the practical strengths of automated higher-order reasoning systems. Additionally, the workshop includes system demonstrations. ESHOL is the successor of the ESCAR and ESFOR workshops held at CADE 2005 and IJCAR 2004.
Wavefront Propagation and Fuzzy Based Autonomous Navigation
Venue: arXiv cs.RO 2006
Year: 2006

Path planning and obstacle avoidance are the two major issues in any navigation system. Wavefront propagation algorithm, as a good path planner, can be used to determine an optimal path. Obstacle avoidance can be achieved using possibility theory. Combining these two functions enable a robot to autonomously navigate to its destination. This paper presents the approach and results in implementing an autonomous navigation system for an indoor mobile robot. The system developed is based on a laser sensor used to retrieve data to update a two dimensional world model of therobot environment. Waypoints in the path are incorporated into the obstacle avoidance. Features such as ageing of objects and smooth motion planning are implemented to enhance efficiency and also to cater for dynamic environments.
A Hybrid Three Layer Architecture for Fire Agent Management in Rescue Simulation Environment
Venue: arXiv cs.RO 2006
Year: 2006

This paper presents a new architecture called FAIS for imple- menting intelligent agents cooperating in a special Multi Agent environ- ment, namely the RoboCup Rescue Simulation System. This is a layered architecture which is customized for solving fire extinguishing problem. Structural decision making algorithms are combined with heuristic ones in this model, so it's a hybrid architecture.
Dynamic Balance Control of Multi-arm Free-Floating Space Robots
Venue: arXiv cs.RO 2006
Year: 2006

This paper investigates the problem of the dynamic balance control of multi-arm free-floating space robot during capturing an active object in close proximity. The position and orientation of space base will be affected during the operation of space manipulator because of the dynamics coupling between the manipulator and space base. This dynamics coupling is unique characteristics of space robot system. Such a disturbance will produce a serious impact between the manipulator hand and the object. To ensure reliable and precise operation, we propose to develop a space robot system consisting of two arms, with one arm (mission arm) for accomplishing the capture mission, and the other one (balance arm) compensating for the disturbance of the base. We present the coordinated control concept for balance of the attitude of the base using the balance arm. The mission arm can move along the given trajectory to approach and capture the target with no considering the disturbance from the coupling of the base. We establish a relationship between the motion of two arm that can realize the zeros reaction to the base. The simulation studies verified the validity and efficiency of the proposed control method.
Robust Motion Control for Mobile Manipulator Using Resolved Acceleration and Proportional-Integral Active Force Control
Venue: arXiv cs.RO 2006
Year: 2006

A resolved acceleration control (RAC) and proportional-integral active force control (PIAFC) is proposed as an approach for the robust motion control of a mobile manipulator (MM) comprising a differentially driven wheeled mobile platform with a two-link planar arm mounted on top of the platform. The study emphasizes on the integrated kinematic and dynamic control strategy in which the RAC is used to manipulate the kinematic component while the PIAFC is implemented to compensate the dynamic effects including the bounded known/unknown disturbances and uncertainties. The effectivenss and robustness of the proposed scheme are investigated through a rigorous simulation study and later complemented with experimental results obtained through a number of experiments performed on a fully developed working prototype in a laboratory environment. A number of disturbances in the form of vibratory and impact forces are deliberately introduced into the system to evaluate the system performances. The investigation clearly demonstrates the extreme robustness feature of the proposed control scheme compared to other systems considered in the study.
Study of Self-Organization Model of Multiple Mobile Robot
Venue: arXiv cs.RO 2006
Year: 2006

A good organization model of multiple mobile robot should be able to improve the efficiency of the system, reduce the complication of robot interactions, and detract the difficulty of computation. From the sociology aspect of topology, structure and organization, this paper studies the multiple mobile robot organization formation and running mechanism in the dynamic, complicated and unknown environment. It presents and describes in detail a Hierarchical- Web Recursive Organization Model (HWROM) and forming algorithm. It defines the robot society leader; robotic team leader and individual robot as the same structure by the united framework and describes the organization model by the recursive structure. The model uses task-oriented and top-down method to dynamically build and maintain structures and organization. It uses market-based techniques to assign task, form teams and allocate resources in dynamic environment. The model holds several characteristics of self-organization, dynamic, conciseness, commonness and robustness.
On the Existence of Universally Decodable Matrices
Venue: arXiv cs.IT 2006
Year: 2006

Universally decodable matrices (UDMs) can be used for coding purposes when transmitting over slow fading channels. These matrices are parameterized by positive integers $L$ and $N$ and a prime power $q$. The main result of this paper is that the simple condition $L \leq q+1$ is both necessary and sufficient for $(L,N,q)$-UDMs to exist. The existence proof is constructive and yields a coding scheme that is equivalent to a class of codes that was proposed by Rosenbloom and Tsfasman. Our work resolves an open problem posed recently in the literature.
Fast Frequent Querying with Lazy Control Flow Compilation
Venue: arXiv cs.PL 2006
Year: 2006

Control flow compilation is a hybrid between classical WAM compilation and meta-call, limited to the compilation of non-recursive clause bodies. This approach is used successfully for the execution of dynamically generated queries in an inductive logic programming setting (ILP). Control flow compilation reduces compilation times up to an order of magnitude, without slowing down execution. A lazy variant of control flow compilation is also presented. By compiling code by need, it removes the overhead of compiling unreached code (a frequent phenomenon in practical ILP settings), and thus reduces the size of the compiled code. Both dynamic compilation approaches have been implemented and were combined with query packs, an efficient ILP execution mechanism. It turns out that locality of data and code is important for performance. The experiments reported in the paper show that lazy control flow compilation is superior in both artificial and real life settings.