数据仓库系统中层次式Cube存储结构

区域查询是数据仓库上支持联机分析处理(on-line analytical processing,简称OLAP)的重要操作.近几年,人们提出了一些支持区域查询和数据更新的Cube存储结构.然而这些存储结构的空间复杂性和时间复杂性都很高,难以在实际中使用.为此,提出了一种层次式Cube存储结构HDC(hierarchical data cube)及其上的相关算法.HDC上区域查询的代价和数据更新代价均为O(log^dn),综合性能为O((logn)^2d)(使用C_qC_u模型)或O(K(logn)^d)(使用C_qn_q+C_un_u模型).理论分析与实验表明,HDC的区域查询代价、数据更新代价、空间代价以及综合性能都优于目前所有的Cube存储结构.     

面向数值型敏感属性的隐私保护方案

针对现有的个性化隐私匿名技术不能很好地解决数值型敏感属性容易遭受近邻泄漏的问题,提出了一种基于聚类技术的匿名模型——（ε_i,k）-匿名模型.该模型首先基于聚类技术将按升序排列的敏感属性值划分到几个值域区间内;然后,提出了针对数值型敏感属性抵抗近邻泄漏的（ε_i,k）-匿名原则;最后,提出了一种最大桶优先算法来实现（ε_i,k）-匿名原则.实验结果表明,与已有的面向数值型敏感属性抗近邻泄漏方案相比,该匿名方案信息损失降低,算法执行效率提高,可以有效地降低用户隐私泄露风险.     

关于有ω-穷自动机的两个新的接受条件*

至今被公开的ω-有穷自动机的接受条件有6个即C₁—C₆，寻找新的接受条件和研究ω-有穷自动机关于新接受条件接受ω-语言的能力是ω-有穷自动机理论中的一个重要课题．本文定义了ω-有穷自动机的两个新的接受条件Z₁和Z₂，并且研究了：(1)ω-U—NFA关于Z_i(i=1,2)接受 ω-语言的能力，得到了 N     

基于余归纳的最小Kripke结构的求解

状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：（1） 对于任意给定的一类Kripke结构（记为K）,在互模拟等价意义下K中最小Kripke结构（记为K₀）的存在唯一性.K₀描述了K中所有Kripke结构的行为而且没有冗余的状态;（2） 对于任意的M∈K（M可能包含无穷多个状态）,在互模拟等价意义下的相对于（M且基于K₀）的最小Kripke结构（记为K_M）的存在唯一性.由此提出一种求解K_M的算法,并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的K_M代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.     

关于二元延迟3步前馈逆有限自动机的结构

前馈逆有限自动机的结构是有限自动机可逆性理论中的基本问题.对延迟步数≥3的前馈逆结构的刻划,则是一个长期的未解决问题.研究了二元延迟3步前馈逆有限自动机的结构.对于自治有限自动机M_a的状态图为圈的二元延迟3步弱可逆半输入存储有限自动机C(M_af ),给出了其长3极小输出权分别为1,2,8三种情形下结构的一种刻画.由于C(M_af )延迟3步弱可逆当且仅当它是延迟3步弱逆,因此,得到了二元延迟3步前馈逆有限自动机结构的一种部分刻画.     

不同通信模型下的全光树环网波长分配算法

研究了波分复用全光树环网在不同通信模型下的波长分配算法及其最坏性能分析.对于静态模型,证明了5L/2是树环网所需波长数的紧界.对于动态模型,提出了一种近似比为∑_i=1^hmax_r∈Ri[log|V(r)|]+h的波长分配算法,其中h为树环网的基树的层数,R_i为树环网中处于第i层的环的集合,|V(r)|为环r上的节点数.对于增量模型,提出了一种近似度为O[log₂(t+1)]的波长分配算法,其中t为树环网中的环数.     

近似最近邻归约问题在泊松点过程上的再研究

在已发表文献中, 研究了基于图灵归约求解$ \varepsilon $-NN的问题, 即给定查询点q、点集P及近似参数$ \varepsilon $, 找到q在P中近似比不超过$ 1 + \varepsilon $的近似最近邻, 并提出了一个具有${\rm{O}}(\log n)$查询时间复杂度的图灵归约算法, 这里的查询时间是调用神谕的次数. 经过对比, 此时间优于所有现存的归约算法. 但是已发表文献中提出的归约算法的缺点在于, 其预处理时间和空间复杂度中有${\rm{O}}({(d/\varepsilon )^d})$的因子, 当维度数d较大或者近似参数$ \varepsilon $较小时, 此因子将变得不可接受. 因此, 重新研究了该归约算法, 在输入点集服从泊松点过程的情况下, 分析算法的期望时间和空间复杂度, 将算法的期望预处理时间复杂度降到${\rm{O}}(n\log n)$, 期望空间复杂度降到${\rm{O}}(n\log n)$, 而期望查询时间复杂度保持${\rm{O}}(\log n)$不变, 从而完成了在已发表文献中所提出的未来工作.     

k-LSAT (k≥3)是NP-完全的

