Temporal Logic of Stochastic Actions for Verification of Probabilistic Systems

摘要：

　　The specification and verification of probabilistic systems were usually based on Computational Tree Logic,and systems and properties were specified by different language respectively.This paper extends and reforms Temporal Logic of Actions,puts foreword Temporal Logic of Stochastic Actions(TLSA),which can use additional state-action probabilistic distribution and probabilistic operator to specify probabilistic systems and their properties in the same logic.

关键词： Specifying systems System verification TLA Probabilistic systems

作者: LI Jun-tao LONG Shi-gong

作者单位: Information College Guizhou University of Finance and Economic Guiyang,china Computer Science and Technology College Guizhou University Guiyang,china

会议类型: 国际会议

会议名称: The 14th International Symposium on Distributed Computing and Applications to Business,Engineering and Science(DCABES 2015)(第十四届分布式计算及其应用国际学术研讨会)

会议地点: 贵阳

会议语种:英文

页码: 62-65

在线出版日期: 2015-08-18（万方平台首次上网日期，不代表论文的发表时间）