The color coding means:
: all participate
: Doctoral students participate
Date  Time  Topic  Speaker  Room 

2015 Apr 14  13:3016:00  Qualitative Ratio and Weight Quantiles  Daniel Krähmann  TU Dresden INF E005 
Forbidden permutation patterns and constraint satisfaction problems  Tom Hanika (TU Dresden) 

2015 Apr 21  13:3015:00  Structural and Epistemic Approaches to Probabilistic Argumentation  Anthony Hunter (University College London) 
Universität Leipzig P 501 FelixKleinHörsaal 
2015 May 05  13:3015:00  From PSL to Transitionbased Generalized Büchi Automata  Alexandre DuretLutz (Epita) 
TU Dresden INF E005 
2015 May 12  13:3016:00  On quantitative firstorder logic  George Rahonis (Aristotle University of Thessaloniki) 
Universität Leipzig P 501 FelixKleinHörsaal 
2015 May 19  13:3015:00  Stochastic Semantics  George Rahonis (Aristotle University of Thessaloniki) 
Universität Leipzig P 501 FelixKleinHörsaal 
2015 Jun 02  13:3015:00  P ≠ P: Why Some Reasoning Problems are More Tractable Than Others  Markus Krötzsch (TU Dresden) 
TU Dresden INF E005 
2015 Jun 09  13:3016:00  Do unambiguous automata suit Markov chains?  David Müller  TU Dresden INF E005 
Open problems session  all Ph.D. students  
2015 Jun 16  09:0018:00  Interviews  Universität Leipzig Beratungsraum A 520 Neues Augusteum, 5. Stock 

2015 Jun 30  13:3015:00  Interactive Markov Chains (a short overview)  Kirstin Peters (TU Berlin/Dresden) 
TU Dresden INF E005 
2015 Jul 07  13:3016:00  Logical Characterization of +ωpicture languages  Parvaneh Babari  Universität Leipzig P 501 FelixKleinHörsaal 
Cancelled due to illness 
(TU München) 

