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.     «

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 reach...     »

Diese Arbeit analysiert das Erreichbarkeitsproblem in verallgemeinerten Pushdown-Modellen, alternierenden Pushdown-Systemen und Pushdown-Netzwerken. Ein Pushdown-Netzwerk kann zur Modellierung nebenläufiger Programme verwendet werden. Die Algorithmen hierfür wurden optimiert und in einem Tool namens jMoped implementiert. Die Arbeit berichtet über praktische Experimente mit jMoped. Alternierende Pushdown-Systeme werden als Modell für Autorisierungs- und Reputations-Systeme vorgestellt, deren Fragestellungen sich auf Erreichbarkeitsprobleme in den Modellen reduzieren lassen.     «

Diese Arbeit analysiert das Erreichbarkeitsproblem in verallgemeinerten Pushdown-Modellen, alternierenden Pushdown-Systemen und Pushdown-Netzwerken. Ein Pushdown-Netzwerk kann zur Modellierung nebenläufiger Programme verwendet werden. Die Algorithmen hierfür wurden optimiert und in einem Tool namens jMoped implementiert. Die Arbeit berichtet über praktische Experimente mit jMoped. Alternierende Pushdown-Systeme werden als Modell für Autorisierungs- und Reputations-Systeme vorgestellt, deren Frag...     »