Model checking and Boolean graphs

Abstract

This paper describes a method for translating a satisfaction problem of the modal μ-calculus into a problem of finding a certain marking of a boolean graph. By giving algorithms to solve the graph problem, we present a global model checking algorithm for the modal μ-calculus of alternation depth one, which has time-complexity |A║T|, where |A| is the size of the assertion and |T| is the size of the model (a labelled transition system). This algorithm extends to an algorithm for the full modal μ-calculus which runs in time (|A║T|)ad, where ad is the alternation depth, improving on earlier presented algorithms. Moreover, a local algorithm is presented for alternation depth one, which runs in time |A║T|log(|A║T|), improving on the earlier published algorithms that are all at least exponential.