A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking

Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and continuous time, respectively. In PCTL and CSL, the possibility of executions satisfying some temporal properties can be quant...

Full description

Bibliographic Details
Main Authors: Takashi Tomita, Shigeki Hagihara, Naoki Yonezaki
Format: Article
Language:English
Published: Open Publishing Association 2011-11-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1111.3111v1