waashk/dblp huggingface dataset:
speed scaling with a solar cell. we consider the setting of a device that obtains its energy from a battery and some regenerative source such as a solar cell. we consider the speed scaling problem of scheduling a collection of tasks with release times, deadlines, and sizes, so as to minimize the energy recharge rate of the regenerative source. this is the first theoretical investigation of speed scaling for devices with a regenerative energy source. we show that the problem can be expressed as a polynomial sized convex program. we show that, using the kkt conditions, one can obtain an efficient algorithm to verify the optimality of a schedule. we show that the energy optimal yds schedule is 2-approximate with respect to the recharge rate. we show that the online algorithm bkp is o(1)-competitive with respect to recharge rate.
lmntal as a hierarchical logic programming language. lmntal (pronounced ''elemental'') is a simple language model based on hierarchical graph rewriting that uses logical variables to represent connectivity and membranes to represent hierarchy. lmntal is an outcome of the attempt to unify constraint-based concurrency and constraint handling rules (chr), the two notable extensions to concurrent logic programming. lmntal is intended to be a substrate language of various computational models, especially those addressing concurrency, mobility and multiset rewriting. although the principal objective of lmntal was to provide a unifying computational model, it is of interest to equip the formalism with a precise logical interpretation. in this paper, we show that it is possible to give lmntal a simple logical interpretation based on intuitionistic linear logic and a flattening technique. this enables us to call lmntal a hierarchical, concurrent linear logic language.
how hard is it to find extreme nash equilibria in network congestion games? we study the complexity of finding extreme pure nash equilibria in symmetric (unweighted) network congestion games. in our context best and worst equilibria are those with minimum respectively maximum makespan. on series-parallel graphs a worst nash equilibrium can be found by a greedy approach while finding a best equilibrium is np-hard. for a fixed number of users we give a pseudo-polynomial algorithm to find the best equilibrium in series-parallel networks. for general network topologies also finding a worst equilibrium is np-hard.
deciding branching time properties for asynchronous programs. asynchronous programming is a paradigm that supports asynchronous function calls in addition to synchronous function calls. programs in such a setting can be modeled by automata with counters that keep track of the number of pending asynchronous calls for each function, as well as a call stack for synchronous recursive computation. these programs have the restriction that an asynchronous call is processed only when the call stack is empty. the decidability of the control state reachability problem for such systems was recently established. in this paper, we consider the problems of checking other branching time properties for such systems. specifically we consider the following problems - termination, which asks if there is an infinite (non-terminating) computation exhibited by the system; control state maintainability, which asks if there is a maximal execution of the system, where all the state visited lie in some ''good'' set; whether the system can be simulated by a given finite state system; and whether the system can simulate a given finite state system. we present decision algorithms for all these problems.
efficient model checking for ltl with partial order snapshots. certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, mazurkiewicz traces. two examples of such properties are serializability of a database and global snapshots of concurrent systems. recently, a modest extension for ltl by an operator that expresses snapshots, has been proposed. it combines the ease of linear (interleaving) specification with this useful partial order concept. the new construct allows one to assert that a global snapshot appeared in the past, perhaps not in the observed execution sequence, but possibly in an equivalent one. originally, a model checking algorithm for this logic that is exponential space in the size of the system was suggested. in this paper, we provide a model checking algorithm that is in polynomial space in the size of the system. our construction can also serve as an efficient (polynomial) algorithm for detecting conjunctive properties (i.e., conjunction of local process properties) in a concurrent history of execution.
hardness results and approximation algorithms for (weighted) paired-domination in graphs. let g=(v,e) be a simple graph without isolated vertices. a vertex set s@?v is a paired-dominating set if every vertex in v-s has a neighbor in s and the induced subgraph g[s] has a perfect matching. in this paper, we investigate the approximation hardness of paired-domination in graphs. for weighted paired-domination, an approximation algorithm in general graphs and an exact dynamic programming style algorithm in trees are also given.
fast algorithms for computing tree lcs. the lcs of two rooted, ordered, and labeled trees f and g is the largest forest that can be obtained from both trees by deleting nodes. we present algorithms for computing tree lcs which exploit the sparsity inherent to the tree lcs problem. assuming g is smaller than f, our first algorithm runs in time o(r@?height(f)@?height(g)@?lglg|g|), where r is the number of pairs (v@?f,w@?g) such that v and w have the same label. our second algorithm runs in time o(lrlgr@?lglg|g|), where l is the size of the lcs of f and g. for this algorithm we present a novel three-dimensional alignment graph. our third algorithm is intended for the constrained variant of the problem in which only nodes with zero or one children can be deleted. for this case we obtain an o(rhlglg|g|) time algorithm, where h=height(f)+height(g).
going weighted: parameterized algorithms for cluster editing. the goal of the cluster editing problem is to make the fewest changes to the edge set of an input graph such that the resulting graph is a disjoint union of cliques. this problem is np-complete but recently, several parameterized algorithms have been proposed. in this paper, we present a number of surprisingly simple search tree algorithms for weighted cluster editing assuming that edge insertion and deletion costs are positive integers. we show that the smallest search tree has size o(1.82^k) for edit cost k, resulting in the currently fastest parameterized algorithm, both for this problem and its unweighted counterpart. we have implemented and compared our algorithms, and achieved promising results.
on the size of boyer-moore automata. in this work we study the size of boyer-moore automata introduced in knuth, morris & pratt's famous paper on pattern matching. we experimentally show that a finite class of binary patterns produce very large boyer-moore automata, and find one particular case which we conjecture, generates automata of size @w(m^6). further experimental results suggest that the maximal size could be a polynomial of o(m^7), or even an exponential o(2^0^.^4^m), where m is the length of the pattern.
online scheduling to minimize modified total tardiness with an availability constraint. we consider online scheduling problems to minimize modified total tardiness. the problems are online in the sense that jobs arrive over time. for each job j"j, its processing time p"j, due date d"j and weight w"j become known at its arrival time (or release time) r"j. preemption is not allowed. we first show that there is no finite competitive ratio for problem 1|online,r"j,d"j|@?w"jt"j. so we focus on problem 1|online,r"j,d"j|@?w"j(t"j+d"j) and show that d-swpt (delayed shortest weighted processing time) algorithm is 3-competitive. we further study two problems 1|online,r"j,d"j,h(1),res|@?w"j(t"j+d"j) and 1|online,r"j,d"j,h(1),n-res|@?w"j(t"j+d"j), where res and n-res denote resumable and non-resumable models respectively, and h(1) denotes a non-available time interval [s,@as] with s>0 and @a>=1. we give a lower bound of 1+@a for both problems and prove that m-d-swpt (modified d-swpt) is 3@a and 6@a-competitive in the resumable and non-resumable models, respectively. moreover, we extend the upper bounds to the scenario of parallel machine scheduling with uniform job weight and an assumption that all machines have the same non-available time interval [s,@as]. a lower bound of min{@a,1+@am} is given as well for the scenario.
abstract interpretation of resolution-based semantics. we extend the abstract interpretation point of view on context-free grammars by cousot and cousot to resolution-based logic programs and proof systems. starting from a transition-based small-step operational semantics of prolog programs (akin to the warren machine), we consider maximal finite derivations for the transition system from most general goals. this semantics is abstracted by instantiation to terms and furthermore to ground terms, following the so-called c- and s-semantics approach. orthogonally, these sets of derivations can be abstracted to sld-trees, call patterns and models, as well as interpreters providing effective implementations (such as prolog). these semantics can be presented in bottom-up fixpoint form. this abstract interpretation-based construction leads to classical bottom-up semantics (such as the s-semantics of computed answers, the c-semantics of correct answers of keith clark, and the minimal-model semantics of logical consequences of maarten van emden and robert kowalski). the approach is general and can be applied to infinite and top-down semantics in a straightforward way.
navigable small-world networks with few random bits. we study small-world graphs in the perspective of their use in the development of efficient as well as easy to implement network infrastructures. our analysis starts from the small-world model proposed by kleinberg: a grid network augmented with directed long-range random links. the choices of the long-range links are independent from one node to another. in this setting greedy routing and some of its variants have been analyzed and shown to produce paths of polylogarithmic expected length. we start from asking whether all the randomness, used in kleinberg's model for establishing the long-range contacts of the nodes, is indeed necessary to assure the existence of short paths. in order to deal with the above question, we impose (stringent) restrictions on the choice of long-range links and we show that such restrictions do not increase the average path length of greedy routing and its variations. we are able to decrease the number of random bits, required to establish each node's long-range link, from @w(logn) to o(loglogn) on a network of size n. diminishing the randomness in the choice of random links has several benefits; in particular, it implies an increase in the clustering of the graph, thus increasing the resilience of the network.
frame rule for mutually recursive procedures manipulating pointers. using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. we prove a powerful hoare total correctness rule for mutually recursive procedures manipulating pointers. the rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. the theory, including the proofs, is implemented in the theorem prover pvs. in this implementation program variables and addresses can store values of almost any type of the theorem prover.
covering arrays avoiding forbidden edges. covering arrays (cas) can be used to detect the existence of faulty pairwise interactions between parameters or components in a software system. the generalization considered here applies to the situation in which some input combinations are invalid, a requirement quite common in software testing. in this paper, we study covering arrays avoiding forbidden edges (cafes), where certain pairwise interactions are forbidden while all others must be covered, and we aim to minimize the number of tests. we establish a theoretical framework for this problem, by providing connections to the edge clique covering problem, lower and upper bounds, complexity results and a recursive construction. we also give an algorithm for the case of binary alphabets.
a new linear time algorithm to compute the genomic distance via the double cut and join distance. the genomic distance problem in the hannenhalli-pevzner (hp) theory is the following: given two genomes whose chromosomes are linear, calculate the minimum number of translocations, fusions, fissions and inversions that transform one genome into the other. this paper presents a new distance formula based on a simple tree structure that captures all the delicate features of this problem in a unifying way, and a linear time algorithm for computing this distance.
the complexity of solitaire. klondike is the well-known 52-card solitaire game available on almost every computer. the problem of determining whether an n-card klondike initial configuration can lead to a win is shown np-complete. the problem remains np-complete when only three suits are allowed instead of the usual four. when only two suits of opposite color are available, the problem is shown nl-hard. when the only two suits have the same color, two restrictions are shown in ac^0 and in nl respectively. when a single suit is allowed, the problem drops in complexity down to ac^0[3], that is, the problem is solvable by a family of constant-depth unbounded-fan-in {and, or, mod"3 }-circuits. other cases are studied: for example, ''no king'' variant with an arbitrary number of suits of the same color and with an empty ''pile'' is nl-complete.
local consistency for extended csps. we extend the framework of constraint satisfaction problems to make it more suitable for/applicable to modern constraint programming languages where both constraint satisfaction and constraint solving have a role. some rough principles for local consistency conditions in the extended framework are developed, appropriate notions of local consistency are formulated, and relationships between the various consistency conditions are established.
on the complexity of 2d discrete fixed point problem. we study a computational complexity version of the 2d sperner problem, which states that any three coloring of vertices of a triangulated triangle, satisfying some boundary conditions, will have a trichromatic triangle. in introducing a complexity class ppad, papadimitriou [c.h. papadimitriou, on graph-theoretic lemmata and complexity classes, in: proceedings of the 31st annual symposium on foundations of computer science, 1990, 794-801] proved that its 3d analogue is ppad-complete about fifteen years ago. the complexity of 2d-sperner itself has remained open since then. we settle this open problem with a ppad-completeness proof. the result also allows us to derive the computational complexity characterization of a discrete version of the 2d brouwer fixed point problem, improving a recent result of daskalakis, goldberg and papadimitriou [c. daskalakis, p.w. goldberg, c.h. papadimitriou, the complexity of computing a nash equilibrium, in: proceedings of the 38th annual acm symposium on theory of computing (stoc), 2006]. those hardness results for the simplest version of those problems provide very useful tools to the study of other important problems in the ppad class.
optimal resilient sorting and searching in the presence of memory faults. we investigate the problem of reliable computation in the presence of faults that may arbitrarily corrupt memory locations. in this framework, we consider the problems of sorting and searching in optimal time while tolerating the largest possible number of memory faults. in particular, we design an o(nlogn) time sorting algorithm that can optimally tolerate up to o(nlogn) memory faults. in the special case of integer sorting, we present an algorithm with linear expected running time that can tolerate o(n) faults. we also present a randomized searching algorithm that can optimally tolerate up to o(logn) memory faults in o(logn) expected time, and an almost optimal deterministic searching algorithm that can tolerate o((logn)^1^-^@e) faults, for any small positive constant @e, in o(logn) worst-case time. all these results improve over previous bounds.
focusing and polarization in linear, intuitionistic, and classical logics. a focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. within linear logic, the focused proof system of andreoli provides an elegant and comprehensive normal form for cut-free proofs. within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. these focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. we present a new, focused proof system for intuitionistic logic, called ljf, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. we also use ljf to design a focused proof system lkf for classical logic. our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in girard's lc and lu proof systems.
s-semantics for logic programming: a retrospective look. the paper provides an overview of the s-semantic approach to the semantics of logic programs which had been developed about twenty years ago. the aim of such an approach was that of providing a suitable base for program analysis by means of a semantics which really captures the operational behavior of logic programs, and thus offers useful notions of observable program equivalences. the semantics is given in terms of extended interpretations, which are more expressive than herbrand interpretations, extends the standard herbrand semantics, and can be obtained as a result of both top-down and bottom-up constructions. the approach has been applied to several extensions of positive logic programs and used to develop semantic-based techniques for program analysis, verification and transformation.
on the shyr-yu theorem. an alternative proof of shyr-yu theorem is given. some generalizations are also considered using fractional root decompositions and fractional exponents of words.
on-the-fly tctl model checking for time petri nets. in this paper, we show how to efficiently model check a subset of tctl properties for the time petri net model (tpn model), using the state class method. the verification proceeds by augmenting the tpn model under analysis with a special tpn, called alarm-clock, to allow the capture of relevant time events. a forward on-the-fly exploration is then applied on the resulting tpn state class space to verify a timed property. a relaxation operation on state classes is also introduced to further improve performances. alarm-clock is the same for all properties, whereas the exploration technique is not. three exploration techniques are presented to cover most interesting tctl properties. we prove the decidability of our verification technique for bounded tpn models and compare it with the reachability algorithm implemented in the tool uppaal [g. behrmann, j. bengtsson, a. david, k.g. larsen, p. pettersson, w. yi, uppaal implementation secrets, in: proc. of the 7th international symposium on formal techniques in real-time and fault-tolerant systems, 2002]. finally, we give some experimental results to show the efficiency of our verification technique.
a sublinear-time approximation scheme for bin packing. the bin packing problem is defined as follows: given a set of n items with sizes 00, we present an algorithm a"@e that has sampling access to the input instance and outputs a value k such that c"o"p"t@?k@?(1+@e)@?c"o"p"t+1, where c"o"p"t is the cost of an optimal solution. it is clear that uniform sampling by itself will not allow a sublinear-time algorithm in this setting; a small number of items might constitute most of the total weight and uniform samples will not hit them. in this work we use weighted samples, where item i is sampled with probability proportional to its weight: that is, with probability w"i/@?"iw"i. in the presence of weighted samples, the approximation algorithm runs in o@?(n@?poly(1/@e))+g(1/@e) time, where g(x) is an exponential function of x. when both weighted sampling and uniform sampling are allowed, o@?(n^1^/^3@?poly(1/@e))+g(1/@e) time suffices. in addition to an approximate value to c"o"p"t, our algorithm can also output a constant-size ''template'' of a packing that can later be used to find a near-optimal packing in linear time.
when ignorance helps: graphical multicast cost sharing games. in non-cooperative games played on highly decentralized networks the assumption that each player knows the strategy adopted by any other player may be too optimistic or even infeasible. in such situations, the set of players of which each player knows the chosen strategy can be modeled by means of a social knowledge graph in which nodes represent players and there is an edge from i to j if i knows j. following the framework introduced in [7], we study the impact of social knowledge graphs on the fundamental multicast cost sharing game in which all the players want to receive the same communication from a given source in an undirected network. in the classical complete information case, such a game is known to be highly inefficient, since its price of anarchy can be as high as the total number of players @r. we first show that, under our incomplete information setting, pure nash equilibria always exist only if the social knowledge graph is directed acyclic (dag). we then prove that the price of stability of any dag is at least 12log@r and provide a dag lowering the classical price of anarchy to a value between 12log@r and log^2@r. if specific instances of the game are concerned, that is if the social knowledge graph can be selected as a function of the instance, we show that the price of stability is at least 4@r@r+3, and that the same bound holds also for the price of anarchy of any social knowledge graph (not only dags). moreover, we provide a nearly matching upper bound by proving that, for any fixed instance, there always exists a dag yielding a price of anarchy less than 4. our results open a new window on how the performances of non-cooperative systems may benefit from the lack of total knowledge among players.
the relevant prefixes of coloured motzkin walks: an average case analysis. in this paper we study some relevant prefixes of coloured motzkin walks (otherwise called coloured motzkin words). in these walks, the three kinds of step can have @a,@b and @c colours, respectively. in particular, when @a=@b=@c=1 we have the classical motzkin walks while for @a=@c=1 and @b=0 we find the well-known dyck walks. by using the concept of riordan arrays and probability generating functions we find the average length of the relevant prefix in a walk of length n and the corresponding variance in terms of @a,@b and @c. this result is interesting from a combinatorial point of view and also provides an average case analysis of algorithms related to the problem of ranking and generating uniformly at random the coloured motzkin words.