Generating Probabilistic Temporal Logic Formulas from Probabilistic Scenario-Based Specifications

Probabilistic Timed Property Sequence Chart(PTPSC) is a new scenario-based specification for specifying probabilistic properties. However, there is currently no model checking tool available to verify probabilistic properties specified by PTPSC specifications. Consequently, as a first step to apply probabilistic model checking technique into PTPSC, this paper links PTPSC to probabilistic temporal logic: Continuous Stochastic Logic (CSL). According to the formal syntax of PTPSC we defined previously, a syntax directed translator is defined to automatically translate a PTPSC specification into a CSL formula. Since CSL is a property specification of existing tool PRISM, the practical implication of the construction is that the tool supports for PTPSC specifications by translating PTPSC specifications into CSL formulas.