TU BRAUNSCHWEIG

Programm (vorläufig)

05.03.2014
ab 19:00 Uhr Dinner in der Tonmühle
06.03.2014
bis 09:00 Uhr Frühstück
Raum 1 Raum 2
09:00 Uhr Begrüßung
09:15 Uhr Lazy TSO Reachability
Georgel Calin
09:45 Uhr Kaffeepause
10:30 Uhr Construction of the Lattices of Prime Event Structures
Evgeny Erofeev
Deciding Robustness against Power
Egor Derevenetc
11:15 Uhr Wachsende Kausalität und Asymmetrische Nebenläufigkeit
David Karcher
Memory Model-aware Testing -- a Unified Complexity Analysis
Florian Furbach
12:00 Uhr Mittagspause
14:00 Uhr

Invited Talk
Pawel Sobocinski

15:00 Uhr Kaffeepause
15:45 Uhr Failure Semantics for Modal Transition Systems
Ferenc Bujtor
Abstraction refinement based on unsatisfiability cores and SMT solving
Grigory Markin
16:30 Uhr Learning Transparent Data Automata
Normann Decker
States in Process Calculi
Christoph Wagner
ab 18:15 Uhr Abendessen
07.03.2014
bis 09:00 Uhr Frühstück
Raum 1 Raum 2
09:15 Uhr  A Framework for the Analysis of Well-structured Graph Transformation Systems
Jan Stückrath
10:00 Uhr Kaffeepause
10:30 Uhr On the Step Branching Time Closure of Free Choice Petri Nets
Stephan Mennicke
Lifting Adjunctions to Coalgebras to (Re)Discover Automata Constructions
Henning Kerstan
11:15 Uhr

Monitoring Modulo Theories
Daniel Thoma

Computing Language Equivalence for Weighted Automata Coalgebraically
Sebastian Küpper
12:00 Uhr Mittagspause
14:00 Uhr Business-Meeting der GI-Fachgruppe "Concurrency Theory"
15:00 Uhr Verabschiedung / Kaffeepause / Abreise

Themenvorschläge (eingereicht bis 07.02.2014)

Insgesamt haben wir 13 Themenvorschläge erhalten. Wie auch bei früheren D-CONs wollen wir von den Teilnehmenden erfahren, welche Vorträge nicht parallel gehalten werden sollten. Auf Basis der Abstimmung wird dann das Programm der D-CON erstellt. Derzeit ist jeder Vortragsslot 45 Minuten lang. Nachfolgend nun die Themenvorschläge.

States in Process Calculi
Christoph Wagner (TU Berlin) en/de
Im Vortrag beschäftigen wir uns mit der Reduzierbarkeit von Zustandsräumen in Prozesskalkülen am Beispiel eines verteilten Konsensalgorithmus. Dieser wurde mit einem Prozesskalkül modelliert, der strukturelle Kongruenz enthält. Wir verwenden Standardformen - eine Art Repräsentanten -, um den durch die Prozessterme aufgespannten Zustandsraum zu reduzieren. Diese Reduktion ermöglicht uns Invarianten ohne explizite Berücksichtigung des Zustandsraumes zu beweisen.
Wachsende Kausalität und Asymmetrische Nebenläufigkeit
David Karcher (TU Berlin) en/de
In Ereignisstrukturen ist Kausalität ein statischer Begriff. Wir haben die Kausalität dynamisiert, d.h. Ereignisse können die Kausalität anderer Ereignisse beeinflussen. In diesem Vortrag beschränke ich mich auf wachsende Kausalität. Wenn man Gleichzeitigkeit von hinzufügenden und betroffenen Ereignissen ausschließt, reicht ein herkömmliches Nebenläufigkeits-Modell aus; falls jedoch nicht, und das Ereignis a dem Ereignis b die Ursache b hizufügt, so ist der Ablauf ba und die nebenläufige Ausführung von a und b erlaubt, nicht jedoch der Ablauf ab. Diese Art von asymmetrischer Nebenläufigkeit untersuchen wir in unserem aktuellen Forschungskontext.
On the Step Branching Time Closure of Free Choice Petri Nets
Stephan Mennicke (TU Braunschweig) en/de

Free-choice Petri nets constitute a non-trivial subclass of Petri nets, excelling in simplicity as well as in analyzability. Extensions of free-choice nets have been investigated and shown to be
translatable back to interleaving-equivalent free-choice nets. In this paper, we investigate extensions of free-choice Petri nets up to step branching time equivalences. For extended free-choice nets, we achieve a generalization of the equivalence result by showing that an existing construction respects weak step bisimulation equivalence. The known translation for behavioral free-choice does not respect step branching time equivalences, which turns out to be a property inherent to all transformation functions from this net class into (extended) free-choice Petri nets. By analyzing the critical structures, we find two subsets of behavioral free-choice nets that are step branching time equivalent to free-choice nets. In the center of this talk, we provide a discussion concerning the actual closure of free-choice Petri nets up to step branching time equivalences.

