On the structure of graphs in the Caucal hierarchy

We investigate the structure of graphs in the Caucal hierarchy. We provide criteria concerning the degree of vertices or the length of paths which can be used to show that a given graph does not belong to a certain level of this hierarchy. Each graph in the Caucal hierarchy corresponds to the configuration graph of some higher-order pushdown automaton. The main part of the paper consists of a study of such configuration graphs. We provide tools to decompose and reassemble their runs, and we prove a pumping lemma for higher-order pushdown automata.     

The fixed point theory of unbounded non-determinism

This paper presents a fixed point theorem for the infinite traces model of CSP. Unlike any other model of CSP, there is no complete partial order over the infinite traces model whose fixed point theory agrees with the operational semantics (A. W. Roscoe, Oxford University Computing Laboratory Technical Monograph PRG-67, 1988). This arises from the introduction of unbounded non-determinism. However, the subset of pre-deterministic processes, that is those which describe the behaviour of a process on some run of its implementation, do form a subset for which the usual order is complete. By requiring that each CSP operator has a monotonic implementation which preserves pre-determinism, it is possible to show that all CSP operators have a least fixed point. In effect, it is the requirement that all operators have a methodical implementation.The author carried out the research for this paper on the Espirit Genesis project at the Programming Research Group, Oxford University.     

A semantic measure of the execution time in linear logic

We give a semantic account of the execution time (i.e. the number of cut elimination steps leading to the normal form) of an untyped MELL net. We first prove that: (1) a net is head-normalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and (2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then give a semantic measure of execution time: we prove that we can compute the number of cut elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut-link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the untyped lambda-calculus.     

On the complexity of extension checking in default logic

The complexity of deciding equivalence of a formula to an extension of a default theory is investigated for the Reiter, justified, constrained, and rational semantics.     

On the parameterized complexity of d-dimensional point set pattern matching

Deciding whether two n-point sets A,B∈Rd are congruent is a fundamental problem in geometric pattern matching. When the dimension d is unbounded, the problem is equivalent to graph isomorphism and is conjectured to be in FPT.When |A|=m<|B|=n, the problem becomes that of deciding whether A is congruent to a subset of B and is known to be NP-complete. We show that point subset congruence, with d as a parameter, is W[1]-hard, and that it cannot be solved in O(mno(d))-time, unless SNP⊂DTIME(²o(n)). This shows that, unless FPT=W[1], the problem of finding an isometry of A that minimizes its directed Hausdorff distance, or its Earth Mover's Distance, to B, is not in FPT.     

On the fixed points of the iterated pseudopalindromic closure operator

First introduced in the study of the Sturmian words by de Luca in 1997, iterated palindromic closure was generalized to pseudopalindromes by de Luca and De Luca in 2006. This operator allows one to construct words with infinitely many pseudopalindromic prefixes, called pseudostandard words. We provide here several combinatorial properties of the fixed points under iterated pseudopalindromic closure.     

Acceleration schemes with application to the EM algorithm

New acceleration schemes and restarting procedures are defined and studied in view of application to the EM algorithm. In most cases the introduced algorithms circumvent the problems of stagnation and degeneracy. Their behavior is analyzed on real data sets.     

On the power of real-time two-way multihead finite automata with jumps

We investigate the relative power of jumps, nondeterminism, and number of heads for real-time automata. Results include showing that jumps and power that cannot be compensated for by nondeterminism and more heads. We also show that k+1 heads are more powerful than k heads, even if the finite automaton is allowed head to head jumps.     

Subword complexity of uniform D0L words over finite groups

We deal with the subword complexity of uniform D0L words obtained from group substitutions. Our main interest is whether the subword complexity is “almost proportional” to the length of the factor. We find necessary and sufficient conditions for that. For some cases we show that this is impossible.     

基于多项Logit模型网上订单的最佳配送时间实证分析

随着互联网的不断普及和飞速发展,上网购买商品正成为人们日常消费的主要方式之一,提供网上购物服务的商家也日益增多.但不同的商家所提供的商品的价格、服务质量不尽相同,因此,商品的价格、订单配送时间的长短等都是影响顾客与商家的买卖是否成交的重要因素.本文就是站在商家的立场上,从顾客对商家所提供的商品价格、服务满意度出发,建立一个顾客选择商家的数学模型——多项Logit模型,然后再以商家的期望收益最大为目标,确定最佳的顾客订单指定配送时间.     

On the Relationship Between BDI Logics and Standard Logics of Concurrency

The behavior of an agent is mainly governed by the specific way in which it handles the rational balance between information and deliberation. Rao and Georgeff's BDI theory is most popular among the formalisms capturing this very balance. This formalism has been proposed as a language for specifying agents in an abstract manner or, alternatively, for verifying various properties of agents implemented in some other programming language. In mainstream computer science, there are formalisms designed for a purpose similar to the BDI theory; not specifically aiming at agents, but at concurrency in general. These formalisms are known as logics of concurrent programs. In this paper these two frameworks are compared with each other for the first time. The result shows that the basic BDI theory, BDI_CTL*, can be captured within a standard logic of concurrency. The logic which is relevant here is Kozen's propositional -calculus. -calculus turns out to be even strictly stronger in expressive power than BDI_CTL* while enjoying a computational complexity which is not higher than that of BD_CTL*'s small fragment CTL. This correspondence puts us in a position to provide the first axiomatization of Rao and Georgeff's full theory. Immediate consequences for the computational complexity of BDI theory are also explored, both for theorem proving and model checking.