MODEL CHECKING AND BOOLEAN GRAPHS

We describe a method for translating a satisfaction problem of the mod al mu-calculus into a problem of finding a certain marking of a boolea n graph. By giving algorithms to solve the graph problem, we present a global model checking algorithm for a subset of the modal mu-calculus , which has time-complexity O(\A\\T\), where \A\ is the size of the as sertion and \T\ is the size of the model (a labelled transition system ). This algorithm is extended to an algorithm for the full modal mu-ca lculus running in time O(\A\ad\S\ad-1\T\), where ad is the alternation depth and \S\ is the number of states in the transition system, impro ving on earlier presented algorithms. Moreover, a local algorithm is p resented for alternation depth one. This algorithm runs in time O(\A\\ T\ log(\A\\T\)) and is also an improvement over earlier algorithms.