Probabilistic Model Checking of Incomplete Models

Arora, S and M V, Panduranga Rao (2016) Probabilistic Model Checking of Incomplete Models. In: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. Lecture Notes in Computer Science, 9952 . Springer International Publishing, pp. 62-76. ISBN 978-3-319-47165-5

Full text not available from this repository. (Request a copy)


It is crucial for accurate model checking that the model be a complete and faithful representation of the system. Unfortunately, this is not always possible, mainly because of two reasons: (i) the model is still under development and (ii) the correctness of implementation of some modules is not established. In such circumstances, is it still possible to get correct answers for some model checking queries? This paper is a step towards answering this question. We formulate the problem for the Discrete Time Markov Chains (DTMC) modeling formalism and the Probabilistic Computation Tree Logic (PCTL) query language. We then propose a simple solution by modifying DTMC and PCTL to accommodate three valued logic. The technique builds on existing model checking algorithms and tools, obviating the need for new ones to account for three valued logic. Finally, we provide an experimental demonstration of our approach.

[error in script]
IITH Creators:
IITH CreatorsORCiD
M V, Panduranga RaoUNSPECIFIED
Item Type: Book Section
Uncontrolled Keywords: Probabilistic models, Probabilistic model checking three-valued logic, Discrete time markov chain, Probabilistic computation tree logic
Subjects: Computer science > Big Data Analytics
Divisions: Department of Electrical Engineering
Depositing User: Team Library
Date Deposited: 18 Nov 2016 07:20
Last Modified: 28 Aug 2017 09:54
Publisher URL:
Related URLs:

Actions (login required)

View Item View Item
Statistics for RAIITH ePrint 2884 Statistics for this ePrint Item