Polytime model checking for timed probabilistic computation tree logic

We consider the model checking problem for Timed Probabilistic Computation Tree Logic (TPCTL) introduced by H.A. Hansson and D. Jonsson, and studied in a recent book by H.A. Hansson [Han94]. The semantics of TPCTL is defined in terms of probabilistic transition systems. It is shown in [Han94] that model checking for TPCTL has exponential time complexity, the latter being measured in terms of the size of formula, the size of transition system and the value of explicit time that appears in the formula. Besides that, [Han94] describes some polytime decidable classes, the proofs being rather voluminous. We show, by a short proof, that this model checking problem is polytime decidable in the general case. The proof is essentially based on results on the complexity of Markov decision processes. Received: 2 May 1996 / 5 January 1998     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

Language-measure-theoretic optimal control of probabilistic finite-state systems

Supervisory control theory for discrete event systems, introduced by Ramadge and Wonham, is based on a non-probabilistic formal language framework. However, models for physical processes inherently involve modelling errors and noise-corrupted observations, implying that any practical finite-state approximation would require consideration of event occurrence probabilities. Building on the concept of signed real measure of regular languages, this paper formulates a comprehensive theory for optimal control of finite-state probabilistic processes. It is shown that the resulting discrete-event supervisor is optimal in the sense of elementwise maximizing the renormalized langauge measure vector for the controlled plant behaviour and is efficiently computable. The theoretical results are validated through several examples including the simulation of an engineering problem.     

具有多值决策过程的广义可能性计算树逻辑模型检测

模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证,在可能性理论、多值逻辑的基础上,研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法,及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型,用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法,该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题,给出一个具体的应用实例。     

ACTLW - An action-based computation tree logic with unless operator

Model checkers for systems represented by labelled transition systems are not as extensively used as those for systems represented by Kripke structures. This is partially due to the lack of an elegant formal language for property specification which would not be as raw as, for example, HML yet also not as complex as, for example, μ-calculus. This paper proposes a new action-based propositional branching-time temporal logic ACTLW, which enhances popular computation tree logic (CTL) with the notion of actions in a similar but more comprehensive way than action-based CTL introduced by De Nicola and Vaandrager [R. De Nicola, F.W. Vaandrager, Action versus logics for transition systems, in: Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, LNCS 469, 1990, pp. 407-419]. ACTLW is defined by using temporal operators until and unless only, whereas all other temporal operators are derived from them. Fixed-point characterisation of the operators together with symbolic algorithms for global model checking are shown. Usage of this new logic is illustrated by an example of verification of mutual-exclusion algorithms.     

基于模糊决策过程的模糊计算树逻辑模型检测

针对由数据表述产生的不确定性模糊系统的模型检测问题,给出模糊计算树逻辑模型检测算法。首先,引入模糊决策过程作为此类系统的模型,其最大特点是在迁移过程中对动作的不确定性选择和状态表述的模糊性。然后,在模糊决策过程基础上,给出模糊计算树逻辑的语法和语义。最后,给出模糊计算树逻辑模型检测算法,该算法是将模糊计算树逻辑模型检测问题转换为模糊矩阵的合成运算,其优势是时间复杂度低、计算过程较为简洁。     

Learning probabilistic logic models from probabilistic examples

We revisit an application developed originally using abductive Inductive Logic Programming (ILP) for modeling inhibition in metabolic networks. The example data was derived from studies of the effects of toxins on rats using Nuclear Magnetic Resonance (NMR) time-trace analysis of their biofluids together with background knowledge representing a subset of the Kyoto Encyclopedia of Genes and Genomes (KEGG). We now apply two Probabilistic ILP (PILP) approaches—abductive Stochastic Logic Programs (SLPs) and PRogramming In Statistical modeling (PRISM) to the application. Both approaches support abductive learning and probability predictions. Abductive SLPs are a PILP framework that provides possible worlds semantics to SLPs through abduction. Instead of learning logic models from non-probabilistic examples as done in ILP, the PILP approach applied in this paper is based on a general technique for introducing probability labels within a standard scientific experimental setting involving control and treated data. Our results demonstrate that the PILP approach provides a way of learning probabilistic logic models from probabilistic examples, and the PILP models learned from probabilistic examples lead to a significant decrease in error accompanied by improved insight from the learned results compared with the PILP models learned from non-probabilistic examples.     

Helping by unambiguous computation and probabilistic computation

Schöning [S] introduced a notion of helping and suggested the study of the class P_help(C) of languages that can be helped by oracles in a given classC. He showed that P_help(BPP) is included in ZPP. Later, Ko [K] introduced a weaker notion of helping, called one-sided helping, and proved that P_1-help(BPP) is included in R and that UP is included in P_1-help(UP). The three inverse inclusions are open problems (see [Hem]). Caiet al. [CHV] constructed a relativized world in which the third open inclusion fails. We show relativized worlds in which all three open inclusions fail in a strong way. In particular, we strengthen the result of Caiet al., showing that P_help(UP) is not included in Few. This is obtained as a corollary of a general result that gives sufficient conditions, on a relativizable complexity classC, to ensure the relativized separation of P_help(UP) fromC. Further separations are also derived. The other two open inclusions are showed to fail strongly by the relativized separation of ZPP from P_1-help(AM ∩ co-AM).     

N-tuple algebra-based probabilistic logic

The concept of “probabilistic logic” known in artificial intelligence needs a more through substantiation. A new approach to constructing probabilistic logic based on the n-tuple algebra developed by the author is proposed. A brief introduction is given to the n-tuple algebra and its properties that provide efficient paralleling of algorithms for solving problems of logical analysis of systems in computer implementation are generalized. Methods for solving direct and inverse problems of probabilistic simulation of logical systems are considered.     

