waashk/dblp huggingface dataset:
conway's angel in three dimensions. the angel-devil game is an infinite game played on an infinite chess board: in each move the angel, a generalized chess king, jumps from his current square to some location at distance at most k, while his opponent, the devil, blocks squares trying to strand the angel. the angel wins if he manages to fly on forever. it is a long-standing open question whether some angel of sufficiently large power k can escape.we show that in the three-dimensional analog of the game the 13-angel can win. our proof is constructive and provides an explicit infinite escape strategy.
automatic verification of real-time systems with discrete probability distributions. we consider the timed automata model of alur and dill (theoret. comput. sci. 126 (1994) 183-235), which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, it is often desirable to express the likelihood of the system making certain transitions. in this paper, we present a model for real-time systems augmented with discrete probability distributions. furthermore, two approaches to model checking are introduced for this model. the first uses the algorithm of baier and kwiatkowska (distributed comput. 11 (1998) 125-155) to provide a verification technique against temporal logic formulae which can refer both to timing properties and probabilities. the second, generally more efficient, technique concerns the verification of probabilistic, real-time reachability properties.
proving sequential function chart programs using timed automata. applications described by sequential function chart (sfc) often being critical, we have investigated the possibilities of program checking. in particular, physical time can be handled by sfc programs using temporizations, which is why we are interested in the quantitative temporal properties. we have proposed a modeling of sfc in timed automata, a formalism which takes time into account. in this modeling, we use the physical constraints of the environment. verification of properties can be carried out using the model-checker kronos. we apply this method to sfc programs of average size like that of the control part of the production cell korso. the size of the programs remains however a limit and we are studying the means of solving this problem. copyright 2001 elsevier science b.v.
a classification of plane and planar 2-trees. we present new functional equations for the species of plane and of planar (in the sense of harary and palmer, graphical enumeration, academic press, new york, 1973) 2-trees and some associated pointed species. we then deduce the explicit molecular expansion of these species, i.e. a classification of their structures according to their stabilizers. therein result explicit formulas in terms of catalan numbers for their associated generating series, including the asymmetry index series. this work is related to the enumeration of polyene hydrocarbons of molecular formula cnhn+2.
a strategy for searching with different access costs. let us consider an ordered set of keys a = {a1 > ... > an}, where the probability of searching ai is 1/n, for i = 1,..., n. if the cost of testing each key is similar, then the standard binary search is the strategy with minimum expected access cost. however, if the cost of testing ai is ci, for i = 1 .... , n, then the standard binary search is not necessarily the best strategy.in this paper, we prove that the expected access cost of an optimal search strategy is bounded above by 4cln(n + 1)/n, where c= σi=1n ci . furthermore, we show that this upper bound is asymptotically tight up to constant factors. the proof of this upper bound is constructive and generates a 4ln(n + 1)-approximated algorithm for constructing near-optimal search strategies. this algorithm runs in o(n2) time and requires o(n) space, which can be useful for practical cases, since the best known exact algorithm for this problem runs in o(n3) time and requires o(n2) space.
soft linear logic and polynomial time. we present a subsystem of second-order linear logic with restricted rules for exponentials so that proofs correspond to polynomial time algorithms, and vice versa.
phase semantics and decidability of elementary affine logic. light, elementary and soft linear logics are formal systems derived from linear logic, enjoying remarkable normalization properties. in this paper, we prove decidability of elementary affine logic, eal. the result is obtained by semantical means, first defining a class of phase models for eal and then proving soundness and (strong) completeness, following okada's technique. phase models for light affine logic and soft linear logic are also defined and shown complete.
strong rabin numbers of folded hypercubes. the strong rabin number of a network w of connectivity k is the minimum l so that for any k + 1 nodes s, d1, d2, ...,dk of w, there exist k node-disjoint paths from s to d1, d2, ..., dk, respectively, whose maximal length is not greater than l, where s ∉ {d1, d2, ...,dk} and d1, d2, ..., dk are not necessarily distinct. in this paper, we show that the strong rabin number of a k-dimensional folded hypercube is ⌈k/2⌉ + 1, where ⌈k/2⌉ is the diameter of the k-dimensional folded hypercube. each node-disjoint path we obtain has length not greater than the distance between the two end nodes plus two. this paper solves an open problem raised by liaw and chang.
game semantics and linear cps interpretation. we present a semantic analysis of the "linearly used continuation-passing interpretation" of functional languages, based on game semantics. this consists of a category of games with a coherence condition on moves--yielding a fully complete model of an affine-type theory--and a syntax-independent and full embedding of a category of hyland-ong/nickau-style "well-bracketed" games into it. we show that this embedding corresponds precisely to linear cps interpretation in its action on a games model of call-by-value pcf, yielding a proof of full abstraction for the associated translation. we discuss extensions of the semantics to deal with recursive types, call-by-name evaluation, nonlocal jumps, and state.
locally boolean domains. bistable bidomains have been used to give a simple order-theoretic construction of a cartesian closed category of sequential functions. in this paper, we investigate the intensional properties of a full subcategory, the locally boolean domains, in which the bistable structure is given by an involution operation. we show that every pointed locally boolean domain is the limit of an ω-chain of "prenex normal forms" constructed using only products and lifted sums. we use this result to describe a model of linear logic (incorporating both intuitionistic and polarized classical fragments). we show that affine and bistable functions correspond to unique "strategies" on the associated normal forms, and that function composition corresponds to "parallel composition plus hiding" of these strategies.
a calculus of coroutines. we describe a simple but expressive calculus of sequential processes, represented as coroutines. we show that this calculus can be used to express a variety of programming language features including procedure calls, labelled jumps, integer references and stacks. we describe the operational properties of the calculus using reduction rules and equational axioms.we describe a notion of categorical model for our calculus, and give a simple example of such a model based on a category of games and strategies. we prove full abstraction results showing that equivalence in the categorical model corresponds to observational equivalence in the calculus, and also to equivalence of evaluation trees, which are infinitary normal forms for the calculus.we show that our categorical model can be used to interpret the untyped λ-calculus and use this fact to extract a sound translation of the latter into our calculus of coroutines.
forcing numbers of stop signs. let g be a graph with a perfect matching m. the forcing number of m is the smallest number of edges in a subset s ⊂ m such that s is contained in no other perfect matching of g. we present methods for determining bounds on forcing numbers and apply these methods to find bounds for the forcing numbers of stop signs. a consequence of our main result is that every perfect matching of a stop sign of size (n,k) contains at least n disjoint alternating cycles.
on-line load balancing of temporary tasks revisited. we study load balancing problems of temporary jobs (i.e., jobs that arrive and depart at unpredictable time) in two different contexts, namely, machines and network paths. such problems are known as machine load balancing and virtual circuit routing in the literature. we present new on-line algorithms and improved lower bounds.
quantifier-free logic for nondeterministic theories. we develop a quantifier-free logic for deriving consequences of multialgebraic theories. multialgebras are used as models for nondeterminism in the context of algebraic specifications. they are many sorted algebras with set-valued operations. formulae are sequents over atoms allowing one to state set-inclusion or identity of 1-element sets (determinacy). we introduce a sound and weakly complete rasiowa-sikorski (r-s) logic for proving multialgebraic tautologies. we then extend this system for proving consequences of specifications based on translation of finite theories into logical formulae. finally, we show how such a translation may be avoided--introduction of the specific cut rules leads to a sound and strongly complete gentzen system for proving directly consequences of specifications. besides giving examples of the general techniques of r-s and the specific cut rules, we improve the earlier logics for multialgebras by providing means to handle empty carriers (as well as empty result-sets) without the use of quantifiers, and to derive consequences of theories without translation into another format and without using general cut.
a type system for jvm threads. the current definition of the java bytecode verifier, as well as the proposals to formalize it, does not include any check about the structured use of locks by monitorenter and monitorexit instructions. so code is run, even if critical sections are corrupted. in this paper, we isolate a sublanguage of the java virtual machine with thread creation and mutual exclusion. for this subset, we define a semantics and a formal verifier that enforces basic properties of threads and lock and unlock operations. the verifier integrates well with previous formalizations of the java bytecode verifier. our analysis of structured use of locks reveals the presence of bugs in the current compilers from sun, ibm and microsoft.
on the power of incremental learning. this paper provides a systematic study of incremental learning from noise-free and from noisy data. as usual, we distinguish between learning from positive data and learning from positive and negative data, synonymously called learning from text and learning from informant. our study relies on the notion of noisy data introduced by stephan.the basic scenario, named iterative learning, is as follows. in every learning stage, an algorithmic learner takes as input one element of an information sequence for some target concept and its previously made hypothesis and outputs a new hypothesis. the sequence of hypotheses has to converge to a hypothesis describing the target concept correctly.we study the following refinements of this basic scenario. bounded example-memory inference generalizes iterative inference by allowing an iterative learner to additionally store an a priori bounded number of carefully chosen data elements, while feedback learning generalizes it by allowing the iterative learner to additionally ask whether or not a particular data element did already appear in the input data seen so far.for the case of learning from noise-free data, we show that, when both positive and negative data are available, restrictions on the accessibility of the input data do not limit the learning capabilities if and only if the relevant iterative learners are allowed to query the history of the learning process or to store at least one carefully selected data element. this insight nicely contrasts the fact that, in case only positive data are available, restrictions on the accessibility of the input data seriously affect the learning capabilities of all versions of incremental learners.for the case of learning from noisy data, we present characterizations of all kinds of incremental learning in terms being independent from learning theory. the relevant conditions are purely structural ones. surprisingly, when learning from noisy text and noisy informant is concerned, even iterative learners are exactly as powerful as unconstrained learning devices.
variants of iterative learning. we investigate the principal learning capabilities of iterative learners in some more details. thereby, we confine ourselves to study the learnability of indexable concept classes. the general scenario of iterative learning is as follows. an iterative learner successively takes as input one element of a text (an informant) for a target concept as well as its previously made hypothesis and outputs a new hypothesis about the target concept. the sequence of hypotheses has to converge to a hypothesis correctly describing the target concept.we study two variants of this basic scenario and compare the learning capabilities of all resulting models of iterative learning to one another as well to the standard learning models finite inference, conservative identification, and learning in the limit.first, we consider the case that an iterative learner has to learn from fat texts (fat informants), only. in this setting, it is guaranteed that relevant information is, in principle, accessible at any time in the learning process. second, we study a variant of iterative learning, where an iterative learner is supposed to learn no matter which initial hypothesis is actually chosen. this variant is suited to describe scenarios that are typical for case-based reasoning.
advanced elementary formal systems. an elementary formal system (efs) is a logic program such as a prolog program, for instance, that directly manipulates strings. arikawa and his co-workers proposed elementary formal systems as a unifying framework for formal language learning.in the present paper, we introduce advanced elementary formal systems (aefss), i.e., elementary formal systems which allow for the use of a certain kind of negation, which is nonmonotonic, in essence, and which is conceptually close to negation as failure.we study the expressiveness of this approach by comparing certain aefs definable language classes to the levels in the chomsky hierarchy and to the language classes that are definable by efss that meet the same syntactical constraints.moreover, we investigate the learnability of the corresponding aefs definable language classes in two major learning paradigms, namely in gold's model of learning in the limit and valiant's model of probably approximately correct learning. in particular, we show which learnability results achieved for efss extend to aefss and which do not.
inductive inference of approximations for recursive concepts. this paper provides a systematic study of inductive inference of indexable concept classes in learning scenarios where the learner is successful if its final hypothesis describes a finite variant of the target concept, i.e., learning with anomalies. learning from positive data only and from both positive and negative data is distinguished.the following learning models are studied: learning in the limit, finite identification, set-driven learning, conservative inference, and behaviorally correct learning.the attention is focused on the case that the number of allowed anomalies is finite but not a priori bounded. however, results for the special case of learning with an a priori bounded number of anomalies are presented, too. characterizations of the learning models with anomalies in terms of finite tell-tale sets are provided. the observed varieties in the degree of recursiveness of the relevant tell-tale sets are already sufficient to quantify the differences in the corresponding learning models with anomalies. finally, a complete picture concerning the relations of all models of learning with and without anomalies mentioned above is derived.
decision lists over regular patterns. the paper introduces the notion of decision lists over regular patterns. this formalism provides a strict extension of regular erasing pattern languages and of containment decision lists.formal properties of the resulting language class, a subclass of the regular languages, are investigated. in particular, we show that decision lists over regular patterns have exactly the same expressive power as decision trees over regular patterns.moreover, we study the learnability of the resulting language class within different formal settings including gold's model of learning in the limit as well as valiant's model of approximately correct learning.
concurrency in timed automata. we introduce concurrent timed automata (ctas) where automata running in parallel are synchronized. we consider the subclasses of ctas obtained by admitting, or not, diagonal clock constraints and constant updates, and by letting, or not, sequential automata to update the same clocks. we prove that such subclasses recognize the same languages but differ w.r.t. the succinctness of the models. moreover, we distinguish between subclasses that are polynomially closed w.r.t. finite union and finite intersection, and subclasses that do not have such properties.
efficient timed model checking for discrete-time systems. we consider model checking of timed temporal formulae in durational transition graphs (dtgs), i.e., kripke structures where transitions have integer durations. two semantics for dtgs are presented and motivated. we consider timed versions ofctl where subscripts put quantitative constraints on the time it takes before a property is satisfied.we exhibit an important gap between logics where subscripts of the form "c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or " ≥ c" (bounded duration).without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes δ2p-complete or pspace-complete depending on the considered semantics.
coalgebra morphisms subsume open maps. we relate two abstract notions of bisimulation, induced by open maps and by coalgebra morphisms, respectively. we show that open maps correspond to coalgebra morphisms for a suitable chosen endofunctor in a category of many sorted sets. this demonstrates that the notion of open-maps bisimilarity is of essentially coalgebraic nature. a central role in our development is played by a category of presheaves, which we show as corresponding to the subcategory of consistent coalgebras with lax cohomomorphisms.
decidability of performance equivalence for basic parallel processes. we study an extension of the class of basic parallel processes (bpp), in which actions are durational and urgent and parallel components have independent local clocks. the main result is decidability of strong bisimilarity, known also as performance equivalence, in this class. this extends the earlier decidability result for plain bpp by christensen et al. our decision procedure is based on decidability of the validity problem for presburger arithmetic. we prove also polynomial complexity in positive-duration fragment, thus properly extending a previous result by bérard et al. both ill-timed and well-timed semantics are treated.
identification of birfsa languages. the task of identifying a language from a set of its words is not an easy one. for instance, it is not feasible to identify regular languages in the general case. therefore, looking for subclasses of regular languages that can be identified in this framework is an interesting problem. one of the most classical identifiable classes is the class of reversible languages, introduced by d. angluin, also called bideterministic languages as they can be represented by deterministic automata (dfa) whose reverse is also deterministic. residual finite state automata (rfsa) on the other hand is a class of non-deterministic automata that shares some properties with dfa. in particular, dfa are rfsa and rfsa can be much smaller. we study here learnability of the class of languages that can be represented by birfsa: rfsa whose reverse are rfsa. we prove that this class is not identifiable in general but we present two subclasses that are learnable, the second one being identifiable in polynomial time.
type systems equivalent to data-flow analyses for imperative languages. we show that a large class of data-flow analyses for imperative languages are describable as type systems in the following technical sense: possible results of an analysis can be described in a language of types so that a program checks with a type if and only if this type is a supertype of the result of applying the analysis. type-checking is easy with the help of a certificate that records the "eureka"-bits of a typing derivation. certificate-assisted type-checking amounts to a form of lightweight analysis à la rose. for secure information flow, we obtain a type system that is considerably more precise than that of volpano et al., but not more sophisticated. importantly, our type systems are compositional.
equivalence of conservative, free, linear program schemas is decidable. a program schema defines a class of programs, all of which have identical statement structures, but whose expressions may differ. we prove that given any two structured schemas which are conservative, linear and free, it is decidable whether they are equivalent.
syntax vs. semantics: a polarized approach. we present a notion of sliced proof-nets for the polarized fragment of linear logic and a corresponding game model. we show that the connection between them is very strong through an equivalence of categories (this contains soundness, full completeness and faithful completeness).
asymptotic analysis of a leader election algorithm. itai and rodeh showed that, on the average, the communication of a leader election algorithm takes no more than ln bits, where l ≃ 2.441716 and n denotes the size of the ring. we give a precise asymptotic analysis of the average number of rounds m(n) required by the algorithm, proving for example that m(∞) := limn→∞ m(n) = 2.441715879..., where n is the number of starting candidates in the election. accurate asymptotic expressions of the second moment m(2)(n) of the discrete random variable at hand, its probability distribution, and the generalization to all moments are given. corresponding asymptotic expansions (n → ∞) are provided for sufficiently large j, where j counts the number of rounds. our numerical results show that all computations perfectly fit the observed values. finally, we investigate the generalization to probability t/n, where t is a non-negative real parameter. the real function m(∞, t) := limn →∞ m(n, t) is shown to admit one unique minimum m(∞, t) on the real segment (0, 2). furthermore, the variations of m(∞, t) on the whole real line are also studied in detail.