The color coding means:

: all participate

: Doctoral students participate

: next seminar

Please find the abstracts below the schedule and note that some of the slides are made available here, internally.

Date | Time | Topic | Speaker | Room |
---|---|---|---|---|

2019 Oct 15 | 12:45-15:45 | The Abstract State Machines Method for High Level System Design and Analysis | Egon Börger (Università di Pisa) |
Universität Leipzig P 501 |

2019 Oct 22 | 13:15-16:15 | On Dualization in Lattices Given by Their Irreducible Elements or by Implication Bases. | Sergei Kuznetsov (National Research University Higher School of Economics, Moscow) |
TU Dresden APB E005 |

2019 Oct 29 | 13:15‑16:15 | TBA | TBA | TU Dresden APB E005 |

2019 Nov 12 | 12:45‑15:45 | Temporal Stream-based Specification Language (TeSSLa) | Torben Scheffel (Universität Lübeck) |
Universität Leipzig P 501 |

2019 Nov 19 | 13:15-16:15 | TU Dresden APB E005 |
||

2019 Nov 26 | 12:45‑15:45 | Universität Leipzig P 501 |
||

2019 Dec 10 | 13:15-16:15 | TBA | Nathanaël Fijalkow (CNRS, LaBRI, Bordeaux) |
TU Dresden APB E005 |

2019 Dec 17 | 13:15-16:15 | TU Dresden APB E005 |
||

2020 Jan 7 | 12:45‑15:45 | TBA | Christian Ikenmeyer (Max Planck Institute for Software Systems, Saarbrücken) |
Universität Leipzig P 501 |

2020 Jan 14 | 12:45‑15:45 | Universität Leipzig P 501 |
||

2020 Jan 21 | 13:15-16:15 | TBA | Sam van Gool (Utrecht University) |
TU Dresden APB E005 |

2020 Feb 4 | 12:45‑15:45 | Universität Leipzig P 501 |

### Abstracts

### Egon Börger: *The Abstract State Machines Method for High Level System Design and Analysis*

We explain the three basic concepts of the Abstract State Machines (ASM) Method for a rigorous development of software intensive systems. The method allows the practitioner to start with an accurate and trustworthy application-domain-centric system model and to link such a `ground model' in a well documented and controllable way through intermediate design steps (called `refinements') to its implementation. The method has been used successfully, under industrial constraints, for the design and analysis of complex hardware/software systems. We highlight some characteristic examples and provide the simple definition of ASMs, starting from scratch. Through its versatility the ASM approach is non-monolithic and integratable at any development level into current software design and analysis environments.

### Sergej Kuznetsov: *On Dualization in Lattices Given by Their Irreducible Elements or by Implication Bases.*

Dualization of a monotone Boolean function can be defined as transformation of the set of minimal 1 values to the set of its maximal 0 values or vice versa. Since dualization is equivalent to many important problems in computer and data sciences, including the famous problem of computing minimal transversals of a hypergraph, the quasi-polynomial dualization algorithm for Boolean lattices proposed by M. Fredman and L. Khachiyan in 1996 was an important breakthrough. It paved the way to generalizations for various classes of structures where dualization in output subexponential time is possible, among them dualization in lattices given by ordered sets of their elements or by products of bounded width lattices, like chains. A well-known fact underlying Formal Concept Analysis (FCA) is that every lattice is determined, up to isomorphism, by the ordered set of its meet (infimum) and join (supremum) irreducible elements. Dualization in the case where a lattice is given by the sets of irreducible elements (i.e., as a concept lattice) has an important application, e.g., it is equivalent to the problem of enumerating minimal hypotheses, a specific type of classifiers in a problem setting about learning from positive and negative examples. We show that dualization for representation of this type is impossible in output polynomial time unless P = NP. However, in an important particular case where the lattice is distributive, a subexponential algorithm can be proposed. We also discuss the complexity of dualization for several partial cases, as well as complexity of dualization when the lattice is given by an implication base.

### Torben Scheffel: *Temporal Stream-based Specification Language (TeSSLa)*

The Temporal Stream-based Specification Language (TeSSLa) is a specification language developed for the specification of properties over real-time constraints and asynchronous arrival of events on the input streams. A formula of TeSSLa is in the end a function mapping a set of input streams to a set of output streams.

This talk will provide a short introduction to TeSSLa and its application domains at first and then focus on the theoretical results for TeSSLa and various fragments of it regarding other well known formalisms like Turing machines, automata and logics as well as complexity results for different decision problems like equivalence of formulas.