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...
Main Authors: | , , |
---|---|
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 |