The slides of the talk are available here.

Als Gast wird Frau Dr. Brands, die
Gleichstellungsbeauftragte der RWTH Aachen, vortragen.
Mehr Informationen:  www.informatik.rwth-aachen.de/Promotionscafe/

All AlgoSyns (doctoral students and professors) are requested
to do their registration.

Schedule

Part A: Algorithmic Game Theory, Mechanism Design, Auction Systems

• Lectures on Computational Complexity in Games and Auctions
  by Constantinos Daskalakis (Massachusetts Institute of Technology)

• Lectures on Linear programming and Mechanism Design
  by Rakesh Vohra (Kellog School of Management)

Part B: Games and Software Synthesis, Automata and Learning, Software Verification

• Lectures on Automata and Learning Based Methods in Software Verification
  by Madhusudan Parthasarathy, University of Illinois at Urbana-Champaign

• Featured talk on Games, Synthesis, Verification and Learning: A Bird’s Eye View of AlgoSyn
  by Wolfgang Thomas, RWTH Aachen U.

Register and more information: here

In this talk I will consider several probabilistic (or quantitative) variants of Kozen’s Modal mu-Calculus, designed for expressing properties of probabilistic-nondeterministic transition systems. Two type of semantics can be defined for these logics: one denotational and one based on a novel kind of games which I call Tree games. I will discuss the main result of my PhD thesis: the equivalence of the two semantics (proved in ZFC set theory extended with Martin’s Axiom at the first uncountable cardinal). I will also present some more recent results (joint work with Alex Simpson).

Abstract: Several notions of bisimulation for Probabilistic Nondeterministic Transition Systems (PNTS) have been proposed in the literature. I will develop the theory of what I call “Upper-Expectation bisimilarity” using standard results of linear algebra and functional analysis and provide strong mathematical foundations for real-valued modal logics for PNTS’s.

In the theory of deterministic automata for languages of infinite words, a fundamental result relates the family of infinitary limits of regular languages and the family of omega-languages recognized by deterministic Buechi automata. Furthermore, a theorem due to L. Landweber states that an omega-regular language is recognized by a deterministic Buechi automaton if and only if it is recognized by a deterministic Muller automaton whose acceptance component is closed under supersets. With the known definitions of asynchronous automata, these results does not extend to the context of traces. We introduce the family of deterministic, synchronization-aware asynchronous automata which allows us to establish these results, while the definition of Muller automata obtained therein captures all omega-regular trace languages. We also positively answer an open question in the theory of traces, namely, whether every omega-regular trace language can be expressed as a finite Boolean combination of deterministically Buechi recognizable languages.