You are here
Home ›Programm
Zeitplan (vorläufig)
Es wird am Donnerstag und Freitag zwei parallele Tracks geben. Die Sitzungen sind mit 45 Minuten kürzer angesetzt als im letzten Jahr.
06.03.2013 

ab 19.00 Uhr  Abendessen Hieronymus  
07.03.2013 

ab 08.30 Uhr  Empfang  3.015  
09.00  09.15  Eröffnung  3.015  
09.15  10.00  How appropriate is optimism for interface automata? Ferenc Péter Buijtor (Uni Augsburg) 
3.015  Formation of Dynamic Coalitions Youssef Arbach (TU Berlin) 
3.014 
10.00  10.30  Pause  
10.30  11.15  AutomataTheoretic Control for Total Store Ordering Architectures Florian Furbach (TU Kaiserslautern) 
3.015  Reachability Analysis for Name Bounded PiCalculus Reiner Hüchting (TU Kaiserslautern) 
3.014 
11.15  12.00  Valence automata as a generalization of automata with storage Georg Zetzsche (TU Kaiserslautern) 
3.015  Relative Ausdrucksmächtigkeit von Prozesskalkülen Christopher Lippert (TU Braunschweig) 
3.014 
12.00  14.00  Mittag  
14.00  15.00  From Priced Timed Automata to Energy Games Kim Larsen (Uni Aalborg) 
3.015  
15.00  15.30  Pause  
15.30  16.15  Partial Model Checking in mCRL2 Kevin van der Pol (RWTH Aachen) 
3.015  Solving Coverability for Wellstructured GTS with Various Orders Jan Stückrath (Uni Duisburg) 
3.014 
16.15  17.00  Software Verification: between Intuition and Proofs Holger Gast (Uni Tübingen) 
3.015  QueueDispatch Asynchronous Systems Alexander Heußner (Uni Bamberg) 

ab 19.30 Uhr  Abendessen Sachers  
08.03.2013 