2015 Jul 14  13:3015:00  Decidability and expressiveness of synchronizing Markov Decision processes and synchronizing Probabilistic automata  Mahsa Shirmohammadi (University of Oxford) 
Universität Leipzig P 501 FelixKleinHörsaal 
Abstracts
Daniel Krähmann: Qualitative Ratio and Weight Quantiles
Using probabilistic modelchecking techniques, quantiles and ratio objectives allow to reason about energyutility tradeoffs in Markov chain models. Whereas former approaches focused on quantiles and ratio objectives in isolation, we deal with a combination thereof. In particular, we show that qualitative ratio quantiles can be efficiently computed. That is, the exact computation of optimal thresholds, which are almost surely or with positive probability exceeded by the ratio between energy and utility, can be done in polynomial time. We also provide polynomialtime algorithms solving related decision problems on ratio and weight objectives.
This is joint a work with Christel Baier, Clemens Dubslaff, and Jana Schubert.
Tom Hanika: Forbidden permutation patterns and constraint satisfaction problems
We investigate a new class of constraint satisfaction problems in the context of forbidden permutation patterns.
For a set of permutations P the set of permutations avoiding all elements of P is denoted by A(P). We define ForbPermCSP(P) to be the computational problem of deciding whether two given binary relations on a finite set can be extended to linear orders coding a permutation in A(P).
Our goal is to classify the complexity of this problem for all finite sets of permutations P. We present polynomialtime algorithms for this problem in the case that P equals {231, 312}, {132, 213}, and {3142, 2413}. For these permutations, A(P) is known as the class of layered permutations, reverse layered permutations, and separable permutations, respectively.
Anthony Hunter: Structural and Epistemic Approaches to Probabilistic Argumentation
Argumentation can be modelled at an abstract level using an argument graph (i.e. a directed graph where each node denotes an argument and each arc denotes an attack by one argument on another). Since argumentation involves uncertainty, it is potentially valuable to consider how this can quantified in argument graphs. In this talk, we will consider two probabilistic approaches for modeling uncertainty in argumentation. The first is the structural approach which involves a probability distribution over the subgraphs of the argument graph, and this can be used to represent the uncertainty over the structure of the graph. The second is the epistemic approach which involves a probability distribution over the subsets of the arguments, and this can be used to represent the uncertainty over which arguments are believed. The epistemic approach can be constrained to be consistent with Dung’s dialectical semantics, but it can also be used as a potential valuable alternative to Dung’s dialectical semantics. We will consider applications of probabilistic argumentation in handling enthymemes (arguments with incomplete premises) and in selecting moves in an argumentation dialogue.
Alexandre DuretLutz: From PSL to Transitionbased Generalized Büchi Automata
Couvreur [FM'99] has introduced a simple yet efficient algorithm to translate LTL formulas into Generalized Büchi Automata with Transitionbased acceptance (TGBA), based on a tableau construction. These TGBA can then be used directly for model checking.
We show how to extend this algorithm to create TGBA from formulas expressed in the linear fragment of PSL, which basically are LTL formulas over regular expressions. Translating PSL formulas is typically done using alternatingautomata (not 1weak, as in the case of LTL). Here we mix some ideas of the MiyanoHayashi construction for alternation removal with the tableau construction of Couvreur, in order to avoid constructing an alternatingautomaton.
George Rahonis: On quantitative firstorder logic
We extend the wellknown expressive equivalence of firstorder logic, LTL, star free languages and counterfree Büchi automata in two quantitative setups. First, over the maxplus semiring with discounting, and second over complete, idempotent and zerodivisor free semirings. We state several open problems for future research.
George Rahonis: Stochastic Semantics
We investigate stochastic systems of equations of tree series and consider their least [IO] and OIsolutions in arbitrary substochastic algebras. We prove that it is decidable whether the components of these solutions are stochastic functions or not. For the class of stochastically OIequational tree series, i.e., the components of the least OIsolutions of stochastic systems in the term algebra, we state a Kleene type theorem. We present two applications of our theory, namely the consistency problem for stochastic tree automata is decidable, and a Kleene theorem for the class of word series generated by stochastic contextfree grammars.
Markus Krötzsch: P ≠ P: Why Some Reasoning Problems are More Tractable Than Others
Knowledge representation and reasoning leads to a wide range of computational problems, and it is of great interest to understand the difficulty of these problems. Today this question is mainly studied using computational complexity theory and algorithmic complexity analysis. For example, entailment in propositional Horn logic is Pcomplete and a specific algorithm is known that runs in linear time. Unfortunately, tight algorithmic complexity bounds are rare and often based on impractical algorithms (e.g., O(n^2.373) for transitive closure by matrix multiplication), whereas computational complexity results abound but are very coarsegrained (e.g., many Pcomplete problems cannot be solved in linear time).
In this talk, we therefore advocate another approach to quantifying the difficulty of a computation: we reformulate computational problems as query answering problems, and then ask how powerful a query language is needed to solve these problems. This reduces reasoning problems to a computational model – query answering – that is supported by many efficient implementations. It is of immediate practical interest to know if a problem can be reduced to query answering in an existing database system. On the theoretical side, it allows us to distinguish problems in a morefine grained manner than computational complexity without being specific to a particular algorithm. We provide several examples of this approach and discuss its merits and limitations.
Kirstin Peters: Interactive Markov Chains (a short overview)
The talk will provide a short introduction into interactive Markov Chains. Interactive Markov Chains are an extension of labelled transition systems with exponentially delayed transitions. They are closed under parallel composition and hiding. Interactive Markov Chains are a natural semantic model for stochastic process algebras.
Parvaneh Babari: Logical Characterization of +ωpicture languages
Languages of finite and infinite twodimensional words (pictures and ωωpictures, respectively) have been considered by several research groups, and several formal models to recognize or generate finite or infinite twodimensional objects have been proposed in literature. Here, we define a new class of twodimensional languages and we call them +ωpicture languages. These are pictures with finite number of rows but infinite number of columns. We have already characterized this family by three different devices, namely, a kind of automata device called Büchi twodimensional online tessellation automata, tiling systems with a Büchi accepting conditions and also domino systems, and we obtained an equivalence theorem for +ωpicture languages describing recognizable languages in terms of our automata model, sets of tiles and sets of dominoes. In this paper, we solve the open problem regarding logical characterization of +ωpicture languages. We define an existential monadic secondorder logic which is equipped with an existential quantifier that is applied to secondorder variables for infinite sets and we prove that the class of +ωpicture languages is Büchi tiling systems recognizable if and only if it is definable in terms of our existential monadic secondorder logic.
Salomon Sickert: Deterministic omegaAutomata for LTL: A safraless, compositional and mechanically verified construction
Recently a new method directly translating linear temporal logic (LTL) formulas to deterministic (generalized) Rabin automata was proposed by Javier Esparza and Jan Křetínsḱy. Compared to the existing approaches of constructing a nondeterministic Buechiautomaton in the first step and then applying a determinization procedure (e.g. some variant of Safra's construction) in a second step, this new approach preservers a relation between the formula and the states of the resulting automaton. While the old approach produced a monolithic structure, the new method is compositional. Furthermore it was shown in experiments that the resulting automata were much smaller then the automata generated by existing approaches. In order to guarantee the correctness of the construction a full verification of it was done using Isabelle/HOL.
In my talk I will introduce the basic concepts and essential ideas of the construction.
Mahsa Shirmohammadi: Decidability and expressiveness of synchronizing Markov Decision processes and synchronizing Probabilistic automata
Markov decision processes (MDPs) are finitestate probabilistic systems with both strategic and random choices, hence wellestablished to model the interactions between a controller and its randomly responding environment. An MDP is viewed as a 1/2player stochastic game played in rounds when the controller chooses an action, and the environment chooses a successor according to a fixed probability distribution.
Recently, MDPs have been viewed as generators of sequences of probability distributions over states, called the distributionoutcome. We introduce synchronizing conditions defined on distributionoutcomes, which intuitively requires that some (group of) state(s) tend to accumulate all the probability mass. We consider the following modes of synchronization: the always mode where all distributions of the distributionoutcome must be synchronized, the eventually mode where some distributions must be synchronized, the weakly mode where infinitely many distributions must be synchronized, and the strongly mode where all but finitely many distributions must be synchronized.
For each synchronizing mode, we study three winning modes: sure, almostsure and limitsure. In this talk, we present the various synchronization modes and winning modes, as well as an overview of the key properties for their analysis.
We also give hints on synchronization in probabilistic automata (PAs), that are kind of MDPs where controllers are restricted to use only wordstrategies; i.e. no ability to observe the history of the system execution, but the number of choices made so far.