Search

Abstract: Classically, geometric constraint solvers use graph-based methods to decompose systems of geometric constraints. These methods have intrinsic limitations, which the witness method overcomes; a witness is a solution of a variant of the system. This paper details the computation of a basis of the vector space of free infinitesimal motions of a typical witness, and explains how to use this basis to interrogate the witness for dependence detection. The paper shows that the witness method detects all kinds of dependences: structural dependences already detectable by graph-based methods, but also non-structural dependences, due to known or unknown geometric theorems, which are undetectable by graph-based methods. It also discusses how to decide about the rigidity of a witness and how to decompose it. [Copyright &y& Elsevier]

Abstract: Bisimulation equivalence is decidable in polynomial time for both sequential and commutative normed context-free processes, known as BPA and BPP, respectively. Despite apparent similarity between the two classes, different algorithmic techniques were used in each case. We provide one polynomial-time algorithm that works in a superclass of both normed BPA and BPP. It is derived in the setting of partially-commutative context-free processes, a new process class introduced in the paper. It subsumes both BPA and BPP and seems to be of independent interest. Expressibility issue of the new class, in comparison with the normed PA class, is also tackled in the paper. [Copyright &y& Elsevier]

Abstract: One of the particularities of information encoded as DNA strands is that a string u contains basically the same information as its Watson–Crick complement, denoted here as . Thus, any expression consisting of repetitions of u and can be considered in some sense periodic. In this paper, we give a generalization of Lyndon and Schützenberger’s classical result about equations of the form , to cases where both sides involve repetitions of words as well as their complements. Our main results show that, for such extended equations, if , then all three words involved can be expressed in terms of a common word t and its complement . Moreover, if , then is an optimal bound. These results are established based on a complete characterization of all possible overlaps between two expressions that involve only some word u and its complement , which is also obtained in this paper. [Copyright &y& Elsevier]

Abstract: This paper proposes a semiring formulation for reasoning about an agent’s changing beliefs: a dynamic epistemic semiring (DES). A DES is a modal semiring extended with epistemic-action operators. The paper concentrates on the revision operator by proposing an axiomatisation, developing a basic calculus and deriving the classical AGM revision axioms in the algebra. Iterated action is also considered. [Copyright &y& Elsevier]

Abstract: This paper considers the problem of performing tasks in asynchronous distributed settings. This problem, called Do-All, has been substantially studied in synchronous models, but there is a dearth of efficient algorithms for asynchronous message-passing processors. Do-All can be trivially solved without any communication by an algorithm where each processor performs all tasks. Assuming p processors and t tasks, this requires work Θ(p · t). Thus, it is important to develop subquadratic solutions (when p and t are comparable) by trading computation for communication. Following the observation that it is not possible to obtain subquadratic work when the message delay d is substantial, e.g., d =Θ(t), this work pursues a message-delay-sensitive approach. Here, the upper bounds on work and communication are given as functions of p, t, and d, the upper bound on message delays, however, algorithms have no knowledge of d and they cannot rely on the existence of an upper bound on d. This paper presents two families of asynchronous algorithms achieving, for the first time, subquadratic work as long as d = o (t). The first family uses as its basis a shared-memory algorithm without having to emulate atomic registers assumed by that algorithm. These deterministic algorithms have work O(tp ε + pd⌈t/d⌉ ε ) for any ε >0. The second family uses specific permutations of tasks, with certain combinatorial properties, to sequence the work of the processors. These randomized (deterministic) algorithms have expected (worst-case) work O(t log p + pd log(2+ t/d)). Another important contribution in this work is the first delay-sensitive lower bound for this problem that helps explain the behavior of our algorithms: any randomized (deterministic) algorithm has expected (worst-case) work of Ω(t + pd log d+1 t). [Copyright &y& Elsevier]

