A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking

Takashi Tomita, Shigeki Hagihara, Naoki Yonezaki

Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and contin…