waashk/dblp huggingface dataset:
maude: specification and programming in rewriting logic. maude is a high-level language and a high-performance system supporting executable specification and declarative programming in rewriting logic. since rewriting logic contains equational logic, maude also supports equational specification and programming in its sublanguage of functional modules and theories. the underlying equational logic chosen for maude is membership equational logic, that has sorts, subsorts, operator overloading, and partiality definable by membership and equality conditions. rewriting logic is reflective, in the sense of being able to express its own metalevel at the object level. reflection is systematically exploited in maude endowing the language with powerful metaprogramming capabilities, including both user-definable module operations and declarative strategies to guide the deduction process. this paper explains and illustrates with examples the main concepts of maude's language design, including its underlying logic, functional, system and object-oriented modules, as well as parameterized modules, theories, and views. we also explain how maude supports reflection, metaprogramming and internal strategies. the paper outlines the principles underlying the maude system implementation, including its semicompilation techniques. we conclude with some remarks about applications, work on a formal environment for maude, and a mobile language extension of maude.
reflection in conditional rewriting logic. we recall general metalogical axioms for a reflective logic based on the notion of a universal theory, that is, a theory that can simulate the deductions of all other theories in a class of theories of interest, including itself. we then show that conditional rewriting logic is reflective, generalizing in two stages: first to the unsorted conditional case, and then to the many-sorted conditional case, the already known result for unconditional and unsorted rewriting logic (reflection in rewriting logic: metalogical foundations and metaprogramming applications. csli publications, 2000). this work should be seen as providing foundations for many useful applications of rewriting logic reflection. the results presented here have greatly influenced the design of the maude language, which implements rewriting logic and supports its reflective capabilities, and have been used as a theoretical foundation for applications such as internal rewrite strategies, reflective design of theorem proving tools, module algebra and metaprogramming, and metareasoning in metalogical frameworks.
string-matching with obdds. ordered binary decision diagrams (obdds) are a very popular graph representation for boolean functions. they can be viewed as finite automata recognizing sets of strings of a fixed length, where the letters of the input strings are read at most once in a predefined ordering. the string matching problem with string w as pattern, consists of determining, given an input string, whether or not it contains w as substring. we show that for a fraction of orderings tending to i when n increases arbitrarily, the minimal size of an obdd solving the string matching problem for strings of length n has a growth which is an exponential in n.
probabilistic temporal logics via the modal mu-calculus. this paper presents a mu-calculus-based modal logic for describing properties of reactive probabilistic labeled transition systems (rpltss) and develops a model-checking algorithm for determining whether or not states in finite-state rpltss satisfy formulas in the logic. the logic is based on the distinction between (probabilistic) "systems" and (nonprobabilistic) "observations": using the modal mu-calculus, one may specify sets of observations, and the semantics of our logic then enable statements to be made about the measures of such sets at various system states. the logic may be used to encode a variety of probabilistic modal and temporal logics; in addition, the model-checking problem for it may be reduced to the calculation of solutions to systems of non-linear equations. finally, the logic induces an equivalence on rpltss that coincides with accepted notions of probabilistic bisimulation in the literature.
a note on decidability questions on presentations of word semigroups. we apply automata-theoretic tools and some recently established compactness properties in the study of f-semigroups, that is, subsemigroups of free semigroups. with each f-semigroup we associate an f-presentation, which turns out to be finite for all finitely generated f-semigroups. connections between f-presentations and ordinary presentations of semigroups are also pointed out. it is also shown that it is undecidable whether two finitely generated f-semigroups satisfy a common relation in their f-presentation.
the commutation of finite sets: a challenging problem. we prove that given a set x of two nonempty words, a set y of nonempty words commutes with x if and only if either y is a union of powers of x or x,yt+ for some primitive word t. we also show that the same holds for certain special types of codes, but does not hold, in general, for sets of cardinality at least 4.
the concept of computability. i explore the conceptual foundations of alan turing's analysis of computability, which still dominates thinking about computability today. i argue that turing's account represents a last vestige of a famous but unsuccessful program in pure mathematics, viz., hilbert's formalist program. it is my contention that the plausibility of turing's account as an analysis of the computational capacities of physical machines rests upon a number of highly problematic assumptions whose plausibility in turn is grounded in the formalist stance towards mathematics. more specifically, the turing account conflates concepts that are crucial for understanding the computational capacities of physical machines. these concepts include the idea of an "operation" or "action" that is "formal," "mechanical," "well-defined," and "precisely described," and the idea of a "symbol" that is "formal," "uninterpreted," and "shaped". when these concepts are disentangled, the intuitive appeal of turing's account is significantly undermined. this opens the way for exploring models of hypercomputability that are fundamentally different from those currently entertained in the literature.
parsing with a finite dictionary. we address the following issue: given a word w ∈ a* and a set of n nonempty words x, how does one determine efficiently whether w ∈ x* or not? we discuss several methods including an o(r × |w| + |x|) algorithm for this problem where r ≤ n is the length of a longest suffix chain of x and |x| is the sum of the lengths of words in x. we also consider the more general problem of providing all the decompositions of w in words of x.
the minimum broadcast range assignment problem on linear multi-hop wireless networks. given a set n of radio stations located on an euclidean space, a source station s and an integer h (1 ≤ h ≤ |n| - 1), the minimum bounded-hop broadcast range assignment problem consists in finding a range assignment for n of minimum total power consumption that allows broadcast operations from s to every station in n in at most h hops. the problem is known to be np-hard on d-dimensional spaces for any d ≥ 2 (18th annual symp. on theoretical aspects of computer science (stacs'01), lecture notes in computer science, vol. 1770, 2000, pp. 651-660.) and some efficient approximation algorithms have been given in clementi et al. and wann et al. (18th annual symp. on theoretical aspects of computer science (stacs'01), lecture notes in computer science, vol. 1770, 2000, pp. 651-660, ieee infocom'01, 2001). in this paper, we address the case in which the stations are arbitrarily located along a line (i.e., the linear case). we provide the first polynomial-time algorithm that returns an optimal solution for any instance of the linear case. the algorithm works in o(h|n|2) time.
distributed broadcast in radio networks of unknown topology. a multi-hop synchronous radio network is said to be unknown if the nodes have no knowledge of the topology. a basic task in radio network is that of broadcasting a message (created by a fixed source node) to all nodes of the network. typical operations in real-life radio networks is the multi-broadcast that consists in performing a set of r independent broadcasts. the study of broadcast operations on unknown radio network is started by the seminal paper of bar-yehuda et al. [j. comput. system sci. 45 (1992) 104] and has been the subject of several recent works.in this paper, we study the completion and the termination time of distributed protocols for both the (single) broadcast and the multi-broadcast operations on unknown networks as functions of the number of nodes n, the maximum eccentricity d, the maximum in-degree δ, and the congestion c of the networks. we establish new connections between these operations and some combinatorial concepts, such as selective families, strongly selective families (also known as superimposed codes), and pairwise r-different families. such connections, combined with a set of new lower and upper bounds on the size of the above families, allow us to derive new lower bounds and new distributed protocols for the broadcast and multi-broadcast operations. in particular, our upper bounds are almost tight and strongly improve over the previous bounds for a large class of networks.
minimal schedulability interval for real-time systems of periodic tasks with offsets. we consider real-time systems in highly safety context where tasks have to meet strict deadlines. tasks are periodic, may have offsets, share critical resources and be precedence constrained. off-line scheduling should be of great help for such systems, but methods proposed in the literature cannot deal with them. our aim is to extend and improve the well-known cyclicity result of leung and merill to every scheduling algorithm and to systems of interacting tasks with offsets. one of the main benefit of our result is to enable the use of off-line scheduling methods for those real-time critical systems.
abstractions for fault-tolerant global computing. global computing (wan programming, internet programming) distinguishes itself from local computing (lan computing) by the fact that it exposes some aspects of the network to the application, rather than seeking to hide them with network transparency, as in lan programming. global computing languages seek to provide useful abstractions for building applications in such environments. the lqp(ċ)-calculus is a family of programming languages that use the abstraction of logs to specify application-specific protocols for distributed agreement and fault tolerance in global applications. reflecting the motivation for global computing, the abstraction of logs isolates the communication requirements of such protocols. two specific instances of the lqp(ċ)-calculus are provided, the lqp(dc)-calculus and the lqp(dcu)-calculus. these are intended as kernel programming languages for fault-tolerant distributed programming. the calculi incorporate various abstractions for fault tolerance, from which several forms of distributed transactions and optimistic computation may be built. as an example application, a calculus of atomic failures is presented, the atf-calculus, and its encoding in the lqp(dc)-calculus used to verify a correctness property.
the computational complexity of distance functions of two-dimensional domains. we study the computational complexity of the distance function associated with a polynomial-time computable two-dimensional domains, in the context of the turing machine-based complexity theory of real functions. it is proved that the distance function is not necessarily computable even if a two-dimensional domain is polynomial-time recognizable. on the other hand, if both the domain and its complement are strongly polynomial-time recognizable, then the distance function is polynomial-time computable if and only if p = np.
computing the maximum agreement of phylogenetic networks. we introduce the maximum agreement phylogenetic subnetwork problem (masn) for finding branching structure shared by a set of phylogenetic networks. we prove that the problem is np-hard even if restricted to three phylogenetic networks and give an o(n2)-time algorithm for the special case of two level-1 phylogenetic networks, where n is the number of leaves in the input networks and where n is called a level-f phylogenetic network if every biconnected component in the underlying undirected graph induces a subgraph of n containing at most f nodes with indegree 2. we also show how to extend our technique to yield a polynomial-time algorithm for any two level-f phylogenetic networks n1, n2 satisfying f = o(log n); more precisely, its running time is o(|v (n1)| ċ |v (n2)| ċ 2f1 + f2), where v (ni) and fi denote the set of nodes in ni and the level of ni, respectively, for i ∈ {1, 2}.
heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances. an analysis of the average-case complexity of solving random 3-satisfiability (sat) instances with backtrack algorithms is presented. we first interpret previous rigorous works in a unifying framework based on the statistical physics notions of dynamical trajectories, phase diagram and growth process. it is argued that, under the action of the davis-putnam-loveland logemann (dpll) algorithm, 3-sat instances are turned into 2+p-sat instances whose characteristic parameters (ratio α of clauses per variable, fraction p of 3-clauses) can be followed during the operation, and define resolution trajectories. depending on the location of trajectories in the phase diagram of the 2+p-sat model, easy (polynomial) or hard (exponential) resolutions are generated. three regimes are identified, depending on the ratio α of the 3-sat instance to be solved. lower satisfiable (sat) phase: for small ratios, dpll almost surely finds a solution in a time growing linearly with the number n of variables. upper sat phase: for intermediate ratios, instances are almost surely satisfiable but finding a solution requires exponential time (∼ 2nω with ω ≥ 0) with high probability. unsat phase: for large ratios, there is almost always no solution and proofs of refutation are exponential. an analysis of the growth of the search tree in both upper sat and unsat regimes is presented, and allows us to estimate ω as a function of α. this analysis is based on an exact relationship between the average size of the search tree and the powers of the evolution operator encoding the elementary steps of the search heuristic.
on tiling under tomographic constraints. given a tiling of a 2d grid with several types of files, we can count for every row and column how many tiles of each type it intersects. these numbers are called the projections. we are interested in the problem of reconstructing a tiling which has given projections. some simple variants of this problem, involving files that are 1 × 1 or 1 × 2 rectangles, have been studied in the past, and were proved to be either solvable in polynomial time or np-complete. in this note, we make progress toward a comprehensive classification of various tiling reconstrction problems, by proving np-completeness results for several sets of tiles.
restriction categories i: categories of partial maps. given a category with a stable system of monics, one can form the corresponding category of partial maps. to each map in this category there is, on the domain of the map, an associated idempotent, which measures the degree of partiality. this structure is captured abstractly by the notion of a restriction category, in which every arrow is required to have such an associated idempotent. categories with a stable system of monics, functors preserving this structure, and natural transformations which are cartesian with respect to the chosen monics, form a 2-category which we call mcat. the construction of categories of partial maps provides a 2-functor par:mcat&rarr;cat. we show that par can be made into an equivalence of 2-categories between mcat and a 2-category of restriction categories. the underlying ordinary functor par&r0:mcat&0 &rarr; ca t0 of the above 2-functor par turns out to be monadic, and, from this, we deduce the completeness and cocompleteness of the 2-categories of m-categories and of restriction categories. we also consider the problem of how to turn a formal system of subobjects into an actual system of subobjects. a formal system of subobjects is given by a functor into the category slat of semilattices. this structure gives rise to a restriction category which, via the above equivalence of 2-categories, gives an m-category. this m-category contains the universal realization of the given formal subobjects as actual subobjects.
restriction categories ii: partial map classification. an algebraic characterization of monads which are abstract partial map classifiers is provided, without the assumption that the categories of total maps possess products. by an abstract partial map classifier we mean a monad whose kleisli category is a full subcategory of a partial map category wherein the induced comonad classifies partial maps in the usual sense. a construction of the corresponding actual partial map classifier from an abstract one is described, and conditions for an abstract partial map classifier to be a real one are provided. the paper uses the notion of a restriction category developed in earlier work, and the characterization of these as full subcategories of partial map categories.
more on randomized on-line algorithms for caching. we address the tradeoff between the competitive ratio and the resources used by randomized on-line algorithms for caching. two algorithms reported in the literature that achieve the optimal ratio hk require a lot of memory and perform extensive computation at each step. on the other hand, a very simple algorithm called rmark has competitive ratio 2hk -- 1, within a factor of 2 of the optimum. a natural question that arises here is whether there is a tradeoff between simplicity and the competitive ratio. in particular, is it possible to achieve a competitive ratio better than 2hk - 1 with a simple algorithm like rmark?we first consider marking algorithms that are natural generalizations of rmark, and we prove that, for any ε > 0, there is no randomized marking algorithm for caching with competitive ratio (2 - ε)hk. thus rmark is essentially optimal among marking algorithms.another model of simple caching algorithms is that of trackless algorithms. these are algorithms that do not store any information about items that are not in the cache. it is known that, for k = 2, there is no randomized trackless algorithm for caching with ratio better than 37/24;≈ 1.5416; the trivial upper bound is 2, achieved even by deterministic algorithms lru and fifo. we reduce this gap by giving a trackless randomized algorithm with competitive ratio 1/4(3 + √13) ≈ 1.6514.
the weighted 2-server problem. we consider a generalization of the 2-server problem in which servers have different costs. we prove that, in uniform spaces, a version of the work function algorithm is 5-competitive, and that no better ratio is possible. we also give a 5-competitive randomized, memoryless algorithm for uniform spaces, and a matching lower bound.for arbitrary metric spaces, in contrast with the non-weighted case, we prove that there is no memoryless randomized algorithm with finite competitive ratio. we also propose a version of the problem in which a request specifies two points to be covered by the servers, and the algorithm must decide which server to move to which point. for this version, we show a 9-competitive algorithm and we prove that no better ratio is possible.
moments of conjugacy classes of binary words. for each nonempty binary word w = c1c2...cq, where ci ∈ {0, 1}, the nonnegative integer σi=1q (q + 1 - i)ci is called the moment of w and is denoted by m(w). let [w] denote the conjugacy class of w. define m([w]) = {m(u): u ∈ [w]}, n(w) = {m(u) - m(w): u ∈ [w]} and δ(w) = max{m(u) - m(v): u, v ∈ [w]}. using these objects, we obtain equivalent conditions for a binary word to be an α-word (respectively, a power of an α-word). for instance, we prove that the following statements are equivalent for any binary word w with |w| ≥ 2: (a) w is an α-word, (b) δ(w)= |w| - 1, (c) w is a cyclic balanced primitive word, (d) m([w]) is a set of |w| consecutive positive integers, (c) n(w) is a set of |w| consecutive integers and 0 ∈ n(w), (f) w is primitive and [w] ⊂ st.
factors of characteristic words of irrational numbers. let β be an irrational number between 0 and 1. the characteristic word f(β) of β is defined to be the infinite word over {0, 1} whose nth letter is [(n + 1)β] -[nβ], n ≥ 1. it is well known that, for each m ≥ 1, f(β) has exactly m + 1 distinct factors of length m. in this paper, we shall develop a method to construct these factors. under our construction, the 1-sets of these m + 1 factors x0(m), x1(m),..., xm(m) are determined, these factors are increasing in the lexicographic order and their moments m(x0(m)), m(x1(m)),..., m(xm(m)) form an increasing sequence of m + 1 consecutive integers. some known results about generating factors of f(β) using the unbordered α-words and their conjugates turn out to be consequences of our main theorem.
performance aspects of distributed caches using ttl-based consistency. the web is the largest distributed database deploying time-to-live-based weak consistency. each object has a lifetime-duration assigned to it by its origin server. a copy of the object fetched from its origin server is received with maximum time-to-live (ttl) that equals its lifetime duration. in contrast a copy obtained through a cache have shorter ttl since the age (elapsed time since fetched from the origin) is deducted from its lifetime duration. a request served by a cache constitutes a hit if the cache has a fresh copy of the object. otherwise, the request is considered a miss and is propagated to another server. it is evident that the number of cache misses depends on the age of the copies the cache receives. thus, a cache that sends requests to another cache would suffer more misses than a cache that sends requests directly to an authoritative server.in this paper, we model and analyze the effect of age on the performance of various cache configurations. we consider a low-level cache that fetches objects either from their origin servers or from other caches and analyze its miss-rate as function of its fetching policy. we distinguish between three basic fetching policies, namely, fetching always from the origin, fetching always from the same high-level cache, and fetching from a "random" high-level cache. we explore the relationships between these policies in terms of the miss-rate achieved by the low-level cache, both on worst-case sequences, and on sequences generated using particular probability distributions.guided by web caching practice, we consider two variations of the basic policies. in the first variation the high-level cache uses pre-term refreshes to keep a copy with lower age. in the second variation the low-level cache uses extended lifetime duration. we analyze how these variations affect the miss-rates. our theoretical results help to understand how age may affect the miss-rate, and imply guidelines for improving performance of web caches.