Information integration systems provide uniform interfaces to varieties of heterogeneous information sources. For query answering in such systems, the current generation of query answering algorithms in local-as-view (source-centric) information integration systems all produce what has been thought of as “the best obtainable” answer, given the circumstances that the source-centric approach introduces incomplete information into the virtual global relations. However, this “best obtainable” answer does not include all information that can be extracted from the sources because it does not allow partial information. Neither does the “best obtainable” answer allow for composition of queries, meaning that querying a result of a previous query will not be equivalentto the composition of the two queries. In this paper, we provide a foundation for information integration, based on the algebraic theory of incomplete information. Our framework allows us to define the semantics of partial facts and introduce the notion of the exact answer—that is the answer that includes partial facts. We show that querying under the exact answer semantics is compositional. We also present two methods for actually computing the exact answer. The first method is tableau-based, and it is a generalization of the “inverse-rules” approach. The second, much more efficient method, is a generalization of the rewriting approach, and it is based on partial containment mappings introduced in the paper. [Copyright &y& Elsevier]

This paper studies nested simulation and nested trace semantics over the language BCCSP, a basic formalism to express finite process behaviour. It is shown that none of these semantics affords finite (in)equational axiomatizations over BCCSP. In particular, for each of the nested semantics studied in this paper, the collection of sound, closed (in)equations over a singleton action set is not finitely based. [Copyright &y& Elsevier]

This paper introduces a novel (bi)simulation-based faster-than preorder which relates asynchronous processes, where the relative speeds of system components are indeterminate, with respect to their worst-case timing behavior. The study is conducted for a conservative extension of the process algebra CCS, called TACS, which permits the specification of upper time bounds on action occurrences. TACS complements work in plain process algebras which compares asynchronous processes with respect to their functional reactive behavior only, and in timed process algebras which focus on analyzing synchronous processes. The most unusual contribution is in showing that the proposed faster-than preorder coincides with several other preorders, two of which consider the absolute times at which actions occur in system runs. The paper also develops the semantic theory of TACS by studying congruence properties, equational laws, and abstractions from internal actions. Two examples, one dealing with mail delivery and one relating two implementations of a simple storage system, testify to the practical utility of the new theory. [Copyright &y& Elsevier]

The Dichotomy Conjecture for the Constraint Satisfaction Problem (CSP) was recently settled, independently by Zhuk and the author. The proofs of this conjecture are rather sophisticated and require deep understanding of the algebraic structure of CSPs. This paper is a precursor of the author's proof of the Dichotomy Conjecture, and represents its main ideas in a simpler and clearer form in a more restricted class of the CSP. There are two well-known types of algorithms for solving CSPs: local propagation and generating a basis of the solution space. For several years the focus of the CSP research has been on 'hybrid' algorithms that somehow combine the two approaches. In this paper we present a new method of such hybridization that allows us to solve certain CSPs that has been out of reach for a quite a while, and eventually leads to resolving the Dichotomy Conjecture. We apply this method to CSPs parametrized by a universal algebra, an approach that has been very popular in the last decade or so. Specifically, we consider a fairly restricted class of algebras we will call semilattice block Mal'tsev. An algebra A is semilattice block Mal'tsev if it has a binary operation f , a ternary operation m , and a congruence σ such that the quotient A σ with operation f is a semilattice, f is a projection on every block of σ , and every block of σ is a Mal'tsev algebra with Mal'tsev operation m. This means that the domain in such a CSP is partitioned into blocks such that if the problem is considered on the quotient set A σ , it can be solved by a simple constraint propagation algorithm. On the other hand, if the problem is restricted on individual σ -blocks, it can be solved by generating a basis of the solution space. We show that the two methods can be combined in a highly nontrivial way, and therefore the constraint satisfaction problem over a semilattice block Mal'tsev algebra is solvable in polynomial time. [ABSTRACT FROM AUTHOR]

Abstract: Algebraic independence is a fundamental notion in commutative algebra that generalizes independence of linear polynomials. Polynomials (over a field K) are called algebraically independent if there is no non-zero polynomial F such that . The transcendence degree, , is the maximal number r of algebraically independent polynomials in the set. In this paper we design blackbox and efficient linear maps φ that reduce the number of variables from n to r but maintain , assuming sparse and small r. We apply these fundamental maps to solve two cases of blackbox identity testing (assuming a large or zero characteristic): [1.] Given a polynomial-degree circuit C and sparse polynomials of transcendence degree r, we can test blackbox for zeroness in time. [2.] Define a circuit to be of the form , where are sparse n-variate polynomials of degree at most δ. For this class of depth-4 circuits we define a notion of rank. Assuming there is a rank bound R for minimal simple identities, we give a time blackbox identity test for circuits. This partially generalizes the state of the art of depth-3 to depth-4 circuits. The notion of transcendence degree works best with large or zero characteristic, but we also give versions of our results for arbitrary fields. [Copyright &y& Elsevier]