09.00  10.00  On the expressivity of process calculi Rob van Glabbeek (NICTA Sydney) 
3.015  
10.00  10.30  Pause  
10.30  11.15  Contextual Locking for Dynamic Pushdown Networks Alexander Wenner (Uni Münster) 
3.015  Concatenation of Recognizable Languages Sebastian Küpper (Uni Duisburg) 
3.014 
11.15  12.00  Constructive Boolean Circuits and the Exactness of Timed Ternary Simulation Michael Mendler (Uni Bamberg) 
3.015  Strong Distributability Criteria for Petri Nets  A Matter of Free Choice Stephan Mennicke (TU Braunschweig) 
3.014 
12.00  14.00  Mittagessen  
14.00  15.00  Business Meeting  
15.00 Uhr  Ende der Veranstaltung (Kaffee und Plätzchen) 
Eingeladener Vortrag
Kim Larsen, Aalborg University, Denmark
From Priced Timed Automata to Energy Games
This talk will offer a comprehensive review of priced timed automata and
energy games high lightening results obtained and problems that remain open.
Priced (or weighted) timed automata was introduced in 2001, and
have emerged as a useful formalism for formulating a wide range of resourceallocation and optimization
problems with applications in areas such as embedded systems.
The initial optimization problem considered was that of costoptimal reachability,
shown to be decidable and PSPACEcomplete . Later decidability
and PSPACEcompleteness of the problem of optimal infinite runs, in terms of
minimal (maximal) cost per time ratio or accumulated discounted cost has been
established.
In 2008 a new class of resourceallocation problems was introduced, namely
that of constructing infinite schedules subject to boundary constraints on the
accumulation of resources, socalled energy games. We review what is know
about decidability and complexity in terms of number of clocks and number of
cost variables for this problem.
We also show how the use of statistical model checking may be used
to efficiently obtain near optimal solutions.
Teilnehmervorträge
Youssef Arbach
TU Berlin
Formation of Dynamic Coalitions
Cooperation of entities in daily life is essential; one kind of cooperation is the formation of Dynamic Coalitions (DCs). For example, in the medical sector, the cooperation of doctors to treat a patient is a typical DC. There are many problems to be investigated in DCs, e.g. Information Sharing, Privacy, Membership etc. We study and formalize the phenomenon of DC formation, as it captures the key feature of DCs: their dynamics. Abstractly, the problem can be seen as a process consisting of events with concurrency, causality and conflicts. Therefore, we apply Event Structures (ES) to model DC formation. However, the medical sector exhibits further requirements and criteria, e.g. urgency and priority, which call for respective enhancements to ES. Furthermore, we are investigating action refinement, to define a higher abstraction to describe DC formation and behavior as a combination of multiple subprocesses.
Ferenc Péter Bujtor
Universität Augsburg
How appropriate is optimism for interface automata?
De Alfaro and Henzinger developed interface automata to model and study behavioural types, which describe communication patterns of systems while abstracting from data. They stipulate a parallel composition with a builtin removal of errors due to unexpected inputs, and alternating bisimulation as refinement relation.
We considered the usual parallel composition and retain errors. Our basic criterion for refinement was “if the specification is error free, the implementation should be as well”. Our first notion of error freeness – an error must not be reached by internal and output actions alone – fits to the optimistic understanding of errors in interface automata. We characterized the coarsest precongruence, which proved correct the parallel composition of De Alfaro and Henzinger, but also showed that their refinement is unnecessarily strict.
In this talk we expand on our fundamental studies by considering two other notions of error freeness: the hyperoptimistic internal approach, where an error is problematic only if it is reached by internal actions alone, and a pessimistic approach also found in literature, where any reachable error is problematic. For each we describe a precongruence, which turns out to be considerably more complicated than the optimistic one.
Surprisingly both these precongruences are strictly finer than the optimistic one and their underlying semantics use a similar treatment of errors.
Florian Furbach
TU Kaiserslautern
AutomataTheoretic Control for Total Store Ordering Architectures
We consider a system architecture that consists of a number of parallel running program components where each sends a sequence of read and write actions to a shared memory. Memory access is very slow compared to operations of the processor and thus, in modern processor architectures, the system does not always suspend the computation during a memory access. However, when designing a program, we work under the assumption of sequential consistency. That means that the actions executed by a program component arrive at the memory in the same order they have been fired. A relaxed memory model may introduce unwanted behaviour by allowing computations that can not be executed in a sequentially consistent system. In particular data race freeness is no longer guaranteed. In order to ensure sequential consistency of a program, it is statically analyzed and additional delays are added in the form of so called fence actions. We concentrate exclusively on the total store ordering architecture (TSO) where every component is equipped with a buffer for write actions while read actions are performed immediately on its buffercontent and the global memory. This work deals with the possiblity to guarantee consistent computations in a TSO system with a controller for the write buffer rather than by creating consistent programs using fencecommands. We explore whether a finite automaton can be used as a controller and its complexity. We further examine a distributed architecture, where multiple elements of a controller communicate using broadcasts and the number of messages needs to be minimized. We introduce the CycleAlgorithm, a distributed algorithm that minimizes the number of communications between its components. A modified version, that can be represented by a deterministic finite automaton with a minimal number of states, will be presented as well.
Holger Gast
Universität Tübingen
Software Verification between Intuition and Proofs
It is wellknown that functional software verification, despite all advances in automated theorem proving, still requires a deep understanding of the program's intentions and behaviour: first, to formulate the specification and the invariants precisely, then to steer the prover towards a proof.
The talk discusses possible interactions between the intuitive understanding and the correctness proofs of programs. The first part considers symbolic execution as an overall framework, both in separation logic and in classical logic. The second part gives examples of background theories that capture the operational understanding of a program, e.g. in list manipuplation and gargabe collection, in such a way that they can be reused between different proofs.
Rob van Glabbeek
NICTA, Sydney, Australien
On the expressivity of process calculi
In this talk I will propose definitions of what it means for one process calculus to encode another one. This enables an ordering of process calculi with respect to expressive power. I compare the proposed definition with other definitions of encoding and expressiveness found in the literature, and apply it on a case study: comparing the expressive power of the picalculus and CCS. I show that there exists no compositional encoding of the picalculus into CCS that respects reduction equivalence. In fact, there is no such encoding of the asynchronous picalculus without matching and restriction. However, I sketch a translation from the picalculus with guarded matching into the extension of CCS with an ACPstyle communication format that is conjectured to be correct up to open bisimilarity.
Alexander Heußner
OttoFriedrichUniversität Bamberg
QueueDispatch Asynchronous Systems
To make the development of efficient multicore applications easier, libraries, such as Grand Central Dispatch (GCD), have been proposed. When using such a library, the programmer writes socalled blocks, which are chunks of codes, and dispatches them, using synchronous or asynchronous calls, to several types of waiting queues. A scheduler is then responsible for dispatching those blocks on the available cores. Blocks can synchronize via a global memory. In this paper, we propose QueueDispatch Asynchronous Systems as a mathematical model based on graph rewriting that faithfully formalizes the synchronization mechanisms and the behavior of the scheduler in those systems. We study in detail their relationships to classical formalisms such as pushdown systems, Petri nets, fifo systems, and counter systems. Our main technical contributions are precise worstcase complexity results for the Parikh coverability problem and the termination question for several subclasses of our model. We give an outlook on extending our model towards verifying inputparametrized forkjoin behaviour with the help of abstractions, and conclude with a handson approach for verifying GCD programs in practice. This is joint work with Gilles Geeraerts and JeanFrançois Raskin from ULB.
Reiner Hüchting
TU Kaiserslautern
Reachability Analysis for Name Bounded PiCalculus
Many typical dynamic networks rely on a bounded address space. Picalculus models of such networks inherit this constraint. They are name bounded, i.e. there is a bound on the number of restricted names that holds for all reachable processes. We show that reachability is decidable for name bounded picalculus processes. To this end, we give a reduction to Petri net reachability. A name bounded process must either instantiate only finitely many new names or it must forget names before instantiating new ones. The key idea to constructing the Petri net is to use a fixed set of names and recycle them when necessary. The difficult part of this construction is to identify names that are no longer in use and thus can be recycled. To this end, reference counters with zero tests have to be implemented in the Petri net. We show that any name that may be reused infinitely often is only visible to a bounded number of process terms at any time. We compute this bound using an extension of the Karp & Miller construction for Petri nets. Thus, we are able to implement the reference counters. As a second result, our Karp & Miller construction yields a compact representation of the coverability set of a name bounded process.
Sebastian Küpper
Universität DuisburgEssen
Concatenation of Recognizable Languages
Christopher Lippert
TU Braunschweig
Relative Ausdrucksmächtigkeit von Prozesskalkülen
Um die relative Ausdrucksmächtigkeit von Prozesssprachen zu untersuchen, werden Übersetzungen zwischen den Sprachen angegeben, die gewisse Kriterien erfüllen müssen. Ein bekannter Kriteriensatz (Kompositionalität, Namensinvarianz, operationelle Korrespondenz, Divergenzreflektion, Success Sensitiveness) stammt von Gorla. Rob van Glabbeek hat im Jahr 2012 alternative Definitionen der Korrektheit und Validität einer Übersetzung angegeben. Wir stellen beide Ansätze vor. Anschließend wählen wir Übersetzungen, die valide nach Gorla sind, und untersuchen sie nach den Kriterien von van Glabbeek. Dabei gehen wir insbesondere auf Boudols Übersetzung vom synchronen piKalkül in den asynchronen piKalkül ein. Mit der LTSSemantik von Milner, Parrow und Walker zeigen wir, dass diese Übersetzung nicht korrekt bis auf schwache Bisimulation, aber valide bis auf schwache Bisimulation ist.
Michael Mendler
Universität Bamberg
Constructive Boolean Circuits and the Exactness of Timed Ternary Simulation
Cyclic boolean systems, such as those arising in the semantics of synchronous programming languages, do not admit a unique canonical execution semantics. Instead, different approaches impose different restrictions on their stabilization behavior. In the talk I will introduce the notion of constructive circuits, for which signals settle to a unique value in bounded time, for any input, under a simple conservative delay model, called the upbounded noninertial (UN) delay. The main result is that ternary simulation, such as the practical algorithm proposed by Malik, decides the class of constructive circuits. We prove that threevalued algebra is able to maintain correct and exact stabilization information under the UNdelay model, and thus provides an adequate electrical interpretation of Malik's algorithm, which has been missing in the literature. Previous work on combinational circuits used the upbounded inertial (UI) delay to justify ternary simulation. It can be shown that the match is not exact and that stabilization under the UImodel, in general, cannot be decided by ternary simulation. This provides, for the first time, a correctness and exactness result for the timing analysis of cyclic circuits. The algorithm is a timed extension of Malik's pure ternary algorithm and closely related to the timed algorithm proposed by Riedel and Bruck, which however was not formally linked with realtime execution models.
Stephan Mennicke
TU Braunschweig
Strong Distributability Criteria for Petri Nets  A Matter of Free Choice
Petri nets provide a precise mathematical foundation for concurrently interacting systems. A special kind of these are distributed systems consisting of computing components and communication channels. In our work, we consider a hierarchy of distributions based on interaction principles of distributed systems. We are particularly interested in notions for distributability based on Petri nets. Inspired by existing notions, we look for stronger (i.e., more discriminating) distributability criteria for Petri nets. Thus, we gain the advantage of possibly easier to (distributedly) implement Petri net classes. An interesting notion so far is free choice distributability. Here, a purely structural definition of distributed net systems appears to be nontrivial w.r.t. its closure in terms of distributability. Finally, we give a perspective which phenomena have influence on the distributability of Petri nets.
Kevin van der Pol
RWTH Aachen
Partial Model Checking in mCRL2
The partial model checking technique, first described by H. R. Andersen [1], aims to use the compositional nature of models to speed up model checking. It considers parts of the model, one by one, and incorporates their behavior in the property, which we still have to check on the remainder. We obtain a new model checking problem with the same solution as the original problem, where part of the model's behavior has been moved to the property. If we can successfully reduce that property's complexity, we have made the original model checking problem smaller. We defined this procedure for properties expressed in mucalculus and models in mCRL2, using Linear Process Equations as atomic processes, and the parallel composition, communication, renaming and abstraction operators. We explore this partial model checking procedure by examples. [1] H. R. Andersen, Partial model checking (extended abstract), In Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1995
Jan Stückrath
Universität DuisburgEssen
Solving Coverability for Wellstructured GTS with Various Orders
Alexander Wenner
Universität Münster
Contextual Locking for Dynamic Pushdown Networks
Contextual locking is a scheme for synchronizing between possibly recursive processes, which allows for arbitrary usage of locks within the same procedure call. It has been introduced by Chadha et al. at TACAS 2012 where it was shown that controlpoint reachablitiy for two processes is decidable in polynomial time. We complement these results and show that in presence of contextual locking, controlpoint reachablitiy becomes PSPACEhard, already if the number of processes is increased to three. On the other hand, we show that PSPACE is both necessary and sufficient for deciding controlpoint reachablitiy of k processes for k > 2, and that this upper bound remains valid even if dynamic spawning of new processes is allowed. Furthermore, we consider the problem of regular reachability, i.e., whether a configuration within a given regular set can be reached. Here, we show that this problem is decidable for recursive processes with dynamic thread creation and contextual locking. Finally, we generalize this result to processes that additionally use a form of join operations.
Georg Zetzsche
TU Kaiserslautern
Valence automata as a generalization of automata with storage
A valence automaton over a monoid $M$ is a finite automaton in which each edge carries an input word and an element of $M$. A word is then accepted if there is a run that spells the word such that the product of the monoid elements is the identity. By choosing appropriate monoids $M$, one can obtain various kinds of automata with storage as special valence automata. Examples include pushdown automata, blind multicounter automata, and partially blind multicounter automata. Therefore, valence automata offer a framework to generalize results on such automata with storage. This talk will present recent results on valence automata. The addressed questions include: For which monoids can we accept nonregular languages? For which monoids can we determinize automata? For which monoids can we avoid silent edges (i.e., those which read no input symbol)?
 News
 Research
 Teaching
 Staff
 Martin Leucker
 Martin Blankenburg
 Gerhard Buntrock
 Lukas Convent
 Normann Decker
 BengtOve Holländer
 Sebastian Hungerecker
 Karam Kharraz
 Nikolas Knickrehm
 Christian Kreutzfeldt
 Felix Lange
 Grigory Markin
 Maria Ostanina
 André Pedro
 Torben Scheffel
 Malte Schmitz
 Nina Strugalla
 Annette Stümpel
 Daniel Thoma
 Dietmar Wolf
 Open Positions
 Contact