Department of Computer Science and Technology

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}
}