Reference:

Dejvuth Suwimonteerabuth, Stefan Schwoon, and Javier Esparza. Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In Susanne Graf and Wenhui Zhang, editors, 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 4218 of Lecture Notes in Computer Science, pages 141–153, Beijing, China, October 2006. Springer.

Abstract:

Motivated by recent applications of pushdown systems to computer security problems, we present an efficient algorithm for the reachability problem of alternating pushdown systems. Although the algorithm is exponential, a careful analysis reveals that the exponent is usually small in typical applications. We show that the algorithm can be used to compute winning regions in pushdown games. In a second contribution, we observe that the algorithm runs in polynomial time for a certain subproblem, and show that the computation of certificate chains with threshold certificates in the SPKI/SDSI authorization framework can be reduced to this subproblem. We present a detailed complexity analysis of the algorithm and its application, and report on experimental results obtained with a prototype implementation.

Suggested BibTeX entry:

@inproceedings{SSE06b,
    address = {Beijing, China},
    author = {Dejvuth Suwimonteerabuth and Stefan Schwoon and Javier Esparza},
    booktitle = {4th International Symposium on Automated Technology for Verification and Analysis (ATVA)},
    editor = {Susanne Graf and Wenhui Zhang},
    month = {October},
    pages = {141--153},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains},
    volume = {4218},
    year = {2006}
}