Publications

Philipp Rohde: On the $\mu$-Calculus Augmented with Sabotage

In: L. Aceto, A. Ingólfsdóttir (Eds.), Foundations of Software Science and Computation Structures: 9th International Conference, FOSSACS 2006, Vienna, Austria, March 25-31, 2006. Proceedings. Lecture Notes in Computer Science, vol. 3921. Springer-Verlag 2006, pp. 142-156. © Springer

Abstract  |  SpringerLink  |  PDF

Philipp Rohde: Moving in a Crumbling Network: The Balanced Case

In: J. Marcinkowski, A. Tarlecki (Eds.), Computer Science Logic: 18th International Workshop, CSL 2004, Karpacz, Poland, September 20-24, 2004. Proceedings. Lecture Notes in Computer Science, vol. 3210. Springer-Verlag 2004, pp. 310-324. © Springer

Abstract  |  SpringerLink  |  PDF

Christof Löding, Philipp Rohde: Model Checking and Satisfiability for Sabotage Modal Logic

In: P.K. Pandya, J. Radhakrishnan (Eds.), FSTTCS 2003: Foundations of Software Technology and Theoretical Computer Science. 23rd Conference, FSTTCS 2003, Mumbai, India, December 15-17, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2914. Springer-Verlag 2003, pp. 302–313. © Springer

Abstract  |  SpringerLink  |  PDF

Philipp Rohde, Wolfgang Thomas: Ein e-Lecture-System für die Theoretische Informatik

In: A. Bode et. al. (Hrsg.), DeLFI 2003: Die 1. e-Learning Fachtagung Informatik. Tagung der Fachgruppe e-Learning der Gesellschaft für Informatik e.V. (GI), 16.-18. September 2003 in Garching, Proceedings. Lecture Notes in Informatics, vol. P-37. Gesellschaft für Informatik 2003, S. 17-26.

Abstract  |  PDF

Christof Löding, Philipp Rohde: Solving the Sabotage Game is PSPACE-hard

In: B. Rovan, P. Vojtas (Eds.), Mathematical Foundations of Computer Science 2003. 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2747. Springer-Verlag 2003, pp. 531-540. © Springer

Abstract  |  SpringerLink  |  PDF

Philipp Rohde, Wolfgang Thomas: E-Learning in Theoretical Computer Science: Experiences From an Undergraduate Course

In: Annual Report 2002, Department of Computer Science, Aachen University. AIB-01-2003, RWTH Aachen 2003, pp. 11-15.

AIB Server  |  PDF

Eva Giani, Philipp Rohde, Wolfgang Thomas: A Presentation and Tutoring Environment for Courses in Theoretical Computer Science

In: Ch. Jutz et. al. (Eds.), 5th International Conference on New Educational Environments (ICNEE), May 26 - 28, 2003, Lucerne, Switzerland, Proceedings. net4net, Berne 2003, pp. 333-338.

Abstract  |  PDF

Christof Löding, Philipp Rohde: Solving the Sabotage Game is PSPACE-hard

Technical Report AIB-05-2003, RWTH Aachen 2003.

Abstract  |  AIB Server  |  PDF

Philipp Rohde: On the Expressive Power of the Monadic Second Order Logic and the Propositional $\mu$-Calculus

In: E. Grädel et. al. (Eds.), Automata, Logics, and Infinite Games. Lecture Notes in Computer Science, vol. 2500. Springer-Verlag 2002, pp. 239-257. © Springer

Abstract  |  SpringerLink  |  PDF

Benedikt Löwe, Philipp Rohde: Games of length omega times two

Proceedings of the American Mathematical Society 130 (2002), pp. 1247-1248.

Abstract  |  PostScript

Dissertation Thesis

Philipp Rohde: On Games and Logics over Dynamically Changing Structures

Thesis supervisor:	Prof. Dr. Dr.h.c. Wolfgang, Thomas Informatik VII, RWTH Aachen
External evaluator:	Prof. Dr. Johan van Benthem Institute for Logic, Language & Computation, University of Amsterdam Department of Philosophy, Stanford University
Date of oral exam:	December 8, 2005

Abstract  |  PDF

Diploma Thesis

Philipp Rohde: Über Erweiterungen des Axioms der Determiniertheit [On Extensions of the Axiom of Determinacy]

March, 2001

Abstract  |  PDF

Abstracts

On the $\mu$-Calculus Augmented with Sabotage

Philipp Rohde In: L. Aceto, A. Ingólfsdóttir (Eds.), Foundations of Software Science and Computation Structures: 9th International Conference, FOSSACS 2006, Vienna, Austria, March 25-31, 2006. Proceedings. Lecture Notes in Computer Science, vol. 3921. Springer-Verlag 2006, pp. 142-156. We study logics and games over dynamically changing structures. Van Benthem’s sabotage modal logic consists of modal logic with a cross-model modality referring to submodels from which a transition has been removed. We add constructors for forming least and greatest monadic fixed-points to that logic and obtain the sabotage $\mu$-calculus. We introduce backup parity games as an extension of standard parity games where in addition, both players are able to delete edges of the arena and to store, resp., restore the current appearance of the arena by use of a fixed number of registers. We show that these games serve as model checking games for the sabotage $\mu$-calculus, even if the access to registers follows a stack discipline. The problem of solving the games with restricted register access turns out to be PSPACE-complete while the more general games without a limited access become EXPTIME-complete (for at least three registers).

Moving in a Crumbling Network: The Balanced Case

Philipp Rohde In: J. Marcinkowski, A. Tarlecki (Eds.), Computer Science Logic: 18th International Workshop, CSL 2004, Karpacz, Poland, September 20-24, 2004. Proceedings. Lecture Notes in Computer Science, vol. 3210. Springer-Verlag 2004, pp. 310-324. In this paper we continue the study of 'sabotage modal logic' SML which was suggested by van Benthem. In this logic one describes the progression along edges of a transition graph in alternation with moves of a saboteur who can delete edges. A drawback of the known results on SML is the asymmetry of the two modalities of 'moving' and 'deleting': Movements are local, whereas there is a global choice for edge deletion. To balance the situation and to obtain a more realistic model for traffic and network problems, we require that also the sabotage moves (edge deletions) are subject to a locality condition. We show that the new logic, called path sabotage logic PSL, already has the same complexities as SML (model checking, satisfiability) and that it lacks the finite model property. The main effort is finding a pruned form of SML-models that can be enforced within PSL and giving appropriate reductions from SML to PSL.

Model Checking and Satisfiability for Sabotage Modal Logic

Christof Löding, Philipp Rohde In: P.K. Pandya, J. Radhakrishnan (Eds.), FSTTCS 2003: Foundations of Software Technology and Theoretical Computer Science. 23rd Conference, FSTTCS 2003, Mumbai, India, December 15-17, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2914. Springer-Verlag 2003, pp. 302–313. We consider the sabotage modal logic SML which was suggested by van Benthem. SML is the modal logic equipped with a ‘transition-deleting’ modality and hence a modal logic over changing models. It was shown that the problem of uniform model checking for this logic is PSPACE-complete. In this paper we show that, on the other hand, the formula complexity and the program complexity are linear, resp., polynomial time. Further we show that SML lacks nice model-theoretic properties such as bisimulation invariance, the tree model property, and the finite model property. Finally we show that the satisfiability problem for SML is undecidable. Therefore SML seems to be more related to FO than to usual modal logic.

Ein e-Lecture-System für die Theoretische Informatik

Philipp Rohde, Wolfgang Thomas In: A. Bode et. al. (Hrsg.), DeLFI 2003: Die 1. e-Learning Fachtagung Informatik. Tagung der Fachgruppe e-Learning der Gesellschaft für Informatik e.V. (GI), 16.-18. September 2003 in Garching, Proceedings. Lecture Notes in Informatics, vol. P-37. Gesellschaft für Informatik 2003, S. 17-26. Es wird ein e-Lecture-System für die Theoretische Informatik vorgestellt, das seit drei Semestern an der RWTH Aachen für Vorlesungen der Automatentheorie erfolgreich eingesetzt wird. Grundlegende Zielsetzung war, eine einfach zu bedienende und flexible Infrastruktur zu schaffen. Im Zentrum stand dabei eine integrierte und flexibel einsetzbare Technik zur Vorbereitung und Präsentation des Kursmaterials, die sich durch sparsamen Einsatz von personellen und technischen Ressourcen auszeichnet. Wir stellen dieses System vor und diskutieren Erfahrungen und Perspektiven.

Solving the Sabotage Game is PSPACE-hard

Christof Löding, Philipp Rohde In: B. Rovan, P. Vojtas (Eds.), Mathematical Foundations of Computer Science 2003. 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2747. Springer-Verlag 2003, pp. 531-540. We consider the sabotage game as presented by van Benthem. In this game one player moves along the edges of a finite multi-graph and the other player takes out a link after each step. One can consider usual algorithmic tasks like reachability, Hamilton path, or complete search as winning conditions for this game. As the game definitely ends after at most the number of edges steps, it is easy to see that solving the sabotage game for the mentioned tasks takes at most PSPACE in the size of the graph. In this paper we establish the PSPACE-hardness of this problem. Furthermore, we introduce a modal logic over changing models to express tasks corresponding to the sabotage games and we show that model checking this logic is PSPACE-complete.

A Presentation and Tutoring Environment for Courses in Theoretical Computer Science

Eva Giani, Philipp Rohde, Wolfgang Thomas In: Ch. Jutz et. al. (Eds.), 5th International Conference on New Educational Environments (ICNEE), May 26 - 28, 2003, Lucerne, Switzerland, Proceedings. net4net, Berne 2003, pp. 333-338. We report on the development of e-lectures in theoretical computer science (more specifically, automata theory). The emphasis is on the development of a simple and flexible infrastructure, which reduces the effort in preparing e-lectures and tutorial units in this field of study. Two components are essential: an integrated and context-independent hardware and software system for the preparation and presentation of the course material, and a tutorial component with dialogue features, which allows to set up problems accompanying the lectures.

Solving the Sabotage Game is PSPACE-hard

Christof Löding, Philipp Rohde Technical Report AIB-05-2003, RWTH Aachen 2003 We consider the sabotage game presented by van Benthem in an essay on the occasion of Jörg Siekmann's 60th birthday. In this game one player moves along the edges of a finite, directed or undirected multi-graph and the other player takes out a link after each step. There are several algorithmic tasks over graphs which can be considered as winning conditions for this game, for example reachability, Hamilton path or complete search. As the game definitely ends after at most the number of edges (counted with multiplicity) steps, it is easy to see that solving the sabotage game for the mentioned tasks takes at most PSPACE in the size of the graph. We will show that on the other hand solving this game in general is PSPACE-hard for all conditions. We extend this result to some variants of the game (removing more than one edge per round and removing vertices instead of edges). Finally we introduce a modal logic over changing models to express tasks corresponding to the sabotage games. We will show that model checking this logic is PSPACE-complete.

On the Expressive Power of the Monadic Second Order Logic and the Propositional $\mu$-Calculus

Philipp Rohde In: E. Grädel et. al. (Eds.), Automata, Logics, and Infinite Games. Lecture Notes in Computer Science, vol. 2500. Springer-Verlag 2002, pp. 239-257. We consider monadic second order logic (MSO) and the propositional $\mu$-calculus ($L$μ) over transition systems. It is well known that every class of transition systems which is definable by a sentence of $L$μ is definable by a sentence of MSO as well. It will be shown that the converse is also true for an important fragment of MSO: every class of transition systems which is MSO-definable and which is closed under bisimulation - i.e., the sentence does not distinguish between bisimilar models - is also $L$μ-definable. Hence we obtain the following expressive completeness result: the bisimulation invariant fragment of MSO and $L$μ are equivalent. The result was proved by David Janin and Igor Walukiewicz. Our presentation is based on their article [JW96]. The main step is the development of automata-based characterizations of $L$μ over arbitrary transition systems and of MSO over transition trees. It turns out that there is a general notion of automaton subsuming both characterizations, so we obtain a common ground to compare these two logics. Further we need the notion of the $\omega$-unravelling for a transition system, on the one hand to obtain a bisimilar transition tree and on the other hand to increase the possibilities of choosing successors. We start with a section introducing the notions of transition systems and transition trees, bisimulations and the $\omega$-unravelling. In Section 3 we repeat the definitions of MSO and $L$μ. In Section 4 we develop a general notion of automaton and acceptance conditions in terms of games to obtain the characterizations of the two logics. In the last section we will prove the main result mentioned above. Literature [JW96] David Janin and Igor Walukiewicz, On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic, Proceedings of the 7th International Conference on Concurrency Theory, CONCUR'96 (U. Montanari and V. Sassone, eds.), Lecture Notes in Computer Science, vol. 1119, Springer-Verlag, August 1996, pp. 263-277.

Games of length omega times two

Benedikt Löwe, Philipp Rohde Proceedings of the American Mathematical Society 130 (2002), pp. 1247-1248 This note combines an unpublished theorem of Woodin's about AD and Uniformisation with combinatorial arguments of Blass' to get a startling consequence for games on $\omega$ of length $\omega \times 2$: The determinacy of these games is equivalent to the Axiom of Real Determinacy.

On Extensions of the Axiom of Determinacy

Philipp Rohde Diploma Thesis (in German), Departement of Mathematics, University of Bonn, Germany, 2001 We are considering infinite two-person games with perfect information. The Axiom of Determinacy AD is the following statement: every game of length $\omega$, where both players choose integers is determined, i.e., one of the two players has a winning strategy. In Chapter 2 we give a short review of the mathematical formalism of the considered games and the notion of determinacy and we discuss some elementary consequences of the Axiom of Determinacy. We are investigating extensions of this axiom. First of all there are two parameters which can be changed to obtain new games: the complexity of the particular moves (in the AD context: natural numbers) and the length of the game, measured by the transfinite scale of the ordinals (in the AD context: omega). In Chapter 3 we discuss the appropriate determinacy hypotheses, in particular their boundaries and the dependencies among each other. For example we show the Theorem of Blass, which says that the determinacy of all games on reals with length $\omega$ is equivalent to that of all games on integers with length $\omega 2$. The main result is a classification of all determinacy hypotheses for games on integers of a fixed countable length. All these hypotheses are equivalent either to AD or to the stronger Axiom of Real Determinacy ADR. The exact boundary in regard to the length of the games is $\omega *2$. This statement combines an unpublished theorem of Woodin about AD and Uniformisation with the mentioned theorem of Blass. In Chapter 4 we consider the relative consistency strength of determinacy hypotheses. We show the existence of constructible models of determinacy and discuss some aspects of the correlation with the theory of large cardinals. It can be shown that under the assumption of determinacy in the universe the canonical constructible model L(R) is indeed a model of AD. But L(R) cannot be a model of the stronger axiom ADR. AD+ is an axiom introduced by Woodin to combine consequences of ADR with the relative consistency with v=L(R). In Chapter 5, we introduce AD+ and show its relative consistency with v=L(R). These results are due to Woodin (unpublished). It is still open whether AD+ is a proper extension of AD.