The Bouquet Algorithm for Model Checking Unbounded Until

TL;DR

This paper introduces a novel algorithm that combines graph theory, statistical, and numerical model checking techniques to efficiently verify the unbounded until property in Markov chains, outperforming standard methods.

Contribution

The paper presents a new algorithm integrating multiple verification techniques specifically for unbounded until properties, improving efficiency over existing statistical model checking methods.

Findings

Outperforms standard statistical model checking for low density DTMCs

Effective in reducing verification time and computational resources

Demonstrated through experimental evaluation

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.