An improved algorithm for the evaluation of fixpoint expressions
作者： A. Browne , E.M. Clarke , S. Jha , D.E. Long , W. Marrero
DOI: 10.1016/S0304-3975(96)00228-9
关键词:
摘要: Many automated finite-state verification procedures can be viewed as fixpoint computations over a finite lattice (typically the powerset of set system states). Hence, calculi such propositional Μ-calculus have proven useful, both ways to describe algorithms and specification formalisms in their own right. We consider problem evaluating expressions calculus given model. A naive algorithm for this task may require time n q , where is maximum length chain depth nesting. In 1986, Emerson Lei presented method requiring about d steps, number alternations between least greatest fixpoints. More recent reduced exponent by one or two, but complexity has remained at nd. paper, we present new that makes extensive use monotonicity considerations solve nd/2 steps. Thus, required our only square root earlier algorithms.
elsevier.com
sci-hub.se 参考文章(19)
E. Allen Emerson, Chin Laung Lei, EFFICIENT MODEL CHECKING IN FRAGMENTS OF THE PROPOSITIONAL MU-CALCULUS. logic in computer science. pp. 267- 278 ,(1986)
Ranee Cleaveland, Marion Klein, Bernhard Steffen, Faster Model Checking for the Modal Mu-Calculus computer aided verification. pp. 410- 422 ,(1992) , 10.1007/3-540-56496-9_32
Kim Guldstrand Larsen, Efficient Local Correctness Checking computer aided verification. pp. 30- 43 ,(1992) , 10.1007/3-540-56496-9_4
Henrik Reif Andersen, Model checking and boolean graphs ESOP '92. ,vol. 126, pp. 1- 19 ,(1992) , 10.1007/3-540-55253-7_1
E. M. Clarke, I. A. Browne, R. P. Kurshan, A unified approach for showing language containment and equivalence between various types of Ω-automata colloquium on trees in algebra and programming. pp. 103- 116 ,(1990) , 10.1007/3-540-52590-4_43
Rance Cleaveland, Bernhard Steffen, A linear-time model-checking algorithm for the alternation-free modal mu-calculus computer aided verification. ,vol. 2, pp. 121- 147 ,(1993) , 10.1007/BF01383878
E.M. Clarke, I.A. Draghicescu, R.P. Kurshan, A unified approach for showing language inclusion and equivalence between various types of Ω-automata Information Processing Letters. ,vol. 46, pp. 301- 308 ,(1993) , 10.1016/0020-0190(93)90069-L
Olivier Coudert, Christian Berthet, Jean Christophe Madre, Verification of synchronous sequential machines based on symbolic execution computer aided verification. ,vol. 407, pp. 365- 373 ,(1989) , 10.1007/3-540-52148-8_30
Colin Stirling, David Walker, Local model checking in the modal mu-calculus international conference on logic programming. ,vol. 89, pp. 161- 177 ,(1991) , 10.1016/0304-3975(90)90110-4
André Arnold, Paul Crubille, A linear algorithm to solve fixed-point equations on transition systems Information Processing Letters. ,vol. 29, pp. 57- 66 ,(1988) , 10.1016/0020-0190(88)90029-4