waashk/dblp huggingface dataset:
on iterating linear transformations over recognizable sets of integers. it has been known for a long time that the sets of integer vectors that are recognizable by finite-state automata are those that can be defined in an extension of presburger arithmetic. in this paper, we address the problem of deciding whether the closure of a linear transformation preserves the recognizable nature of sets of integer vectors. we solve this problem by introducing an original extension of the concept of recognizability to sets of vectors with complex components. this generalization allows to obtain a simple necessary and sufficient condition over linear transformations, in terms of the eigenvalues of the transformation matrix. we then show that these eigenvalues do not need to be computed explicitly in order to evaluate the condition, and we give a full decision procedure based on simple integer arithmetic. the proof of this result is constructive, and can be turned into an algorithm for applying the closure of a linear transformation that satisfies the condition to a finite-state representation of a set. finally, we show that the necessary and sufficient condition that we have obtained can straightforwardly be turned into a sufficient condition for linear transformations with linear guards.
counting the solutions of presburger equations without enumerating them. the number decision diagram (ndd) has recently been introduced as a powerful representation system for sets of integer vectors. ndds can notably be used for handling sets defined by arbitrary presburger formulas, which makes them well suited for representing the set of reachable states of finite-state systems extended with unbounded integer variables. in this paper, we address the problem of counting the number of distinct elements in a set of numbers or, more generally, of vectors, represented by an ndd. we give an algorithm that is able to produce an exact count without enumerating explicitly the vectors, which makes it capable of handling very large sets. as an auxiliary result, we also develop an efficient projection method that allows to construct efficiently ndds from quantified formulas, and thus makes it possible to apply our counting technique to sets specified by formulas. our algorithms have been implemented in the verification tool lash, and applied successfully to various counting problems.
an analysis of loop checking mechanisms for logic programs. we systemically study loop checking mechanisms for logic programs by considering their soundness, completeness, relative strength and related concepts. we introduce a natural concept of a simple loop check and prove that no sound and complete simple loop check exists, even for programs without function symbols. then we introduce a number of sound simple loop checks and identify natural classes of prolog programs without function symbols for which they are complete. in these classes a limited form of recursion is allowed. as a by-product we obtain an implementation of the closed world assumption of reiter and a query evaluation algorithm for these classes of logic programs.
measuring with jugs. we study the jug problem in its most general form: given a set of jugs of fixed capacities, find out which quantities are measurable, and provide upper and lower bounds on the number of steps necessary for measurements.
independent domination in finitely defined classes of graphs. we study the independent dominating set problem restricted to graph classes defined by finitely many forbidden induced subgraphs. the main result is two sufficient conditions for the problem to be np-hard in a finitely defined class of graphs. we conjecture that those conditions are also necessary and describe several classes of graphs verifying the conjecture.
message-passing automata are expressively equivalent to emso logic. we study the expressiveness of finite message-passing automata with a priori unbounded fifo channels and show them to capture exactly the class of msc languages that are definable in existential monadic second-order logic interpreted over mscs. furthermore, we prove the monadic quantifier-alternation hierarchy over mscs to be infinite and conclude that the class of msc languages accepted by message-passing automata is not closed under complement.
parity graph-driven read-once branching programs and an exponential lower bound for integer multiplication. branching programs are a well-established computation model for boolean functions, especially read-once branching programs have been studied intensively. exponential lower bounds for read-once branching programs are known for a long time. on the other hand, the problem of proving superpolynomial lower bounds for parity read-once branching programs is still open. in this paper restricted parity read-once branching programs are considered and an exponential lower bound on the size of the so-called well-structured parity graph-driven read-once branching programs for integer multiplication is proven. this is the first strongly exponential lower bound on the size of a parity nonoblivious read-once branching program model for an explicitly defined boolean function. in addition, more insight into the structure of integer multiplication is yielded.
union of shadows. our aim in this note is to show that if a is a family of (k 3) 3-sets then there are at least (k 4) 4-sets that may be written as unions of two 2-sets in the shadow of a. this is the first non-trivial case of a more general conjecture about unions of shadows.
a hierarchy of failures-based models: theory and application. consistency between a process and its specification expressed in csp is typically presented as a refinement check. within the traces model consistency is measured by examining only the traces of the systems, whilst in the finer stable failures model the possibility of subsequently refusing a combination of events is also taken into consideration.in this paper, we begin by motivating the need for alternative measures of consistency. we then identify the failures class-a class of semantic models for describing concurrent systems in which each model is associated with a predicate that determines how much availability information is recorded. we show how refinement within members of this class corresponds to confirmation of non-standard measures of consistency, and identify application areas for these measures of consistency. we show how refinement in each model can be automatically tested.we also carry out a theoretical examination of the failures class. we prove that the class forms a complete lattice, and investigate the positions of particular models within that lattice. we also identify the maximal subset of the language over which each model is compositional.
polynomial equation solving by lifting procedures for ramified fibers. let be given a parametric polynomial equation system which represents a generically unramified family of zero-dimensional algebraic varieties. we exhibit an efficient algorithm which computes a complete description of the solution set of an arbitrary parameter instance from a complete description of the infinitesimal structure of a particular ramified parameter instance of our family. this generalizes in the case of space curves previous methods of heintz et al. and schost, which require the given parameter instance to be unramified. we illustrate our method solving particular polynomial equation systems by deformation techniques.
normalisation for higher-order calculi with explicit substitutions. explicit substitutions (es) were introduced as a bridge between the theory of rewrite systems with binders and substitution, such as the λ-calculus, and their implementation. in a seminal paper melliès observed that the dynamical properties of a rewrite system and its es-based implementation may not coincide: he showed that a strongly normalising term (i.e. one which does not admit infinite derivations) in the λ-calculus may lose this status in its es-based implementation. this paper studies normalisation for the latter systems in the general setting of higher-order rewriting: based on recent work extending the theory of needed strategies to non-orthogonal rewrite systems we show that needed strategies normalise in the es-based implementation of any orthogonal pattern higher-order rewrite system.
when ambients cannot be opened. we investigate expressiveness of a fragment of the ambient calculus, a formalism for describing distributed and mobile computations. more precisely, we study expressiveness of the pure and public ambient calculus from which the capability open has been removed, in terms of the reachability problem of the reduction relation. surprisingly, we show that even for this very restricted fragment, the reachability problem is not decidable. at a second step, for a slightly weaker reduction relation, we prove that reachability can be decided by reducing this problem to markings reachability for petri nets. finally, we show that the name-convergence problem as well as the model-checking problem turn out to be undecidable for both the original and the weaker reduction relation.
watermelon uniform random generation with applications. watermelons are particular configurations of vicious walkers. in these configurations, each path starts and ends at the same ordinate. we present a simple uniform random generation algorithm of watermelons based on enumeration formulas of star configurations (with or without a wall). the performance of this algorithm is better than earlier ones in the case of watermelons with few walkers.using appropriate bijections, these algorithms can also generate underdiagonal paths, realizers (or schnyder trees), twin parallelogram polyominoes according to their perimeter and width, baxter permutations according to the number of rises, etc. moreover, we present some experimental results on the height of watermelons and realizers.
randomness in secret sharing and visual cryptography schemes. secret sharing schemes allow a secret to be shared among a group of participants so that only qualified subsets of participants can recover the secret. a visual cryptography scheme (vcs) is a special kind of secret sharing scheme in which the secret to share consists of an image and the shares consist of xeroxed transparencies which are stacked to recover the shared image.in this paper, we analyze the relationship between secret sharing schemes and vcss, focusing our attention on the amount of randomness required to generate the shares. we prove that secret sharing schemes for a set of secrets of size two (bsss) and vcss are "equivalent" with respect to the randomness. indeed, we show how to transform a bss for a given access structure into a vcs for the same access structure while preserving the randomness of the original scheme. we provide both upper and lower bounds on the randomness of bsss.all vcss presented in this paper allow a perfect reconstruction of black pixels.
constructions of generalized superimposed codes with applications to group testing and conflict resolution in multiple access channels. in this paper we introduce a parameterized generalization of the well known superimposed codes. we give algorithms for their construction and provide non-existential results. we apply our new combinatorial structures to the efficient solution of new group testing problems and access coordination issues in multiple access channels.
the structure of reflexive regular splicing languages via sch6uuml;tzenberger constants. the splicing operation was introduced in 1987 by head as a mathematical model of the recombination of dna molecules under the influence of restriction and ligases enzymes. this operation allows us to define a computing (language generating) device, called a splicing system. other variants of this original definition were also proposed by paun and pixton respectively. the computational power of splicing systems has been thoroughly investigated. nevertheless, an interesting problem is still open, namely the characterization of the class of regular languages generated by finite splicing systems. in this paper, we will solve the problem for a special class of finite splicing systems, termed reflexive splicing systems, according to each of the definitions of splicing given by paun and pixton. this special class of systems contains, in perticular, finite head splicing systems. the notion of a constant, given by schützenberger, once again intervenes.
regular splicing languages and subclasses. recent developments in the theory of finite splicing systems have revealed surprising connections between long-standing notions in the formal language theory and splicing operation. more precisely, the syntactic monoid and schützenberger constant have strong interaction with the investigation of regular splicing languages. this paper surveys results of structural characterization of classes of regular splicing languages based on the above two notions and discusses basic questions that motivate further investigations in this field.in particular, we improve the result in [6] that provides a structural characterization of reflexive symmetric splicing languages by showing that it can be extended to the class of all reflexive splicing languages: this is the larger class for which a characterization is known.
reconciling a gene tree to a species tree under the duplication cost model. the general problem of reconciling the information from evolutionary trees representing the relationships between distinct gene families is of great importance in bioinformatics and has been popularized among the computer science researchers by ma et al. [from gene trees to species trees, siam j. comput. 30(3) (2000) 729-752] where the authors pose the intriguing question if a certain definition of minimum tree that reconciles a gene tree and a species tree is correct. we answer affirmatively to this question; moreover, we show an efficient algorithm for computing such minimum-leaf reconciliation trees and prove the uniqueness of such trees. we then tackle some different versions of the biological problem by showing that the exemplar problem, arising from the exemplar analysis of multigene genomes, is np-hard even when the number of copies of a given label is at most two. finally, we introduce two novel formulations for the problem of recombining evolutionary trees, extending the gene duplication problem studied in [ma et al., from gene trees to species trees, siam j. comput. 30(3) (2000) 729-752; m. fellows et al., on the multiple gene duplication problem, in: proc. ninth internat. symp. on algorithms and computation (isaac98), 1998; r. page, maps between trees and cladistic analysis of historical associations among genes, systematic biology 43 (1994) 58-77; r.m. page, j. cotton, vertebrate phylogenomics: reconciled trees and gene duplications, in: proc. pacific symp. on biocomputing 2002 (psb2002), 2002, pp. 536-547; r. guigò et al., reconstruction of ancient molecular phylogeny, mol. phy. and evol. 6(2) (1996) 189-213], and we give an exact algorithm (via dynamic programming) for one of these formulations.
a transition system semantics for the control-driven coordination language manifold. coordination languages are a new class of parallel programming languages which manage the interactions among concurrent programs. basically, coordination is achieved either by manipulating data values shared among all active processes or by dynamically evolving the interconnections among the processes as a consequence of observations of their state changes. the latter, also called control-driven coordination, is supported by manifold. we present the formal semantics of a kernel of manifold, based on a two-level transition system model: the first level is used to specify the ideal behavior of each single component in a manifold system, whereas the second level captures their interactions. although we apply our two-level model in this paper to define the semantics of a control-oriented coordination language, this approach is useful for the formal studies of other coordination models and languages as well.
generalized metric spaces: completion, topology, and powerdomains via the yoneda embedding. generalized metric spaces are a common generalization of preorders and ordinary metric spaces (lawvere 1973). combining lawvere''s (1973) enriched-categorical and smyth'' (1988, 1991) topological view on generalized metric spaces, it is shown how to construct 1. completion, 2. topology, and 3. powerdomains for generalized metric spaces. restricted to the special cases of preorders and ordinary metric spaces, these constructions yield, respectively: 1. chain completion and cauchy completion; 2. the alexandroff and the scott topology, and the epsilon-ball topology; 3. lower, upper, and convex powerdomains, and the hyperspace of compact subsets. all constructions are formulated in terms of (a metric version of) the yoneda (1954) embedding.
context-freeness of the power of context-free languages is undecidable. the power of a language l is the set of all powers of the words in l. in this paper, the following decision problem is investigated. given a context-free language l, is the power of l context-free? we show that this problem is decidable for languages over unary alphabets, but it is undecidable whenever languages over alphabets with at least two letters are considered.
on the number of components in cooperating distributed grammar systems. it is proved that the number of components in context-free cooperating distributed (cd) grammar systems can be reduced to 3 when they are working in the so-called sf-mode of derivation, which is the cooperation protocol which has been considered first for cd grammar systems, in this derivation mode, a component continues the derivation until and unless there is a nonterminal in the sentential form which cannot be rewritten according to that component. moreover, it is shown that cd grammar systems in sf-mode with only one component can generate only the context-free languages but they can generate non-context-free languages if two components are used. the sf-mode of derivation is compared with other well-known cooperation protocols with respect to the hierarchies induced by the number of components.
a method for symbolic analysis of security protocols. in security protocols, message exchange between the intruder and honest participants induces a form of state explosion which makes protocol models infinite. we propose a general method for automatic analysis of security protocols based on the notion of frame, essentially a rewrite system plus a set of distinguished terms called messages. frames are intended to model generic crypto-systems. based on frames, we introduce a process language akin to abadi and fournet's applied pi. for this language, we define a symbolic operational semantics that relies on unification and provides finite and effective protocol models. next, we give a method to carry out trace analysis directly on the symbolic model. we spell out a regularity condition on the underlying frame, which guarantees completeness of our method for the considered class of properties, including secrecy and various forms of authentication. we show how to instantiate our method to some of the most common crypto-systems, including shared-and public-key encryption, hashing and diffie-hellman key exchange.
processes as formal power series: a coinductive approach to denotational semantics. we characterize must testing equivalence on csp in terms of the unique homomorphism from the moore automaton of csp processes to the final moore automaton of partial formal power series over a certain semiring. the final automaton is then turned into a csp-algebra: operators and fixpoints are defined, respectively, via behavioural differential equations and simulation relations. this structure is then shown to be preserved by the final homomorphism. as a result, we obtain a fully abstract compositional model of csp phrased in purely set-theoretical terms.
divergence in testing and readiness semantics. many variants of must-testing semantics have been put forward that are equally sensitive to deadlock, but differ for the stress they put on divergence, i.e. on the possibility for systems of getting involved in infinite internal computations. safe-testing is one such variant, that naturally pops up when studying the behavioural pre-congruences induced by certain basic observables. here, we study the relationship between safe-testing and olderog's readiness semantics, a semantics induced by a natural process logic. we show that safe-testing is finer than readiness, and coincides with a refinement of readiness obtained by tuning olderog's definition. for both safe-testing and the original readiness semantics we propose simple complete axiomatizations, which permit a fuller appreciation of their similarities and differences. copyright 2001 elsevier science b.v.
palindromic factors of billiard words. we study palindromic factors of billiard words, in any dimension. there are differences between the two-dimensional case, and higher dimension. arbitrary long palindrome factors exist in any dimension, but arbitrary long palindromic prefixes exist in general only in dimension 2.
a high-level modular definition of the semantics of c#. we propose a structured mathematical definition of the semantics of c# programs to provide a platform-independent interpreter view of the language for the c# programmer, which can also be used for a precise analysis of the ecma standard of the language and as a reference model for teaching. the definition takes care to reflect directly and faithfully--as much as possible without becoming inconsistent or incomplete--the descriptions in the c# standard to become comparable with the corresponding models for java in stärk et al. (java and java virtual machine--definition, verification, validation, springer, berlin, 2001) and to provide for implementors the possibility to check their basic design decisions against an accurate high-level model. the model sheds light on some of the dark corners of c# and on some critical differences between the ecma standard and the implementations of the language.
flow metrics. we introduce flow metrics as a relaxation of path metrics (i.e. linear orderings). they are defined by polynomial-sized linear programs and have interesting properties including spreading. we use them to obtain relaxations for several np-hard linear ordering problems such as minimum linear arrangement and minimum pathwidth. our approach has the advantage of achieving the best-known approximation guarantees for these problems using the same relaxation and essentially the same rounding algorithm for all the problems while varying only the objective function from problem to problem. this is in contrast to the current state of the literature where each problem either has a new relaxation or a new rounding or both. we also characterize a natural projection of the flow polyhedron.
elan from a rewriting logic point of view. elan implements computational systems, a concept that combines two first class entities: rewrite rules and rewriting strategies. elan can be used either as a logical framework or to describe and execute deterministic as well as non-deterministic rule-based processes. with the general goal to make precise a rewriting logic-based semantics of elan, this paper has three contributions: a presentation of the concepts of rules and strategies available in elan, an expression of rewrite rules with matching conditions in conditional rewriting logic, and finally an enrichment mechanism of a rewrite theory into a strategy theory in conditional rewriting logic.