waashk/dblp huggingface dataset:
testing against a non-controllable stream x-machine using state counting. stream x-machines are a form of extended finite state machines that has received extensive study in recent years. a stream x-machine describes a system as a finite set of states, an internal store, called memory, and a finite number of transitions between the states, labelled by function names (the processing functions). one of the great benefits of using a stream x-machine to specify a system is its associated testing method. under certain design for test conditions, this method produces a test suite that can determine the correctness of the implementation, provided that the processing functions of the stream x-machine specification have been correctly implemented (this can be checked by a separate testing process, using the same method or alternative functional methods). however, the application of the stream x-machine based testing method is often encumbered by the restrictive design for test conditions required. in practical applications, these conditions are achieved by designing extra functionality that will have to be disabled after testing has been completed. this is a time consuming process and can often be a source of error. this paper provides a strong generalisation of the existing method, which requires much laxer design for test conditions; these are naturally satisfied in practical applications and, furthermore, can be introduced into any stream x-machine specification without the need to add extra functionality. consequently, the generalised method can be applied to virtually any system that can be specified by a stream x-machine.
the passport control problem or how to keep a dynamic service system load balanced? in many real life situations (such as department stores, or passport control booths in airports) parallel queues are formed in front of control stations. typically, some of the stations are manned while others are not. classical queuing theory considers the configuration constant, and concentrates on the arrival process. this work explores a new line of research--the case in which the configuration is dynamic, and the customers can plan to cope with anticipated changes. specifically, as the queues build up, management assigns additional officers to the unmanned stations. when this happens--some people move to the newly manned queues from nearby busy queues. in anticipation, people may prefer to line up in busy queues next to unmanned ones.mathematically we discuss the problem of dynamic arrangement of the queues in a service system where at any time each server can be in either an active or an inactive mode. a balancing strategy determines how customers will be reallocated when a station becomes active. given a balancing strategy, we seek a partition of customers to queues that minimizes the maximum wait time of a customer in each of the active stations, thereby keeping the system balanced at all times. we study two balancing strategies that we call split and trim. for the split strategy we discuss a special case (the stations are ordered on a line and a single unmanned station is at one end). we show how an optimal partition can be calculated recursively. we then give partitions that approximate the minimal expected wait time within a factor of 1 + o(1/n), under each of these strategies, where n is the number of stations. we obtain similar bounds (to within factor 2) for the case, where the number of active servers can be any 1 ≤ n ≤ n - 1, and the balancing strategy is trim.
single backup table schemes for shortest-path routing. we introduce a new recovery scheme that needs only one extra backup routing table for networks employing shortest-path routing. by precomputing this backup table, the network recovers from any single link failure immediately after the failure occurs. to compute the backup routing table for this scheme, we use an almost linear time algorithm to solve the {r, v}-problem, which is a variation of the best swap problem presented by nardelli et al. we further show that the same solution can be computed in exactly linear time if the underlying graph is unweighted.
constructible functions in cellular automata and their applications to hierarchy results. we investigate time-constructible functions in one-dimensional cellular automata (ca). it is shown that (i) if a function t(n) is computable by an o(t(n)n)-time turing machine, then t(n) is time constructible by ca and (ii) if two functions are time constructible by ca, then the sum, product, and exponential functions of them are time constructible by ca. as an application, it is shown that if t1(n) and t2(n) are time constructible functions such that limnt1(n)/t2(n)=0 and t1(n)n, then there is a language which can be recognized by a ca in t2(n) time but not by any ca in t1(n) time.
non-cryptographic primitive for pseudorandom permutation. four round feistel permutation (like des) is super-pseudorandom if each round function is random or a secret universal hash function. a similar result is known for five round misty type permutation. it seems that each round function must be at least either random or secret in both cases.in this paper, however, we show that the second round permutation g in five round misty type permutation need not be cryptographic at all, i.e., no randonmess nor secrecy is required. g has only to satisfy that g(x)⊕x ≠ g(x')⊕x' for any x ≠ x'. this is the first example such that a non-cryptographic primitive is substituted to construct the minimum round super-pseudorandom permutation. further we show efficient constructions of super-pseudorandom permutations by using above mentioned g.
coalgebras and monads in the semantics of java. this paper describes the basic structures in the denotational and axiomatic semantics of sequential java, both from a monadic and a coalgebraic perspective. this semantics is an abstraction of the one used for the verification of (sequential) java programs using proof tools in the loop project at the university of nijmegen. it is shown how the monadic perspective gives rise to the relevant computational structure in java (composition, extension and repetition), and how the coalgebraic perspective offers an associated program logic (with invariants, bisimulations, and hoare logics) for reasoning about the computational structure provided by the monad.
analytical depoissonization and its applications. in combinatorics and analysis of algorithms a poisson version of a problem (henceforth called a poisson model or poissonization) is often easier to solve than the original one, which we name here the bernoulli model. poissonization is a technique that replaces the original input (e.g., think of balls thrown into urns) by a poisson process (e.g., think of balls arriving according to a poisson process into urns). more precisely, analytical poisson transform maps a sequence (e.g., characterizing the bernoulli model) into a generating function of a complex variable. however, after poissonization one must depoissonize in order to translate the results of the poisson model into the original (i.e., bernoulli) model. we present in this paper several analytical depoissonization results that fall into the following general scheme: if the poisson transform has an appropriate growth in the complex plane, then an asymptotic expansion of the sequence can be expressed in terms of the poisson transform and its derivatives evaluated on the real line. not surprisingly, actual formulations of depoissonization results depend on the nature of the growth of the poisson transform, and thus we have polynomial and exponential depoissonization theorems. normalization (e.g., as in the central limit theorem) introduces another twist that led us to formulate the so-called diagonal depoissonization theorems. finally, we illustrate our results on numerous examples from combinatorics and the analysis of algorithms and data structures (e.g., combinatorial assemblies, digital trees, multiaccess protocols, probabilistic counting, selecting a leader, data compression, etc.). &mdash;authors' abstract
on the computational content of the lawson topology. an element of an effectively given domain is computable iff its basic scott open neighbourhoods are recursively enumerable. we thus refer to computable elements as scott computable and define an element to be lawson computable if its basic lawson open neighbourhoods are recursively enumerable. since the lawson topology is finer than the scott topology, a stronger notion of computability is obtained. for example, in the powerset of the natural numbers with its standard effective presentation, an element is scott computable iff it is a recursively enumerable set, and it is lawson computable iff it is a recursive set. among other examples, we consider the upper powerdomain of euclidean space, for which we prove that scott and lawson computability coincide with two notions of computability for compact sets recently proposed by brattka and weihrauch in the framework of type-two recursion theory.
how the (1+1) es using isotropic mutations minimizes positive definite quadratic forms. the (1+1) evolution strategy (es), a simple, mutation-based evolutionary algorithm for continuous optimization problems, is analyzed. in particular, we consider the most common type of mutations, namely gaussian mutations, and the 1/5-rule for mutation adaptation, and we are interested in how the runtime/number of function evaluations to obtain a predefined reduction of the approximation error depends on the dimension of the search space.the most discussed function in the area of es is the so-called sphere-function given by sphere: rn → r with x↦x⊤ix (where i ∈ rn×n is the identity matrix), which also has already been the subject of a runtime analysis. this analysis is extended to arbitrary positive definite quadratic forms that induce ellipsoidal fitness landscapes which are "close to being spherically symmetric", showing that the order of the runtime does not change compared to sphere. furthermore, certain positive definite quadratic forms frn → r with x↦x⊤qx, where q ∈ rn×n, inducing ellipsoidal fitness landscapes that are "far away from being spherically symmetric" are exemplarily investigated, namely f(x)=ξċ(x12 +...+ xn/22)+xn/2+12 +...+ xn2 with ξ= poly(n) such that 1/ξ → 0 as n → ∞. it is proved that the optimization very quickly stabilizes and that, subsequently, the runtime to halve the approximation error is θ(ξ ċ n) compared to θ(n) for sphere.
on learning of functions refutably. learning of recursive functions refutably informally means that for every recursive function, the learning machine has either to learn this function or to refute it, that is to signal that it is not able to learn it. three modi of making precise the notion of refuting are considered. we show that the corresponding types of learning refutably are of strictly increasing power, where already the most stringent of them turns out to be of remarkable topological and algorithmical richness. furthermore, all these types are closed under union, though in different strengths. also, these types are shown to be different with respect to their intrinsic complexity; two of them do not contain function classes that are "most difficult" to learn, while the third one does. moreover, we present several characterizations for these types of learning refutably. some of these characterizations make clear where the refuting ability of the corresponding learning machines comes from and how it can be realized, in general.for learning with anomalies refutably, we show that several results from standard learning without refutation stand refutably. from this we derive some hierarchies for refutable learning. finally, we prove that in general one cannot trade stricter refutability constraints for more liberal learning criteria.
on the learnability of recursively enumerable languages from good examples. the present paper investigates identification of indexed families l of recursively enumerable languages from good examples. we distinguish class-preserving learning from good examples (the good examples have to be generated with respect to a hypothesis space having the same range as l) and class-comprising learning from the good examples (the good examples have to be selected with respect to a hypothesis space comprising the range of l). a learner is required to learn a target language on every finite superset of the good examples for it. if the learner's first and only conjecture is correct then the underlying learning model is referred to as finite identification from good examples and if the learner makes a finite number of incorrect conjectures before always outputting a correct one, the model is referred to as limit identification from good examples. in the context of class-preserving learning, it is shown that the learning power of finite and limit identification from good text examples coincide. when class comprising learning from good text examples is concerned, limit identification is strictly more powerful than finite learning. furthermore, if learning from good informant examples is considered, limit identification is superior to finite identification in the class preserving as well as in the class-comprising case. finally, we relate the models of learning from good examples to one another as well as to the standard learning models in the context of gold-style language learnin
mind change complexity of learning logic programs. the present paper motivates the study of mind change complexity for learning minimal models of length-bounded logic programs. it establishes ordinal mind change complexity bounds for learnability of these classes both from positive facts and from positive and negative facts. building on angluin's notion of finite thickness and wright's work on finite elasticity, shinohara defined the property of bounded finite thickness to give a sufficient condition for learnability of indexed families of computable languages from positive data. this paper shows that an effective version of shinohara's notion of bounded finite thickness gives sufficient conditions for learnability with ordinal mind change bound, both in the context of learnability from positive data and for learnability from complete (both positive and negative) data. let ω be a notation for the first limit ordinal. then, it is shown that if a language defining framework yields a uniformly decidable family of languages and has effective bounded finite thickness, then for each natural number m > 0, the class of languages defined by formal systems of length ≤ m: • is identifiable in the limit from positive data with a mind change bound of ω m; • is identifiable in the limit from both positive and negative data with an ordinal mind change bound of ω × m. the above sufficient conditions are employed to give an ordinal mind change bound for learnability of minimal models of various classes of length-bounded prolog programs, including shapiro's linear programs, arimura and shinohara's depth-bounded linearly covering programs, and krishna rao's depth-bounded linearly moded programs. it is also noted that the bound for learning from positive data is tight for the example classes considered.
learning how to separate. the main question addressed in the present work is how to find effectively a recursive function separating two sets drawn arbitrarily from a given collection of disjoint sets. in particular, it is investigated when one can find better learners which satisfy additional constraints. such learners are the following: confident learners which converge on all data-sequences; conservative learners which abandon only definitely wrong hypotheses; set-driven learners whose hypotheses are independent of the order and the number of repetitions of the data-items supplied; learners where either the last or even all hypotheses are programs of total recursive functions.the present work gives a complete picture of the relations between these notions: the only implications are that whenever one has a learner which only outputs programs of total recursive functions as hypotheses, then one can also find learners which are conservative and set-driven. the following two major results need a nontrivial proof: (1) there is a class for which one can find, in the limit, recursive functions separating the sets in a confident and conservative way, but one cannot find even partial-recursive functions separating the sets in a set-driven way. (2) there is a class for which one can find, in the limit, recursive functions separating the sets in a confident and set-driven way, but one cannot find even partial-recursive functions separating the sets in a conservative way.
approximate strong separation with application in fractional graph coloring and preemptive scheduling. in this paper we show that approximation algorithms for the weighted independent set and s-dimensional knapsack problem with ratio a can be turned into approximation algorithms with the same ratio for fractional weighted graph coloring and preemptive resource constrained scheduling. in order to obtain these results, we generalize known results by grötschel, lovasz and schrijver on separation, non-emptiness test, optimization and violation in the direction of approximability.
an asymptotic fully polynomial time approximation scheme for bin covering. in the bin covering problem there is a group l = (a1,...,an) of items with sizes s(ai) ∈ (0, 1), and the goal is to find a packing of the items into bins to maximize the number of bins that receive items of total size at least 1. this is a dual problem to the classical bin packing problem. in this paper we present the first asymptotic fully polynomial-time approximation scheme for the problem.
on average sequence complexity. in this paper we study the average behavior of the number of distinct substrings in a text of size n over an alphabet of cardinality k. this quantity is called the complexity index and it captures the "richness of the language" used in a sequence. for example, sequences with low complexity index contain a large number of repeated substrings and they eventually become periodic (e.g., tandem repeats in a dna sequence). in order to identify unusually low- or high-complexity strings one needs to determine how far are the complexities of the strings under study from the average or maximum string complexity. while the maximum string complexity was studied quite extensively in the past, to the best of our knowledge there are no results concerning the average complexity. we first prove that for a sequence generated by a mixing model (which includes markov sources) the average complexity is asymptotically equal to n2/2 which coincides with the maximum string complexity. however, for a memoryless source we establish a more precise result, namely the average string complexity is n2/2 - n logk n + (1 + ( 1 - γ)/ln k + φk (logkn) + o(1))n where γ ≈ 0.577 and φk(x) is a periodic function with a small amplitude for small alphabet size.
inferring a level-1 phylogenetic network from a dense set of rooted triplets. we consider the following problem: given a set j of rooted triplets with leaf set l, determine whether there exists a phylogenetic network consistent with j, and if so, construct one. we show that if no restrictions are placed on the hybrid nodes in the solution, the problem is trivially solved in polynomial time by a simple sorting network-based construction. for the more interesting (and biologically more motivated) case where the solution is required to be a level-1 phylogenetic network, we present an algorithm solving the problem in o(|t|2) time when t is dense, i.e., when t contains at least one rooted triplet for each cardinality three subset of l. we also give an o(|t|5/3)-time algorithm for finding the set of all phylogenetic networks having a single hybrid node attached to exactly one leaf (and having no other hybrid nodes) that are consistent with a given dense set of rooted triplets.
from truth to computability i. the recently initiated approach called computability logic is a formal theory of interactive computation. it understands computational problems as games played by a machine against its environment, and uses logical formalism to describe valid principles of computability, with formulas representing computational problems and logical operators standing for operations on computational problems. the concept of computability that lies under this approach is a generalization of church-turing computability from simple, two-step (question/answer, input/output) problems to problems of arbitrary degrees of interactivity. restricting this concept to predicates, which are understood as computational problems of zero degree of interactivity, yields exactly classical truth. this makes computability logic a generalization and refinement of classical logic.the foundational paper "introduction to computability logic" [g. japaridze, ann. pure appl. logic 123 (2003) 1-99] was focused on semantics rather than syntax, and certain axiomatizability assertions in it were only stated as conjectures. the present contribution contains a verification of one of such conjectures: a soundness and completeness proof for the deductive system cl3 which axiomatizes the most basic first-order fragment of computability logic called the finite-depth, elementary-base fragment. cl3 is a conservative extension of classical predicate calculus in the language which, along with all of the (appropriately generalized) logical operators of classical logic, contains propositional connectives and quantifiers representing the so called choice operations. the atoms of this language are interpreted as elementary problems, i.e. predicates in the standard sense. among the potential application areas for cl3 are the theory of interactive computation, constructive applied theories, knowledgebase systems, systems for resource-bound planning and action.this paper is self-contained as it reintroduces all relevant definitions as well as main motivations. it is meant for a wide audience and does not assume that the reader has specialized knowledge in any particular subarea of logic or computer science.
a theory of bisimulation for a fragment of concurrent ml with local names. concurrent ml is an extension of standard ml with π-calculus-like primitives for multithreaded programming. cml has a reduction semantics, but to date there has been no labelled transition system semantics provided for the entire language. in this paper, we present a labelled transition semantics for a fragment of cml called µvcml which includes features not covered before: dynamically generated local channels and thread identifiers. we show that weak bisimilarity for µvcml is a congruence, and coincides with barbed bisimulation congruence. we also provide a variant of sangiorgi's normal bisimulation for µvcml, and show that this too coincides with bisimilarity.
a fully abstract may testing semantics for concurrent objects. this paper provides a fully abstract semantics for a variant of the concurrent object calculus. we define may testing for concurrent object components and then characterise it using a trace semantics inspired by uml interaction diagrams. the main result of this paper is to show that the trace semantics is fully abstract for may testing. this is the first such result for a concurrent object language.