Probabilistic Model Checking for Propositional Projection Temporal Logic

TL;DR

This paper develops a probabilistic model checking approach for Propositional Projection Temporal Logic (PPTL) using normal form graphs and Markov chains, enabling verification of linear-time properties in hardware and software systems.

Contribution

It introduces a novel normal form graph for PPTL and algorithms for generating, determinizing, and minimizing it within a probabilistic model checking framework.

Findings

Defines NFG_inf to capture infinite paths of PPTL formulas

Provides algorithms for generating and determinizing NFG_inf

Enables verification of linear-time properties in probabilistic systems

Abstract

Propositional Projection Temporal Logic (PPTL) is a useful formalism for reasoning about period of time in hardware and software systems and can handle both sequential and parallel compositions. In this paper, based on discrete time Markov chains, we investigate the probabilistic model checking approach for PPTL towards verifying arbitrary linear-time properties. We first define a normal form graph, denoted by NFG_inf, to capture the infinite paths of PPTL formulas. Then we present an algorithm to generate the NFG_inf. Since discrete-time Markov chains are the deterministic probabilistic models, we further give an algorithm to determinize and minimize the nondeterministic NFG_inf following the Safra's construction.