waashk/dblp huggingface dataset:
logical systems for structured specifications. we study proof systems for reasoning about logical consequences and refinement of structured specifications, based on similar systems proposed earlier in the literature (inform. and comput. 76 (1988) 165; in: f.l. bauer, w. brauer, h. schwichtenberg (eds.), logic and algebra of specification, nato asi series f: computer and systems sciences, vol. 94, springer, berlin, 1991, p. 411). following goguen and burstall, the notion of an underlying logical system over which we build specifications is formalized as an institution and extended to a more general notion, called (d, j)-institution. we show that under simple assumptions (essentially: amalgamation and interpolation) the proposed proof systems are sound and complete. the completeness proofs are inspired by proofs due to cengarle (ph.d. thesis, institut für informatik, ludwig-maximilians-universität müenchen, 1994) for specifications in first-order logic and the logical systems for reasoning about them. we then propose a methodology for reusing proof systems built over institutions rich enough to satisfy the properties required for the completeness results for specifications built over poorer institutions where these properties need not hold.
transition systems without transitions. we study the problem of embedding partial 2-structures into set 2-structures such that the target structure is full and forward closed and it is minimal w.r.t, these properties.ehrenfeucht and rozenberg introduced the notion of partial 2-structures--an abstract form of transition systems--and studied the problem of representing them as partial set 2-structures--directed graphs made of sets and their ordered symmetric differences. they constructed a representation and gave the conditions under which the representation is an isomorphism.we propose an alternative representation of partial 2-structures by partial set 2-structures which are complete graphs, hence their transitions may be left implicit, yielding a static representation of dynamic systems.
competitive online routing in geometric graphs. we consider online routing algorithms for finding paths between the vertices of plane graphs. although it has been shown in bose et al. (internat. j. comput. geom. 12(4) (2002) 283) that there exists no competitive routing scheme that works on all triangulations, we show that there exists a simple online o(1)-memory c-competitive routing strategy that approximates the shortest path in triangulations possessing the diamond property, i.e., the total distance travelled by the algorithm to route a message between two vertices is at most a constant c times the shortest path. our results imply a competitive routing strategy for certain classical triangulations such as the delaunay, greedy, or minimum-weight triangulation, since they all possess the diamond property. we then generalize our results to show that the o(1)-memory c-competitive routing strategy works for all plane graphs possessing both the diamond property and the good convex polygon property.
automatic verification of recursive procedures with one integer parameter. context-free processes (bpa) have been used for dataflow analysis in recursive procedures with applications in optimizing compilers (proceedings of fossacs'99, lecture notes in computer science, vol. 1578, springer, berlin, 1999, pp. 14-30). we introduce a more refined model called bpa(z) that can model not only recursive dependencies, but also the passing of an integer parameter to a subroutine. moreover, this parameter can be tested against conditions expressible in presburger arithmetic. this new and more expressive model can still be analyzed automatically. we define z-input 1-cm, a new class of 1-counter machines (cm) that take integer numbers as input, to describe sets of configurations of bpa(z). we show that the post* (the set of successors) of a set of bpa(z)-configurations described by a z-input 1-cm can be effectively constructed. the pre* (set of predecessors) of a regular set can be effectively constructed as well. however, the pre* of a set described by a z-input 1-cm cannot be represented by a z-input 1-cm, in general, and has an undecidable membership problem. then we develop a new temporal logic based on reversal-bounded counter machines (i.e. machines which use counters such that the change between increasing and decreasing mode of each counter is bounded (j. assoc. comput. mach. 25 (1978) 116) that can be used to describe properties of bpa(z) and show that the model-checking problem is decidable.
model checking for time petri nets. this paper aims at applying the ctl* model checking method to the time petri net (tpn) model. we show here how to contract its generally infinite state space into a graph that captures all its ctl* properties. this graph, called atomic state class graph (ascg), is finite if and only if, the model is bounded. our approach is based on a partition refinement technique, similarly to what is proposed in [berthomieu, vernadat, state class constructions for branching analysis of time petri nets, lecture notes in computer science, vol. 2619, 2003; yoneda, ryuba, ctl model checking of time petri nets using geometric regions, ieice trans. inf. syst. e99-d(3) (1998)]. in such a technique, an intermediate abstraction (contraction) of the tpn state space is first built, then refined until ctl* properties are restored. our approach improves the construction of the ascg in two ways. the first way deals with speeding up the refinement process by using a much more compact intermediate contraction of the tpn state space than those used in [berthomieu, vernadat, state class constructions for branching analysis of time petri nets, lecture notes in computer science, vol. 2619, 2003; yoneda, ryuba, ctl model checking of time petri nets using geometric regions, ieice trans. inf. syst. e99-d(3) (1998)]. the second way deals with computing each ascg node in o(n2) instead of o(n3), n being the number of transitions enabled at the node. experimental results have shown that our improvements have a good impact on performances.
listing all potential maximal cliques of a graph. a potential maximal clique of a graph is a vertex set that induces a maximal clique in some minimal triangulation of that graph. it is known that if these objects can be listed in polynomial time for a class of graphs, the treewidth and the minimum fill-in are polynomially tractable for these graphs. we show here that the potential maximal cliques of a graph can be generated in polynomial time in the number of minimal separators of the graph. thus, the treewidth and the minimum fill-in are polynomially tractable for all classes of graphs with a polynomial number of minimal separators.
noninterference for concurrent programs and thread systems. we propose a type system to ensure the property of noninterference in a system of concurrent programs, described in a standard imperative language enriched with parallelism. our proposal is in the line of some recent work by irvine, volpano and smith. our type system seems more natural and less restrictive than that originally presented by these authors for the concurrent case. moreover, we show how to extend the language in order to formalise scheduling policies for systems of sequential threads. the type system is extended to the new constructs, and we show that noninterference still holds, while remaining in a nonprobabilistic setting.
reconstructing (h, v)-convex 2-dimensional patterns of objects from approximate horizontal and vertical projections. the problem of reconstructing a pattern of an object from its approximate discrete orthogonal projections in a 2-dimensional grid, may have no solution because the inaccuracy in the measurements of the projections may generate an inconsistent problem. to attempt to overcome this difficulty, one seeks to reconstruct a pattern with projection values having possibly some bounded differences with the given projection values and minimizing the sum of the absolute differences.this paper addresses the problem of reconstructing a pattern with a difference at most equal to +1 or -1 between each of its projection values and the corresponding given projection value. we deal with the case of patterns which have to be horizontally and vertically convex and the case of patterns which have to be moreover connected, the so-called convex polyominoes. we show that in both cases, the problem of reconstructing a pattern can be transformed into a satisfiability (sat) problem. this is done in order to take advantage of the recent advances in the design of solvers for the sat problem. we show, experimentally, that by adding two important features to csat (an efficient sat solver), optimal patterns can be found if there exist feasible ones. these two features are: first, a method that extracts in linear time an optimal pattern from a set of feasible patterns grouped in a generic pattern (obtaining a generic pattern may be exponential in the worst case) and second, a method that computes actively a lower bound of the sum of absolute differences that can be obtained from a partially defined pattern. this allows to prune the search tree if this lower bound exceeds the best sum of absolute differences found so far.
observational proofs by rewriting. observability concepts contribute to a better understanding of software correctness. in order to prove observational properties, the concept of context induction has been developed by hennicker (hennicker, formal aspects of computing 3(4) (1991) 326-345). we propose in this paper to embed context induction in the implicit induction framework of (bouhoula and rusinowitch, journal of automated reasoning 14(2) (1995) 189-235). the proof system we obtain applies to conditional specifications. it allows for many rewriting techniques and for the refutation of false observational conjectures. under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. moreover this proof system is operational: it has been implemented within the spike prover and interesting computer experiments are reported.
counting with range concatenation grammars. the class of range concatenation grammars appears to be a convincing challenger as a syntactic base for various tasks, especially in natural language processing. these grammars are powerful, since they strictly contain the class of mildly context-sensitive formalisms, while staying computationally tractable, since their sentences can be parsed in polynomial time. the output of their parsers are structures of polynomial size that can be seen as a generalization of classical context-free shared forest. moreover, this formalism allows a form of modularity which may lead to the design of libraries of reusable grammatical components. and, finally, it can act as a syntactic backbone upon which decorations from other domains (say feature structures) can be grafted. in this paper we explore the behavior of range concatenation grammars in counting, a domain in which bad reputation of other classical syntactic formalisms is well known. this study leads to some surprising results.
entropy rates and finite-state dimension. the effective fractal dimensions at the polynomial-space level and above can all be equivalently defined as the c-entropy rate where c is the class of languages corresponding to the level of effectivization. for example, pspace-dimension is equivalent to the pspace-entropy rate.at lower levels of complexity the equivalence proofs break down. in the polynomial-time case, the p-entropy rate is a lower bound on the p-dimension. equality seems unlikely, but separating the p-entropy rate from p-dimension would require proving p ≠ np.we show that at the finite-state level, the opposite of the polynomial-time case happens: the reg-entropy rate is an upper bound on the finite-state dimension. we also use the finite-state genericity of ambos-spies and busse [automatic forcing and genericity: on the diagonalization strength of finit automata, in: proc. fourth int. conf. on discrete mathematics and theoretical computer science, 2003, springer, berlin, pp. 97-108] to separate finite-state dimension from the reg-entropy rate.however, we point out that a block-entropy rate characterization of finite-state dimension follows from the work of ziv and lempel [compression of individual sequences via variable rate coding, ieee trans. inform. theory 24 (1978) 530-536] on finite-state compressibility and the compressibility characterization of finite-state dimension by dai et al. [finite-state dimension, theoret. comput. sci. 310(1-3) (2004) 1-33].as applications of the reg-entropy rate upper bound and the block-entropy rate characterization, we prove that every regular language has finite-state dimension 0 and that normality is equivalent to finite-state dimension 1.
elementarily computable functions over the real numbers and r-sub-recursive functions. we present an analog and machine-independent algebraic characterization of elementarily computable functions over the real numbers in the sense of recursive analysis: we prove that they correspond to the smallest class of functions that contains some basic functions, and closed by composition, linear integration, and a simple limit schema.we generalize this result to all higher levels of the grzegorczyk hierarchy.this paper improves several previous partial characterizations and has a dual interest: • concerning recursive analysis, our results provide machine-independent characterizations of natural classes of computable functions over the real numbers, allowing to define these classes without usual considerations on higher-order (type 2) turing machines. • concerning analog models, our results provide a characterization of the power of a natural class of analog models over the real numbers and provide new insights for understanding the relations between several analog computational models.
chess endgames: 6-man data and strategy. while nalimov's endgame tables for western chess are the most used today, their depth-to-mate metric is not the most efficient or effective in use. the authors have developed and used new programs to create tables to alternative metrics and recommend better strategies for endgame play.
walks confined in a quadrant are not always d-finite. we consider planar lattice walks that start from a prescribed position, take their steps in a given finite subset of z2, and always stay in the quadrant x ≥ 0, y ≥ 0. we first give a criterion which guarantees that the length generating function of these walks is d-finite, that is, satisfies a linear differential equation with polynomial coefficients. this criterion applies, among others, to the ordinary square lattice walks. then, we prove that walks that start from (1,1), take their steps in {(2,-1), (-1, 2)} and stay in the first quadrant have a non-d-finite generating function. our proof relies on a functional equation satisfied by this generating function, and on elementary complex analysis.
two bijective proofs for the arborescent form of the good-lagrange formula and some applications to colored rooted trees and cacti. goulden and kulkarni (j. combin. theory ser. a 80 (2) (1997) 295) give a bijective proof of an arborescent form of the good-lagrange multivariable inversion formula. this formula was first stated explicitly by bender and richmond (electron. j. combin. 5 (1) (1998) 4pp) but is implicit in goulden and kulkarni (1997). in this paper, we propose two new simple bijective proofs of this formula and we illustrate the interest of these proofs by applying them to the enumeration and random generation of colored rooted trees and rooted m-ary cacti.
updatable timed automata. we investigate extensions of alur and dill's timed automata, based on the possibility to update the clocks in a more elaborate way than simply reset them to zero. we call these automata updatable timed automata. they form an undecidable class of models, in the sense that emptiness checking is not decidable. however, using an extension of the region graph construction, we exhibit interesting decidable subclasses. in a surprising way, decidability depends on the nature of the clock constraints which are used, diagonal-free or not, whereas these constraints play identical roles in timed automata. we thus describe in a quite precise way the thin frontier between decidable and undecidable classes of updatable timed automata.we also study the expressive power of updatable timed automata. it turns out that any up-datable automaton belonging to some decidable subclass can be effectively transformed into an equivalent timed automaton without updates but with silent transitions. the transformation suffers from an enormous combinatorics blow-up which seems unavoidable. therefore, updatable timed automata appear to be a concise model for representing and analyzing large classes of timed systems.
the maximum resource bin packing problem. usually, for bin packing problems, we try to minimize the number of bins used or in the case of the dual bin packing problem, maximize the number or total size of accepted items. this paper presents results for the opposite problems, where we would like to maximize the number of bins used or minimize the number or total size of accepted items. we consider off-line and on-line variants of the problems.for the off-line variant, we require that there be an ordering of the bins, so that no item in a later bin fits in an earlier bin. we find the approximation ratios of two natural approximation algorithms, first-fit-increasing and first-fit-decreasing for the maximum resource variant of classical bin packing.for the on-line variant, we define maximum resource variants of classical and dual bin packing. for dual bin packing, no on-line algorithm is competitive. for classical bin packing, we find the competitive ratio of various natural algorithms.we study the general versions of the problems as well as the parameterized versions where there is an upper bound of 1/k on the item sizes, for some integer k.
efficient exhaustive listings of reversible one dimensional cellular automata. this paper looks at an algebraic formulation of one dimensional cellular automata. using the formulation connections to combinatorial structures and graph theory become clear. strong results about uniqueness and isomorphism allows us to outline effective algorithms for the generation of exhaustive lists of reversible one dimensional cellular automata, and to count the number of distinct examples that exist. these algorithms use the "orderly algorithm" methods to avoid the pitfalls of brute force searches.
model checking for process rewrite systems and a class of action-based regular properties. we consider the model checking problem for process rewrite systems (prs), an infinite-state formalism (non turing-powerful) which subsumes many common models such as pushdown processes and petri nets. prs can be adopted as a formal model for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. the model-checking problem of prs against action-based linear temporal logic (altl) is undecidable. however, decidability for some interesting fragment of altl remains an open question. in this paper, we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewriting) in prs. as a consequence, we obtain decidability of the model-checking problem (restricted to infinite runs) of prs against a meaningful fragment of altl.
labelled domains and automata with concurrency. we investigate an operational model of concurrent systems, called automata with concurrency relations. these are labelled transition systems a in which the event set is endowed with a collection of binary concurrency relations which indicate when two events, in a particular state of the automaton, commute. this model generalizes asynchronous transition systems, and as in trace theory we obtain, through a permutation equivalence for computation sequences of a , an induced domain da, &le; . here, we construct a categorical equivalence between a large category of (&ldquo;cancellative&rdquo;) automata with concurrency relations and the associated domains. we show that each cancellative automaton can be reduced to a minimal cancellative automaton generating, up to isomorphism, the same domain. furthermore, when fixing the event set, this minimal automaton is unique. &mdash;authors' abstract
finite graph automata for linear and boundary graph languages. graph grammars can be regarded as a generalization of context-free grammars from strings to graphs. over the past 30 years a rich theory of graph grammars and their languages has been developed. however, there are no graph automata. there is no duality between generative and recognizing devices, as it is known for the chomsky hierarchy of formal languages.here we introduce graph automata as devices for the recognition of sets of undirected node labelled graphs. a graph automaton consists of a finite state control, a finite set of instructions, and a collection of heads or guards. it reads an input graph in a systematic way and performs a graph search directed by the instructions. as our main results we show that finite graph automata recognize exactly the set of graph languages generated by linear nce graph grammars and that alternating finite graph automata recognize exactly the languages of boundary graph grammars. finally, we generalize some automata theoretic properties from string to graph automata, integrate the connectivity of graphs into graph automata, and explain why graph automata cannot be generalized to deal with dynamic edge relabellings and ence graph languages.
tree spanners on chordal graphs: complexity and algorithms. a tree t-spanner t in a graph g is a spanning tree of g such that the distance in t between every pair of vertices is at most t times their distance in g. the tree t-spanner problem asks whether a graph admits a tree t-spanner, given t. we substantially strengthen the hardness result of cai and corneil (siam j. discrete math. 8 (1995) 359-387) by showing that, for any t ≥ 4, tree t-spanner is np-complete even on chordal graphs of diameter at most t + 1 (if t is even), respectively, at most t + 2 (if t is odd). then we point out that every chordal graph of diameter at most t - 1 (respectively, t - 2) admits a tree t-spanner whenever t ≥ 2 is even (respectively, t ≥ 3 is odd), and such a tree spanner can be constructed in linear time.the complexity status of tree 3-spanner still remains open for chordal graphs, even on the subclass of undirected path graphs that are strongly chordal as well. for other important subclasses of chordal graphs, such as very strongly chordal graphs (containing all interval graphs), 1-split graphs (containing all split graphs) and chordal graphs of diameter at most 2, we are able to decide tree 3-spanner efficiently.
recursive quasi-metric spaces. in computable analysis recursive metric spaces play an important role, since these are, roughly speaking, spaces with computable metric and limit operation. unfortunately, the concept of a metric space is not powerful enough to capture all interesting phenomena which occur in computable analysis. some computable objects are naturally considered as elements of asymmetric spaces which are not metrizable. nevertheless, most of these spaces are t0-spaces with countable bases and thus at least quasi-metrizable. we introduce a definition of recursive quasi-metric spaces in analogy to recursive metric spaces. we show that this concept leads to similar results as in the metric case and we prove that the most important spaces of computable analysis can be naturally considered as recursive quasi-metric spaces. especially, we discuss some hyper and function spaces.