Local Model Checking Algorithm Based on Mu-calculus with Partial Orders
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, n 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.
Keywords: model checking,
propositional mu-calculus, computational complexity, fixpoint, partitioned dependency
graph
Author: Hua Jiang, Qianli Li,
Rongde Lin
Journal Code: jptkomputergg170098
