Technical reports
Local computation of alternating fixed-points
Henrik Reif Anderson
June 1992, 21 pages
DOI: 10.48456/tr-260
Abstract
In this paper we consider the problem of alternating fixed-points of monotone functions on finite boolean lattices. We describe a local (demand-driven, lazy) algorithm for computing a boolean expression with two alternating fixed-points, i.e. with a minimal and a maximal fixed-point intertwined. Such expressions arise naturally in the modal μ-calculus and are the main source of its expressive power – and its difficult model checking problem. By a translation of the model checking problem of the modal μ-calculus into a problem of finding fixed-points on boolean lattices, we get a local model checker for two alternating fixed-points which runs in time O(|A|(|T|²)log(|A||T|)), where |A| is the size of the assertion and |T| the size of the model, a labelled transition system. This extends earlier results by the author and improves on earlier published local algorithms. We also sketch how the algorithm can be extended to arbitrary alternations.
Due to the generality of the algorithm it can be applied to other (alternating or non-alternating) fixed-point problems.
Full text
PDF (1.4 MB)
BibTeX record
@TechReport{UCAM-CL-TR-260, author = {Anderson, Henrik Reif}, title = {{Local computation of alternating fixed-points}}, year = 1992, month = jun, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-260.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-260}, number = {UCAM-CL-TR-260} }