waashk/dblp huggingface dataset:
a compositional approach to ctl* verification. the paper presents a compositional approach to the verification of ctl* properties over reactive systems. both symbolic model-checking (smc) and deductive verification are considered. both methods are based on two decomposition principles. a general state formula is decomposed into basic state formulas which are ctl* formulas with no embedded path quantifiers. to deal with arbitrary basic state formulas, we introduce another reduction principle which replaces each basic path formula, i.e., path formulas whose principal operator is temporal and which contain no embedded temporal operators or path quantifiers, by a newly introduced boolean variable which is added to the system. thus, both the algorithmic and the deductive methods are based on two statification transformations which successively replace temporal formulas by assertions which contain no path quantifiers or temporal operators. performing these decompositions repeatedly, we remain with basic assertional formulas, i.e., formulas of the form efp and afp for some assertion p. in the model-checking method we present a single symbolic algorithm to verify both universal and existential basic assertional properties. in the deductive method we present a small set of proof rules and show that this set is sound and relatively complete for verifying universal and existential basic assertional properties over reactive systems. together with two proof rules for the decompositions, we obtain a sound and relatively complete proof system for arbitrary ctl* properties. interestingly, the deductive approach for ctl* presented here, offers a viable new approach to the deductive verification of arbitrary ltl formulas.
principality and type inference for intersection types using expansion variables. principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. type inference is the problem of finding a typing for a given term, if possible. we define an intersection type system which has principal typings and types exactly the strongly normalizable λ-terms. more interestingly, every finite-rank restriction of this system (using leivant's first notion of rank) has principal typings and also has decidable type inference. this is in contrast to system f where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). in our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. a unification-based type inference algorithm is presented using a new form of unification, β-unification.
on the longest perpetual reductions in orthogonal expression reduction systems. we study perpetual reductions in orthogonal (or conflict-free) fully extended expression reduction systems (oers). ers is a formalism for rewriting that subsumes term rewriting systems (trss) and the &lgr;-calculus. we design a strategy that, for any given term t in a fully extended oers, constructs a longest reduction starting from t if t is strongly normalizing and otherwise constructs an infinite reduction. we call this strategy a limit strategy. for a large class of oerss a limit strategy is computable. the conservation theorem for fully extended oerss follows easily from the properties of the strategy. we develop a method for computing the lengths of longest developments in oerss. copyright 2001 elsevier science b.v.
relating conflict-free stable transition and event models via redex families. we describe an event-style (or poset) semantics for conflict-free rewrite systems, including term and graph rewriting (possibly with bound variables), the λ-calculus, and other stable transition systems with a residual relation. our interpretation is based on considering redex-families as events. it treats permutation-equivalent reductions as representing the same concurrent computation. due to erasure of redexes, event structures are inadequate for such an interpretation. we therefore extend the prime event structure model in two different but equivalent ways: by axiomatizing permutation-equivalence on finite configurations, and by axiomatizing the erasure of events, for the conflict-free case, and show that these extended models are equivalent to stable transition models with axiomatized residual and family relations. we then construct finitary prime algebraic domains from the set of configurations in these extended models by defining orderings relative to stable sets of 'results'. all useful sets of results for which the normalization (by neededness) theorem can be proved are stable.
the conflict-free reduction geometry. we investigate mutual dependencies of subexpressions of computable expressions in orthogonal rewrite systems, and identify conditions for their independent concurrent computation. to this end, we introduce concepts familiar from ordinary euclidean geometry (such as basis, projection, distance, etc.) for reduction spaces. we show how a basis at an expression can be constructed so that any reduction starting from that expression can be decomposed as the sum of its projections on the axes of the basis. to make the concepts computationally more relevant, we relativize them w.r.t. stable sets of results (such as the set of normal forms, head-normal forms, and weak-head-normal forms, in the λ-calculus), and show that an optimal concurrent computation of an expression w.r.t. s consists of optimal computations of its s-independent subexpressions. all these results are obtained in the framework of deterministic family structures, which are abstract reduction systems with axiomatized residual and family relations on redexes, that model all orthogonal rewrite systems.
parameterized complexity of finding subgraphs with hereditary properties. we consider the parameterized complexity of the following problem under the framework introduced by downey and fellows: given a graph g, an integer parameter k and a nontrivial hereditary property ii, are there k vertices of g that induce a subgraph with property ii? this problem has been proved np-hard by lewis and yannakakis. we show that if ii includes all trivial graphs but not all complete graphs or vice versa, then the problem is complete for the parameterized class w[1] and is fixed parameter tractable otherwise. our proofs of both the tractability and hardness involve nontrivial use of the theory of ramsey numbers.
on algebraic and logical specifications of classes of regular languages. the paper studies classes of regular languages based on algebraic constraints imposed on transitions of automata and discusses issues related to specifications of these classes from algebraic, computational and logical points of view.
collage system: a unifying framework for compressed pattern matching. we introduce a general framework which is suitable to capture the essence of compressed pattern matching according to various dictionary-based compressions. it is a formal system to represent a string by a pair of dictionary d and sequence s of phrases in d. the basic operations are concatenation, truncation, and repetition. we also propose a compressed pattern matching algorithm for the framework. the goal is to find all occurrences of a pattern in a text without decompression, which is one of the most active topics in string matching. our framework includes such compression methods as lempel-ziv family (lz77, lzss, lz78, lzw), re-pair, sequitur, and the static dictionary-based method. the proposed algorithm runs in o((||d|| + |s|)- height(d) + m2 + r) time with o(||d|| + m2) space, where ||d|| is the size of d, |s| is the number of tokens in s, height(d) is the maximum dependency of tokens in d, m is the pattern length, and r is the number of pattern occurrences. for a subclass of the framework that contains no truncation, the time complexity is o(||d|| + |s| + m2 + r).
hypercomputation with quantum adiabatic processes. despite the recursive non-computability of hilbert's tenth problem, we outline and argue for a quantum algorithm that is based on the quantum adiabatic theorem. it is explained how this algorithm can solve hilbert's tenth problem. the algorithm is then considered in the context of several "no-go" arguments against such hypercomputation. logical arguments are usually based on cantor's diagonal technique used for proving non-computability of the turing halting problem, which is related to hilbert's tenth problem. physical arguments are related to the limited computability of a class of quantum computation based on qubits and dimensionally finite quantum logical gates.
scheduling broadcasts with deadlines. we investigate the problem of scheduling broadcasts in data delivering systems via broadcast, where a number of requests from several clients can be simultaneously satisfied by one broadcast of a server. most of prior work has focused on minimizing the total flow time of requests. it assumes that once a request arrives, it will be held until satisfied. in this paper, we are concerned with the situation that clients may leave the system if their requests are still unsatisfied after waiting for some time, that is, each request has a deadline. the problem of maximizing the throughput, for example, the total number of satisfied requests, is developed, and there are given online algorithms achieving constant competitive ratios.
generalizations of suffix arrays to multi-dimensional matrices. we propose multi-dimensional index data structures that generalize suffix arrays to square matrices and cubic matrices. giancarlo proposed a two-dimensional index data structure, the lsuffix tree, that generalizes suffix trees to square matrices. however, the construction algorithm for lsuffix trees maintains complicated data structures and uses a large amount of space. we present simple construction algorithms for multi-dimensional suffix arrays by applying a new partitioning technique to lexicographic sorting. our contributions are the first efficient algorithms for constructing two-dimensional and three-dimensional suffix arrays directly.
online paging and file caching with expiration times. we consider a paging problem in which each page is assigned an expiration time at the time it is brought into the cache. the expiration time indicates the latest time that the fetched copy of the page may be used. requests that occur later than the expiration time must be satisfied by bringing a new copy of the page into the cache. the problem has applications in caching of documents on the world wide web (www). we show that a natural extension of the well-studied least recently used (lru) paging algorithm is strongly competitive for the uniform retrieval cost, uniform size case. we then describe a similar extension of the recently proposed landlord algorithm for the case of arbitrary retrieval costs and sizes, and prove that it is strongly competitive. the results extend to the loose model of competitiveness as well. copyright 2001 elsevier science b.v.
upper bounds for sorting integers on random access machines. two models of random access machines suitable for sorting integers are presented. our main results show that i) a ram with addition, subtraction, multiplication, and integer division can sort $n$ integers in the range $[0,2^{cn}]$ in $o(n \log c + n)$ steps; ii) a ram with addition, subtraction, and left and right shifts can sort any $n$ integers in linear time; iii) a ram with addition, subtraction, and left and right shifts can sort $n$ integers in the range $[0,n^{c}]$ in $o(n \log c + n)$ steps, where all intermediate results are bounded in value by the largest input.
two techniques in the area of the star problem in trace monoids. this paper deals with decision problems related to the star problem in trace monoids which means to determine whether the iteration of a recognizable trace language is recognizable. due to a theorem by richomme (in: i. privara et al. (eds.), mfcs'94 proc., lecture notes in computer science, vol. 841, springer, berlin, 1994, pp. 577-586), we know that the star problem is decidable in trace monoids which do not contain a submonoid of the form {a,c}* × {b,d}*. [cf. theory comput. systems 34(3) (2001) 193-227].here, we consider a more general problem: is it decidable whether for some recognizable trace language r and some recognizable or finite trace language p the intersection r ∩ p* is recognizable? if p is recognizable, then we show that this problem is decidable iff the underlying trace monoid does not contain a submonoid of the form {a, c}* × b*. in the case of finite languages p, this problem is decidable in {a,c}* × b* but undecidable in {a,c}* × {b,d}*.
segmental partially ordered generalized patterns. we continue the study of partially ordered generalized patterns (pogps) considered in [e. babson, e. steingrímsson, generalized permutation patterns and a classification of the mahonian statistics, séminaire lotharingien de combinatoire, 2000, b44b:18pp] for permutations and in [a. burstein, t. mansour, words restricted by patterns with at most 2 distinct letters, electron. j. combin. 9 (2) (2002) #r3] for words. we deal with segmental pogps (spogps). we state some general results and treat a number of patterns of length 4. we prove a result from [s. kitaev, multi-avoidance of generalized patterns, discrete math. 260 (2003) 89-100] in a much simpler way and also establish a connection between spogps and walks on lattice points starting from the origin and remaining in the positive quadrant. we give a combinatorial interpretation of the powers of the (generalized) fibonacci numbers. the entire distribution of the maximum number of non-overlapping occurrences of a generalized pattern with no dashes in permutations or words studied in [s. kitaev, partially ordered generalized patterns, discrete math. to appear, s. kitaev, t. mansour, partially ordered generalized patterns and k-ary words, ann. combin. 7 (2003) 191-200], respectively, has its counterpart in case of spogps.
smoothness prior approach to explore mean structure in large-scale time series. this article is addressed to the problem of modeling and exploring mean value structure of large-scale time series data and time-space data. a smoothness prior modeling approach (smoothness prior analysis of time series, lecture notes in statistics, vol. 116, springer, new york, 1996.) is taken. in this approach, the observed series are decomposed into several components each of which are expressed by smoothness priors models. in the analysis of pos and gps data, various useful information were extracted by this decomposition, and result in discoveries in these areas.
algebraic testing and weight distributions of codes. we study the testing problem, that is, the problem of determining (maybe probabilistically) if a function to which one has oracle access satisfies a given property.we propose a framework in which to formulate and carry out the analysis of several known tests. this framework establishes a connection between testing and the theory of weight distributions of codes. we illustrate this connection by giving a coding theoretic interpretation of several tests that fall under the label of low-degree tests. we also show how the connection naturally suggests a new way of testing for linearity over finite fields.we derive from the macwilliams theorems a general result, the duality testing lemma, and use it to analyze the simpler tests that fall into our framework. in contrast to other analyses of tests, the ones we present elicit the fact that a test's probability of rejecting a fuction depends on how far away the function is from every function that satisfies the property of interest.
the chilean highway problem. we consider the problem faced by a server offering multiple services with adversarial service request sequences. the server may offer a single service at a time and suffers a fixed latency whenever it switches the type of offered service. this problem captures realistic features of traffic and packet routing on network components such as multiplexers. we state the problem as a packet routing problem on bounded size buffer networks and then examine the crucial issue of stability--under what conditions will the number of unserviced requests remain bounded as the system runs for an arbitrarily long period of time? we obtain a tight characterization in terms of a natural packet density criterion for star networks with bounded buffer size.
on floyd and rivest's select algorithm. we show that several versions of floyd and rivest's algorithm select for finding the kth smallest of n elements require at most n + min{k, n - k} + o (n) comparisons on average and with high probability. this rectifies the analysis of floyd and rivest, and extends it to the case of nondistinct elements. our computational results confirm that select may be the best algorithm in practice.
shallow grates. this note proves the existence of acyclic directed graphs of logarithmic depth, such that a superlinear number of input-output pairs remain connected after the removal of any sufficiently small linearly sized subset of the vertices. the technique can be used to prove the analogous, and asymptotically optimal, result for graphs of arbitrary depth, generalizing schnitger''s grate construction for graphs large depth. interest in this question relates to efforts to use graph theoretic methods to prove circuit complexity lower bounds for algebraic problems such as matrix multiplication. in particular, it establishes the optimality of valiant''s depth reduction technique as a method of reducing the number of connected input-output pairs. the proof uses schnitger''s grate construction, but also involves a lemma on expanding graphs which may be of independent interest.
on the least exponential growth admitting uncountably many closed permutation classes. we show that the least exponential growth of counting functions which admits uncountably many closed permutation classes lies between 2n and (2.33529...)n.
deterministic turing machines in the range between real-time and linear-time. deterministic k-tape and multitape turing machines with one-way, two-way and without a separated input tape are considered. we investigate the classes of languages acceptable by such devices with time bounds of the form n + r(n), where r ∈ o(n) is a sublinear function. it is shown that there exist infinite time hierarchies of separated complexity classes in that range. for these classes weak closure properties are proved.
fast one-way cellular automata. space-bounded one-way cellular language acceptors (oca) are investigated. the only inclusion known to be strict in their time hierarchy from real-time to exponential-time is between real-time and linear-time! we show the surprising result that there exists an infinite hierarchy of properly included oca-language families in that range. a generalization of a method in terrier (theoret. comput. sci. 156 (1-2) (1996) 281) is shown which provides a tool for proving that languages are not acceptable by ocas with small time bounds. the hierarchies are established by such a language and a translation result. in addition, a notion of constructibility for cas is introduced, along with some of its properties. we prove several closure properties of the families in the hierarchy.
verified bytecode verifiers. using the theorem prover isabelle/hol we have formalized and proved correct and executable bytecode verifier in the style of kildall's algorithm for a significant subset of the java virtual machine (jvm). first an abstract framework for proving correctness of data flow based type inference algorithms for assembly languages is formalized. it is shown that under certain conditions kildall's algorithm yields a correct bytecode verifier. then the framework is instantiated with our previous work about the jvm. finally, we demonstrate the flexibility of the framework by extending our previous jvm model and the executable bytecode verifier with object initialization.
a tight upper bound for the path length of avl trees. we prove that the internal path length of an avl tree of size $n$ is bounded from above by 1.4404n(\log_2 n-\log_2\log_2 n)+o(n) and show that this bound is achieved by an infinite family of avl trees. but avl trees of maximal height do not have maximal path length. these results carry over to the comparison cost of brother trees.
a ptas for the minimization of polynomials of fixed degree over the simplex. we consider the problem of computing the minimum value pmin taken by a polynomial p(x) of degree d over the standard simplex δ. this is an np-hard problem already for degree d = 2. for any integer k ≥ 1, by minimizing p(x) over the set of rational points in δ with denominator k, one obtains a hierarchy of upper bounds pδ(k) converging to pmin as k → ∞. these upper approximations are intimately linked to a hierarchy of lower bounds for pmin constructed via pólya's theorem about representations of positive forms on the simplex. revisiting the proof of pólya's theorem allows us to give estimates on the quality of these upper and lower approximations for pmin. moreover, we show that the bounds pδ(k) yield a polynomial time approximation scheme for the minimization of polynomials of fixed degree d on the simplex, extending an earlier result of bomze and de klerk for degree d = 2.
deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton. finite automata with weights in the max-plus semiring are considered. the main result is: it is decidable whether a series that is recognized by a finitely ambiguous max-plus automaton is unambiguous, or is sequential. furthermore, the proof is constructive. a collection of examples is given to illustrate the hierarchy of max-plus series with respect to ambiguity.
specification and refinement of mobile systems in mtla and mobile uml. we define the spatio-temporal logic mtla as an extension of lamport's temporal logic of actions tla for the specification, verification, and formal development of systems that rely on mobile code. the formalism is validated by an encoding of models written in the mobile uml notation. we identify refinement principles for mobile systems and justify refinements of mobile uml state machines with the help of the mtla semantics.
the height of a binary search tree: the limiting distribution perspective. we study the height of the binary search tree--the most fundamental data structure used for searching. we assume that the binary search tree is built from a random permutation of n elements. under this assumption, we study the limiting distribution of the height as n → ∞. we show that the distribution has six asymptotic regions (scales). these correspond to different ranges of k and n, where pr{hn ≤ k} is the height distribution. in the critical region (the so-called central region), where most of the probability mass is concentrated, the limiting distribution satisfies a non-linear integral equation. while we cannot solve this equation exactly, we show that both tails of the distribution are roughly of a double exponential form. from our analysis, we conclude that the average height e[hn] ∼ a log n - 3/2[a/(a-1)]log log n, where a = 4.311 ... is the unique solution of x logx - x - xlog2 + 1 = 0, x > 1, while the variance var[hn] = o(1). the second term in the expansion of e[{kn] and the rate of growth of the variance were also recently obtained by b. reed who used probabilistic arguments, while m. drmota established the growth of the variance by analytic methods. our analysis makes certain assumptions about the forms of some asymptotic expansions, as well as their asymptotic matching.