合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNF_≥k是子句长度大于或等于k的CNF公式子类,判定问题LSA(≥k)的NP-完全性与LCNF(≥k)中是否含有不可满足公式密切相关.即LSAT_≥k的NP-完全性取决于LCNF_≥k是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF_≥3和LCNF_≥4中的不可满足公式,并提出公开问题:对于k≥5,LCNF_≥k是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的.     

Fq上具有极大1-error线性复杂度的周期序列

线性复杂度是衡量序列密码学强度的重要指标,设计具有大的线性复杂度和k-error线性复杂度的序列是密码学和通信中的热点问题.Niederreiter首次发现了F_q上许多满足这个要求的周期序列.通过序列的广义离散傅立叶变换构造了一些F_q上具有极大1-error线性复杂度的周期序列,这些结果远远优于已知的结果.     

面向移动对象连续k近邻查询的双层索引结构

移动对象连续k近邻（CKNN）查询是指给定一个连续移动的对象集合,对于任意一个k近邻查询q,实时计算查询q的k近邻并在查询有效时间内对查询结果进行实时更新.现实生活中,交通出行、社交网络、电子商务等领域许多基于位置的应用服务都涉及移动对象连续k近邻查询这一基础问题.已有研究工作解决连续k近邻查询问题时,大多需要通过多次迭代确定一个包含k近邻的查询范围,而每次迭代需要根据移动对象的位置计算当前查询范围内移动对象的数量,整个迭代过程的计算代价占查询代价的很大部分.为此,提出了一种基于网络索引和混合高斯函数移动对象分布密度的双重索引结构（grid GMM index,GGI）,并设计了移动对象连续k近邻增量查询算法（incremental search for continuous k nearest neighbors,IS-CKNN）.GGI索引结构的底层采用网格索引对海量移动对象进行维护,上层构建混合高斯模型模拟移动对象在二维空间中的分布.对于给定的k近邻查询q,IS-CKNN算法能够基于混合高斯模型直接确定一个包含q的k近邻的查询区域,减少了已有算法求解该区域的多次迭代过程;当移动对象和查询q位置发生变化时,进一步提出一种高效的增量查询策略,能够最大限度地利用已有查询结果减少当前查询的计算量.最后,在滴滴成都网约车数据集以及两个模拟数据集上进行大量实验,充分验证了算法的性能.     

Performance analysis of probabilistic timed automata using digital clocks

Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a modelling formalism suitable for describing formally both nondeterministic and probabilistic aspects of real-time systems, and is amenable to model checking against probabilistic timed temporal logic properties. However, the previously developed verification algorithms either suffer from high complexity, give only approximate results, or are restricted to a limited class of properties. In the case of classical (non-probabilistic) timed automata it has been shown that for a large class of real-time verification problems correctness can be established using an integral model of time (digital clocks) as opposed to a dense model of time. Based on these results we address the question of under what conditions digital clocks are sufficient for the performance analysis of probabilistic timed automata and show that this reduction is possible for an important class of systems and properties including probabilistic reachability and expected reachability. We demonstrate the utility of this approach by applying the method to the performance analysis of three probabilistic real-time protocols: the dynamic configuration protocol for IPv4 link-local addresses, the IEEE 802.11 wireless local area network protocol and the IEEE 1394 FireWire root contention protocol.

An Efficient Algorithm for Minimizing Real-Time Transition Systems

We address the problem of performing simultaneously reachability analysis and minimization of real-time transition systems represented by timed automata, i.e., automata extended with a finite set of clock variables. The transitions of the automaton may depend on the values of the clocks and may reset some of the clocks. An efficient algorithm is presented for minimizing a system with respect to a given initial partition that respects the enabling conditions of the transitions of the timed automaton. Our algorithm generates the portion of the minimized system that is reachable from a given initial configuration in time polynomial in the input and the size of the minimal reachable system.     

Dynamical Properties of Timed Automata