Comments on the computation of interval Routh approximants

In Bandyopadhyay et al. (1994, 1997), the Routh approximation method was extended to derive reduced-order interval models for linear interval systems. In this paper, the authors show that: 1) interval Routh approximants to a high-order interval transfer function depend on the implementation of interval Routh expansion and inversion algorithms; 2) interval Routh expansion algorithms cannot guarantee the success in generating a full interval Routh array; 3) some interval Routh approximants may not be robustly stable even if the original interval system is robustly stable; and 4) an interval Routh approximant is in general not useful for robust controller design because its dynamic uncertainties (in terms of robust frequency responses) do not cover those of the original interval system     

A Petri net model for probabilistic logic

In this article we investigate the use of Petri nets for the representation of possible worlds in probabilistic logic. We propose a method to generate possible worlds based upon the reachability tree of the Petri net model. The number of columns in the matrix of possible worlds grows exponentially with the problem size. Nilsson [Proceedings of 1976 National Computer Conference and Readings in Artificial Intelligence, Morgan Kaufmann, Los Altos, CA, 1981, pp. 192-199] suggested a method to generate only those columns of the possible world matrix that are likely to be important for the solution. We provide Petri net models for the method suggested by Nilsson and show that they lead to intuitive and simple computational methods. © 1996 John Wiley & Sons, Inc.     

概率逻辑、不确定逻辑和模糊逻辑之比较

通过一个实例分析比较了概率逻辑、主观概率逻辑、不确定逻辑和模糊逻辑的思想方法。提出了自己的观点：基于数据统计的概率逻辑是最科学的。不确定逻辑比主观概率逻辑更科学。当具有不确定性的原子命题具有独立性时,不确定逻辑和模糊逻辑的观点是一致的。而对于处理带有不确定性的相关性命题,不确定逻辑比模糊逻辑更科学。但是模糊逻辑在建立推理理论方面见长。     

Borel型概率计量逻辑

视全体赋值之集为通常乘积拓扑空间,利用该空间上的Borel概率测度在二值命题逻辑中引入了公式的概率真度概念.该方法既克服了计量逻辑学要求赋值集上的概率测度必须为均匀概率测度的无穷可数乘积的局限,又弥补了概率逻辑学只讲局部而缺乏整体性的不足;证明了计量逻辑学中公式的真度、随机真度以及概率逻辑学中公式的概率等概念都可作为本文提出的概率真度的特例而纳入到统一的框架中,从而实现了计量逻辑学与概率逻辑学的融合与统一;证明了逻辑闭理论与赋值空间中的拓扑闭集是一一对应的以及概率真度函数与赋值空间上的Borel概率测度是一样多的等若干结论;本文的第4节给出了公式的概率真度的公理化定义,证明了公式集上满足Kolmogorov公理的任一[0,1]值函数均可由赋值空间上的某Borel概率测度按本文的方法所表出,从而建立了二值命题逻辑框架下的概率计量逻辑的理论体系.     

Learning hierarchical probabilistic logic programs

Machine Learning - Probabilistic logic programming (PLP) combines logic programs and probabilities. Due to its expressiveness and simplicity, it has been considered as a powerful tool for learning...     

Borel probabilistic and quantitative logic

The present paper introduces the notion of the probabilistic truth degree of a formula by means of Borel probability measures on the set of all valuations,endowed with the usual product topology,in classical two-valued propositional logic.This approach not only overcomes the limitations of quantitative logic,which require the probability measures on the set of all valuations to be the countably infinite product of uniform probability measures,but also remedies the drawback that probability logic behaves onl...     

Reasoning about probabilistic sequential programs in a probabilistic logic

We introduce a notion of strong monotonicity of probabilistic predicate transformers. This notion enables us to establish a normal form theorem for monotone probabilistic predicate transformers. Three other healthiness conditions, namely, conjunctivity, disjunctivity and continuity for probabilistic predicate transformers are also examined, and they are linked to strong monotonicity. A notion of probabilistic refinement index is proposed, and it provides us with a continuous strength spectrum of refinement relations which may be used to describe more flexible refinement between probabilistic programs. A notion of probabilistic correctness is introduced too. We give a probabilistic weakest-precondition, choice and game semantics to the contract language, and present a probabilistic generalization of the winning strategy theorem. Received: 16 April 2002 / 20 January 2003 RID="a" ID="a" This work was partly supported by the National Key Project for Fundamental Research of China (Grant No: 1998030905) and the National Foundation of Natural Sciences of China (Grant No: 60273003)     

一种概率XML数据树的化简算法*

针对概率XML数据树分布节点冗余的问题,提出一种化简概率XML数据树的算法。通过分析概率XML数据树中的路径类型,把概率XML数据树划分为稀疏和紧凑两种形式结构,通过消除概率级联、计算绝对路径的相容类集合和等价类集合等过程把前者变换为后者。理论研究和实例分析表明,该化简算法是有效的,能够解决概率XML数据树的化简问题。     

基于纳米电路的概率逻辑

具有概率特性的逻辑学适合表示纳米器件的状态.本文介绍了该逻辑学和其在计算纳米级门电路的概率分布方面的应用.此应用是基于马尔可夫随机场的新特性:势团势能,初始节点的概率密度.我们利用初级门电路和判断电路证明了该方法的有效性.分析证明器件的概率分布主要依赖于系统结构和温度参数.