Lazy TSO Reachability
Georgel Calin (TU Kaiserslautern) en
Reachability is a paramount problem in concurrency. Checking reachability for programs with a sequentially consistent (SC) semantics is known to be PSpace-complete. If the programs are subject to a semantics weaker than SC, checking reachability is usually harder -- e.g. non-primitive recursive for Total Store Order (TSO). Due to how difficult reachability is, the research community has sought for other easier -- yet relevant! -- problems to ensure system safety. Such a problem, proved PSpace-complete for TSO and not only (see next abstract), is checking robustness of concurrent programs. Intuitively, robustness requires that a program's weak behavior and its SC behavior match. This motivates our key question: how can one -- similarly to using SAT for SC reachability -- employ (iterative) robustness to solve TSO reachability? Our contribution is a (sound and complete) semi-decision procedure for TSO reachability based on robustness. Our method uses robustness queries to lazily emulate TSO delays that are necessary for finding reachability witnesses.
Deciding Robustness against Power
Egor Derevenetc (TU Kaiserslautern) en
Power is a RISC architecture developed by IBM, Freescale and several other companies and implemented in a series of POWER processors. The architecture features a complicated memory model providing very weak guarantees with respect to the ordering of memory accesses and the store atomicity of operations. Consequently, concurrent programs running on Power may exhibit behaviors that are not possible on a sequentially consistent architecture.

We call a program robust against Power if every Power computation of this program has the same data and control dependencies as some sequentially consistent (SC) computation. Robust programs are guaranteed to produce the same results on Power and SC architectures, which means that they only need to be verified for one of them. We present an algorithm for deciding robustness against Power. This is the first decidability result for Power architectures, and the first decidability result for non-store atomic memory models.

We obtain the algorithm in three steps. First, we reformulate robustness in terms of acyclicity of a happens-before relation. Second, we prove that among computations with cyclic happens-before relation there is always one in a certain normal form. Finally, we reduce checking the existence of such a normal form computation to a language emptiness problem. Altogether, this reduction shows a PSPACE algorithm for checking robustness. The problem is actually PSPACE-hard by a reduction of SC state reachability to robustness.
Memory Model-aware Testing -- a Unified Complexity Analysis
Florian Furbach (TU Kaiserslautern) en
To improve performance, multiprocessor systems implement weak memory consistency models -- and a number of models have been developed over the past years. Weak memory models, however, lead to unforeseen program behavior, and indeed there is a current need for memory model-aware program analysis techniques. The problem is that every memory model calls for new verification algorithms.

We study a prominent approach to program analysis: testing. The testing problem takes as input sequences of operations, one for each process in the concurrent program. The task is to check whether these sequences can be interleaved to an execution of the entire program that respects the constraints of the memory model. We determine the complexity of the testing problem for most of the known memory models. Moreover, we study the impact on the complexity of parameters like the number of concurrent processes, the length of their executions, and the number of shared variables.

What differentiates our approach from related results is a unified analysis. Instead of considering one memory model after the other, we build upon work of Steinke and Nutt. They showed that the existing memory models form a natural hierarchy where one model is called weaker than another one if it includes the latter's behavior.

Using the Steinke-Nutt hierarchy, we develop three general concepts that allow us to quickly determine the complexity of a testing problem. (i) We generalize the technique of problem reductions from complexity theory. So-called range reductions allow us to propagate hardness results between memory models, and we apply them to establish NP-lower bounds for the stronger memory models. (ii) For the weaker models, we present polynomial-time testing algorithms. Here, the common idea is determinization. (iii) Finally, we give a single SAT encoding of the testing problem that works for all memory models in the Steinke-Nutt hierarchy and shows membership in NP. Our results are general enough to classify future weak memory models and ensure that SAT solvers are adequate tools for their analysis.
Failure Semantics for Modal Transition Systems
Ferenc Bujtor (Uni Augsburg) en/de
With the aim to preserve deadlock freedom, we define a new refinement relation for modal transition systems (MTS), using an MTS-specific variant of testing in the sense of De Nicola and Hennessy. We characterise this refinement with a kind of failure semantics, and we show that it ‘supports itself’ e.g. in the sense of thoroughness – in contrast to the standard modal refinement. We present a conjunction operator w.r.t. our new refinement; this operator is very different from others found in the literature, and it demonstrates that the conjunction of two MTSs is an MTS – again in contrast to the case of modal refinement. Finally, we also consider a may-testing approach.
A Framework for the Analysis of Well-structured
Graph Transformation Systems
Jan Stückrath (Uni Duisburg-Essen) en/de
Well-structured transition systems are one of the main sources for decidability results for infinite-state systems. Well-structured transition systems equip a state space with a partial order, which must be a well-quasi-order and a simulation relation for the transition relation. The graph minor ordering, a well-quasi-order on the set of all graphs, forms such well-structured transition systems with lossy graph transformation systems, i.e. graph transformation systems containing edge contraction rules. For well-structured transition systems the coverability problem is decidable, i.e. the problem of deciding whether from the initial state, a state can be reached which is larger than some final state. With this one can model an error of a system by a set of error graphs and check whether a graph can be reached which contains one of these errors.

