Model checking conditional CSL for continuous-time Markov chains

Model checking conditional CSL for continuous-time Markov chains

0.00 Avg rating0 Votes
Article ID: iaor20127402
Volume: 113
Issue: 1-2
Start Page Number: 44
End Page Number: 50
Publication Date: Jan 2013
Journal: Information Processing Letters
Authors: , , ,
Keywords: simulation, stochastic processes
Abstract:

In this paper, we consider the model‐checking problem of continuous‐time Markov chains (CTMCs) with respect to conditional logic. To the end, we extend Continuous Stochastic Logic introduced in Aziz et al. (2000) [1] to Conditional Continuous Stochastic Logic (CCSL) by introducing a conditional probabilistic operator. CCSL allows us to express a richer class of properties for CTMCs. Based on a parameterized product obtained from the CTMC and an automaton extracted from a given CCSL formula, we propose an approximate model checking algorithm and analyse its complexity.

Reviews

Required fields are marked *. Your email address will not be published.