The first QuantLA spring school takes place from 10th to 15th of March in Gohrisch. Our guest lecturer is Anca Muscholl.
Internal information on the Spring School can be found: here
Time Table
Updated: 7. March
Course Programme
Automata and Logic: Franz Baader
This course considers finite automata that work on finite or infinite words. The course concentrates on the connection between these automata and logics that play an important role in computer science, such as first-order logic and monadic second-order logic. It will be shown how closure and decidability results for the automata can be used to obtain decidability results for these logics.
The course is divided into the following three sessions:
- First-order logic and star-free languages
- Languages of infinite words and Büchi automata
- Monadic second-order logic and regular languages of infinite words.
4 × 60 min.
Probabilistic Model Checking: Christel Baier
Markov chains and Markov decision processes are the most prominent probabilistic models and widely used for the model-based quantitative system analysis. Both Markov chains and Markov decision processes can be understood as automata with annotated stochastic distributions that e.g. can serve to specify execution times of jobs or the frequency of failures or represent the effect of coin tossing actions in randomized algorithms. Using Markovian models to formalize the operational system behavior, one is typically interested in quantitative properties stating that the probability for a certain event or the expected value of a random variable meets a given bound. For a round-based randomized leader-election protocol, for instance, one might require that the probability for a leader to be elected within ten rounds is at least 0.995 and that the average number of rounds until a leader has been elected is below five. For another example, for a mutual exclusion protocol that coordinates the access to shared resources by processes whose execution times for the critical and noncritical actions are specified stochastically, one might be interested in the average time some process has to wait for the shared resource and the probability for scenarios where some process is continuously denied requested resources (starvation).
The tutorial will present the main concepts of discrete-time Markovian models and techniques to establish quantitative properties for them. For this, we will consider probabilistic computation tree logic, one of the prominent temporal logics to specify quantitative properties of probabilistic systems, and present model checking algorithms for finite-state Markov chains and Markov decision processes.
2 × 60 min.
Weighted Automata: Manfred Droste
We give an introduction into the area of weighted automata. They consist of classical finite automata in which the transitions carry weights. These weights may model, e.g., the cost, the consumption of resources, or the reliability or probability of the successful execution of the transitions. We will present different weight structures like semirings, bimonoids, lattices, and also computations of behaviors of recent interest like average sum or discounted sum of costs. If time permits, we present a characterization of the possible behaviors by rational series.
2 × 60 min.
Handling exceptions in Knowledge Representation: An Introduction to Nonmonotonic Reasoning: Gerd Brewka
In nonmonotonic reasoning additional knowledge may invalidate former conclusions. Given that most of our commonsense knowledge comes in the form of generic statements which may have exceptions, this kind of reasoning is essential for models of human reasoning. The lecture will introduce some of the most influential formal accounts of nonmonotonic reasoning. Starting from a simple, highly restricted form, namely reasoning under the closed world assumption, we will explore three main variants that have been described in the literature:
1) reasoning based on preferences among the formulas in a knowledge base (Poole systems, preferred subtheories),
2) reasoning based on preferred models (circumscription),
3) reasoning based on nonstandard inference rules (default logic).
We also cover logic programs with default negation under stable model semantics and the answer set programming paradigm.
2 × 60 min.
Description Logics: Anni-Yasmin Turhan
Description Logics (DLs) can be used to represent the conceptual knowledge of an application domain in a structured and formally well-understood way. Based on their formal semantics, many reasoning procedures have been defined and investigated for a range of DLs. This course introduces basic notions underlying knowledge representation with DLs, reasoning procedures for DLs and their complexity. We also take a look at the Semantic Web ontology language OWL and its profiles, which are based on DLs.
2 × 60 min.
Order, lattices, and formal concepts: Bernhard Ganter
We give an introduction to the theory of Formal Concept Analysis (FCA), a research field at the TU Dresden mathematics department. FCA associates to almost arbitrary data sets an algebraic structure, called the concept lattice. These lattices are then used for knowledge communication and processing.
Although there are many connections to the topics of the Quantla Research Training Group, there are also considerable differences in language and methodology. The main part of the two lectures therefore consists of examples demonstrating the representation of concrete data sets in the algebraic manner. Mathematical and algorithmic aspects are only sketched.
2 × 60 min.
Synthesis—going distributed : Anca Muscholl
Synthesis is the task of constructing a system from a given specification. When the system is reactive, meaning that it faces an (uncontrollable) environment, synthesis amounts to solving games. In this tutorial we focus on synthesis in a distributed setting. This topic is very challenging for several reasons. First, the undecidability borderline is very close. Second, an extension of the classical theory on logic and automata over trees to distributed systems still has to be developed. We present results on distributed in two different models - a synchronous one due to Pnueli and Rosner, and an asynchronous one, based on Zielonka automata.
3 × 60 min.
Real-timed automata: Karin Quaas
Timed automata extend finite automata with a finite number of real-valued clock variables. A clock variable measures the time that is spent in one state of the automaton. Transitions between states can be labelled with clock constraints of, e.g., the form x<2: the transition can only be taken if the current value of the clock variable x is less than 2. In this way, timed automata can be used to model real-time systems, i.e., systems whose behaviour depends on time. Due to the real-valued clock variables, the state-transition-system induced by a timed automaton is infinite. In this course, we learn that none-the-less the reachability problem for timed automata is decidable. The proof is based on the region-graph construction, which is the basis for many other decidability proofs in the theory of timed automata
2 × 60 min.
Statistical Machine Translation of Natural Languages: Heiko Vogler
In this course we will consider the expectation-maximization (EM) algorithm which allows, e.g., to deduce from a bilingual corpus (like the parliament proceedings English-French) a dictionary for the two involved languages. Eventually the EM algorithm generates a probability distribution which, in the above example, shows the most probable translation of a word.
2 × 60 min.
Descriptive Complexity Theory: Markus Lohrey
The course will give an introduction into descriptive complexity theory. The aim of this branch of finite model theory is to characterize complexity classes by logics. One of the first and most fundamental results in descriptive complexity theory is Fagin's theorem from 1974: A class C of finite structures (over a fixed relational signature) belongs to the complexity class NP (nondeterministic polynomial time) if and only if C can be defined by a sentence of existential second-order logic. In the course, I will present a proof of this result. If time permits, I will also mention logical characterizations of other complexity classes (L, NL, Ptime, PSPACE).
2 × 60 min.
