Qianli Li
Minnan Normal University

Published : 1 Documents Claim Missing Document
Claim Missing Document
Check
Articles

Found 1 Documents
Search

Local Model Checking Algorithm Based on Mu-calculus with Partial Orders Hua Jiang; Qianli Li; Rongde Lin
TELKOMNIKA (Telecommunication Computing Electronics and Control) Vol 15, No 1: March 2017
Publisher : Universitas Ahmad Dahlan

Show Abstract | Download Original | Original Source | Check in Google Scholar | DOI: 10.12928/telkomnika.v15i1.3546

Abstract

The propositionalμ-calculus can be divided into two categories, global model checking algorithm and local model checking algorithm. Both of them aim at reducing time complexity and space complexity effectively. This paper analyzes the computing process of alternating fixpoint nested in detail and designs an efficient local model checking algorithm based on the propositional μ-calculus by a group of partial ordered relation, and its time complexity is O(d2(dn)d/2+2) (d is the depth of fixpoint nesting,  is the maximum of number of nodes), space complexity is O(d(dn)d/2). As far as we know, up till now, the best local model checking algorithm whose index of time complexity is d. In this paper, the index for time complexity of this algorithm is reduced from d to d/2. It is more efficient than algorithms of previous research.