Abstract: Goldʼs original paper on inductive inference introduced a notion of an optimal learner. Intuitively, a learner identifies a class of objects optimally iff there is no other learner that: requires as little of each presentation of each object in the class in order to identify that object, and, for some presentation of some object in the class, requires less of that presentation in order to identify that object. Beick considered this notion in the context of function learning, and gave an intuitive characterization of an optimal function learner. Jantke and Beick subsequently characterized the classes of functions that are algorithmically, optimally identifiable. Herein, Goldʼs notion is considered in the context of language learning. It is shown that a characterization of optimal language learners analogous to Beickʼs does not hold. It is also shown that the classes of languages that are algorithmically, optimally identifiable cannot be characterized in a manner analogous to that of Jantke and Beick. Other interesting results concerning optimal language learning include the following. It is shown that strong non-U-shapedness, a property involved in Beickʼs characterization of optimal function learners, does not restrict algorithmic language learning power. It is also shown that, for an arbitrary optimal learner F of a class of languages , F optimally identifies a subclass of iff F is class-preserving with respect to . [Copyright &y& Elsevier]

Abstract: A classical measure of similarity between strings is the length of the longest common subsequence (LCS) between the two given strings. The search for efficient algorithms for finding the LCS has been going on for more than three decades. To date, all known algorithms may take quadratic time (shaved by logarithmic factors) to find large LCS. In this paper, the problem of approximating LCS is studied, while focusing on the hard inputs for this problem, namely, approximating LCS of near-linear size in strings over a relatively large alphabet (of size at least for some constant , where is the length of the string). We show that, any given string over a relatively large alphabet can be embedded into a locally non-repetitive string. This embedding has a negligible additive distortion for strings that are not too dissimilar in terms of the edit distance. We also show that LCS can be efficiently approximated in locally-non-repetitive strings. Our new method (the embedding together with the approximation algorithm) gives a strictly sub-quadratic time algorithm (i.e., of complexity for some constant ) which can find common subsequences of linear (and near linear) size that cannot be detected efficiently by the existing tools. [Copyright &y& Elsevier]

Abstract: Subsequential transducers combine (input) language recognition with transduction and thereby generalise classic deterministic automata as well as Mealy and Moore type state machines. These well known subclasses all have a natural coalgebraic characterisation, and the question arises whether their coalgebraic modelling can be extended to subsequential transducers and their underlying structures. In this paper, we show that although subsequential structures cannot generally be regarded as coalgebras, the subclass of normalised structures do form a subcategory of coalgebras. Moreover, normalised structures are reflective in the category of all subsequential structures, and a final normalised structure exists. The existence and properties of the minimal subsequential transducer can be derived from this result. We also show that for the class of subsequential structures in which all states are accepting, an alternative coalgebraic representation is obtained by taking differentials. This differential representation gives rise to a new method of deciding equivalence and computing minimal representations which does not involve normalisation. Both normalisation and taking differentials can be formalised as functors into reflective subcategories of coalgebras, and we can therefore see these constructions as coalgebraisation. [Copyright &y& Elsevier]

Abstract: The structure map turning a set into the carrier of a final coalgebra is not unique. This fact is well known, but commonly elided. In this paper, we argue that any such concrete representation of a set as a final coalgebra is potentially interesting on its own. We discuss several examples, in particular, we consider different coalgebra structures that turn the set of infinite streams into the carrier of a final coalgebra. After that we focus on coalgebra structures that are made up using so-called cooperations. We say that a collection of cooperations is complete for a given set X if it gives rise to a coalgebra structure that turns X into the carrier set of a subcoalgebra of a final coalgebra. Any complete set of cooperations yields a coalgebraic proof and definition principle. We exploit this fact and devise a general definition scheme for constants and functions on a set X that is parametrical in the choice of the complete set of cooperations for X. [Copyright &y& Elsevier]

