An Improved Algorithm for the Evaluation of Alternating Fixpoint Expressions in the mu-Calculus

Author

Jiang, Hua ; Li, Xiang

Author_Institution

Guizhou Univ., Guiyang

fYear

2008

fDate

7-9 April 2008

Firstpage

1245

Lastpage

1248

Abstract

Based on the function monotonicity in the mu- calculus formula, this paper presents a global model-checking algorithm for calculating the alternating nesting mu - calculus formula, whose time complexity is 0((2n +1 )^{lfloor(d+3)I4rfloor} ^{+lfloor(d+2)/4rfloor}) and space complexity is O(dn) . It is the first known algorithm whose space complexity is O(dn) and the exponent part of time complexity is d /2 for a global model-checking algorithm in the full mu- calculus formula at present.

Keywords

computational complexity; formal verification; process algebra; alternating fixpoint expressions; alternating nesting mu-calculus formula; function monotonicity; global model-checking algorithm; space complexity; time complexity; Algorithm design and analysis; Calculus; Circuits; Computer science; Explosions; Information technology; Logic; Polynomials; State-space methods; Model Checking; NP and co-NP problem; calculation complexity; mu-Calculus;

fLanguage

English

Publisher

ieee

Conference_Titel

Information Technology: New Generations, 2008. ITNG 2008. Fifth International Conference on

Conference_Location

Las Vegas, NV

Print_ISBN

0-7695-3099-0

Type

conf

DOI

10.1109/ITNG.2008.93

Filename

4492678

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3290279