Theoretical Computer Science

Theorie-Workshop 2018: Automata, Languages, and Games

Zur Veranstaltung

Am Donnerstag werden wir um 19.00 Uhr im Restaurant Kleine Burg (Burgstraße 2, 26122 Oldenburg) essen. Es ist für zwölf Personen reserviert. Ab- und weitere Zusagen bitte per Mail an Frau Soleinsky (a.soleinsky@tu-bs.de).

Programm (Donnerstag)

Vorträge

1. Decomposing Finite Automata
   Peter Chini, TU Braunschweig

The parallelization of processes has wide influence on software and hardware architecture. For instance, memory/space consumption and running time of systems can be drastically reduced. From a theoretical point of view, parallelization corresponds to decomposing the chosen model of computation. In this talk we present an algorithm for the decomposition of one of the standard models: Nondeterministic finite automata (NFA).

Given an arbitrary NFA A over an alphabet Sigma and an encoding of the states, the algorithm outputs several smaller NFAs over a new alphabet Gamma. The product of these NFAs is isomorphic to A, up to a homomorphism h from Gamma to Sigma. We show that the homomorphism cannot be avoided and that choosing h and Gamma as small as possible is an NP-hard problem.

The quality of the output further relies on the given encoding of the states. We suggest binary encodings and prime encodings, encodings based on the Chinese Remainder Theorem. However, finding an efficient encoding of one of these two kinds is difficult. It is not tractable to compare all possible encodings. Instead, we introduce a measure, called the distance, which captures the quality of an encoding. Then we look for an encoding of small distance.

2. Towards Local Winning Conditions for Petri Games
   Manuel Gieseking, C.v.O. Universität Oldenburg

Petri games are used for the synthesis of distributed systems with causal memory. The processes are modeled as the token of a Petri net and are considered to be the players of a multi-player game. It has been shown by Finkbeiner and Olderog that whether the system players have a cooperative strategy such that one environment player and an arbitrary number of system players never reach a bad place can be decided in single-exponential time in the size of the Petri net.

This talk gives a short overview of this model and its solving techniques. We mainly focus on the decision procedure and give a short glimpse of a semi-decision procedure — the bounded synthesis approach. We furthermore introduce a new idea for specifying local winning condition such as existential and universal safety and reachability conditions. Exemplarily, this enables us to ask whether there is a strategy such that at least one process stays on safe places. Finally, we can have a short look into ADAM and the prototype web interface, a tool which automatically creates the desired strategies if existent.

3. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems
   Roland Meyer, TU Braunschweig

We give a polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games over the same class of graphs. We show that reductions from parity to safety by Bernet et al. for finite graphs and Fridman and Zimmermann for pushdown graphs generalize to both higher-order pushdown systems and their extension, collapsible pushdown systems. Moreover, the exponential blow-up of these reductions can be avoided because higher-order stacks can encode large numbers and the parity condition has a stack-like behaviour (in a precise sense). As well as providing theoretical interest, our result fits into a recent trend of reducing liveness properties to safety, allowing the advanced state-of-the-art in safety checking to be used for more expressive specifications.

4. Regular Separability of Well-Structured Transition Systems
   Sebastian Muskalla, TU Braunschweig

We investigate the languages recognized by well-structured transition systems (WSTS). We show that, under mild assumptions, every two disjoint WSTS languages are regularly separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. For the case of Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator.

5. Denotational sematics for context-free games and an outlook to term games
   Elisabeth Neumann, TU Braunschweig

We consider the problems of safety and liveness synthesis for recursive programs. To this end, we study two-player games played over the infinite graph of sentential forms induced by either a context-free or an omega-context-free grammar (that comes with an ownership partitioning of the non-terminals). The winning condition is inclusion of the derived terminal word in the language of a finite or a Büchi automaton. Our contributions are denotational semantics of the games, giving rise to new algorithms to decide the winning player and to compute her strategy.

For the safety case, our approach is based on a novel representation of all plays starting in a non-terminal. The representation (the semantics) uses the domain of Boolean formulas over the transition monoid of the target automaton. The elements of the monoid are essentially procedure summaries, and our approach can be seen as the first summary-based algorithm for the synthesis of recursive programs.

For the liveness case, we generalize the summary-based algorithm from finite to infinite words, proceeding as follows. In a first step, we determinize the given Büchi automaton into a parity automaton. The second step computes formula summaries for safety games that have the parity automaton as the right-hand side. Finally, we connect the formula summaries to a parity game and solve it to determine the winner of the omega-context-free game.

For both problems, our algorithms have optimal doubly-exponential time complexity.

In a small outlook, we analyse the denotational semantics of non-deterministic computations in sequential, recursive programs more closely. We consider non-determinism in a broad sense, including not only angelic and demonic choices but also perfect and imperfect information about the computation. The key insight is that, despite targeting sequential computation, the programming model should have multiple players. Each player corresponds to a form of non-determinism. We propose term games and their semantics as a model that implements this insight and forms the vehicle for our study. In particular, (safety) synthesis for recursive programs can be reduced to term games.

6. Parity Games over Hyperedge Replacement Grammars
   Christoph Peuser, C.v.O. Universität Oldenburg

We consider correctness of hyperedge replacement grammars under adverse conditions. In contrast to existing approaches, the influence of an adverse environment is considered in addition to system behaviour. To this end, we construct a hyperedge replacement game where rules represent the moves available to players and a temporal condition specifies the systems desired properties. In particular, the construction of parity pushdown games from hyperedge replacement grammars results in a decidable class of games.

7. Petrinetz-Synthese
   Uli Schlachter, C.v.O. Universität Oldenburg

Es werden die Grundlagen der Petrinetz-Synthese vorgestellt. Dies bedeutet, dass aus einem gegebenen Verhalten in Form eines beschrifteten Transitionssystems (LTS) ein Petrinetz erzeugt werden soll, dessen Erreichbarkeitsgraph isomorph zur Eingabe ist. Hierfür wird auf Regionentheorie und Separierungsprobleme eingegangen und ein einfacher Algorithmus formuliert. Die vorgestellten Resultate basieren auf dem Buch “Petri Net Synthesis“ von Badouel, Bernardinello und Darondeau.

Aufbauend hierauf wird ein Algorithmus zur kleinsten Überapproximation eines LTS entwickelt. Anstatt zu einer unlösbaren Eingabe einen Fehlschlag zu liefern, verändert dieser Algorithmus das LTS, damit die Petrinetz-Synthese möglich wird.

8. Erreichbarkeit bei Petrinetzen
   Harro Wimmel, C.v.O. Universität Oldenburg

Der Vortrag soll — ohne dabei zu tief in die mathematischen Details einzusteigen — eine Vorstellung davon liefern, wie man das Erreichbarkeitsproblem bei Petrinetzen, also die Frage, ob in einem gegebenen Petrinetz mit zwei Markierungen die eine Markierung von der anderen aus durch Feuern von Transitionen erreicht werden kann, allgemein algorithmisch lösen kann. Die gezeigten Beweistechniken können dann genutzt werden, um die Problemstellung in verschiedene Richtungen zu erweitern, etwa indem weitere Markierungen hinzugefügt werden, die “zwischendurch“ passiert werden müssen, oder indem Abhängigkeiten zwischen den beteiligten Markierungen erzwungen werden können, oder indem anstelle einzelner Markierungen komplette lineare oder semi-lineare Mengen von Markierungen als Start und Ziel festgelegt werden.