Abstract: This paper studies several applications of the notion of a presentation of a functor by operations and equations. We show that the technically straightforward generalisation of this notion from the one-sorted to the many-sorted case has several interesting consequences. First, it can be applied to give equational logic for the binding algebras modelling abstract syntax. Second, it provides a categorical approach to algebraic semantics of first-order logic. Third, this notion links the uniform treatment of logics for coalgebras of an arbitrary type T with concrete syntax and proof systems. Analysing the many-sorted case is essential for modular completeness proofs of coalgebraic logics. [Copyright &y& Elsevier]

Abstract: Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to formal reasoning about well-behaved structural operational semantics (SOS). An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of syntax and system behaviour, thus treating various kinds of operational descriptions in a uniform fashion. In this paper, bialgebraic semantics is combined with a coalgebraic approach to modal logic in a novel, general approach to proving the compositionality of process equivalences for languages defined by structural operational semantics. To prove compositionality, one provides a notion of behaviour for logical formulas, and defines an SOS-like specification of modal operators which reflects the original SOS specification of the language. This approach can be used to define SOS congruence formats as well as to prove compositionality for specific languages and equivalences. [Copyright &y& Elsevier]

Branching Algebra is the natural branching-time generalization of Allen's Interval Algebra. As in the linear case, the consistency problem for Branching Algebra is NP-hard. Branching Algebra has many potential applications in different areas of Artificial Intelligence; therefore, being able to efficiently solve classical problems expressed in Branching Algebra is very important. This can be achieved in two steps: first, by identifying expressive enough, yet tractable fragments of the whole algebra, and, second, by using such fragments to boost the performances of a backtracking algorithm for the whole language. In this paper we study the properties of several such fragments, both from the algebraic and the computational point of view, and we give an almost complete picture of tractable and non-tractable fragments of the Branching Algebra. [ABSTRACT FROM AUTHOR]

Abstract: We study the problem of scheduling transmissions on the downlink of IEEE 802.16/WiMAX systems that use the OFDMA technology. These transmissions are scheduled using a matrix whose dimensions are frequency and time, where every matrix cell is a time slot on some carrier channel. The IEEE 802.16 standard mandates that: (i) every transmission occupies a rectangular set of cells, and (ii) transmissions must be scheduled according to a given order. We show that if the number of cells required by a transmission is not limited (up to the matrix size), the problem of maximizing matrix utilization is very hard to approximate. On the positive side we show that if the number of cells of every transmission is limited to some constant fraction of the matrix area, the problem can be approximated to within a constant factor. As far as we know this is the first paper that considers this sequential rectangle placement problem. [Copyright &y& Elsevier]

Abstract: A vertex ranking of an undirected graph G is a labeling of the vertices of G with integers such that every path connecting two vertices with the same label i contains an intermediate vertex with label . A vertex ranking of G is called optimal if it uses the minimum number of distinct labels among all possible vertex rankings. The problem of finding an optimal vertex ranking for general graphs is NP-hard, and NP-hard even for chordal graphs which form a superclass of block graphs. In this paper, we present the first polynomial algorithm which runs in time for finding an optimal vertex ranking of a block graph G, where n and denote the number of vertices and the maximum degree of G, respectively. [Copyright &y& Elsevier]

Abstract: The proceedings of FOCS’98 contain a paper by Zakariae Bouziane, who sketches a new representation of the Petri net reachability problem and claims to provide a new algorithm solving the problem. In this note, the essence of Bouziane’s approach is explained, and a serious flaw of the algorithm is exposed. [Copyright &y& Elsevier]