I will present a general framework for solving this problem which can handle arbitrary orders and also state sufficient conditions for correctness and termination. For this we generalized well-structured transition systems and allowed the order to be a well-quasi-order on a restricted set of graphs and not necessarily on all graphs. Of special interest is the subgraph ordering, which is a well-quasi-order only on a restricted set of graphs where path lengths are bounded, but is a simulation relation on a larger class of graph transformation systems than the minor ordering. Another alternative is the induced subgraph ordering, which is even more restricted on the set of graphs and less restricted on the class of transformation systems.
Computing Language Equivalence for Weighted
Automata Coalgebraically
Sebastian Küpper (Uni Duisburg-Essen) en/de
We want to discuss a coalgebraic algorithm to compute language equivalence for weighted automata. Coalgebras have proven to be a flexible concept that allows to define a variety of different systems and analyse them, e.g. for behavioural equivalence, yielding abstract algorithms that can be instantiated to different automaton models. Here, we investigate weighted automata, where each transition from a state x to a state y via label $a$ gets assigned a weight $s\in S$, where S is an arbitrary semiring.

In order to find language equivalence for weighted automata, we will use a variation of the well-studied final chain algorithm. By factorizing the intermediate steps of the final chain through split-monomorphisms we will be able to guarantee termination in finitely many steps for several interesting classes of semirings. This approach can be generalized to arbitrary coalgebraically defined automaton models, in order to keep the presentation simple, we will focus on the case of weighted automata, though. An interesting aspect of our new algorithm is that it slightly generalizes a decidability result on language equivalence for weighted automata by Droste and Kuske.
Lifting Adjunctions to Coalgebras to
(Re)Discover Automata Constructions
Henning Kerstan (Uni Duisburg-Essen) en/de
It is a well-known fact that a nondeterministic automaton can be transformed into an equivalent deterministic automaton via the powerset construction. From a categorical perspective this construction is the right adjoint to the inclusion functor from the category of deterministic automata to the category of nondeterministic automata. This is in fact an adjunction between two categories of coalgebras: deterministic automata are coalgebras over Set and nondeterministic automata are coalgebras over Rel. I will first explain, how this adjunction between coalgebras originates from a canonical adjunction between Set and Rel. Based on this example I'll show how, in a quite generic setting, an adjunction can be lifted to coalgebras. After giving some additional examples, I will finally present how to use the lifted adjunction to check behavioral equivalence.

In order to prepare the audience for the categorical concepts needed for this talk, I'll give a very brief introduction to categories, coalgebra and adjunctions prior to the actual talk.
Monitoring Modulo Theories
Daniel Thoma (Uni Lübeck) en/de
We consider a generic approach to runtime verification of temporal properties over first-order theories. This allows especially for the verification of multi-threaded, object-oriented systems. It presents a general framework lifting the monitor synthesis for propositional temporal logics to a temporal logic over structures within some first-order theory. To evaluate such temporal properties, SMT solving and classical monitoring of propositional temporal properties is combined. The monitoring procedure was implemented for linear temporal logic (LTL) based on the Z3 SMT solver and evaluated regarding runtime performance.
Learning Transparent Data Automata
Normann Decker (Uni Lübeck) en/de
We study the problem of learning data automata (DA), a recently introduced model for defining languages of data words. Data words are finite sequences of pairs of a letter from a finite alphabet and a data value from some infinite domain.

The model of DA is closely related to Petri nets, for which no active learning algorithms have been introduced so far. We define and study transparent data automata (tDA) as a strict subclass of DA for which language equivalence is decidable.

In the spirit of Angluin's L* algorithm we present an active learning procedure for tDA. Transparent data automata are incomparable to register automata and variants, for which learning algorithms were given recently.
Abstraction refinement based on unsatisfiability cores and SMT solving
Grigory Markin (Uni Lübeck) en/de
Counterexample-guided abstraction refinement (CEGAR) based on satisfiability modulo theories (SMT) is widely accepted for software model checking. For specific theories, in particular the theory of linear rational arithmetic (LRA), new predicates can efficiently be inferred by Craig interpolation. However, for bit-precise reasoning, models are usually formalized in the theory of bit vectors and arrays, for which Craig interpolants are inefficient or unavailable, respectively. We therefore propose an optimization of the refinement step for arbitrary SMT theories, relying on an extraction of an unsatisfiability core and a projection of the spurious counterexample trace.
Construction of the Lattices of Prime Event Structures
Evgeny Erofeev (Uni Oldenburg) en
The intention of this work is to study interconnections of basic relations in concurrency systems represented by the prime event structures. Starting from these relations restricted to the substructures and using the notion of "causally closed subset", one can construct algebraic lattices for these substructures. A characterization of K-density is given, related to the algebraicity of the obtained lattice.

  aktualisiert am 24.02.2014
TU_Icon_E_Mail_1_17x17_RGB Zum Seitenanfang