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

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Hua Jiang Articles by Xiang Li

Fifth International Conference on Information Technology: New Generations (itng 2008)

April 07-April 09

ISBN: 978-0-7695-3099-4

	ASCII Text	x
	Hua Jiang, Xiang Li, "An Improved Algorithm for the Evaluation of Alternating Fixpoint Expressions in the mu-Calculus," Information Technology: New Generations, Third International Conference on, pp. 1245-1248, Fifth International Conference on Information Technology: New Generations (itng 2008), 2008.

	BibTex	x
	@article{ 10.1109/ITNG.2008.93, author = {Hua Jiang and Xiang Li}, title = {An Improved Algorithm for the Evaluation of Alternating Fixpoint Expressions in the mu-Calculus}, journal ={Information Technology: New Generations, Third International Conference on}, volume = {0}, year = {2008}, isbn = {978-0-7695-3099-4}, pages = {1245-1248}, doi = {http://doi.ieeecomputersociety.org/10.1109/ITNG.2008.93}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Information Technology: New Generations, Third International Conference on TI - An Improved Algorithm for the Evaluation of Alternating Fixpoint Expressions in the mu-Calculus SN - 978-0-7695-3099-4 SP1245 EP1248 A1 - Hua Jiang, A1 - Xiang Li, PY - 2008 KW - Model Checking KW - mu-Calculus KW - calculation complexity KW - NP and co-NP problem VL - 0 JA - Information Technology: New Generations, Third International Conference on ER -

Hua Jiang

Xiang Li

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ITNG.2008.93

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 O((2n+1)^((d+3)/4+(d+2)/4)) 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 calculus formula at present.

Index Terms:

Model Checking, mu-Calculus, calculation complexity, NP and co-NP problem

Citation:

Hua Jiang, Xiang Li, "An Improved Algorithm for the Evaluation of Alternating Fixpoint Expressions in the mu-Calculus," itng, pp.1245-1248, Fifth International Conference on Information Technology: New Generations (itng 2008), 2008

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.