Timed automata are an important model for specifying and analyzing real-time systems. The main analysis performed on timed automata is the reachability analysis. In this paper we show that the standard approach for performing reachability analysis is not correct when the clocks drift even by a very small amount. Our formulation of the reachability problem for timed automata is as follows: we define the set R ^*(T,Z ₀)=_>0 Reach(T, Z ₀ where T is obtained from timed automaton T by allowing an drift in the clocks. R ^*(T,Z ₀) is the set of states which can be reached in the timed automatonT from the initial states in Z₀ when the clocks drift by an infinitesimally small amount. We present an algorithm for computing R ^*(T,Z ₀)and provide a proof of its correctness. We show that R ^*(T,Z ₀)is robust with respect to various types of modeling errors. To prove the correctness of our algorithm, we need to understand the dynamics of timed automata—in particular, the structure of the limit cycles of timed automata.     

Communication Complexity Method for Measuring Nondeterminism in Finite Automata

While deterministic finite automata seem to be well understood, surprisingly many important problems concerning nondeterministic finite automata (nfa's) remain open. One such problem area is the study of different measures of nondeterminism in finite automata and the estimation of the sizes of minimal nondeterministic finite automata. In this paper the concept of communication complexity is applied in order to achieve progress in this problem area. The main results are as follows:1. Deterministic communication complexity provides lower bounds on the size of nfa's with bounded unambiguity. Applying this fact, the proofs of several results about nfa's with limited ambiguity can be simplified and presented in a uniform way.2. There is a family of languages KON_k² with an exponential size gap between nfa's with polynomial leaf number/ambiguity and nfa's with ambiguity k. This partially provides an answer to the open problem posed by B. Ravikumar and O. Ibarra (1989, SIAM J. Comput.18, 1263–1282) and H. Leung (1998, SIAM J. Comput.27, 1073–1082).     

Exact Acceleration of Real-Time Model Checking

Different time scales do often occur in real-time systems, e.g., a polling real-time system samples the environment many times per second, whereas the environment may only change a few times per second. When these systems are modeled as (networks of) timed automata, the validation using symbolic model checking techniques can significantly be slowed down by unnecessary fragmentation of the symbolic state space. This paper introduces a syntactical adjustment to a subset of timed automata that addresses this fragmentation problem and that can speed-up forward symbolic reachability analysis in a significant way. We prove that this syntactical adjustment does not alter reachability properties and that it indeed is effective. We illustrate our exact acceleration technique with run-time data obtained with the model checkers Uppaal and Kronos. Moreover, we demonstrate that automated application of our exact acceleration technique can significantly speed-up the verification of the run-time behavior of LEGO Mindstorms programs.     

An extension of the inverse method to probabilistic timed automata

Probabilistic timed automata can be used to model systems in which probabilistic and timing behaviour coexist. Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation π ₀ of the timing parameters. Given such a parameter valuation, we present a method for obtaining automatically a constraint K ₀ on timing parameters for which the reachability probabilities (1) remain invariant and (2) are equal to the reachability probabilities for the reference valuation. The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the “inverse method”. The method presents the following advantages. First, since K ₀ corresponds to a dense domain around π ₀ on which the system behaves uniformly, it gives us a measure of robustness of the system. Second, it allows us to obtain a valuation satisfying K ₀ which is as small as possible while preserving reachability probabilities, thus making the probabilistic analysis of the system easier and faster in practice. We provide examples of the application of our technique to models of randomized protocols, and introduce an extension of the method allowing the generation of a “probabilistic cartography” of a system.     

On the optimal reachability problem of weighted timed automata

We study the cost-optimal reachability problem for weighted timed automata such that positive and negative costs are allowed on edges and locations. By optimality, we mean an infimum cost as well as a supremum cost. We show that this problem is PSpace-Complete. Our proof uses techniques of linear programming, and thus exploits an important property of optimal runs: their time-transitions use a time τ which is arbitrarily close to an integer. We then propose an extension of the region graph, the weighted discrete graph, whose structure gives light on the way to solve the cost-optimal reachability problem. We also give an application of the cost-optimal reachability problem in the context of timed games. Research supported by the FRFC project “Centre Fédéré en Vérification” funded by the Belgian National Science Foundation (FNRS) under grant nr 2.4530.02.     

Computing Accumulated Delays in Real-time Systems

We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem.     

Fault diagnosis of timed discrete event systems using Dioid Algebra

This paper deals with the fault diagnosis problem in a concurrent Timed Discrete Event System (TDES). In a TDES, concurrency leads to more complexity in the diagnoser and appears where, at a certain time, some user must choose among several resources. To cope with this problem, a new model-based diagnoser is proposed in this paper. This diagnoser uses Durational Graph (DG), a main subclass of timed automata for representing the time evolution of the TDES. The proposed diagnoser predicts all possible timed-event trajectories that may be generated by the DG. This prediction procedure is complicated for nondeterministic DG’s that are obtained for concurrent TDES’s. To solve this problem, a new Dioid Algebra, Union-Plus Algebra is introduced in this paper. Based on this Algebra, a reachability matrix is defined for a DG that plays an essential role in predicting the time behavior of TDES. By using reachability matrix, a prediction procedure is carried on via an effective equation set that is similar to linear system state equations in ordinary algebra. These results provide a suitable framework for designing an observer-based diagnoser that is illustrated by an example.     

Updatable timed automata with one updatable clock

Updatable timed automata (UTAs) proposed by Bouyer et.al., is an extension of timed automata (TAs) having the extra ability to update clocks in a more elaborate way than simply reset them to zero. The reachability of UTAs is generally undecidable, which can be easily gained by regarding a pair of clocks as updatable counters. This paper investigates a subclass of UTAs by restricting the number of updatable clocks to be one. We will show that (1) the reachability of general UTAs with one updatable clock (UTA1s) is still undecidable, and (2) that of UTA1s under diagonal-free constraints is decidable, and the complexity is Pspace-complete. The former is achieved by encoding Minsky machines to the general UTA1s, where two counters are simulated by the updatable clock. The latter is gained by regarding a region of a UTA1 to be an unbounded digiword, and encoding sets of digiwords that are accepted by a one counter automaton where regions are generated as the value of the counter.