Reachability in Pushdown Systems: Algorithms and Applications
Dejvuth Suwimonteerabuth · mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich) · 2009
This thesis analyzes reachability in generalized pushdown models, alternating pushdown systems and pushdown networks. A pushdown network can be used for modeling multithreaded programs. The reachability algorithms have been optimized and implemented in a tool called jMoped. Several practical experiments with jMoped are reported. Alternating pushdown systems are shown to be suitable models for authorization systems and reputation systems, where reasoning in the systems boils down to solving reachability in the models.