Abstract: This paper investigates both the precision and the model checking efficiency of abstract models designed to preserve branching time logics w.r.t. a 3-valued semantics. Current abstract models use ordinary transitions to over approximate the concrete transitions, while they use hyper transitions to under approximate the concrete transitions. In this work, we refer to precision measured w.r.t. the choice of abstract states, independently of the formalism used to describe abstract models. We show that current abstract models do not allow maximal precision. We suggest a new class of models and a construction of an abstract model which is most precise w.r.t. any choice of abstract states. As before, the construction of such models might involve an exponential blowup, which is inherent by the use of hyper transitions. We therefore suggest an efficient algorithm in which the abstract model is constructed during model checking, by need. Our algorithm achieves maximal precision w.r.t. the given property while remaining quadratic in the number of abstract states. To complete the picture, we incorporate it into an abstraction-refinement framework. [Copyright &y& Elsevier]

Abstract: A Siromoney matrix grammar is a simple device for the generation of rectangular pictures. In this paper we discuss Siromoney matrix grammars whose picture language are slender, i.e., they contain only a bounded number of pictures for each size. In particular, it is shown that the slenderness decision problem is decidable for Siromoney matrix grammars with context-free rules. Moreover, some closure and decidability questions for slender Siromoney matrix languages are discussed. [Copyright &y& Elsevier]

Abstract: Permutominoes are polyominoes defined by suitable pairs of permutations. In this paper we provide a formula to count the number of convex permutominoes of given perimeter. To this aim we define the transform of a generic pair of permutations, we characterize the transform of any pair defining a convex permutomino, and we solve the counting problem in the transformed space. [Copyright &y& Elsevier]

Abstract: This paper compares the expressiveness of different fragments of ambient calculi via leader election problems. We consider Mobile Ambients (MA), Safe Ambients (SA) and the Push and Pull Ambient Calculus (PAC). Cardelli and Gordon encoded the asynchronous π-calculus into MA. Zimmer has shown that the synchronous π-calculus without choice can be encoded in pure (no communication) SA. We show that pure MA without restriction has symmetric electoral systems, that is, it is possible to solve the problem of electing a leader in a symmetric network. By the work of Palamidessi, this implies that this fragment of MA is not encodable (under certain conditions) in the π-calculus with separate choice. Moreover, we use the same technique to show that fragments of SA and PAC are not encodable (under certain conditions) in the π-calculus with separate choice. We also show that particular fragments of ambient calculi do not admit a solution to leader election problems, in the same way as the π-calculus with separate choice. This yields a fine-grained hierarchy within ambient calculi. [Copyright &y& Elsevier]

Abstract: This paper investigates the word problem for inverse monoids generated by a set Γ subject to relations of the form e = f, where e and f are both idempotents in the free inverse monoid generated by Γ. It is shown that for every fixed monoid of this form the word problem can be solved both in linear time on a RAM as well as in deterministic logarithmic space, which solves an open problem of Margolis and Meakin. For the uniform word problem, where the presentation is part of the input, EXPTIME-completeness is shown. For the Cayley-graphs of these monoids, it is shown that the first-order theory with regular path predicates is decidable. Regular path predicates allow to state that there is a path from a node x to a node y that is labeled with a word from some regular language. As a corollary, the decidability of the generalized word problem is deduced. [Copyright &y& Elsevier]

Abstract: Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols are based on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the execution of a protocol. We are interested in the intruder deduction problem, that is vulnerability to passive attacks in presence of equational theories which model the protocol specification and properties of the cryptographic operators. In the present paper, we consider the case where the encryption distributes over the operator of an Abelian group or over an exclusive-or operator. We prove decidability of the intruder deduction problem in both cases. We obtain a PTIME decision procedure in a restricted case, the so-called binary case. These decision procedures are based on a careful analysis of the proof system modeling the deductive power of the intruder, taking into account the algebraic properties of the equational theories under consideration. The analysis of the deduction rules interacting with the equational theory relies on the manipulation of -modules in the general case, and on results from prefix rewriting in the binary case. [Copyright &y& Elsevier]

Abstract: Congruence closure algorithms for deduction in ground equational theories are ubiquitous in many (semi-)decision procedures used for verification and automated deduction. In many of these applications one needs an incremental algorithm that is moreover capable of recovering, among the thousands of input equations, the small subset that explains the equivalence of a given pair of terms. In this paper we present an algorithm satisfying all these requirements. First, building on ideas from abstract congruence closure algorithms, we present a very simple and clean incremental congruence closure algorithm and show that it runs in the best known time O(n log n). After that, we introduce a proof-producing union-find data structure that is then used for extending our congruence closure algorithm, without increasing the overall O(n log n) time, in order to produce a k-step explanation for a given equation in almost optimal time (quasi-linear in k). Finally, we show that the previous algorithms can be smoothly extended, while still obtaining the same asymptotic time bounds, in order to support the interpreted functions symbols successor and predecessor, which have been shown to be very useful in applications such as microprocessor verification. [Copyright &y& Elsevier]

