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)


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:
IITH CreatorsORCiD
Panduranga Rao, M VUNSPECIFIED
Item Type: Conference or Workshop Item (Paper)
Uncontrolled Keywords: Discrete time Markov chains; Low density; Sampling-based; Show through; Statistical model checking; Temporal logic formula
Subjects: Computer science
Divisions: Department of Computer Science & Engineering
Depositing User: . LibTrainee 2021
Date Deposited: 15 Jul 2021 04:44
Last Modified: 18 Feb 2022 08:54
Publisher URL:
Related URLs:

Actions (login required)

View Item View Item
Statistics for RAIITH ePrint 8329 Statistics for this ePrint Item