waashk/dblp huggingface dataset:
compressed data structures: dictionaries and data-aware measures. in this paper, we propose measures for compressed data structures, in which space usage is measured in a data-aware manner. in particular, we consider the fundamental dictionary problem on set data, where the task is to construct a data structure for representing a set s of n items out of a universe u={0,...,u-1} and supporting various queries on s. we use a well-known data-aware measure for set data called gap to bound the space of our data structures. we describe a novel dictionary structure that requires gap+o(nlog(u/n)/logn)+o(nloglog(u/n)) bits. under the ram model, our dictionary supports membership, rank, and predecessor queries in nearly optimal time, matching the time bound of andersson and thorup's predecessor structure [a. andersson, m. thorup, tight(er) worst-case bounds on dynamic searching and priority queues, in: acm symposium on theory of computing, stoc, 2000], while simultaneously improving upon their space usage. we support select queries even faster in o(loglogn) time. our dictionary structure uses exactly gap bits in the leading term (i.e., the constant factor is 1) and answers queries in near-optimal time. when seen from the worst-case perspective, we present the first o(nlog(u/n))-bit dictionary structure that supports these queries in near-optimal time under the ram model. we also build a dictionary which requires the same space and supports membership, select, and partial rank queries even more quickly in o(loglogn) time. we go on to show that for many (real-world) datasets, data-aware methods lead to a worthwhile compression over combinatorial methods. to the best of our knowledge, these are the first results that achieve data-aware space usage and retain near-optimal time.
the class constrained bin packing problem with applications to video-on-demand. in this paper we present approximation results for the class constrained bin packing problem that has applications to video-on-demand systems. in this problem we are given bins of size b with c compartments, and n items of q different classes, each item i@?{1,...,n} with class c"i and size s"i. the problem is to pack the items into bins, where each bin contains at most c different classes and has total items size at most b. we present several approximation algorithms for offline and online versions of the problem.
s4 enriched multimodal categorial grammars are context-free. bar-hillel et al. [y. bar-hillel, c. gaifman, e. shamir, on categorial and phrase structure grammars, bulletin of the research council of israel f (9) (1960) 1-16] prove that applicative categorial grammars weakly recognize the context-free languages. buszkowski [w. buszkowski, generative capacity of non-associative lambek calculus, bulletin of the polish academy of sciences: mathematics 34 (1986) 507-518] proves that grammars based on the product-free fragment of the non-associative lambek calculus nl recognize exactly the context-free languages. kandulski [m. kandulski, the equivalence of non-associative lambek categorial grammars and context-free grammars, zeitschrift fur mathematische logik und grundlagen der mathematik 34 (1988) 41-52] furthers this result by proving that grammars based on nl also recognize exactly the context-free languages. jager [g. jager, residuation, structural rules and context freeness, journal of logic, language and information 13 (2004) 47-59] proves that categorial grammars based on nl@?, the non-associative lambek calculus enriched with residuated modalities, weakly recognize exactly the context-free languages. we extend this result, proving that categorial grammars based on nl"s"4, the enrichment of nl@? by the axioms 4 and t, weakly recognize exactly the context-free languages.
modular construction of complete coalgebraic logics. we present a modular approach to defining logics for a wide variety of state-based systems. the systems are modelled as coalgebras, and we use modal logics to specify their observable properties. we show that the syntax, semantics and proof systems associated with such logics can all be derived in a modular fashion. moreover, we show that the logics thus obtained inherit soundness, completeness and expressiveness properties from their building blocks. we apply these techniques to derive sound, complete and expressive logics for a wide variety of probabilistic systems, for which no complete axiomatisation has been obtained so far.
control of discrete-event systems with modular or distributed structure. most of the large scale state transition (also called discrete-event) systems are formed as parallel compositions of many small subsystems (modules). control of modular and distributed discrete-event systems appears as an approach to handle computational complexity of synthesizing supervisory controllers for large scale systems. for both modular and distributed discrete-event systems sufficient and necessary conditions are derived for modular control synthesis to equal global control synthesis, while enforcing a safety specification in an optimal way (the language of the controlled system is required to be the supremal one achievable by an admissible controller and included in a safety specification language). the two cases of local (decomposable) and global (indecomposable) specifications are considered. the modular control synthesis has a much lower computational complexity than the corresponding global control synthesis for the respective sublanguages. the complexity is compared using explicit formulas.
wcet free time analysis of hard real-time systems on multiprocessors: a regular language-based model. this paper presents the initial step of an aid design method earmarked for operational validation of hard real-time systems. we consider systems that are composed of sequential hard real-time tasks, which are embedded on centralized multiprocessor architectures. we introduce a model based upon untimed finite automata and meant to collect the operational behaviors of the system compatible with its time specifications, and we go on to provide a feasibility decision result for systems composed of tasks presenting cpu loads which are exact values: execution times are not wcet values. this is why we call this approach wcet-free analysis. the results we have achieved likewise involve hardware specifications such as multiprocessors and speeds of processors.
belnap's logic and conditional composition. we study two alternative bases for belnap's four-valued logic and provide complete equational axiomatizations for them. one is called conditional composition logic. it has a single, ternary if-then-else connective with a sequential, operational reading, and four constants for the truth values. the other logic is called guard logic. the main motivation for this logic lies in its technical properties. it admits a useful type of canonical form (term representation), and a relatively simple strategy for equational reasoning.
tutorial on separation results in process calculi via leader election problems. we compare the expressive power of process calculi by studying the problem of electing a leader in a symmetric network of processes. we consider the @p-calculus with mixed choice, separate choice and internal mobility, value-passing ccs and mobile ambients, together with other ambient calculi (safe ambients, the push and pull ambient calculus and boxed ambients). we provide a unified approach for all these calculi using reduction semantics.
verification of boolean programs with unbounded thread creation. most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. boolean programs [t. ball, s.k. rajamani, bebop: a symbolic model checker for boolean programs, in: spin 00, in: lecture notes in computer science, vol. 1885, springer, 2000, pp. 113-130] are the most popular representation for these abstractions. unfortunately, today's symbolic software model checkers are limited to the analysis of sequential programs due to the fact that reachability in boolean programs with unbounded thread creation is undecidable. we address this limitation with a novel algorithm for over-approximating reachability in boolean programs with unbounded thread creation. although the boolean programs are not of finite state, the algorithm always reaches a fix-point. the fixed points are detected by projecting the state of the threads to the globally visible parts, which are finite.
optimality and condensing of information flow through linear refinement. detecting information flows inside a program is useful to check non-interference or independence of program variables, an important aspect of software security. in this paper we present a new abstract domain c expressing constancy of program variables. we then apply giacobazzi and scozzari's linear refinement to build a domain c->c which contains all input/output dependences between the constancy of program variables. we show that c->c is optimal, in the sense that it cannot be further linearly refined, and condensing, in the sense that a compositional, input-independent static analysis over c->c has the same precision as a non-compositional, input-driven analysis. moreover, we show that c->c has a natural representation in terms of boolean formulas, which is important since it allows one to use the efficient binary decision diagrams in its implementation. we then prove that c->c coincides with genaim, giacobazzi and mastroeni's if domain for information flows and with amtoft and banerjee's independ domain for independence. this lets us extend to if and independ the properties that we proved for c->c: optimality, condensing and representation in terms of boolean formulas. as a secondary result, it lets us conclude that if and independ are actually the same abstract domain, although completely different static analyses have been based on them.
algebras with parametrized iterativity. iterative algebras, as studied by nelson and tiuryn, are generalized to algebras whose iterativity is parametrized in the sense that only some variables can be used for iteration. for example, in the case of one binary operation, the free iterative algebra is the algebra of all rational binary trees; if only the left-hand variable is allowed to be iterated, then the free iterative algebra is the algebra of all right-well-founded rational binary trees. in order to express such parametrized iterativity, we work with parametrized endofunctors of set, i.e. finitary endofunctors h:setxset->set, and introduce the concept of iterativity for algebras for the endofunctor x@?h(x,x). we then describe free iterative h-algebras.
selective strictness and parametricity in structural operational semantics, inequationally. parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. the formal background of such 'free theorems' is well developed for extensions of the girard-reynolds polymorphic lambda calculus by algebraic datatypes and general recursion, provided the resulting calculus is endowed with either a purely strict or a purely nonstrict semantics. but modern functional languages like clean and haskell, while using nonstrict evaluation by default, also provide means to enforce strict evaluation of subcomputations at will. the resulting selective strictness gives the advanced programmer explicit control over evaluation order, but is not without semantic consequences: it breaks standard parametricity results. this paper develops an operational semantics for a core calculus supporting all the language features emphasized above. its main achievement is the characterization of observational approximation with respect to this operational semantics via a carefully constructed logical relation. this establishes the formal basis for new parametricity results, as illustrated by several example applications, including the first complete correctness proof for short cut fusion in the presence of selective strictness. the focus on observational approximation, rather than equivalence, allows a finer-grained analysis of computational behavior in the presence of selective strictness than would be possible with observational equivalence alone.
domain-theoretical models of parametric polymorphism. we present a domain-theoretical model of parametric polymorphism based on admissible per's over a domain-theoretical model of the untyped lambda calculus. the model is shown to be a model of abadi & plotkin's logic for parametricity, by the construction of an lapl-structure as defined by the authors in [l. birkedal, r.e. mogelberg, r.l. petersen, parametric domain-theoretical models of polymorphic intuitionistic/linear lambda calculus, in: m. escardo, a. jung, m. mislove (eds.), proceedings of mathematical foundations of programming semantics 2005, vol. 155, 2005, pp. 191-217; l. birkedal, r.e. mogelberg, r.l. petersen, category theoretical models of linear abadi & plotkin logic, 2006 (submitted for publication)]. this construction gives formal proof of solutions to a large class of recursive domain equations, which we explicate. as an example of a computation in the model, we explicitly describe the natural numbers object obtained using parametricity. the theory of admissible per's can be considered a domain theory for (impredicative) polymorphism. by studying various categories of admissible and chain complete per's and their relations, we discover a picture very similar to that of domain theory.
concurrent games with tail objectives. we study infinite stochastic games played by two players over a finite state space, with objectives specified by sets of infinite traces. the games are concurrent (players make moves simultaneously and independently), stochastic (the next state is determined by a probability distribution that depends on the current state and chosen moves of the players) and infinite (proceed for an infinite number of rounds). the analysis of concurrent stochastic games can be classified into: quantitative analysis, analyzing the optimum value of the game and @e-optimal strategies that ensure values within @e of the optimum value; and qualitative analysis, analyzing the set of states with optimum value 1 and @e-optimal strategies for the states with optimum value 1. we consider concurrent games with tail objectives, i.e., objectives that are independent of the finite-prefix of traces, and show that the class of tail objectives is strictly richer than that of the @w-regular objectives. we develop new proof techniques to extend several properties of concurrent games with @w-regular objectives to concurrent games with tail objectives. we prove the positive limit-one property for tail objectives. the positive limit-one property states that for all concurrent games if the optimum value for a player is positive for a tail objective @f at some state, then there is a state where the optimum value is 1 for the player for the objective @f. we also show that the optimum values of zero-sum (strictly conflicting objectives) games with tail objectives can be related to equilibrium values of nonzero-sum (not strictly conflicting objectives) games with simpler reachability objectives. a consequence of our analysis presents a polynomial time reduction of the quantitative analysis of tail objectives to the qualitative analysis for the subclass of one-player stochastic games (markov decision processes).
component refinement and csc-solving for stg decomposition. stgs (signal transition graphs) give a formalism for the description of asynchronous circuits based on petri nets. to overcome the state explosion problem one may encounter during circuit synthesis, a nondeterministic algorithm for decomposing stgs was suggested by chu and improved by one of the present authors. here we study how csc-solving-which is essential for circuit synthesis-can be combined with decomposition. for this purpose, the correctness definition for decomposition is enhanced with internal signals and hierarchical decomposition is proven correct. based on this, it is shown that speed-independent csc-solving preserves correctness and can be combined with decomposition. furthermore, we use our new correctness definition to give the first correctness proof for the decomposition method of carmona and cortadella. finally, we compare three different implementation relations for stgs: one derived from our correctness definition; one defined by dill based on trace structures; and one derived from i/o-compatibility defined by carmona and cortadella.
query-point visibility constrained shortest paths in simple polygons. in this paper, we study the problem of finding the shortest path between two points inside a simple polygon such that there is at least one point on the path from which a query point is visible. we provide an algorithm which preprocesses the input in o(n^2+nk) time and space and provides logarithmic query time. the input polygon has n vertices and k is a parameter dependent on the input polygon which is o(n^2) in the worst case but is much smaller for most polygons. the preprocessing algorithm sweeps an angular interval around every reflex vertex of the polygon to store the optimal contact points between the shortest paths and the windows separating the visibility polygons of the query points from the source and the destination.
the complexity of two problems on arithmetic circuits. by using arithmetic circuits, encoding multivariate polynomials may be drastically more efficient than writing down the list of monomials. via the study of two examples, we show however that such an encoding can be hard to handle with a turing machine even if the degree of the polynomial is low. namely we show that deciding whether the coefficient of a given monomial is zero is hard for p^#^p under strong nondeterministic turing reductions. as a result, this problem does not belong to the polynomial hierarchy unless this hierarchy collapses. for polynomials over fields of characteristic k>0, this problem is mod"kp-complete. this gives a conp^m^o^d^"^k^p algorithm for deciding an upper bound on the degree of a polynomial given by a circuit in fields of characteristic k>0.
on complexity of grammars related to the safety problem. leftist grammars were introduced by motwani et al., who established the relationship between the complexity of the accessibility problem (or safety problem) for certain general protection systems and the membership problem for these grammars. the membership problem for leftist grammars is decidable. this implies the decidability of the accessibility problem. it is shown that the membership problem for leftist grammars is pspace-hard. therefore, the accessibility problem in the appropriate protection systems is pspace-hard as well. furthermore, the pspace-hardness result is adapted to a very restricted class of leftist grammars, if the grammar is a part of the input.
identity-based ring signatures from rsa. shamir proposed in 1984 the first identity-based signature scheme, whose security relies on the rsa problem. a similar scheme was proposed by guillou and quisquater in 1988. formal security of these schemes was not argued and/or proved until many years later [d. pointcheval, j. stern, security arguments for digital signatures and blind signatures, journal of cryptology 13 (3) (2000) 361-396; y. dodis, j. katz, s. xu, m. yung, strong key-insulated signature schemes, in: proceedings of pkc'03, in: lncs, vol. 2567, springer-verlag, 2002, pp. 130-144; m. bellare, c. namprempre, g. neven, security proofs for identity-based identification and signature schemes, in: proceedings of eurocrypt'04, in: lncs, vol. 3027, springer-verlag, 2004, pp. 268-286]. taking the guillou-quisquater scheme as the starting point, we design and analyze in this work ring signature schemes and distributed ring signature schemes for identity-based scenarios whose security is based on the hardness of the rsa problem. these are the first identity-based ring signature schemes which do not employ bilinear pairings. furthermore, the resulting schemes satisfy an interesting property: the real author(s) of a ring signature can later open the anonymity and prove that he is actually the person who signed the message.
mirror substitutions and palindromic sequences. by introducing the notion of mirror substitution, we show that, given a substitutive sequence over two letters, it is palindromic (that is, it contains arbitrarily long palindromes) if and only if its language is mirror-invariant (that is, it is closed under the mirror image map). then we solve a question of hof, knill and simon in the 2-letter case, and also, by constructing a counterexample, we give a negative answer to the open problem 4 in the webpage: http://iml.univ-mrs.fr/~bernat/openquestions.html.
upward separations and weaker hypotheses in resource-bounded measure. we consider resource-bounded measure in double-exponential-time complexity classes. in contrast to complexity class separation translating downwards, we show that measure separation translates upwards. for example, @m"p(np)0@?@m"e"x"p(nexp)
a solution to the angel problem. we solve the angel problem, by describing a strategy that guarantees the win of an angel of power 2 or greater. basically, the angel should move north as quickly as possible. however, he should detour around eaten squares, as long as the extra distance does not exceed twice the number of eaten squares evaded. we show that an angel following this strategy will always spot a trap early enough to avoid it.
np-hard graph problems and boundary classes of graphs. any graph problem, which is np-hard in general graphs, becomes polynomial-time solvable when restricted to graphs in special classes. when does a difficult problem become easy? to answer this question we study the notion of boundary classes. in the present paper we define this notion in its most general form, describe several approaches to identify boundary classes and apply them to various graph problems.
towards a theory of data entanglement. we give a formal model for systems that store data in entangled form. we propose a new notion of entanglement, called all-or-nothing integrity (aoni) that binds the users' data in a way that makes it hard to corrupt the data of any one user without corrupting the data of all users. aoni can be a useful defense against negligent or dishonest storage providers who might otherwise be tempted to discard documents belonging to users without much clout. we show that, if all users use a fixed standard recovery algorithm, we can implement aoni using a mac, but, if some of the users adopt instead a non-standard recovery algorithm provided by the dishonest storage provider, aoni can no longer be achieved. however, even for the latter scenario, we describe a simple entangling mechanism that provides aoni for a restricted class of destructive adversaries.
strict partitions and discrete dynamical systems. we prove that the set of partitions with distinct parts of a given positive integer under dominance ordering can be considered as a configuration space of a discrete dynamical model with two transition rules and with the initial configuration being the singleton partition. this allows us to characterize its lattice structure, fixed point, and longest chains as well as their length, using chip firing game theory. finally, we study the recursive structure of infinite extension of the lattice of strict partitions.
on the subword complexity of thue-morse polynomial extractions. let the (subword) complexity of a sequence u=(u"n)"n"="0^~ over a finite set @s be the function m@?p"u(m), where p"u(m) is the number of distinct blocks of length m in u. let t=(t"n)"n"="0^~ denote the thue-morse sequence. in this paper we study the complexity of the sequences t"h=(t"h"("n"))"n"="0^~, when h(n)@?q[n] is a polynomial with h(n)@?n. in particular, we solve an open problem of allouche and shallit regarding (t"n"^"2)"n"="0^~. we also study the vector space over z/2z, spanned by the sequences t"h.