Abstract: In this paper we present a solution to the long-standing problem of characterising the coarsest liveness-preserving pre-congruence with respect to a full (TCSP-inspired) process algebra. In fact, we present two distinct characterisations, which give rise to the same relation: an operational one based on a De Nicola–Hennessy-like testing modality which we call should-testing, and a denotational one based on a refined notion of failures. One of the distinguishing characteristics of the should-testing pre-congruence is that it abstracts from divergences in the same way as Milner’s observation congruence, and as a consequence is strictly coarser than observation congruence. In other words, should-testing has a built-in fairness assumption. This is in itself a property long sought-after; it is in notable contrast to the well-known must-testing of De Nicola and Hennessy (denotationally characterised by a combination of failures and divergences), which treats divergence as catastrophic and hence is incompatible with observation congruence. Due to these characteristics, should-testing supports modular reasoning and allows to use the proof techniques of observation congruence, but also supports additional laws and techniques. Moreover, we show decidability of should-testing (on the basis of the denotational characterisation). Finally, we demonstrate its advantages by the application to a number of examples, including a scheduling problem, a version of the Alternating Bit-protocol, and fair lossy communication channels. [Copyright &y& Elsevier]

Abstract: Term algebras can model recursive data structures which are widely used in programming languages. To verify programs we must be able to reason about these structures. However, as programming languages often involve multiple data domains, in program verification decision procedures for a single theory are usually not applicable. An important class of mixed constraints consists of combinations of data structures with integer constraints on the size of data structures. Such constraints can express memory safety properties such as absence of memory overflow and out-of-bound array access, which are crucial for program correctness. In this paper we extend the theory of term algebras with the length function which maps a term to its size, resulting in a combined theory of term algebras and Presburger arithmetic. This arithmetic extension provides a natural but tight coupling between the two theories, and hence the general purpose combination methods like Nelson-Oppen combination are not applicable. We present decision procedures for quantifier-free theories in structures with an infinite constant domain and with a finite constant domain. We also present a quantifier elimination procedure for the extended first-order theory that can remove a block of existential quantifiers in one step. [Copyright &y& Elsevier]

Abstract: Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T—also known as Satisfiability Modulo Theory, or SMT(T)—rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory T is the combination of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e.g. Nelson–Oppen, Shostak). In this paper we propose a new approach to SMT, where the enumerator of truth assignments is integrated with two decision procedures, one for T 1 and one for T 2, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i.e., cheaper reasoning first, and more often). We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions () and Linear Arithmetic (), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance. [Copyright &y& Elsevier]

Abstract: Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics—which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics. [Copyright &y& Elsevier]

Abstract: P. Shor proposed a polynomial time algorithm for prime factorization on quantum computers. For a given number N, he gave an algorithm for finding the order r of an element x in the multiplicative group (mod N). The method succeeds because factorization can be reduced to finding the order of an element using randomization. But the algorithm has two shortcomings, the order of the number must be even and the output might be a trivial factor. Actually, these drawbacks can be overcome in a particular case, i.e., N is an RSA modulus. In this paper, we propose a new quantum algorithm for factoring RSA modulus without the two drawbacks. Moreover, we show that the cost of the algorithm mainly depends on the calculation of ord N (2). [Copyright &y& Elsevier]

The subsequence character count problem has as its input an array S=S[1],…,S[n] of symbols over alphabet Σ and a natural number m. Its output is: for every i, i=1,…,n−m+1, the number of different alphabet symbols occurring in the subsequence S[i],S[i+1],…,S[i+m−1]. The subsequence character count problem is a natural problem that has many uses. It can be solved in linear time for finite alphabets and in time O(nlogm) for infinite alphabets. When the character count problem is generalized to two dimensions it becomes the submatrix character count problem. Its input is an n×n matrix T over alphabet Σ and a natural number m. Its output is: for every i,j, i,j=1,…,n−m+1, the number of different alphabet symbols occurring in the submatrix T[i+k,j+ℓ], k=0,…,m−1;ℓ=0,…,m−1. The straightforward one-dimensional solution slides a window along the text adding an element and deleting an element at every step. The problem with two dimensions is that at every move of the window there are m elements added and m deleted. In this paper, we present an alternate one-dimensional solution that generalizes to two dimensions. We achieve a O(n2) time solution to the submatrix character count problem over a finite alphabet and a O(n2logm) solution over an infinite alphabet. [Copyright &y& Elsevier]

We have recently proved that there is a bound for the sequence equivalence problem of polynomially bounded D0L systems depending only on the cardinality of the underlying alphabet. In this paper we deduce a similar bound for the language equivalence problem of polynomially bounded D0L systems. More generally, we prove that if a given class of D0L systems (satisfying certain natural conditions) has a uniform bound for sequence equivalence then it also has a uniform bound for language equivalence. [Copyright &y& Elsevier]

The paper describes a Petri net as well as a structural operational semantics for an algebra of process expressions. It specifically addresses this problem for the box algebra, a model of concurrent computation which combines Petri nets and standard process algebras. The main result is that it is possible to obtain a framework where process expressions can be given two, entirely consistent, kinds of semantics: one based on Petri nets, the other on SOS rules. This consistency can also be extended to a partial order semantics. [Copyright &y& Elsevier]

Given a qualitative constraint network (QCN), a singleton-style consistency focuses on each base relation (atom) of a constraint separately, rather than the entire constraint altogether. This local consistency is essential for tackling fundamental reasoning problems associated with QCN s, such as minimal labeling, but can suffer from redundant constraint checks, especially when checks occur far from where the pruning usually takes place. In this paper, we propose singleton-style consistencies that are applied just on the neighbourhood of a singleton-checked constraint instead of the whole network. We make a theoretical comparison with existing consistencies and consequently prove some properties of the new ones. Further, we propose algorithms to enforce our consistencies, as well as parsimonious variants thereof, that are more efficient in practice than the state of the art. An experimental evaluation with random and structured QCN s of Allen's Interval Algebra in the phase transition region demonstrates the potential of our approach. [ABSTRACT FROM AUTHOR]

Finite-state machines, a simple class of finite Petri nets, were equipped in [16] with an efficiently decidable, truly-concurrent, bisimulation-based, behavioral equivalence, called team equivalence, which conservatively extends classic bisimulation equivalence on labeled transition systems and which is checked in a distributed manner. This paper addresses the problem of defining variants of this equivalence which are insensitive to silent moves. We define (rooted) weak team equivalence and (rooted) branching team equivalence as natural transposition to finite-state machines of Milner's weak bisimilarity [25] and van Glabbeek and Weijland's branching bisimilarity [12] on labeled transition systems. The process algebra CFM [15] is expressive enough to represent all and only the finite-state machines, up to net isomorphism. Here we first prove that the rooted versions of these equivalences are congruences for the operators of CFM, then we show some algebraic properties, and, finally, we provide finite, sound and complete, axiomatizations for them. [ABSTRACT FROM AUTHOR]

This paper contributes to a generic theory of behaviour of "finite-state" systems. Systems are coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to the locally finite fixpoint (LFF), a new fixpoint of the endofunctor. The LFF exists provided that the endofunctor is finitary and preserves monomorphisms, is a subcoalgebra of the final coalgebra, i.e. it is fully abstract w.r.t. behavioural equivalence, and it is characterized by two universal properties: as the final locally finitely generated coalgebra, and as the initial fg-iterative algebra. Instances of the LFF are: regular languages, rational streams, rational formal power-series, regular trees etc. Moreover, we obtain e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S -algebraic formal power-series (in general, the behaviour of finite coalgebras under the coalgebraic language semantics arising from the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten), and the monad of Courcelle's algebraic trees. [ABSTRACT FROM AUTHOR]