The Bouquet Algorithm for Model Checking Unbounded Until Properties

Arora, S. and Panduranga Rao, M. V. (2020) The Bouquet Algorithm for Model Checking Unbounded Until Properties. In: Proceedings - 2020 International Symposium on Theoretical Aspects of Software Engineering, TASE 2020, 11 December 2020 - 13 December 2020.

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

Abstract

The problem of verifying the 'Unbounded Until' fragment in temporal logic formulas has been studied extensively in the past, especially in the context of statistical model checking. Statistical model checking, a computationally inexpensive sampling based alternative to the more expensive numerical model checking technique, presents the following decision dilemma-what length of the sample is enough in general? In this paper, we discuss an algorithm for this problem that combines ideas from graph theory, statistical model checking and numerical model checking. We analyze the algorithm, and show through experiments that this approach outperforms the standard statistical model checking algorithm for verifying unbounded until for low density Discrete Time Markov Chains.

[error in script]

IITH Creators: