# Publications (Games and Automata for Synthesis and Validation Network)

### Parosh A. Abdulla

• P. A. Abdulla, A. Bouajjani, and J. d'Orso. Deciding Monotonic Games. In Proceedings of the 12th Annual Conference of the European Association for Computer Science Logic, CSL 2003, LNCS. Springer-Verlag, 2003.

### Luca de Alfaro

• L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, P. Roy, and M. Sorea. Sociable Interfaces. In Proceedings of 5th International Workshop on Frontiers of Combining Systems, vol. 3717 of Lecture Notes in Computer Science, pp. 81–105. Springer, 2005.
• A. Chakrabarti, L. de Alfaro, T. A. Henzinger, M. Jurdziński, and F. Mang. Interface Compatibility Checking for Software Modules. In Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings (E. Brinksma and K. G. Larsen, Eds.), vol. 2404 of Lecture Notes in Computer Science, pp. 428–441, Copenhagen, Denmark. Springer-Verlag, 2002.

### June Andronick

• J. Andronick, B. Chatali, and O. Ly. Using COQ to Verify Java Card Applet Isolation Properties. In 16th International Conference on Theorem Proving in Higher Order Logics, LNCS. Springer-Verlag, 2003.
• J. Andronick, B. Chatali, and O. Ly. Formal Verification of the Integrity Property in Java Card Technology. In Proceedings of e-SMART, 2003.

### André Arnold

• A. Arnold and L. Santocanale. Ambiguous Classes in the Games $\mu$-Calculus Hierarchy. In FOSSACS'03, vol. 2620 of LNCS, pp. 70–86, 2003.
• A. Arnold, A. Vincent, and I. Walukiewicz. Games for synthesis of controllers with partial observation. Theoretical Computer Science, vol. 303(1), pp. 7–34, 2003.

### Robert Baumgartner

• R. Baumgartner, M. Ceresna, and G. Ledermueller. Automating Web Navigation in Web Data Extraction. In Proceedings of International Conference on Intelligent Agents, Web Technology and Internet Commerce, Vienna, Austria, 2005.

### Therese Berg

• T. Berg, B. Jonsson, M. Leucker, and M. Saksena. Insights to Angluin's Learning. Technical Report. Department of Information Technology, Uppsala University, 2003.

### Julien Bernet

• J. Bernet and D. Janin. Automata theory for discrete distributed games. In Foundation of Computing Theory, vol. 3623 of LNCS. Springer-Verlag, 2005.
• J. Bernet, D. Janin, and I. Walukiewicz. Permissive strategies: from parity games to safety games. Theoretical Informatics and Applications (RAIRO), vol. 36, pp. 251–275, 2002.

### Dietmar Berwanger

• D. Berwanger. Games and Logical Expressiveness. PhD thesis, RWTH Aachen, 2005.
• D. Berwanger and E. Grädel. Entanglement - A Measure for the Complexity of Directed Graphs with Applications to Logic and Games. In Proceedings of LPAR 2004, Montevideo, Uruguay, vol. 3452 of LNCS, pp. 209–223. Springer-Verlag, 2005.
• D. Berwanger and G. Lenzi. The variable hierarchy of the $\mu$-calculus is strict. In STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science, vol. 3404 of LNCS, pp. 97–109. Springer-Verlag, 2005.
• D. Berwanger and E. Grädel. Fixed-Point Logics and Solitaire Games. Theory of Computing Systems, vol. 37, pp. 675–694, 2004.
• D. Berwanger, E. Grädel, and S. Kreutzer. Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games. In Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning, vol. 2850 of LNCS, pp. 226–240. Springer-Verlag, 2003.
• D. Berwanger and E. Grädel. Fixed point formulae and solitaire games. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.
• D. Berwanger, E. Grädel, and G. Lenzi. On the variable hierarchy of the modal mu-calculus. In Computer Science Logic, CSL 2002 (J. Bradfield, Ed.), vol. 2471 of LNCS, pp. 352–366. Springer-Verlag, 2002.

### Henrik Björklund

• H. Björklund, S. Sandberg, and S. Vorobyov. A Discrete Subexponential Algorithm for Parity Games. In 20th International Symposium on Theoretical Aspects of Computer Science, STACS'2003 (H. Alt and M. Habib, Eds.), vol. 2607 of Lecture Notes in Computer Science, pp. 663–674, Berlin. Springer-Verlag, 2003.
• H. Björklund, S. Sandberg, and S. Vorobyov. Complexity of Model Checking by Iterative Improvement: the Pseudo-Boolean Framework. In Andrei Ershov Fifth International Conference “Perspectives of System Informatics'' (A. Zamulin, Ed.), pp. 262–270, 2003.
• H. Björklund, S. Sandberg, and S. Vorobyov. Memoryless Determinacy of Parity Games: A Simple Proof. Theoretical Computer Science, 2003.
• H. Björklund and S. Sandberg. Algorithms for Combinatorial Optimization and Games Adapted from Linear Programming. In Proceedings of the Eighth ESSLLI Student Session (B. ten Cate, Ed.), 2003.

### Achim Blumensath

• A. Blumensath and E. Grädel. Finite Presentations of Infinite Structures. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.

### Mikołaj Bojańczyk

• M. Bojańczyk and T. Colcombet. Tree-Walking Automata Do Not Recognize All Regular Languages. In ACM Symposium on Theory of Computing, 2005.
• M. Bojańczyk. A Bounding Quantifier. In Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings (J. Marcinkowski and A. Tarlecki, Eds.), vol. 3210 of Lecture Notes in Computer Science, pp. 41–55. Springer, 2004.
• M. Bojańczyk and T. Colcombet. Tree-Walking Automata Cannot Be Determinized. Lecture Notes in Computer Science, vol. 3142, pp. 246–256, 2004.
• M. Bojańczyk and I. Walukiewicz. Characterizing EF and EX Tree Logics. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings (P. Gardner and N. Yoshida, Eds.), vol. 3170 of Lecture Notes in Computer Science, pp. 131–145. Springer-Verlag, 2004.
• M. Bojańczyk. The Finite Graph Problem for Two-Way Alternating Automata. Theoretical Computer Science, vol. 298, pp. 511–528, 2003.
• M. Bojańczyk. 1-bounded TWA Cannot be Determinized. In Proceedings of FSTTCS'03, 2003.

### Benedikt Bollig

• B. Bollig and M. Leucker. Verifying Qualitative Properties of Probabilistic Programs. In Validation of Stochastic Systems, Lecture Notes in Computer Science. Springer, 2003.
• B. Bollig, M. Leucker, and P. Lucas. Extending Compositional Message Sequence Graphs. In Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'02) (M. Baaz and A. Voronkov, Eds.), vol. 2514 of Lecture Notes in Artificial Intelligence, pp. 68–85. Springer, 2002.

### Yves Bontemps

• Y. Bontemps, P. Y. Schobbens, and C. Löding. Synthesis of Open Reactive Systems from Scenario-Based Specifications. Fundamenta Informaticae, vol. 62(2), pp. 139–169, 2004.

### Ahmed Bouajjani

• A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejeck. Reachability Analysis of Multithreaded Software with Asynchronous Communication. In Proc. 25th Conf. on Found. of Software Technology and Theoretical Computer Science (FSTTCS'05), Lecture Notes in Computer Science, Madras, India. Springer Pub., 2005.
• A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In Proc. 12th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Lecture Notes in Computer Science, Edinburgh, UK. Springer Pub., 2005.
• A. Bouajjani, M. Müller-Olm, and T. Touili. Regular Symbolic Analysis of Dynamic Networks of Pushdown Processes. In Proc. (CONCUR'05), vol. 3653 of Lecture Notes in Computer Science, San Franciso (Ca), USA, 2005.
• A. Bouajjani and T. Touili. On Computing Reachability Sets of Process Rewrite Systems. In Proc. 16th Intern. Conf. on Rewriting Techniques and Applications (RTA'05), vol. 3467 of Lecture Notes in Computer Science, Nara, Japan. Springer Pub., 2005.
• A. Bouajjani, J. Esparza, and T. Touili. Reachability Analysis of Synchronized PA Systems. In Proc. 6th Intern. Workshop on Verification of Infinite-State Systems (Infinity'04), London, UK. to appear in ENTCS, 2004.
• A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract Regular Model Checking. In Proc. 16th Intern. Conf. on Computer Aided Verification (CAV'04), vol. 3114 of Lecture Notes in Computer Science, Boston (MA), USA. Springer Pub., 2004.
• A. Bouajjani, A. Legay, and P. Wolper. Handling Liveness Properties in (omega-)Regular Model Checking. In Proc. 6th Intern. Workshop on Verification of Infinite-State Systems (Infinity'04), London, UK. to appear in ENTCS, 2004.
• A. Bouajjani and A. Meyer. Symbolic Reachability Analysis of Higher-Order Context-Free Processes. In Proc. 24rd Conf. on Found. of Software Technology and Theoretical Computer Science (FSTTCS'04), vol. 3328 of Lecture Notes in Computer Science, Madras, India. Springer Pub., 2004.
• P. A. Abdulla, A. Bouajjani, and J. d'Orso. Deciding Monotonic Games. In Proceedings of the 12th Annual Conference of the European Association for Computer Science Logic, CSL 2003, LNCS. Springer-Verlag, 2003.
• A. Bouajjani. Verification of Infinite State Systems (Tutorial). In Proceedings of CSL'03, vol. 2803 of LNCS. Springer-Verlag, 2003.
• A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In Conference Record of POPL'03: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, pp. 62–73. ACM, 2003.
• A. Bouajjani and T. Touili. Reachability Analysis of Process Rewrite Systems. In Proc. 23rd Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03), vol. 2914 of Lecture Notes in Computer Science, 2003.

### Alexis Bouquet

• A. Bouquet, O. Serre, and I. Walukiewicz. Pushdown games with unboundedness and regular conditions. In Proceedings of FSTTCS'03, vol. 2914 of LNCS, pp. 88–99. Springer-Verlag, 2003.

### Julian Bradfield

• J. Bradfield, J. Duparc, and S. Quickert. Transfinite Extension of the Mu-Calculus. In Computer Science Logic (L. Ong, Ed.), pp. 384–396. Springer-Verlag, 2005.
• J. Bradfield and S. Kreutzer. The complexity of independence-friendly fixpoint logic. , pp. 355–368, 2005.
• J. Bradfield. On independence-friendly fixpoint logics. Philosophia Scientiae, vol. 8, pp. 125–144, 2004.

### Véronique Bruyère

• V. Bruyère, O. Carton, and G. Sénizergues. Tree automata and automata on linear orderings. In Proceedings WORDS'03, vol. 27 of LNCS, pp. 222–231. TUCS General Publication, 2003.

### Thierry Cachat

• T. Cachat. Games on Pushdown Graphs and Extensions. PhD thesis, RWTH Aachen, 2003.
• T. Cachat. Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games. In Proceedings of the 30th International Colloquium on Automata, Languages, and Programming, vol. 2719 of LNCS, pp. 556–569. Springer-Verlag, 2003.
• T. Cachat. Two-Way Tree Automata Solving Pushdown Games. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), vol. 2500 of LNCS, pp. 303–317. Springer-Verlag, 2002.
• T. Cachat, J. Duparc, and W. Thomas. Solving Pushdown Games with a Sigma-3 Winning Condition. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002, vol. 2471 of LNCS, pp. 322–336. Springer-Verlag, 2002.
• T. Cachat. Uniform Solution of Parity Games on Prefix-Recognizable Graphs. In Proceedings of the 4th International Workshop on Verification of Infinite-State Systems (A. Kucera and R. Mayr, Eds.), vol. 68 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2002.
• T. Cachat. Symbolic Strategy Synthesis for Games on Pushdown Graphs. In Proceedings of the 29th International Colloquium on Automata, Languages, and Programming, vol. 2380 of LNCS, pp. 704–715. Springer-Verlag, 2002.

### Arnaud Carayol

• A. Carayol and S. Wöhrle. The Caucal Hierarchy of Infinite Graphs In Terms of Logic and Higher-order Pushdown Automata. In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2003, vol. 2914 of Lecture Notes in Computer Science, pp. 112–123. Springer, 2003.

### Olivier Carton

• V. Bruyère, O. Carton, and G. Sénizergues. Tree automata and automata on linear orderings. In Proceedings WORDS'03, vol. 27 of LNCS, pp. 222–231. TUCS General Publication, 2003.

### Michal Ceresna

• R. Baumgartner, M. Ceresna, and G. Ledermueller. Automating Web Navigation in Web Data Extraction. In Proceedings of International Conference on Intelligent Agents, Web Technology and Internet Commerce, Vienna, Austria, 2005.
• G. Gottlob and M. Ceresna. Query Based Learning of XPath Fragments. In Proceedings of Dagstuhl Seminar on Machine Learning for the Semantic Web (05071), Dagstuhl, Germany, 2005.
• M. Ceresna. Supervised Learning of Wrappers from Structured Data Sources. PhD thesis, Vienna University of Technology, 2005.
• M. Ceresna. Interactive Generation of HTML Wrappers Using Attribute Classification. In Proceedings of the First International Workshop on Representation and Analysis of Web Space, pp. 137–142, Prague-Tocna, Czech Republic, 2005.

### Arindam Chakrabarti

• A. Chakrabarti, L. de Alfaro, T. A. Henzinger, M. Jurdziński, and F. Mang. Interface Compatibility Checking for Software Modules. In Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings (E. Brinksma and K. G. Larsen, Eds.), vol. 2404 of Lecture Notes in Computer Science, pp. 428–441, Copenhagen, Denmark. Springer-Verlag, 2002.

### Boutheina Chatali

• J. Andronick, B. Chatali, and O. Ly. Using COQ to Verify Java Card Applet Isolation Properties. In 16th International Conference on Theorem Proving in Higher Order Logics, LNCS. Springer-Verlag, 2003.
• J. Andronick, B. Chatali, and O. Ly. Formal Verification of the Integrity Property in Java Card Technology. In Proceedings of e-SMART, 2003.

### Krishnendu Chatterjee

• K. Chatterjee, T. A. Henzinger, and M. Jurdziński. Mean-Payoff Parity Games. In Proceedings, Twentieth Annual IEEE Symposium on Logic in Computer Science, LICS 2005, pp. 178–187. IEEE Computer Society Press, 2005.
• K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Quantitative Stochastic Parity Games. In Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, pp. 114–123. ACM/SIAM, 2004.
• K. Chatterjee, T. A. Henzinger, and M. Jurdziński. Games with Secure Equilibria. In Proceedings, Nineteenth Annual IEEE Symposium on Logic in Computer Science, LICS 2004, pp. 160–169. IEEE Computer Society Press, 2004.
• K. Chatterjee, R. Majumdar, and M. Jurdziński. On Nash Equilibria in Stochastic Games. In CSL 2004 (J. Marcinkowski and A. Tarlecki, Eds.), vol. 3210 of LNCS, pp. 26–40. Springer-Verlag, 2004.
• K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Simple Stochastic Parity Games. In Proceedings of 12th Annual Conference of the European Association for Computer Science Logic, CSL 2003 (J. Makowsky and M. Baaz, Eds.), Lecture Notes in Computer Science. Springer, 2003.

### Thomas Colcombet

• M. Bojańczyk and T. Colcombet. Tree-Walking Automata Do Not Recognize All Regular Languages. In ACM Symposium on Theory of Computing, 2005.
• M. Bojańczyk and T. Colcombet. Tree-Walking Automata Cannot Be Determinized. Lecture Notes in Computer Science, vol. 3142, pp. 246–256, 2004.
• T. Colcombet and C. Löding. On the Expressiveness of Deterministic Transducers over Infinite Trees. In Proceedings of the 21st International Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science. Springer-Verlag, 2004.
• T. Colcombet and D. Niwinski. On the positional determinacy of edge–labeled games. Warsaw University, submitted, 2004.

### Bruno Courcelle

• B. Courcelle and P. Weil. The recognizability of sets of graphs is a robust property. Tcs, vol. 342, pp. 173–228, 2005.

### Julien Cristau

• J. Cristau, C. Löding, and W. Thomas. Deterministic Automata on Unranked Trees. In Proceedings of the 15th International Symposium on Fundamentals of Computation Theory, FCT 2005, vol. 3623 of Lecture Notes in Computer Science, pp. 68–79. Springer, 2005.

### Julien d'Orso

• P. A. Abdulla, A. Bouajjani, and J. d'Orso. Deciding Monotonic Games. In Proceedings of the 12th Annual Conference of the European Association for Computer Science Logic, CSL 2003, LNCS. Springer-Verlag, 2003.

### Anuj Dawar

• A. Dawar, E. Grädel, and S. Kreutzer. Backtracking Games and Inflationary Fixed Points. In Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, vol. 3142 of LNCS, pp. 420–432. Springer-Verlag, 2004.
• A. Dawar and D. Janin. On the bisimulation invariant fragment of Monadic $\Sigma_1$ in the finite. In FSTTCS, vol. 3328 of LNCS, pp. 224–237. Springer-Verlag, 2004.
• A. Dawar, E. Grädel, and S. Kreutzer. Inflationary Fixed Points in Modal Logic. ACM Transactions on Computational Logic, vol. 5, 2004.
• A. Dawar and S. Kreutzer. Generalising Automaticity to Modal Properties of Finite Structures. In Proc. 22nd Conf. on Foundations of Software Technology and Theoretical Computer Science, LNCS. Springer, 2002.
• A. Dawar and D. Richerby. Fixed-Point Logics with Nondeterministic Choice. Journal of Logic and Computation, 2002.

### Aldric Degorre

• L. Hélouët, M. Zeitoun, and A. Degorre. Scenarios and Covert channels, another game... In Proc. of Games in Design and Verification, GDV'04, vol. 119 of Electronic Notes in Theoretical Computer Science, pp. 93–116. Elsevier, 2004.

### Volker Diekert

• V. Diekert and P. Gastin. Local temporal logic is expressively complete for cograph dependence alphabets. Information and Computation, vol. 195(1-2), pp. 30–52, 2004.
• V. Diekert and P. Gastin. Pure Future Local Temporal Logics Are Expressively Complete for Mazurkiewicz Traces. In Proceedings of LATIN'04, vol. 2976 of LNCS, pp. 232–241. Springer-Verlag, 2004.

### Jacques Duparc

• J. Bradfield, J. Duparc, and S. Quickert. Transfinite Extension of the Mu-Calculus. In Computer Science Logic (L. Ong, Ed.), pp. 384–396. Springer-Verlag, 2005.
• J. Duparc. Positive Games and Persistent Strategies. In Proceedings of the 12th Annual Conference of the European Association for Computer Science Logic, CSL 2003, LNCS. Springer-Verlag, 2003.
• J. Duparc. The Steel Hierarchy of Ordinal Valued Borel Mappings. Journal of Symbolic Logic, vol. 68(1), pp. 187–234, 2003.
• J. Duparc and M. Riss. The Missing Link for \omega-Rational Sets, Automata, and Semigroups. International Journal of Algebra and Computation, 2003.
• T. Cachat, J. Duparc, and W. Thomas. Solving Pushdown Games with a Sigma-3 Winning Condition. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002, vol. 2471 of LNCS, pp. 322–336. Springer-Verlag, 2002.

### Zoltán Ésik

• Z. Ésik and P. Weil. Algebraic recognizability of regular tree languages. Theoretical Computer Science, vol. 340, pp. 291–321, 2005.
• Z. Ésik and P. Weil. On logically defined recognizable tree languages. In Proceedings FSTTCS 2003, vol. 2914 of LNCS, pp. 195–207. Springer-Verlag, 2003.

### Javier Esparza

• A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejeck. Reachability Analysis of Multithreaded Software with Asynchronous Communication. In Proc. 25th Conf. on Found. of Software Technology and Theoretical Computer Science (FSTTCS'05), Lecture Notes in Computer Science, Madras, India. Springer Pub., 2005.
• A. Bouajjani, J. Esparza, and T. Touili. Reachability Analysis of Synchronized PA Systems. In Proc. 6th Intern. Workshop on Verification of Infinite-State Systems (Infinity'04), London, UK. to appear in ENTCS, 2004.
• A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In Conference Record of POPL'03: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, pp. 62–73. ACM, 2003.
• A. Stefanescu, J. Esparza, and A. Muscholl. Synthesis of distributed algorithms using asynchronous automata. In Proceedings of CONCUR'03, 2003.

### Marco Faella

• L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, P. Roy, and M. Sorea. Sociable Interfaces. In Proceedings of 5th International Workshop on Frontiers of Combining Systems, vol. 3717 of Lecture Notes in Computer Science, pp. 81–105. Springer, 2005.
• M. Faella and A. Legay. Some Models and Tools for Open Systems. In Proceedings of 1th Workshop on Foundation of Interface Technologies, 2005.

### Jörg Flum

• M. Frick, J. Flum, and M. Grohe. Query evaluation via tree-decompositions. Journal of the ACM, vol. 46(6), pp. 716–752, 2002.

### Séverine Fratani

• S. Fratani and G. Sénizergues. Iterated Pushdown Automata and Sequences of Rational Numbers. In St Petersburg second Logic Days, 2003.

### Markus Frick

• M. Frick, M. Grohe, and C. Koch. Query Evaluation on Compressed Trees. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS'03), 2003.
• M. Frick, J. Flum, and M. Grohe. Query evaluation via tree-decompositions. Journal of the ACM, vol. 46(6), pp. 716–752, 2002.

### Sibylle Fröschle

• S. Fröschle. The Decidability Border of Hereditary History Preserving Bisimilarity. Information Processing Letters, vol. 93(6), pp. 289–293, 2005.
• S. Fröschle. Composition and decomposition in true-concurrency. In Proceedings of FOSSACS'05, vol. 3441 of LNCS, pp. 333–347. Springer-Verlag, 2005.
• S. Fröschle and S. Lasota. Decomposition and complexity of hereditary history preserving bisimulation on BPP. In Proceedings of CONCUR'05, vol. 3656 of LNCS, pp. 263–277. Springer-Verlag, 2005.
• S. Fröschle and S. Lasota. Causality versus true-concurrency. In Proceedings of EXPRESS'05, Electronic Notes in Theoretical Computer Science. Elsevier, 2005.
• S. Fröschle. Decidability and Coincidence of Equivalences for Concurrency. PhD thesis, University of Edinburgh, 2004.

### Paul Gastin

• P. Gastin and D. Kuske. Uniform Satisfiability Problem for Local Temporal Logics over Mazurkiewicz Traces. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05) (M. Abadi and L. de Alfaro, Eds.), vol. 3653 of Lecture Notes in Computer Science, pp. 533–547. Springer, 2005.
• V. Diekert and P. Gastin. Local temporal logic is expressively complete for cograph dependence alphabets. Information and Computation, vol. 195(1-2), pp. 30–52, 2004.
• V. Diekert and P. Gastin. Pure Future Local Temporal Logics Are Expressively Complete for Mazurkiewicz Traces. In Proceedings of LATIN'04, vol. 2976 of LNCS, pp. 232–241. Springer-Verlag, 2004.
• P. Gastin, B. Lerman, and M. Zeitoun. Distributed games and distributed control for asynchronous systems. In Proc. of the 6th Symposium Latin American Theoretical INformatics, LATIN'04 (M. Farach-Colton, Ed.), vol. 2976 of Lect. Notes Comp. Sci., pp. 455–465. Springer, 2004.
• P. Gastin, B. Lerman, and M. Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In Proc. of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'04, vol. 3328 of Lect. Notes Comp. Sci., pp. 275–286. Springer, 2004.
• P. Gastin, P. Moro, and M. Zeitoun. Minimization of counterexamples in SPIN. In Model Checking Software: Proc. of the 11th International SPIN Workshop, SPIN'04, vol. 2989 of Lect. Notes Comp. Sci., pp. 92–108. Springer, 2004.
• P. Gastin and D. Oddoux. LTL with past and two-way very-weak alternating automata. In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS'03) (B. Rovan and P. Vojtávs, Eds.), LNCS, pp. 439–448. Springer-Verlag, 2003.

### Blaise Genest

• B. Genest, D. Kuske, A. Muscholl, and D. Peled. Snapshot Verification. In Tools and Algorithms for Construction and Analysis of Systems, (TACAS'05), LNCS, pp. 510–525. Springer Verlag, 2005.
• B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. Journal of Computer and System Sciences, 2005.
• B. Genest, D. Kuske, and A. Muscholl. A Kleene Theorem for a Class of Communicating Automata with Effective Algorithms. In Developments in Language Theory (DLT'04), LNCS, pp. 30–48. Springer Verlag, 2004.
• B. Genest, M. Minea, A. Muscholl, and D. Peled. Specifying and Verifying Partial Order Properties Using Template MSCs. In Proceedings of FoSSaCS'04, vol. 2987 of LNCS, pp. 195–210. Springer-Verlag, 2004.
• B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. In Proc. of the 29th International Colloquium on Automata, Languages and Programming, ICALP'02 (P. Widmayer et al., Eds.), vol. 2380 of Lect. Notes Comp. Sci., pp. 657–668, Malaga, Spain. Springer, 2002.

### Silvio Ghilardi

• S. Ghilardi and L. Santocanale. Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics. In LPAR'03 (Logic for Programming Artificial Intelligence and Reasoning), 2003.

### Hugo Gimbert

• H. Gimbert and W. Zielonka. Games Where You Can Play Optimally Without Any Memory. In Proceedings of CONCUR'05, vol. 3653 of Lecture Notes in Theoretical Computer Science, pp. 428. Springer-Verlag, 2005.
• H. Gimbert. Parity and exploration games on infinite graphs. In Proceedings of CSL'04, vol. 3210 of LNCS, pp. 56–70. Springer-Verlag, 2004.
• H. Gimbert and W. Zielonka. When Can You Play Positionally? In Proceedings of MFCS'04, vol. 3153 of LNCS, pp. 686–697. Springer-Verlag, 2004.
• H. Gimbert and W. Zielonka. Discounting Infinite Games but How and Why? In Games in Design and Verification 04, vol. 119 of Electronic Notes in Theoretical Computer Science, pp. 3–9. Elsevier, 2004.

### Georg Gottlob

• G. Gottlob and M. Ceresna. Query Based Learning of XPath Fragments. In Proceedings of Dagstuhl Seminar on Machine Learning for the Semantic Web (05071), Dagstuhl, Germany, 2005.
• G. Gottlob, C. Koch, and R. Pichler. The complexity of XPath query evaluation. In Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS-03), pp. 179–190, New York. ACM Press, 2003.
• G. Gottlob and C. Koch. Monadic Datalog over Trees and the Expressive Power of Languages for Web Information Extraction. In Proceedings of the twenty-first ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS-02), pp. 17–28, New York. ACM Press, 2002.
• G. Gottlob and C. Koch. Monadic Queries over Tree-Structured Data. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp. 189–202. IEEE Computer Society, 2002.

### Erich Grädel

• D. Berwanger and E. Grädel. Entanglement - A Measure for the Complexity of Directed Graphs with Applications to Logic and Games. In Proceedings of LPAR 2004, Montevideo, Uruguay, vol. 3452 of LNCS, pp. 209–223. Springer-Verlag, 2005.
• D. Berwanger and E. Grädel. Fixed-Point Logics and Solitaire Games. Theory of Computing Systems, vol. 37, pp. 675–694, 2004.
• A. Dawar, E. Grädel, and S. Kreutzer. Backtracking Games and Inflationary Fixed Points. In Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, vol. 3142 of LNCS, pp. 420–432. Springer-Verlag, 2004.
• E. Grädel. Positional Determinacy of Infinite Games. In Proceedings of STACS 2004: 21st Annual Symposium on Theoretical Aspects of Computer Science, vol. 2996 of LNCS, pp. 2–18. Springer-Verlag, 2004.
• A. Dawar, E. Grädel, and S. Kreutzer. Inflationary Fixed Points in Modal Logic. ACM Transactions on Computational Logic, vol. 5, 2004.
• D. Berwanger, E. Grädel, and S. Kreutzer. Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games. In Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning, vol. 2850 of LNCS, pp. 226–240. Springer-Verlag, 2003.
• E. Grädel and S. Kreutzer. Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions. In Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 158–167, 2003.
• D. Berwanger and E. Grädel. Fixed point formulae and solitaire games. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.
• D. Berwanger, E. Grädel, and G. Lenzi. On the variable hierarchy of the modal mu-calculus. In Computer Science Logic, CSL 2002 (J. Bradfield, Ed.), vol. 2471 of LNCS, pp. 352–366. Springer-Verlag, 2002.
• A. Blumensath and E. Grädel. Finite Presentations of Infinite Structures. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.
• E. Grädel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games. Springer-Verlag, 2002.
• E. Grädel. Model Checking Games. In Proceedings of WOLLIC 02, vol. 67 of Electronic Notes in Theoretical Computer Science. Elsevier, 2002.

### Olga Grinchtein

• O. Grinchtein and M. Leucker. Network Invariants for Real-time Systems. In Electronic Notes in Theoretical Computer Science, vol. 91 of. Elsevier Science Publishers, 2003.

### Martin Grohe

• M. Frick, M. Grohe, and C. Koch. Query Evaluation on Compressed Trees. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS'03), 2003.
• M. Frick, J. Flum, and M. Grohe. Query evaluation via tree-decompositions. Journal of the ACM, vol. 46(6), pp. 716–752, 2002.

### Peter Habermehl

• A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In Proc. 12th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Lecture Notes in Computer Science, Edinburgh, UK. Springer Pub., 2005.
• A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract Regular Model Checking. In Proc. 16th Intern. Conf. on Computer Aided Verification (CAV'04), vol. 3114 of Lecture Notes in Computer Science, Boston (MA), USA. Springer Pub., 2004.
• H. Seidl, T. Schwentick, A. Muscholl, and P. Habermehl. Counting in Trees for Free. In International Colloquium on Automata, Languages and Programming (ICALP'04), LNCS, pp. 1136–1149. Springer Verlag, 2004.

### Loïc Hélouët

• L. Hélouët, M. Zeitoun, and A. Degorre. Scenarios and Covert channels, another game... In Proc. of Games in Design and Verification, GDV'04, vol. 119 of Electronic Notes in Theoretical Computer Science, pp. 93–116. Elsevier, 2004.
• L. Hélouët, C. Jard, and M. Zeitoun. Covert channels detection in protocols using scenarios. In Proc. of SPV'03, Security Protocols Verification (M. Rusinowitch, Ed.), pp. 21–25, 2003.

### Thomas A. Henzinger

• K. Chatterjee, T. A. Henzinger, and M. Jurdziński. Mean-Payoff Parity Games. In Proceedings, Twentieth Annual IEEE Symposium on Logic in Computer Science, LICS 2005, pp. 178–187. IEEE Computer Society Press, 2005.
• K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Quantitative Stochastic Parity Games. In Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, pp. 114–123. ACM/SIAM, 2004.
• K. Chatterjee, T. A. Henzinger, and M. Jurdziński. Games with Secure Equilibria. In Proceedings, Nineteenth Annual IEEE Symposium on Logic in Computer Science, LICS 2004, pp. 160–169. IEEE Computer Society Press, 2004.
• K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Simple Stochastic Parity Games. In Proceedings of 12th Annual Conference of the European Association for Computer Science Logic, CSL 2003 (J. Makowsky and M. Baaz, Eds.), Lecture Notes in Computer Science. Springer, 2003.
• A. Chakrabarti, L. de Alfaro, T. A. Henzinger, M. Jurdziński, and F. Mang. Interface Compatibility Checking for Software Modules. In Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings (E. Brinksma and K. G. Larsen, Eds.), vol. 2404 of Lecture Notes in Computer Science, pp. 428–441, Copenhagen, Denmark. Springer-Verlag, 2002.
• M. Jurdziński, O. Kupferman, and T. A. Henzinger. Trading Probability for Fairness. In Computer Science Logic, Proceedings (J. C. Bradfield, Ed.), vol. 2471 of LNCS, pp. 292–305. Springer-Verlag, 2002.

### David Janin

• J. Bernet and D. Janin. Automata theory for discrete distributed games. In Foundation of Computing Theory, vol. 3623 of LNCS. Springer-Verlag, 2005.
• A. Dawar and D. Janin. On the bisimulation invariant fragment of Monadic $\Sigma_1$ in the finite. In FSTTCS, vol. 3328 of LNCS, pp. 224–237. Springer-Verlag, 2004.
• J. Bernet, D. Janin, and I. Walukiewicz. Permissive strategies: from parity games to safety games. Theoretical Informatics and Applications (RAIRO), vol. 36, pp. 251–275, 2002.
• D. Janin and G. Lenzi. On the logical definability of topologically closed recognizable languages of infinite trees. Computing and Informatics, vol. 21, pp. 185–203, 2002.

### Claude Jard

• L. Hélouët, C. Jard, and M. Zeitoun. Covert channels detection in protocols using scenarios. In Proc. of SPV'03, Security Protocols Verification (M. Rusinowitch, Ed.), pp. 21–25, 2003.

### Bengt Jonsson

• T. Berg, B. Jonsson, M. Leucker, and M. Saksena. Insights to Angluin's Learning. Technical Report. Department of Information Technology, Uppsala University, 2003.

### Marcin Jurdziński

• M. Jurdziński, M. Paterson, and U. Zwick. A Deterministic Subexponential Algorithm for Solving Parity Games. In Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, pp. 114–123. ACM/SIAM, 2006.
• K. Chatterjee, T. A. Henzinger, and M. Jurdziński. Mean-Payoff Parity Games. In Proceedings, Twentieth Annual IEEE Symposium on Logic in Computer Science, LICS 2005, pp. 178–187. IEEE Computer Society Press, 2005.
• K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Quantitative Stochastic Parity Games. In Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, pp. 114–123. ACM/SIAM, 2004.
• K. Chatterjee, T. A. Henzinger, and M. Jurdziński. Games with Secure Equilibria. In Proceedings, Nineteenth Annual IEEE Symposium on Logic in Computer Science, LICS 2004, pp. 160–169. IEEE Computer Society Press, 2004.
• K. Chatterjee, R. Majumdar, and M. Jurdziński. On Nash Equilibria in Stochastic Games. In CSL 2004 (J. Marcinkowski and A. Tarlecki, Eds.), vol. 3210 of LNCS, pp. 26–40. Springer-Verlag, 2004.
• K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Simple Stochastic Parity Games. In Proceedings of 12th Annual Conference of the European Association for Computer Science Logic, CSL 2003 (J. Makowsky and M. Baaz, Eds.), Lecture Notes in Computer Science. Springer, 2003.
• M. Jurdziński, M. Nielsen, and J. Srba. Undecidability of Domino Games and Hhp-Bisimilarity. Information and Computation, vol. 184(2), pp. 343–368, 2003.
• A. Chakrabarti, L. de Alfaro, T. A. Henzinger, M. Jurdziński, and F. Mang. Interface Compatibility Checking for Software Modules. In Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings (E. Brinksma and K. G. Larsen, Eds.), vol. 2404 of Lecture Notes in Computer Science, pp. 428–441, Copenhagen, Denmark. Springer-Verlag, 2002.
• M. Jurdziński, O. Kupferman, and T. A. Henzinger. Trading Probability for Fairness. In Computer Science Logic, Proceedings (J. C. Bradfield, Ed.), vol. 2471 of LNCS, pp. 292–305. Springer-Verlag, 2002.

### Łukasz Kaiser

• Ł. Kaiser. Game Quantification on Automatic Structures and Hierarchical Model Checking Games. In Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006 (Z. Esik, Ed.), vol. 4207 of LNCS, pp. 411–425. Springer-Verlag, 2006.
• Ł. Kaiser. Confluence of Right Ground Term Rewriting Systems is Decidable. In FOSSACS 2005, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, LNCS. Springer-Verlag, 2005.

### Teodor Knapik

• T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe Grammars and Panic Automata. In ICALP, vol. 3580 of Lecture Notes in Computer Science, pp. 1450–1461, 2005.

### Christoph Koch

• M. Frick, M. Grohe, and C. Koch. Query Evaluation on Compressed Trees. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS'03), 2003.
• G. Gottlob, C. Koch, and R. Pichler. The complexity of XPath query evaluation. In Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS-03), pp. 179–190, New York. ACM Press, 2003.
• G. Gottlob and C. Koch. Monadic Datalog over Trees and the Expressive Power of Languages for Web Information Extraction. In Proceedings of the twenty-first ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS-02), pp. 17–28, New York. ACM Press, 2002.
• G. Gottlob and C. Koch. Monadic Queries over Tree-Structured Data. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp. 189–202. IEEE Computer Society, 2002.

### Pavel Krčál

• P. Krčál and R. Pelánek. On Sampled Semantics of Timed Systems. In Proceedings of FSTTCS'05, Hyderabad, India. (R. Ramanujam and S. Sen, Eds.), vol. 3821 of Lecture Notes in Computer Science. Springer-Verlag, 2005.
• P. Krčál, L. Mokrushin, P. S. Thiagarajan, and W. Yi. Timed vs. Time Triggered Automata. In Proc. of CONCUR'04, London, UK. (P. Gardner and N. Yoshida, Eds.), vol. 3170 of Lecture Notes in Computer Science, pp. 340–354. Springer-Verlag, 2004.
• P. Krčál and W. Yi. Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. In Proceedings of TACAS'04, Barcelona, Spain. (K. Jensen and A. Podelski, Eds.), vol. 2988 of Lecture Notes in Computer Science, pp. 236–250. Springer-Verlag, 2004.

### Erik Krebs

• E. Krebs. Effiziente Berechnung optimaler Strategien für Paritätsspiele. Dipl.-Arb.-Nr. 21468, März 2004, Universität Stuttgart, 2004.

### Stephan Kreutzer

• J. Bradfield and S. Kreutzer. The complexity of independence-friendly fixpoint logic. , pp. 355–368, 2005.
• A. Dawar, E. Grädel, and S. Kreutzer. Backtracking Games and Inflationary Fixed Points. In Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, vol. 3142 of LNCS, pp. 420–432. Springer-Verlag, 2004.
• A. Dawar, E. Grädel, and S. Kreutzer. Inflationary Fixed Points in Modal Logic. ACM Transactions on Computational Logic, vol. 5, 2004.
• D. Berwanger, E. Grädel, and S. Kreutzer. Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games. In Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning, vol. 2850 of LNCS, pp. 226–240. Springer-Verlag, 2003.
• E. Grädel and S. Kreutzer. Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions. In Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 158–167, 2003.
• A. Dawar and S. Kreutzer. Generalising Automaticity to Modal Properties of Finite Structures. In Proc. 22nd Conf. on Foundations of Software Technology and Theoretical Computer Science, LNCS. Springer, 2002.

### Orna Kupferman

• M. Jurdziński, O. Kupferman, and T. A. Henzinger. Trading Probability for Fairness. In Computer Science Logic, Proceedings (J. C. Bradfield, Ed.), vol. 2471 of LNCS, pp. 292–305. Springer-Verlag, 2002.
• O. Kupferman, N. Piterman, and M. Vardi. Pushdown Specifications. In 9th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Lecture Notes in Artificial Inteligence, 2002.

### Robert Kurshan

• R. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün. Combining software and hardware verification techniques. Formal Methods in System Design, vol. 21(3), pp. 251–280, 2002.

### Dietrich Kuske

• B. Genest, D. Kuske, A. Muscholl, and D. Peled. Snapshot Verification. In Tools and Algorithms for Construction and Analysis of Systems, (TACAS'05), LNCS, pp. 510–525. Springer Verlag, 2005.
• P. Gastin and D. Kuske. Uniform Satisfiability Problem for Local Temporal Logics over Mazurkiewicz Traces. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05) (M. Abadi and L. de Alfaro, Eds.), vol. 3653 of Lecture Notes in Computer Science, pp. 533–547. Springer, 2005.
• B. Genest, D. Kuske, and A. Muscholl. A Kleene Theorem for a Class of Communicating Automata with Effective Algorithms. In Developments in Language Theory (DLT'04), LNCS, pp. 30–48. Springer Verlag, 2004.

### Martin Lange

• M. Lange and R. Somla. The Complexity of Model Checking Higher Order Fixpoint Logic. In Proc.\ 30th Int.\ Symp.\ on Math.\ Foundations of Computer Science, MFCS'05 (J. Jedrzejowicz and A. Szepietowski, Eds.), vol. 3618 of LNCS, pp. 640–651. Springer, 2005.
• M. Lange and C. Stirling. Model checking games for branching time logics. Journal of Logic and Computation, vol. 12(4), pp. 623–639, 2002.

### Sławomir Lasota

• S. Fröschle and S. Lasota. Decomposition and complexity of hereditary history preserving bisimulation on BPP. In Proceedings of CONCUR'05, vol. 3656 of LNCS, pp. 263–277. Springer-Verlag, 2005.
• S. Fröschle and S. Lasota. Causality versus true-concurrency. In Proceedings of EXPRESS'05, Electronic Notes in Theoretical Computer Science. Elsevier, 2005.
• S. Lasota and I. Walukiewicz. Alternating Timed Automata. In Proc. FOSSACS'05, vol. 3441 of LNCS, pp. 250–265. Springer-Verlag, 2005.
• S. Lasota. A Polynomial-Time Algorithm for Deciding True Concurrency Equivalences of Basic Parallel Processes. In Proc. 28th International Symposium on Mathematical Foundations of Computer Science (MFCS'03), vol. 2747 of LNCS, pp. 521–530. Springer-Verlag, 2003.
• S. Lasota. Decidability of strong bisimilarity for timed BPP. In 13th International Conference on Concurrency Theory (CONCUR'02), vol. 2421 of LNCS, pp. 562–578. Springer-Verlag, 2002.

### Gerald Ledermueller

• R. Baumgartner, M. Ceresna, and G. Ledermueller. Automating Web Navigation in Web Data Extraction. In Proceedings of International Conference on Intelligent Agents, Web Technology and Internet Commerce, Vienna, Austria, 2005.

### Axel Legay

• L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, P. Roy, and M. Sorea. Sociable Interfaces. In Proceedings of 5th International Workshop on Frontiers of Combining Systems, vol. 3717 of Lecture Notes in Computer Science, pp. 81–105. Springer, 2005.
• M. Faella and A. Legay. Some Models and Tools for Open Systems. In Proceedings of 1th Workshop on Foundation of Interface Technologies, 2005.
• A. Bouajjani, A. Legay, and P. Wolper. Handling Liveness Properties in (omega-)Regular Model Checking. In Proc. 6th Intern. Workshop on Verification of Infinite-State Systems (Infinity'04), London, UK. to appear in ENTCS, 2004.

### Giacomo Lenzi

• D. Berwanger and G. Lenzi. The variable hierarchy of the $\mu$-calculus is strict. In STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science, vol. 3404 of LNCS, pp. 97–109. Springer-Verlag, 2005.
• D. Berwanger, E. Grädel, and G. Lenzi. On the variable hierarchy of the modal mu-calculus. In Computer Science Logic, CSL 2002 (J. Bradfield, Ed.), vol. 2471 of LNCS, pp. 352–366. Springer-Verlag, 2002.
• D. Janin and G. Lenzi. On the logical definability of topologically closed recognizable languages of infinite trees. Computing and Informatics, vol. 21, pp. 185–203, 2002.

### Benjamin Lerman

• P. Gastin, B. Lerman, and M. Zeitoun. Distributed games and distributed control for asynchronous systems. In Proc. of the 6th Symposium Latin American Theoretical INformatics, LATIN'04 (M. Farach-Colton, Ed.), vol. 2976 of Lect. Notes Comp. Sci., pp. 455–465. Springer, 2004.
• P. Gastin, B. Lerman, and M. Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In Proc. of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'04, vol. 3328 of Lect. Notes Comp. Sci., pp. 275–286. Springer, 2004.

### Martin Leucker

• T. Berg, B. Jonsson, M. Leucker, and M. Saksena. Insights to Angluin's Learning. Technical Report. Department of Information Technology, Uppsala University, 2003.
• B. Bollig and M. Leucker. Verifying Qualitative Properties of Probabilistic Programs. In Validation of Stochastic Systems, Lecture Notes in Computer Science. Springer, 2003.
• O. Grinchtein and M. Leucker. Network Invariants for Real-time Systems. In Electronic Notes in Theoretical Computer Science, vol. 91 of. Elsevier Science Publishers, 2003.
• M. Leucker, R. Somla, and M. Weber. Parallel Model Checking for LTL, CTL{$^*$} and $L_{\mu^2$}. In Electronic Notes in Theoretical Computer Science (L. Brim and O. Grumberg, Eds.), vol. 89 of. Elsevier Science Publishers, 2003.
• B. Bollig, M. Leucker, and P. Lucas. Extending Compositional Message Sequence Graphs. In Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'02) (M. Baaz and A. Voronkov, Eds.), vol. 2514 of Lecture Notes in Artificial Intelligence, pp. 68–85. Springer, 2002.
• M. Leucker. Prefix-Recognizable Graphs and Monadic Second Order Logic. In Automata, Logics and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), vol. 2500 of Lecture Notes in Computer Science, pp. 263–283. Springer, 2002.
• M. Leucker, P. Madhusudan, and S. Mukhopadhyay. Dynamic Message Sequence Charts. In Proceedings of 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02) (M. Agrawal and A. Seth, Eds.), vol. 2556 of Lecture Notes in Computer Science. Springer, 2002.

### Vladimir Levin

• R. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün. Combining software and hardware verification techniques. Formal Methods in System Design, vol. 21(3), pp. 251–280, 2002.

### Christof Löding

• J. Cristau, C. Löding, and W. Thomas. Deterministic Automata on Unranked Trees. In Proceedings of the 15th International Symposium on Fundamentals of Computation Theory, FCT 2005, vol. 3623 of Lecture Notes in Computer Science, pp. 68–79. Springer, 2005.
• Y. Bontemps, P. Y. Schobbens, and C. Löding. Synthesis of Open Reactive Systems from Scenario-Based Specifications. Fundamenta Informaticae, vol. 62(2), pp. 139–169, 2004.
• T. Colcombet and C. Löding. On the Expressiveness of Deterministic Transducers over Infinite Trees. In Proceedings of the 21st International Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science. Springer-Verlag, 2004.
• C. Löding. Reachability Problems on Regular Ground Tree Rewriting Graphs. 2004.
• C. Löding, P. Madhusudan, and O. Serre. Visibly Pushdown Games. In Proceedings of FSTTCS'04, vol. 3328 of LNCS, pp. 408–420. Springer-Verlag, 2004.
• C. Löding and P. Rohde. Solving the Sabotage Game is PSPACE-hard. Technical Report. RWTH Aachen, 2003.
• C. Löding and P. Rohde. Solving the Sabotage Game is PSPACE-hard. In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science, MFCS '03, vol. 2474 of LNCS, pp. 531–540. Springer, 2003.
• C. Löding and P. Rohde. Model Checking and Satisfiability for Sabotage Modal Logic. In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'03, vol. 2914 of LNCS, pp. 302–313. Springer, 2003.

### Philipp Lucas

• B. Bollig, M. Leucker, and P. Lucas. Extending Compositional Message Sequence Graphs. In Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'02) (M. Baaz and A. Voronkov, Eds.), vol. 2514 of Lecture Notes in Artificial Intelligence, pp. 68–85. Springer, 2002.

### Olivier Ly

• J. Andronick, B. Chatali, and O. Ly. Using COQ to Verify Java Card Applet Isolation Properties. In 16th International Conference on Theorem Proving in Higher Order Logics, LNCS. Springer-Verlag, 2003.
• J. Andronick, B. Chatali, and O. Ly. Formal Verification of the Integrity Property in Java Card Technology. In Proceedings of e-SMART, 2003.
• O. Ly. Automatic Graph and D0L-sequences of finite graphs. Journal of Computer and System Sciences, vol. 67(3), 2003.

### Parthasarathy Madhusudan

• C. Löding, P. Madhusudan, and O. Serre. Visibly Pushdown Games. In Proceedings of FSTTCS'04, vol. 3328 of LNCS, pp. 408–420. Springer-Verlag, 2004.
• M. Leucker, P. Madhusudan, and S. Mukhopadhyay. Dynamic Message Sequence Charts. In Proceedings of 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02) (M. Agrawal and A. Seth, Eds.), vol. 2556 of Lecture Notes in Computer Science. Springer, 2002.

### Rupak Majumdar

• K. Chatterjee, R. Majumdar, and M. Jurdziński. On Nash Equilibria in Stochastic Games. In CSL 2004 (J. Marcinkowski and A. Tarlecki, Eds.), vol. 3210 of LNCS, pp. 26–40. Springer-Verlag, 2004.

### Freddy Mang

• A. Chakrabarti, L. de Alfaro, T. A. Henzinger, M. Jurdziński, and F. Mang. Interface Compatibility Checking for Software Modules. In Computer Aided Verification, 14th International Conference, CAV 2002, Proceedings (E. Brinksma and K. G. Larsen, Eds.), vol. 2404 of Lecture Notes in Computer Science, pp. 428–441, Copenhagen, Denmark. Springer-Verlag, 2002.

### Antoine Meyer

• A. Bouajjani and A. Meyer. Symbolic Reachability Analysis of Higher-Order Context-Free Processes. In Proc. 24rd Conf. on Found. of Software Technology and Theoretical Computer Science (FSTTCS'04), vol. 3328 of Lecture Notes in Computer Science, Madras, India. Springer Pub., 2004.

### Marius Minea

• B. Genest, M. Minea, A. Muscholl, and D. Peled. Specifying and Verifying Partial Order Properties Using Template MSCs. In Proceedings of FoSSaCS'04, vol. 2987 of LNCS, pp. 195–210. Springer-Verlag, 2004.
• R. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün. Combining software and hardware verification techniques. Formal Methods in System Design, vol. 21(3), pp. 251–280, 2002.

### Leonid Mokrushin

• P. Krčál, L. Mokrushin, P. S. Thiagarajan, and W. Yi. Timed vs. Time Triggered Automata. In Proc. of CONCUR'04, London, UK. (P. Gardner and N. Yoshida, Eds.), vol. 3170 of Lecture Notes in Computer Science, pp. 340–354. Springer-Verlag, 2004.

### Pierre Moro

• A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In Proc. 12th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Lecture Notes in Computer Science, Edinburgh, UK. Springer Pub., 2005.
• P. Gastin, P. Moro, and M. Zeitoun. Minimization of counterexamples in SPIN. In Model Checking Software: Proc. of the 11th International SPIN Workshop, SPIN'04, vol. 2989 of Lect. Notes Comp. Sci., pp. 92–108. Springer, 2004.

### Supratik Mukhopadhyay

• M. Leucker, P. Madhusudan, and S. Mukhopadhyay. Dynamic Message Sequence Charts. In Proceedings of 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02) (M. Agrawal and A. Seth, Eds.), vol. 2556 of Lecture Notes in Computer Science. Springer, 2002.

### Markus Müller-Olm

• A. Bouajjani, M. Müller-Olm, and T. Touili. Regular Symbolic Analysis of Dynamic Networks of Pushdown Processes. In Proc. (CONCUR'05), vol. 3653 of Lecture Notes in Computer Science, San Franciso (Ca), USA, 2005.

### Andrzej Murawski

• A. Murawski, L. Ong, and I. Walukiewicz. Idealized Algol with Ground Recursion, and DPDA Equivalence. In ICALP'05, vol. 3580 of LNCS, pp. 917–929, 2005.
• A. Murawski and I. Walukiewicz. Third-Order Idealized Algol with Iteration is Decidable. In FOSSACS'05, vol. 3441 of LNCS, pp. 202–218, 2005.

### Anca Muscholl

• B. Genest, D. Kuske, A. Muscholl, and D. Peled. Snapshot Verification. In Tools and Algorithms for Construction and Analysis of Systems, (TACAS'05), LNCS, pp. 510–525. Springer Verlag, 2005.
• B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. Journal of Computer and System Sciences, 2005.
• T. Schwentick, A. Muscholl, and L. Segoufin. Active Context-Free Games. Theory of Computing Systems (TOCS), vol. , pp. , 2005.
• A. Muscholl and I. Walukiewicz. An NP-complete fragment of LTL. International Journal of Foundations of Computer Science, vol. 16(4), pp. 743–455, 2005.
• B. Genest, D. Kuske, and A. Muscholl. A Kleene Theorem for a Class of Communicating Automata with Effective Algorithms. In Developments in Language Theory (DLT'04), LNCS, pp. 30–48. Springer Verlag, 2004.
• B. Genest, M. Minea, A. Muscholl, and D. Peled. Specifying and Verifying Partial Order Properties Using Template MSCs. In Proceedings of FoSSaCS'04, vol. 2987 of LNCS, pp. 195–210. Springer-Verlag, 2004.
• A. Muscholl, T. Schwentick, and L. Segoufin. Active Context-Free Games. In Proceedings of STACS'04, vol. 2996 of LNCS, pp. 452–464. Springer-Verlag, 2004.
• A. Muscholl and I. Walukiewicz. An NP-complete fragment of LTL. In Proceedings of DLT'04, LNCS. Springer-Verlag, 2004.
• H. Seidl, T. Schwentick, A. Muscholl, and P. Habermehl. Counting in Trees for Free. In International Colloquium on Automata, Languages and Programming (ICALP'04), LNCS, pp. 1136–1149. Springer Verlag, 2004.
• A. Stefanescu, J. Esparza, and A. Muscholl. Synthesis of distributed algorithms using asynchronous automata. In Proceedings of CONCUR'03, 2003.
• B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. In Proc. of the 29th International Colloquium on Automata, Languages and Programming, ICALP'02 (P. Widmayer et al., Eds.), vol. 2380 of Lect. Notes Comp. Sci., pp. 657–668, Malaga, Spain. Springer, 2002.

### Jakub Neumann

• J. Neumann, A. Szepietowski, and I. Walukiewicz. On the complexity of weak conditions. Information Processing Letters, vol. 84, pp. 181–187, 2002.

### Mogens Nielsen

• M. Jurdziński, M. Nielsen, and J. Srba. Undecidability of Domino Games and Hhp-Bisimilarity. Information and Computation, vol. 184(2), pp. 343–368, 2003.

### Damian Niwinski

• T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe Grammars and Panic Automata. In ICALP, vol. 3580 of Lecture Notes in Computer Science, pp. 1450–1461, 2005.
• D. Niwinski and I. Walukiewicz. Deciding Nondeterministic Hierarchy of Deterministic Tree Automata. Electr. Notes Theor. Comput. Sci., vol. 123, pp. 195–208, 2005.
• T. Colcombet and D. Niwinski. On the positional determinacy of edge–labeled games. Warsaw University, submitted, 2004.
• D. Niwinski and I. Walukiewicz. A gap property of deterministic tree languages. Theoretical Computer Sciences, vol. 303(1), pp. 215–231, 2003.

### Jan Obdržálek

• J. Obdržálek. DAG-width - Connectivity Measure for Directed Graphs. In SODA'06, 2006.
• J. Obdržálek. Fast Mu-calculus Model Checking when Tree-width is Bounded. In CAV'03, vol. 2725 of LNCS, pp. 80–92. Springer, 2003.

### Denis Oddoux

• P. Gastin and D. Oddoux. LTL with past and two-way very-weak alternating automata. In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS'03) (B. Rovan and P. Vojtávs, Eds.), LNCS, pp. 439–448. Springer-Verlag, 2003.

### Luke Ong

• A. Murawski, L. Ong, and I. Walukiewicz. Idealized Algol with Ground Recursion, and DPDA Equivalence. In ICALP'05, vol. 3580 of LNCS, pp. 917–929, 2005.

### Mike Paterson

• M. Jurdziński, M. Paterson, and U. Zwick. A Deterministic Subexponential Algorithm for Solving Parity Games. In Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, pp. 114–123. ACM/SIAM, 2006.

### Radek Pelánek

• P. Krčál and R. Pelánek. On Sampled Semantics of Timed Systems. In Proceedings of FSTTCS'05, Hyderabad, India. (R. Ramanujam and S. Sen, Eds.), vol. 3821 of Lecture Notes in Computer Science. Springer-Verlag, 2005.

### Doron Peled

• B. Genest, D. Kuske, A. Muscholl, and D. Peled. Snapshot Verification. In Tools and Algorithms for Construction and Analysis of Systems, (TACAS'05), LNCS, pp. 510–525. Springer Verlag, 2005.
• B. Genest, M. Minea, A. Muscholl, and D. Peled. Specifying and Verifying Partial Order Properties Using Template MSCs. In Proceedings of FoSSaCS'04, vol. 2987 of LNCS, pp. 195–210. Springer-Verlag, 2004.
• R. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün. Combining software and hardware verification techniques. Formal Methods in System Design, vol. 21(3), pp. 251–280, 2002.

### Dominique Perrin

• D. Perrin and J. Pin. Infinite Words. Elsevier, 2004.

### Reinhard Pichler

• G. Gottlob, C. Koch, and R. Pichler. The complexity of XPath query evaluation. In Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS-03), pp. 179–190, New York. ACM Press, 2003.

### Jean-Éric Pin

• D. Perrin and J. Pin. Infinite Words. Elsevier, 2004.
• J. Pin. The expressive power of existential first order sentences of Büchi's sequential calculus. Discrete Mathematics, vol. , pp. , 2004.

### Nir Piterman

• N. Piterman and M. Vardi. Micro-Macro Stack Systems: A New Frontier of Decidability for Sequential Systems. In 17th IEEE Symposium on Logic in Computer Science, 2003.
• O. Kupferman, N. Piterman, and M. Vardi. Pushdown Specifications. In 9th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Lecture Notes in Artificial Inteligence, 2002.

### Sandra Quickert

• J. Bradfield, J. Duparc, and S. Quickert. Transfinite Extension of the Mu-Calculus. In Computer Science Logic (L. Ong, Ed.), pp. 384–396. Springer-Verlag, 2005.

### David Richerby

• A. Dawar and D. Richerby. Fixed-Point Logics with Nondeterministic Choice. Journal of Logic and Computation, 2002.

### Mariane Riss

• J. Duparc and M. Riss. The Missing Link for \omega-Rational Sets, Automata, and Semigroups. International Journal of Algebra and Computation, 2003.

### Philipp Rohde

• C. Löding and P. Rohde. Solving the Sabotage Game is PSPACE-hard. Technical Report. RWTH Aachen, 2003.
• C. Löding and P. Rohde. Solving the Sabotage Game is PSPACE-hard. In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science, MFCS '03, vol. 2474 of LNCS, pp. 531–540. Springer, 2003.
• C. Löding and P. Rohde. Model Checking and Satisfiability for Sabotage Modal Logic. In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'03, vol. 2914 of LNCS, pp. 302–313. Springer, 2003.

### Pritam Roy

• L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, P. Roy, and M. Sorea. Sociable Interfaces. In Proceedings of 5th International Workshop on Frontiers of Combining Systems, vol. 3717 of Lecture Notes in Computer Science, pp. 81–105. Springer, 2005.

### Mayank Saksena

• T. Berg, B. Jonsson, M. Leucker, and M. Saksena. Insights to Angluin's Learning. Technical Report. Department of Information Technology, Uppsala University, 2003.

### Sven Sandberg

• H. Björklund, S. Sandberg, and S. Vorobyov. A Discrete Subexponential Algorithm for Parity Games. In 20th International Symposium on Theoretical Aspects of Computer Science, STACS'2003 (H. Alt and M. Habib, Eds.), vol. 2607 of Lecture Notes in Computer Science, pp. 663–674, Berlin. Springer-Verlag, 2003.
• H. Björklund, S. Sandberg, and S. Vorobyov. Complexity of Model Checking by Iterative Improvement: the Pseudo-Boolean Framework. In Andrei Ershov Fifth International Conference “Perspectives of System Informatics'' (A. Zamulin, Ed.), pp. 262–270, 2003.
• H. Björklund, S. Sandberg, and S. Vorobyov. Memoryless Determinacy of Parity Games: A Simple Proof. Theoretical Computer Science, 2003.
• H. Björklund and S. Sandberg. Algorithms for Combinatorial Optimization and Games Adapted from Linear Programming. In Proceedings of the Eighth ESSLLI Student Session (B. ten Cate, Ed.), 2003.

### Luigi Santocanale

• A. Arnold and L. Santocanale. Ambiguous Classes in the Games $\mu$-Calculus Hierarchy. In FOSSACS'03, vol. 2620 of LNCS, pp. 70–86, 2003.
• S. Ghilardi and L. Santocanale. Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics. In LPAR'03 (Logic for Programming Artificial Intelligence and Reasoning), 2003.
• L. Santocanale. On the Equational Definition of the Least Prefixed Point. Theoretical Computer Science, vol. 295(1-3), pp. 341–370, 2003.
• L. Santocanale. Logical Construction of Final Coalgebras. In Coalgebraic Methods in Computer Science (H. P. Gumm, Ed.), vol. 82 of Electronic Notes in Theoretical Computer Science. Elsevier, 2003.
• L. Santocanale. $\mu$-Bicomplete Categories and Parity Games. Theoretical Informatics and Applications, vol. 36, pp. 195–227, 2002.

### Pierre Yves Schobbens

• Y. Bontemps, P. Y. Schobbens, and C. Löding. Synthesis of Open Reactive Systems from Scenario-Based Specifications. Fundamenta Informaticae, vol. 62(2), pp. 139–169, 2004.

### Thomas Schwentick

• T. Schwentick, A. Muscholl, and L. Segoufin. Active Context-Free Games. Theory of Computing Systems (TOCS), vol. , pp. , 2005.
• A. Muscholl, T. Schwentick, and L. Segoufin. Active Context-Free Games. In Proceedings of STACS'04, vol. 2996 of LNCS, pp. 452–464. Springer-Verlag, 2004.
• H. Seidl, T. Schwentick, A. Muscholl, and P. Habermehl. Counting in Trees for Free. In International Colloquium on Automata, Languages and Programming (ICALP'04), LNCS, pp. 1136–1149. Springer Verlag, 2004.

### Stefan Schwoon

• A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejeck. Reachability Analysis of Multithreaded Software with Asynchronous Communication. In Proc. 25th Conf. on Found. of Software Technology and Theoretical Computer Science (FSTTCS'05), Lecture Notes in Computer Science, Madras, India. Springer Pub., 2005.

### Luc Segoufin

• T. Schwentick, A. Muscholl, and L. Segoufin. Active Context-Free Games. Theory of Computing Systems (TOCS), vol. , pp. , 2005.
• A. Muscholl, T. Schwentick, and L. Segoufin. Active Context-Free Games. In Proceedings of STACS'04, vol. 2996 of LNCS, pp. 452–464. Springer-Verlag, 2004.

### Helmut Seidl

• B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. Journal of Computer and System Sciences, 2005.
• H. Seidl, T. Schwentick, A. Muscholl, and P. Habermehl. Counting in Trees for Free. In International Colloquium on Automata, Languages and Programming (ICALP'04), LNCS, pp. 1136–1149. Springer Verlag, 2004.
• B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. In Proc. of the 29th International Colloquium on Automata, Languages and Programming, ICALP'02 (P. Widmayer et al., Eds.), vol. 2380 of Lect. Notes Comp. Sci., pp. 657–668, Malaga, Spain. Springer, 2002.

### Géraud Sénizergues

• G. Sénizergues. The Bisimulation Problem for Equational Graphs of Finite Out-Degree. SIAM Journal on Computing, Volume 34, Number 5, pp. 1025–1106, 2005.
• V. Bruyère, O. Carton, and G. Sénizergues. Tree automata and automata on linear orderings. In Proceedings WORDS'03, vol. 27 of LNCS, pp. 222–231. TUCS General Publication, 2003.
• S. Fratani and G. Sénizergues. Iterated Pushdown Automata and Sequences of Rational Numbers. In St Petersburg second Logic Days, 2003.
• G. Sénizergues. The Equivalence Problem for t-Turn DPDA Is Co-NP. In Proceedings ICALP'03, vol. 2719 of LNCS, pp. 478–489. Springer-Verlag, 2003.

### Olivier Serre

• O. Serre. Games with Winning Conditions of High Borel Complexity. Theoretical Computer Science, 2006.
• C. Löding, P. Madhusudan, and O. Serre. Visibly Pushdown Games. In Proceedings of FSTTCS'04, vol. 3328 of LNCS, pp. 408–420. Springer-Verlag, 2004.
• O. Serre. Contribution à l'étude des jeux sur des graphes de processus à pile. PhD thesis, Université Paris 7, 2004.
• O. Serre. Games with Winning Conditions of High Borel Complexity. In Proceedings of ICALP'04, vol. 3142 of LNCS, pp. 1150–1162. Springer-Verlag, 2004.
• A. Bouquet, O. Serre, and I. Walukiewicz. Pushdown games with unboundedness and regular conditions. In Proceedings of FSTTCS'03, vol. 2914 of LNCS, pp. 88–99. Springer-Verlag, 2003.
• O. Serre. Note on Winning Positions on Pushdown Games with $\omega$-Regular Conditions. Information Processing Letters, vol. 85, pp. 285–291, 2003.

### Leandro Dias da Silva

• L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, P. Roy, and M. Sorea. Sociable Interfaces. In Proceedings of 5th International Workshop on Frontiers of Combining Systems, vol. 3717 of Lecture Notes in Computer Science, pp. 81–105. Springer, 2005.

### Rafał Somla

• M. Lange and R. Somla. The Complexity of Model Checking Higher Order Fixpoint Logic. In Proc.\ 30th Int.\ Symp.\ on Math.\ Foundations of Computer Science, MFCS'05 (J. Jedrzejowicz and A. Szepietowski, Eds.), vol. 3618 of LNCS, pp. 640–651. Springer, 2005.
• R. Somla. New Algorithms for Solving Simple Stochastic Games. In Proceedings of the Workshop on Games in Design and Verification (GDV 2004), vol. 119 of Electronic Notes in Theoretical Computer Science, pp. 51–65. Elsevier, 2005.
• M. Leucker, R. Somla, and M. Weber. Parallel Model Checking for LTL, CTL{$^*$} and $L_{\mu^2$}. In Electronic Notes in Theoretical Computer Science (L. Brim and O. Grumberg, Eds.), vol. 89 of. Elsevier Science Publishers, 2003.

### Maria Sorea

• L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, P. Roy, and M. Sorea. Sociable Interfaces. In Proceedings of 5th International Workshop on Frontiers of Combining Systems, vol. 3717 of Lecture Notes in Computer Science, pp. 81–105. Springer, 2005.

### Jiří Srba

• M. Jurdziński, M. Nielsen, and J. Srba. Undecidability of Domino Games and Hhp-Bisimilarity. Information and Computation, vol. 184(2), pp. 343–368, 2003.

### Alin Stefanescu

• A. Stefanescu, J. Esparza, and A. Muscholl. Synthesis of distributed algorithms using asynchronous automata. In Proceedings of CONCUR'03, 2003.

### Colin Stirling

• M. Lange and C. Stirling. Model checking games for branching time logics. Journal of Logic and Computation, vol. 12(4), pp. 623–639, 2002.

### Jan Strejeck

• A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejeck. Reachability Analysis of Multithreaded Software with Asynchronous Communication. In Proc. 25th Conf. on Found. of Software Technology and Theoretical Computer Science (FSTTCS'05), Lecture Notes in Computer Science, Madras, India. Springer Pub., 2005.

### Andrzej Szepietowski

• J. Neumann, A. Szepietowski, and I. Walukiewicz. On the complexity of weak conditions. Information Processing Letters, vol. 84, pp. 181–187, 2002.

### Jennifer Tenzer

• J. Tenzer. GUIDE: Games with UML for Interactive Design Exploration. In Proceedings of the 4th International Conference on Software Methodologies, Tools, and Techniques, SoMeT'05.. IOS Press, 2005.
• J. Tenzer. Exploration games for safety-critical system design with UML 2.0. In Proceedings of the 3rd International Workshop on Critical Systems Development with UML, CSDUML'04, Technical Report I0415, pp. 41–55. Technische Universität München", 2004.

### P. S. Thiagarajan

• P. Krčál, L. Mokrushin, P. S. Thiagarajan, and W. Yi. Timed vs. Time Triggered Automata. In Proc. of CONCUR'04, London, UK. (P. Gardner and N. Yoshida, Eds.), vol. 3170 of Lecture Notes in Computer Science, pp. 340–354. Springer-Verlag, 2004.

### Wolfgang Thomas

• J. Cristau, C. Löding, and W. Thomas. Deterministic Automata on Unranked Trees. In Proceedings of the 15th International Symposium on Fundamentals of Computation Theory, FCT 2005, vol. 3623 of Lecture Notes in Computer Science, pp. 68–79. Springer, 2005.
• S. Wöhrle and W. Thomas. Model Checking Synchronized Products of Infinite Transition Systems. In Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS), pp. 2–11. IEEE Computer Society, 2004.
• T. Cachat, J. Duparc, and W. Thomas. Solving Pushdown Games with a Sigma-3 Winning Condition. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002, vol. 2471 of LNCS, pp. 322–336. Springer-Verlag, 2002.
• E. Grädel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games. Springer-Verlag, 2002.

### Tayssir Touili

• A. Bouajjani, M. Müller-Olm, and T. Touili. Regular Symbolic Analysis of Dynamic Networks of Pushdown Processes. In Proc. (CONCUR'05), vol. 3653 of Lecture Notes in Computer Science, San Franciso (Ca), USA, 2005.
• A. Bouajjani and T. Touili. On Computing Reachability Sets of Process Rewrite Systems. In Proc. 16th Intern. Conf. on Rewriting Techniques and Applications (RTA'05), vol. 3467 of Lecture Notes in Computer Science, Nara, Japan. Springer Pub., 2005.
• A. Bouajjani, J. Esparza, and T. Touili. Reachability Analysis of Synchronized PA Systems. In Proc. 6th Intern. Workshop on Verification of Infinite-State Systems (Infinity'04), London, UK. to appear in ENTCS, 2004.
• A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In Conference Record of POPL'03: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, pp. 62–73. ACM, 2003.
• A. Bouajjani and T. Touili. Reachability Analysis of Process Rewrite Systems. In Proc. 23rd Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03), vol. 2914 of Lecture Notes in Computer Science, 2003.

### Michael Ummels

• M. Ummels. Rational Behaviour and Strategy Construction in Infinite Multiplayer Games. Master's thesis, RWTH Aachen, 2005.

### Pawel Urzyczyn

• T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe Grammars and Panic Automata. In ICALP, vol. 3580 of Lecture Notes in Computer Science, pp. 1450–1461, 2005.

### Moshe Vardi

• N. Piterman and M. Vardi. Micro-Macro Stack Systems: A New Frontier of Decidability for Sequential Systems. In 17th IEEE Symposium on Logic in Computer Science, 2003.
• O. Kupferman, N. Piterman, and M. Vardi. Pushdown Specifications. In 9th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Lecture Notes in Artificial Inteligence, 2002.

### Aymeric Vincent

• A. Arnold, A. Vincent, and I. Walukiewicz. Games for synthesis of controllers with partial observation. Theoretical Computer Science, vol. 303(1), pp. 7–34, 2003.

### Tomas Vojnar

• A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In Proc. 12th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), Lecture Notes in Computer Science, Edinburgh, UK. Springer Pub., 2005.
• A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract Regular Model Checking. In Proc. 16th Intern. Conf. on Computer Aided Verification (CAV'04), vol. 3114 of Lecture Notes in Computer Science, Boston (MA), USA. Springer Pub., 2004.

### Sergei Vorobyov

• H. Björklund, S. Sandberg, and S. Vorobyov. A Discrete Subexponential Algorithm for Parity Games. In 20th International Symposium on Theoretical Aspects of Computer Science, STACS'2003 (H. Alt and M. Habib, Eds.), vol. 2607 of Lecture Notes in Computer Science, pp. 663–674, Berlin. Springer-Verlag, 2003.
• H. Björklund, S. Sandberg, and S. Vorobyov. Complexity of Model Checking by Iterative Improvement: the Pseudo-Boolean Framework. In Andrei Ershov Fifth International Conference “Perspectives of System Informatics'' (A. Zamulin, Ed.), pp. 262–270, 2003.
• H. Björklund, S. Sandberg, and S. Vorobyov. Memoryless Determinacy of Parity Games: A Simple Proof. Theoretical Computer Science, 2003.

### Igor Walukiewicz

• T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe Grammars and Panic Automata. In ICALP, vol. 3580 of Lecture Notes in Computer Science, pp. 1450–1461, 2005.
• S. Lasota and I. Walukiewicz. Alternating Timed Automata. In Proc. FOSSACS'05, vol. 3441 of LNCS, pp. 250–265. Springer-Verlag, 2005.
• A. Muscholl and I. Walukiewicz. An NP-complete fragment of LTL. International Journal of Foundations of Computer Science, vol. 16(4), pp. 743–455, 2005.
• A. Murawski, L. Ong, and I. Walukiewicz. Idealized Algol with Ground Recursion, and DPDA Equivalence. In ICALP'05, vol. 3580 of LNCS, pp. 917–929, 2005.
• A. Murawski and I. Walukiewicz. Third-Order Idealized Algol with Iteration is Decidable. In FOSSACS'05, vol. 3441 of LNCS, pp. 202–218, 2005.
• D. Niwinski and I. Walukiewicz. Deciding Nondeterministic Hierarchy of Deterministic Tree Automata. Electr. Notes Theor. Comput. Sci., vol. 123, pp. 195–208, 2005.
• I. Walukiewicz. Difficult Configurations – On the Complexity of LTrL. Formal Methods in System Design, vol. 26(1), pp. 27–43, 2005.
• I. Walukiewicz. How to fix it: using fixpoints in different contexts. In LPAR'04, vol. 3452 of LNAI, pp. 184–194, 2005.
• M. Bojańczyk and I. Walukiewicz. Characterizing EF and EX Tree Logics. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings (P. Gardner and N. Yoshida, Eds.), vol. 3170 of Lecture Notes in Computer Science, pp. 131–145. Springer-Verlag, 2004.
• A. Muscholl and I. Walukiewicz. An NP-complete fragment of LTL. In Proceedings of DLT'04, LNCS. Springer-Verlag, 2004.
• I. Walukiewicz. A landscape with games in the background. In IEEE LICS'04, pp. 356–366, 2004.
• A. Arnold, A. Vincent, and I. Walukiewicz. Games for synthesis of controllers with partial observation. Theoretical Computer Science, vol. 303(1), pp. 7–34, 2003.
• A. Bouquet, O. Serre, and I. Walukiewicz. Pushdown games with unboundedness and regular conditions. In Proceedings of FSTTCS'03, vol. 2914 of LNCS, pp. 88–99. Springer-Verlag, 2003.
• D. Niwinski and I. Walukiewicz. A gap property of deterministic tree languages. Theoretical Computer Sciences, vol. 303(1), pp. 215–231, 2003.
• J. Bernet, D. Janin, and I. Walukiewicz. Permissive strategies: from parity games to safety games. Theoretical Informatics and Applications (RAIRO), vol. 36, pp. 251–275, 2002.
• J. Neumann, A. Szepietowski, and I. Walukiewicz. On the complexity of weak conditions. Information Processing Letters, vol. 84, pp. 181–187, 2002.
• I. Walukiewicz. Deciding low levels of tree-automata hierarchy. In WoLLIC'02, vol. 67 of ENTCS, 2002.
• I. Walukiewicz. Local logics for traces. Journal of Automata, Languages and Combinatorics, vol. 7, pp. 259–290, 2002.

### Michael Weber

• M. Leucker, R. Somla, and M. Weber. Parallel Model Checking for LTL, CTL{$^*$} and $L_{\mu^2$}. In Electronic Notes in Theoretical Computer Science (L. Brim and O. Grumberg, Eds.), vol. 89 of. Elsevier Science Publishers, 2003.

### Pascal Weil

• B. Courcelle and P. Weil. The recognizability of sets of graphs is a robust property. Tcs, vol. 342, pp. 173–228, 2005.
• Z. Ésik and P. Weil. Algebraic recognizability of regular tree languages. Theoretical Computer Science, vol. 340, pp. 291–321, 2005.
• P. Weil. Algebraic recognizability of languages. In Proceedings MFCS 2004, vol. 3153 of LNCS, pp. 149–175. Springer-Verlag, 2004.
• P. Weil. On the logical definability of certain graph and poset languages. Journal Automata, Languages and Computation, vol. 9, pp. 147–165, 2004.
• Z. Ésik and P. Weil. On logically defined recognizable tree languages. In Proceedings FSTTCS 2003, vol. 2914 of LNCS, pp. 195–207. Springer-Verlag, 2003.

### Thomas Wilke

• E. Grädel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games. Springer-Verlag, 2002.

### Stefan Wöhrle

• S. Wöhrle. Decision Problems over Infinite Graphs: Higher-order Pushdown Systems and Synchronized Products. PhD thesis, RWTH Aachen, 2005.
• S. Wöhrle and W. Thomas. Model Checking Synchronized Products of Infinite Transition Systems. In Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS), pp. 2–11. IEEE Computer Society, 2004.
• A. Carayol and S. Wöhrle. The Caucal Hierarchy of Infinite Graphs In Terms of Logic and Higher-order Pushdown Automata. In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2003, vol. 2914 of Lecture Notes in Computer Science, pp. 112–123. Springer, 2003.

### Pierre Wolper

• A. Bouajjani, A. Legay, and P. Wolper. Handling Liveness Properties in (omega-)Regular Model Checking. In Proc. 6th Intern. Workshop on Verification of Infinite-State Systems (Infinity'04), London, UK. to appear in ENTCS, 2004.

### Hüsnü Yenigün

• R. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün. Combining software and hardware verification techniques. Formal Methods in System Design, vol. 21(3), pp. 251–280, 2002.

### Wang Yi

• P. Krčál, L. Mokrushin, P. S. Thiagarajan, and W. Yi. Timed vs. Time Triggered Automata. In Proc. of CONCUR'04, London, UK. (P. Gardner and N. Yoshida, Eds.), vol. 3170 of Lecture Notes in Computer Science, pp. 340–354. Springer-Verlag, 2004.
• P. Krčál and W. Yi. Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. In Proceedings of TACAS'04, Barcelona, Spain. (K. Jensen and A. Podelski, Eds.), vol. 2988 of Lecture Notes in Computer Science, pp. 236–250. Springer-Verlag, 2004.

### Marc Zeitoun

• B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. Journal of Computer and System Sciences, 2005.
• P. Gastin, B. Lerman, and M. Zeitoun. Distributed games and distributed control for asynchronous systems. In Proc. of the 6th Symposium Latin American Theoretical INformatics, LATIN'04 (M. Farach-Colton, Ed.), vol. 2976 of Lect. Notes Comp. Sci., pp. 455–465. Springer, 2004.
• P. Gastin, B. Lerman, and M. Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In Proc. of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'04, vol. 3328 of Lect. Notes Comp. Sci., pp. 275–286. Springer, 2004.
• P. Gastin, P. Moro, and M. Zeitoun. Minimization of counterexamples in SPIN. In Model Checking Software: Proc. of the 11th International SPIN Workshop, SPIN'04, vol. 2989 of Lect. Notes Comp. Sci., pp. 92–108. Springer, 2004.
• L. Hélouët, M. Zeitoun, and A. Degorre. Scenarios and Covert channels, another game... In Proc. of Games in Design and Verification, GDV'04, vol. 119 of Electronic Notes in Theoretical Computer Science, pp. 93–116. Elsevier, 2004.
• L. Hélouët, C. Jard, and M. Zeitoun. Covert channels detection in protocols using scenarios. In Proc. of SPV'03, Security Protocols Verification (M. Rusinowitch, Ed.), pp. 21–25, 2003.
• B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. In Proc. of the 29th International Colloquium on Automata, Languages and Programming, ICALP'02 (P. Widmayer et al., Eds.), vol. 2380 of Lect. Notes Comp. Sci., pp. 657–668, Malaga, Spain. Springer, 2002.

### Wiesław Zielonka

• H. Gimbert and W. Zielonka. Games Where You Can Play Optimally Without Any Memory. In Proceedings of CONCUR'05, vol. 3653 of Lecture Notes in Theoretical Computer Science, pp. 428. Springer-Verlag, 2005.
• H. Gimbert and W. Zielonka. When Can You Play Positionally? In Proceedings of MFCS'04, vol. 3153 of LNCS, pp. 686–697. Springer-Verlag, 2004.
• H. Gimbert and W. Zielonka. Discounting Infinite Games but How and Why? In Games in Design and Verification 04, vol. 119 of Electronic Notes in Theoretical Computer Science, pp. 3–9. Elsevier, 2004.
• W. Zielonka. An invitation to play. In Mathematical Foundations of Computer Science 2005, vol. 3618 of LNCS, pp. 58–70. Springer, 2004.
• W. Zielonka. Perfect-information Stochastic Parity Games. In Proceedings of FOSSACS'04, vol. 2987 of LNCS, pp. 499–513. Springer-Verlag, 2004.

### Uri Zwick

• M. Jurdziński, M. Paterson, and U. Zwick. A Deterministic Subexponential Algorithm for Solving Parity Games. In Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, pp. 114–123. ACM/SIAM, 2006.