TY - GEN
T1 - Fully local and efficient evaluation of alternating fixed points
T2 - 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1998, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998
AU - Liu, Xinxin
AU - Ramakrishnan, C. R.
AU - Smolka, Scott A.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1998.
PY - 1998
Y1 - 1998
N2 - We introduce Partitioned Dependency Graphs (PDGs), an abstract framework for the specification and evaluation of arbitrarily nested alternating fixed points. The generality of PDGs subsumes that of similarly proposed models of nested fixed-point computation such as Boolean graphs, Boolean equation systems, and the prepositional modal mu-calculus. Our main result is an efficient local algorithm for evaluating PDG fixed points. Our algorithm, which we call LAFP, combines the simplicity of previously proposed induction-based algorithms (such as Winskel's tableau method for ν-calculus model checking) with the efficiency of semantics-based algorithms (such as the bit-vector method of Cleaveland, Klein, and Steffen for the equational μ-calculus). In particular, LAFP is simply specified, we provide a completely rigorous proof of its correctness, and the number of fixed-point iterations required by the algorithm is asymptotically the same as that of the best existing global algorithms. Moreover, preliminary experimental results demonstrate that LAFP performs extremely well in practice. To our knowledge, this makes LAFP the first efficient local algorithm for computing fixed points of arbitrary alternation depth to appear in the literature.
AB - We introduce Partitioned Dependency Graphs (PDGs), an abstract framework for the specification and evaluation of arbitrarily nested alternating fixed points. The generality of PDGs subsumes that of similarly proposed models of nested fixed-point computation such as Boolean graphs, Boolean equation systems, and the prepositional modal mu-calculus. Our main result is an efficient local algorithm for evaluating PDG fixed points. Our algorithm, which we call LAFP, combines the simplicity of previously proposed induction-based algorithms (such as Winskel's tableau method for ν-calculus model checking) with the efficiency of semantics-based algorithms (such as the bit-vector method of Cleaveland, Klein, and Steffen for the equational μ-calculus). In particular, LAFP is simply specified, we provide a completely rigorous proof of its correctness, and the number of fixed-point iterations required by the algorithm is asymptotically the same as that of the best existing global algorithms. Moreover, preliminary experimental results demonstrate that LAFP performs extremely well in practice. To our knowledge, this makes LAFP the first efficient local algorithm for computing fixed points of arbitrary alternation depth to appear in the literature.
UR - https://www.scopus.com/pages/publications/84947904189
U2 - 10.1007/bfb0054161
DO - 10.1007/bfb0054161
M3 - Conference contribution
AN - SCOPUS:84947904189
SN - 3540643567
SN - 9783540643562
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 5
EP - 19
BT - Tools and Algorithms for the Construction and Analysis of Systems - 4th International Conference, TACAS 1998 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1998, Proceedings
A2 - Steffen, Bernhard
PB - Springer Verlag
Y2 - 28 March 1998 through 4 April 1998
ER -