Academic
Publications
Fixpoint Logics over Hierarchical Structures

Fixpoint Logics over Hierarchical Structures,10.1007/s00224-009-9227-1,Theory of Computing Systems / Mathematical Systems Theory,Stefan Göller,Markus

Fixpoint Logics over Hierarchical Structures   (Citations: 4)
BibTex | RIS | RefWorks Download
Hierarchical graph definitions allow a modular description of graphs using mod- ules for the specification of repeated substructures. Beside this modularity, hierarchi- cal graph definitions also allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational com- plexity of decision problems. In this paper, the model-checking problem for the modal µ-calculus and (monadic) least fixpoint logic on hierarchically defined input graphs is investigated. In order to analyze the modal µ-calculus, parity games on hierar- chically defined input graphs are investigated. Precise upper and lower complexity bounds are derived. A restriction on hierarchical graph definitions that leads to more efficient model-checking algorithms is presented.
Journal: Theory of Computing Systems / Mathematical Systems Theory - MST , vol. 48, no. 1, pp. 93-131, 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...In a subsequent conference paper [20], the research program from [32] was extended to parity games and various fixpoint logics...

    Markus Lohrey. Model-Checking Hierarchical Structures

    • ...Our results are collected in Table 1 in Section 2. Proofs that are omitted due to space restrictions can be found in the full version [7]...
    • ...A hierarchical graph definition can be translated in polynomial time into an SLP defining the same structure [7, 16]...

    Stefan Gölleret al. Fixpoint Logics on Hierarchical Structures

    • ...The work since then was focused on recursive systems, with the exception of [12, 17, 20]...
    • ...The closest to our work here is [12], which proved that the model-checking problem for the µ-calculus and hierarchical systems is Pspace-complete (as opposed to the recursive setting, in which µ-calculus model checking is Exptime-complete)...
    • ...As we specify below, the µ-calculus model-checking algorithm that our approach induces enjoys several advantages with respect to the one in [12]...
    • ...While the algorithm in [12] is better than the naive “flattening” approach in terms of space complexity, no attention is given to its time complexity...
    • ...We found no specific analysis of the time complexity of the algorithm in [12]...
    • ...Indeed, while the “flattening” approach for model-checking a µ-calculus formula ’ in a hierarchical system K is exponential only in the nesting depth of K and the alternation depth l of ’, the algorithm in [12] is super-exponential also in the formula and in an expression3 that depends on the number of boxes and...
    • ...Hence, beyond having a polynomial space complexity, the time complexity of our algorithm is usually much better than the one that follows the “flattening” approach, and in all cases it is much better than the one in [12]...
    • ...be solved by solving a polynomial number of parity games, the work in [12] had to provide a special analysis in order to show the weaker result that such games are in NP\co-NP...
    • ...Third, the algorithm presented in [12] does not deal directly with hierarchical systems...
    • ...Finally, unlike the uniform treatment that our approach suggests, the algorithm presented in [12] cannot be easily generalized to handle more settings...
    • ...For example, while it is immediate from our algorithm that the model-checking problem of constant size µ-calculus formulas over hierarchical systems with a constant number of exits is in Ptime, proving the same result in [12] required arguments that are orthogonal to the algorithm there, and are based on Courcelle’s technique for evaluating fixed MSO-formulas over bounded-width graphs...
    • ...Let h be the number of states of A’, observe that |V| = |K| · h, exits(V) = exits(K) · h and the number of sub-arenas of V is h times the number of sub-structures of K. As we show in Theorem 4 our algorithm for solving hierarchical parity games can be implemented in polynomial space, which gives an alternative proof of the Pspace upper bound for the hierarchical µ-calculus model checking given in [12]...

    Benjamin Aminofet al. Improved Model Checking of Hierarchical SystemsI

Sort by: