Reasoning about efficiency within a probabilistic μ-calculus

作     者：A.K. McIver 

作者机构：Programming Research Group Oxford University UK 

出 版 物：《Electronic Notes in Theoretical Computer Science》 

年 卷 期：1999年第22卷

页      面：138-155页

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Probabilistic semantics predicate transformers nondeterminism verification refinement imperative programming time efficiency, complexity 

摘      要：Expectation-based probabilistic predicate transformers [15] provide a logic for probabilistic sequential programs, giving access to expressions such as ‘the probability that predicate A is achieved finally’. Using expectations more generally however, we can express μ-calculus formulae for the expected path-length of a computation tree. Moreover within an expectation-based μ-calculus such efficiency measures and more conventional (but probabilistic) temporal operators [14] can be related.