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.

Eingeladener Vortrag

Kim Larsen, Aalborg University, Denmark
From Priced Timed Automata to Energy Games

• Presentation slides (PDF)

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 resource-allocation and optimization
problems with applications in areas such as embedded systems.
The initial optimization problem considered was that of cost-optimal reachability,
shown to be decidable and PSPACE-complete . Later decidability
and PSPACE-completeness 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 resource-allocation problems was introduced, namely
that of constructing infinite schedules subject to boundary constraints on the
accumulation of resources, so-called 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 built-in 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 hyper-optimistic 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
Automata-Theoretic 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 fence-commands. 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 Cycle-Algorithm, 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 well-known 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 re-used 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 pi-calculus and CCS. I show that there exists no compositional encoding of the pi-calculus into CCS that respects reduction equivalence. In fact, there is no such encoding of the asynchronous pi-calculus without matching and restriction. However, I sketch a translation from the pi-calculus with guarded matching into the extension of CCS with an ACP-style communication format that is conjectured to be correct up to open bisimilarity.

Alexander Heußner
Otto-Friedrich-Universität Bamberg
Queue-Dispatch Asynchronous Systems
To make the development of efficient multi-core applications easier, libraries, such as Grand Central Dispatch (GCD), have been proposed. When using such a library, the programmer writes so-called 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 Queue-Dispatch 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 worst-case 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 input-parametrized fork-join behaviour with the help of abstractions, and conclude with a hands-on approach for verifying GCD programs in practice. This is joint work with Gilles Geeraerts and Jean-François Raskin from ULB.

Reiner Hüchting
TU Kaiserslautern
Reachability Analysis for Name Bounded Pi-Calculus
Many typical dynamic networks rely on a bounded address space. Pi-calculus 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 pi-calculus 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 re-used 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 Duisburg-Essen
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 pi-Kalkül in den asynchronen pi-Kalkül ein. Mit der LTS-Semantik 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 up-bounded non-inertial (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 three-valued algebra is able to maintain correct and exact stabilization information under the UN-delay 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 up-bounded inertial (UI) delay to justify ternary simulation. It can be shown that the match is not exact and that stabilization under the UI-model, 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 real-time 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 non-trivial 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 mu-calculus 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 Duisburg-Essen
Solving Coverability for Well-structured 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 control-point reachablitiy for two processes is decidable in polynomial time. We complement these results and show that in presence of contextual locking, control-point reachablitiy becomes PSPACE-hard, 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 control-point 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 non-regular languages? For which monoids can we determinize automata? For which monoids can we avoid silent edges (i.e., those which read no input symbol)?