The Distributed and Embeeded Systems unit is running regular seminars where both local speakers as well as external visitors give talks on a wide range of topics from the concurrency theory and practice. The seminars are not only aimed at the local audience but also to any interested visitors from outside of the unit or the department.

List of Seminars

Ingo van Duijn, Dept. of Computer Science, Aalborg University, Denmark.
Wednesday 13.12.2017 at 13:30 in 0.2.90.

The List Update Problem Revisited: Featuring Pairwise Access

Abstract: In the classical List Update Problem, a linear list of n elements is maintained.The list is used to serve requests, where a request asks for a single element in the list. Upon a request, a cursor scans the list starting at the front, until it finds the requested element and the request is served. To make things interesting, the algorithm is now allowed to rearrange elements to facilitate faster scanning times for future requests.
This talk will serve as a brief refreshment on online algorithms and competitive analysis, and includes work in progress and open questions in the area. Serving as an example will be the aptly named algorithm "Move-To-Front" (MTF) solving the List Update Problem. MTF moves the requested element to the front of the list, and since it makes this decision without knowledge of future requests, it is an online algorithm. I will show how under a restrictive cost model, this algorithm operates within a constant factor of the optimal offline algorithm.
However, with a slightly more relaxed cost model, MTF -- and any other online algorithm -- can a factor n/logn more costly than optimal. Our own research introduced the notion of "pairwise access" in the list update problem. A request now consists of two elements (u,v); the cursor starts scanning at u and needs to reach v to serve the request. Not much is known about this problem, and in the rest of the talk I will discuss the known hurdles and our preliminary results on the Pairwise List Update Problem.


Martin Tappler, Institute of Software Technology, Graz University of Technology, Austria.
Wednesday 29.11.2017 at 14:00 in 0.2.90.

Test-Based Model Learning

Abstract: Test-Based model learning derives formal models of black-box systems from test observations. It thereby enables model-based analysis for systems with unknown structure. Recent works successfully applied model learning for instance in combination with model checking to find faults in implementations of well-known protocols such as TCP. In my talk, I will discuss two applications of model learning: (1) reachability checking for stochastic systems and (2) automatic creation of timed automata. For the former, we iteratively refine testing strategies with the help of learned models. Experiments showed that these strategies reach the specified 
goals with high probability. To automatically create timed automata, we developed a genetic programming framework. We basically search for timed automata that are consistent with test observations. Initial experiments showed promising results.


Marco Chiesa, ICTEAM, Université Catholique de Louvain, Belgium.
Monday 13.11.2017 at 14:00 in 0.2.90.

Bootstrapping Internet Routing Innovation

Abstract: The Internet plays a crucial role in interconnecting billions of devices, users, and applications. To serve its purpose, the Internet infrastructure should accommodate the ever-more-demanding performance requirements of new applications (streaming video, VoIP, algotrading, and beyond). Yet, despite extensive efforts by both researchers and practitioners, the Internet infrastructure has remained fairly stagnant for decades and, consequently, suffers from both bad performance and alarming security vulnerabilities.
I will discuss two promising approaches for bootstrapping innovation in the Internet: (1) exploiting network programmability at Internet eXchange Points (IXPs), the crossroads of Internet traffic, to provide new network functionalities, and (2) enhancing the expressiveness of today's legacy networks without modifying the network infrastructure. I will then present COYOTE, an SDN-inspired legacy-compatible approach to optimize network flows, and SIXPACK, a theory-informed approach for route-computation at IXPs that both provides richer expressiveness in route selection and is provably privacy-preserving.


Frederik Meyer Bønneland, Dept. of Computer Science - Aalborg University, Aalborg, Denmark.
Monday 30.10.2017 at 14:30 in 0.2.11.

Stubborn Versus Structural Reductions for Petri Nets

Abstract: We present a comparison of stubborn and structural reductions for petri nets and investigate the effect of combining the techniques. We present an interpretation of stubborn sets, described using labelled transitions systems, and applied to petri nets with inhibitor arcs. We extend reachability preserving stubborns sets to include preservation of fireability, cardinality, and deadlock properties, and base it on generating an interesting set of transitions for a given formula. We implement and benchmark stubborn sets and the combination with structural reduction in TAPAAL. Our experiments show that the combination of structural reduction and stubborn reduction generally yields considerable performance improvements, but that the combination conflicts on some models.


Isabella Kaufmann, Dept. of Computer Science - Aalborg University, Aalborg, Denmark.
Monday 30.10.2017 at 14:00 in 0.2.11.

Symbolic Synthesis for Non-Negative Multi-Weighted Games

Abstract: We provide a framework to describe non-negative multi-weighted Kripke structures and non-negative multi-weighted games. We investigate how to synthesize strategies for controller components with discrete weights using the framework. We show that model checking multi-weighted CTL over multi-weighted Kripke structures is undecidable with 3 weights and provide a decidable sub-logic, that can still express branching time properties. We also provide an algorithm utilizing a symbolic weight representation to synthesize finite memory strategies for multi-weighted games with reachability objectives and show that the problem is EXPTIME-complete


Peyman Afshani, Dept. of Computer Science - Center for Massive Data Algoritmics, Aarhus, Denmark.
Thursday 19.10.2017 at 14:00 in 0.2.90.

Independent Range Sampling, Revisited

Abstract: In the independent range sampling (IRS) problem, given an input set P of n points in R^d, the task is to build a data structure, such that given a range "R" and an integer "t >= 1", it returns t points that are uniformly and independently drawn from inside "R". The samples must satisfy inter-query independence, that is, the samples returned by every query must be independent of the samples returned by all the previous queries. This problem was first tackled by Hu, Qiao and Tao in 2014, who proposed optimal structures for one-dimensional dynamic IRS problem in internal memory and one-dimensional static IRS problem in external memory.
In this talk, we will first look at the classical results in range searching and discuss that they cannot always solve independent range sampling queries in a satisfactory manner. Then we will look at two natural extensions of the independent range sampling problem. In the first extension, we consider the static IRS problem in two and three dimensions. We obtain data structures with optimal space-query tradeoffs for 3D halfspace, 3D dominance, and 2D three-sided queries. The second extension considers weighted IRS problem. Each point is associated with a real-valued weight, and given a query range "R", a sample is drawn independently such that each point in "R" is selected with probability proportional to its weight. We will conclude with a list of open problems (joint work with Zhewei Wei).


Bruna Soares Peres, Dept. of Computer Science, Universidade Federal de Minas Gerais (UFMG), Belo Horizonte, Brazil.
Thursday 14.09.2017 at 14:00 in 0.2.90.

Distributed Self-Adjusting Networks

Abstract: Traditional communication networks are designed to optimize static performance metrics (such as diameter, degree, or bisection bandwidth), and as such, are oblivious to the actual workload they serve. We investigate an alternative model: communication networks which adapt, at runtime, to the communication patterns. We present and evaluate DiSplayNet, the first distributed self-adjusting network. DiSplayNets support fully decentralized and concurrent adjustments to the demand as well as local routing.


Matthias Rost, Dept. of Telecommunication Systems - Technische Universität Berlin, Germany.
Friday 18.08.2017 at 14:00 in CISS/DEIS Sofa room.

Beyond the Stars: Revisiting Virtual Cluster Embeddings

Abstract: It is well-known that cloud application performance can critically depend on the network. Over the last years, several systems have been developed which provide the application with the illusion of a virtual cluster: a star-shaped virtual network topology connecting virtual machines to a logical switch with absolute bandwidth guarantees.
In this work, we debunk some of the myths around the virtual cluster embedding problem. First, we show that the virtual cluster embedding problem is not NP-hard, and present the polynomial-time embedding algorithm VC-ACE yielding optimal solutions for arbitrary datacenter topologies.
Second, we argue that resources may be wasted by enforcing star-topology embeddings, and alternatively promote a hose embedding approach. We discuss the computational complexity of hose embeddings and derive the HVC-ACE algorithm. Using simulations we substantiate the benefits of hose embeddings in terms of acceptance ratio and resource footprint.


Arsany Basta, Technische Universität München, Germany.
Tuesday 13.06.2017 at 14:00 in 0.2.13.

Towards the Next Generation Software Defined Virtual Mobile Core Network

Abstract: With the rapid growth of user traffic, service innovation, and the persistent necessity to reduce costs, today’s mobile operators are faced with several challenges. Recent networking concepts offer an opportunity to address these challenges, namely Network Functions Virtualization (NFV), Network Virtualization (NV) and Software Defined Networking (SDN). NFV leverages the concepts of IT virtualization to network functions, where functions can be implemented in software and deployed on commodity hardware. NV enables the operation of multiple logical virtual networks, i.e., slices, on the same physical infrastructure. SDN, on the other hand, decouples the data and control planes of network functions and introduces an open interface between the decoupled planes.
In this talk, we will explore the application of these concepts towards the next generation software defined virtual mobile core network. The talk covers the following questions; how to design and model an optimal core network based on SDN and NFV?  How to exploit the co-existence of both concepts in order to improve the network operation? How to provide reliable isolated virtual slices among multiple tenants? How to support the network dynamic changes required by the virtual slices?


K. Subramani, Lane Dept. of Computer Science and Electrical Engineering, West Virginia University, USA.
Tuesday 16.05.2017 and Friday 19.05.2017 at 14:00 in 0.2.90.

1- Optimal-length resolution refutation for difference constraints 
2- Small certificates for tree-like proofs in UTVPI constraint systems

Abstract: In these talks, I will discuss the computational complexities of identifying small certificates of infeasibility in two classes of constraints, viz., Difference constraints and UTVPI constraints. Both these classes arise in abstract interpretation (program verification). An important feature of certificates is their type. Three important types of certificates are read-once, tree-like and dag-like In the case of difference constraints, all three type of certificates coincide; in the case of the latter, they are distinct. I will discuss two deterministic algorithms and a randomized algorithm for read-once refutations in difference constraints.
I will also discuss a deterministic algorithm and a randomized algorithm for tree-like certificates in the case of UTVPI constraints.


Nathanaël Fijalkow, Alan Turing Institute of Data Science in London (affiliated with University of Warwick), UK.
Wednesday 10.05.2017 at 14:00 in 0.2.90.

Trace Equivalence for Markov Decision Processes

Abstract: In this talk, I will look at the notion of trace equivalence in the context of Markov Decision Processes. I will show algorithmic and logical properties.


Ingo van Duijn, Department of Computer Science, Aarhus University, Denmark.
Wednesday 19.04.2017 at 14:00 in 0.2.90.

Permuting lower bounds in the I/O model

Abstract: The I/O model is an elegant model to analyze problems where the size N of the input far exceeds the available memory. The model assumes a finite internal memory of size M and an infinite external storage disk. Data can be transferred between internal memory and disk in blocks of size B. The complexity of an algorithm is determined by the number of I/O's, whereas computation is free but can only be performed in internal memory.
Surprisingly, permuting is as hard as sorting in the I/O model, and therefore perhaps one of its most fundamental problems. In this talk I will discuss the folkloric counting lower bound showing that permuting and sorting takes O(N/B log_M/B N/B) I/Os. Further topics include the limitations of this lower bound, and the advantages of stronger lower bound techniques. As an example, I will show how we prove time lower bounds for batched geometric queries under certain assumptions on B.


Adrien Le Coënt, CMLA, ENS Paris-Saclay, France.
Wednesday 01.03.2017 at 14:30 in 0.2.11.

Distributed Control Synthesis for (Nonlinear) Switched Systems

Abstract: We present an algorithm of control synthesis for nonlinear switched systems, based on an existing procedure of state-space bisection and made available for nonlinear systems with the help of validated simulation. The use of validated simulation also permits to take bounded perturbations and varying parameters into account. Given an objective region R of the state space, the method builds a capture set S and a control which steers any element of S into R. The method works by iterated backward reachability from R. More precisely, S is given as a parametric extension of R, and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within R all the states starting in R. We explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and 2^11 = 2048 switching modes. The whole approach is entirely guaranteed and the induced controllers are correct-by-design. 


Thomas Hildebrandt, IT University of Copenhagen (ITU), Denmark.
Monday 28.11.2016 at 11:00 in 0.2.90.

In the Nick of Time: Proactive Prevention of Obligation Violations

Abstract: We present a system model, an enforcement mechanism, and a policy language for the proactive enforcement of timed provisions and obligations. Our approach improves upon existing formalisms in two ways: (1) we exploit the target system’s existing functionality to avert policy violations proactively, rather than compensate for them reactively; and, (2) instead of requiring the manual specification of remedial actions in the policy, we automatically deduce required actions directly from the policy. As a policy language, we employ timed dynamic condition response (DCR) processes. DCR primitives declaratively express timed provisions and obligations as causal relationships between events, and DCR states explicitly represent pending obligations. As key technical results, we show that enforceability of DCR policies is decidable, we give a sufficient polynomial time verifiable condition for a policy to be enforceable, and we give an algorithm for determining from a DCR state a sequence of actions that discharge impending obligations.


Torsten Liebke, Institut für Informatik, Universität Rostock, Germany.
Wednesday 23.11.2016 at 15:00 in 0.2.90

LoLA 2.0 - State space tool for place transition nets

Abstract: LoLA is a tool that can check whether a system (given as Petri net) satisfies a specified property. The property is evaluated by exhaustive and explicit exploration of a reduced state space. LoLA uses a broad range of state-of-the-art reduction techniques most of which can be applied jointly. Hence, LoLA typically needs to explore only a tiny fraction of the actual state space. The particularly strength of LoLA is the evaluation of simple properties such as deadlock freedom or reachability. Here, additional reduction techniques and specialized variants of techniques are applied. The talk will also include a demonstration of the tool.


Søren Enevoldsen, Aalborg University, DEIS, Denmark.
Thursday 03.11.2016 at 14:00 in 0.2.90.

Distributed Computation of Fixed Points on Dependency Graphs

Abstract: Dependency graph is an abstract mathematical structure for representing complex causal dependencies among its vertices. Several equivalence and model checking questions, boolean equation systems and other problems can be reduced to fixed-point computations on dependency graphs. We develop a novel distributed algorithm for computing such fixed points, prove its correctness and provide an efficient, open-source implementation of the algorithm.  The algorithm works in an on-the-fly manner, eliminating the need to generate a priori the entire dependency graph. We evaluate the applicability of our approach by a number of experiments  that verify weak simulation/bisimulation equivalences between CCS processes and we compare the performance with the well-known CWB tool. Even though the fixed-point computation, being a P-complete problem, is difficult to parallelize in theory, we achieve significant speed-ups in the performance as demonstrated  on a Linux cluster with several hundreds of cores.


Ehsan Khamespanah, University of Tehran, School of ECE, Iran.
Tuesday 25.10.2016 at 13:00 in 0.2.90.

On Time Actors

Abstract: Actor model is a concurrent object-based computational model in which actors are the units of concurrency and communicate via asynchronous message passing. Timed Rebeca is an actor-based modeling language which is designed for modeling and analyzing of event-based and asynchronous systems with time constraints. Timed Rebeca is equipped with analysis techniques based on the standard semantics of timed systems, and also an innovative event-based semantics that is tailored for timed actor models. The developed techniques are applied on different applications using Afra toolset, the integrated development environment of Timed Rebeca. This talk is a survey on the published work on Timed Rebeca, its semantics, supporting tools, and applications.


John McCabe-Dansted, School of Computer Science and Software Engineering, University of Western Australia.
Thursday 20.10.2016 at 14:00 in 0.2.90.

Modelling Systems over General Linear Time

Abstract: It has been shown that every temporal logic formula satisfiable over general linear time has a model than can be expressed as a finite Model Expression (ME). The reals are a subclass of general linear time, so similar techniques can be used for the reals. Although MEs are expressive enough for this task, they represent only a single class of elementary equivalent models. In the case where time is represented by integers, regular expressions are equivalent to automata. An ME is more similar to a single run of an automaton than the automaton itself. In linear time it is often useful to model a system as an automaton (or regular expression) rather than a single run of the automaton. In this paper we extend MEs with the operators from Regular Expressions to produce Regular Model Expressions (RegMEs). It is known that model checking temporal logic formulas over MEs is PSPACE-complete. We show that model checking temporal logic formulas over RegMEs is also PSPACE-complete. 
This is a joint work with Mark Reynolds and Tim French.


Giorgio Bacci, Department of Computer Science, Aalborg University, Denmark.
Wednesday 07.09.2016 at 14:00 in 0.2.90.

Complete Axiomatization for the Bisimilarity Distance on Markov Chains

Abstract: We propose a complete axiomatization of the bisimilarity distance of Desharnais et al. for the class of finite labelled Markov chains. Our axiomatization is given in the style of a quantitative extension of equational logic recently proposed by Mardare, Panangaden, and Plotkin (LICS'16) that uses equality relations t =_e s indexed by rationals, expressing that "t is approximately equal to s up to an error e". Notably, our quantitative deductive system extends in a natural way the equational system for probabilistic bisimilarity given by Stark and Smolka by introducing an axiom for dealing with the Kantorovich distance between probability distributions.


Alessandro Abate, Department of Computer Science, University of Oxford, UK.
Tuesday 28.06.2016 at 14:00 in 0.2.90.

Data-driven and Model-Based Quantitative Verification of Cyber-Physical Systems

Abstract: I discuss a new and formal, measurement-driven and model-based automated verification technique, to be applied on quantitative properties over systems with partly unknown dynamics. I focus on physical systems (with spatially continuous variables, possibly noisy), driven by external inputs and accessed under noisy measurements, and suggest that the approach can be as well generalized over CPS. I formulate this new setup as a data-driven Bayesian model inference problem, formally embedded within a quantitative, model-based verification procedure. 
While emphasizing the generality of the approach over a number of diverse model classes, this talk later zooms in on systems represented via stochastic hybrid models (SHS), which are probabilistic models with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear) - as such, SHS are quite a natural framework for CPS. With focus on model-based verification procedures, I provide the characterization of general temporal specifications based on Bellman’s dynamic programming. Further, the computation of such properties is attained via the development of formal abstraction techniques based on quantitative approximations, and concepts such as that of (approximate probabilistic) bisimulation. Theory is complemented by algorithms, all packaged in a software tool (FAUST2) that is freely available to users.


Manuela Bujorianu, Department of Computer Science, University of Leicester, UK.
Thursday 12.05.2016 at 14:00 in 0.2.90.

Hyper-Verification: Challenges from Cyber-Physical Systems

Abstract: Cyber-physical systems represent an evolving paradigm promoting a holistic view on engineered systems. The holistic view makes the formal verification look like a restrictive or specialised approach. In this way, a research challenge appears: How to leverage formal verification to cope with the holistic character of cyber-physical systems?
The holistic aspects include: emergent behaviours, complex faults (like hybrid discrete continuous), severe uncertainty, rich interactions, interdependence of critical components, potential disasters due to climate change.
In this talk, we introduce the concept of hyper-verification and sketch the fundamentals of a suitable formal framework to investigate it.


Matteo Mio, CNRS, École Normale Supérieure de Lyon, France.
Thursday 31.03.2016 at 14:00 in 0.2.90.

Regular Languages of Trees and Probability

Abstract: The decidability of the SAT(isfiability) problem for most branching-time temporal logics (such as CTL) follows from Rabin’s theorem about the decidability of the Monadic Second Order Theory of Two Successors (S2S). However, the decidability of the SAT problem for probabilistic logics (such as probabilistic CTL) is open. In an attempt to solve this problem it is natural to investigate probability-related variants and extensions of Rabin’s theorem. In this talk I will present some recent results on this line of research.


Peter Gjøl Jensen, Department of Computer Science, Aalborg University, Denmark.
Tuesday 29.03.2016 at 14:00 in 0.2.13.

Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization

Abstract: Automatic strategy synthesis for a given control objective can be used to generate correct-by-construction controllers of reactive systems. The existing symbolic approach for continuous timed games is a computationally hard task and current tools like UPPAAL TiGa often scale poorly with the model complexity. We suggest an explicit approach for strategy synthesis in the discrete-time setting and show that even for systems with closed guards, the existence of a safety discrete-time strategy does not imply the existence of a safety continuous-time strategy and vice versa. Nevertheless, we prove that the answers to the existence of discrete-time and continuous-time safety strategies coincide on a practically motivated subclass of urgent controllers that either react immediately after receiving an environmental input or wait with the decision until a next event is triggered by the environment. We then develop an on-the-fly synthesis algorithm for discrete timed-arc Petri net games. The algorithm is implemented in our tool TAPAAL and based on the experimental evidence, we discuss the advantages of our approach compared to the symbolic continuous-time techniques.


Stephane Le Roux, Department of Computer Science, Université Libre de Bruxelles, Belgium.
Tuesday 22.03.2016 at 14:00 in 0.2.90

Stable States of Perturbed Markov Chains

Abstract: Given an infinitesimal perturbation of a discrete-time finite Markov chain, we seek the states that are stable despite the perturbation, i.e. the states whose weights in the stationary distributions can be bounded away from 0 as the noise fades away. If the perturbation maps (and their multiplications) satisfy f = O(g) or g = O(f), we prove the existence of and compute the stable states in cubic time. Conversely, if the big-O assumption does not hold, we build a perturbation with these maps and no stable state. This is joint work with Volker Betz.


Doron Peled, Department of Computer Science, Bar Ilan University, Ramat Gan, Israel.
Wednesday 24.02.2016 at 14:00 in 0.2.90

Synthesis of Concurrent Programs Using Genetic Programming

Abstract: We present a method and system for automatically generating concurrent code using genetic programming, based on model checking. This is a directed search in the space of syntactically matching programs, which uses model checking to provide the fitness between the solution and the specification. 
The problem of synthesizing concurrent code is in general undecidable, hence our method cannot be completely automatic: the user needs the intervene by tuning parameters and supplying specification and hints that would steer the search for correct code in the right direction. We demonstrate how various hard-to-program protocols are generated using our method. We show how a commonly used protocol for coordinating concurrent interactions was found to be incorrect using our tool, and was then subsequently fixed.


Stefan Schmid, Department of Computer Science, Aalborg University, Denmark. 
Wednesday 9.12.2015 at 14:00 in 0.2.12.

The Art of Consistent Network Updates

Abstract: Software-defined networking is a promising new paradigm which currently receives a lot of attention both in industry and in academia. This paradigm also introduces several new theoretical challenges and practically relevant problems. In this talk, I will discuss some of these challenges and problems. In particular, I will present our recent results on consistent network update algorithms (taken from ACM HotNets 2014, ACM PODC 2015, IEEE INFOCOM 2015, etc.).


Robert Furber, Institute for Computing and Information Sciences, Radboud University, Nijmegen, Netherland.
Tuesday 17.11.2015 at 10:30 in 0.2.90.

Probability Monads and their Kleisli Categories

Abstract: For each many kinds of probability distribution there is an associated monad, which takes a space to the space of probability distributions on it. In the case of discrete probability distributions, we can represent Markov chains in the Kleisli category of the monad. We discuss two other monads, the Giry monad, G, which works with measurable spaces, and the Radon monad, R, which works with compact Hausdorff spaces. We present an alternative description of the Kleisli category of R from joint work with Bart Jacobs, and then compare it to a description of the Kleisli category of the Giry monad given by Dexter Kozen in 1983.


Søren Enevoldsen, Department of Computer Science, Aalborg University, Denmark. 
Wednesday 21.10.2015 at 14:15 in 0.2.90.

CAAL: Concurrency Workbench, Aalborg Edition

Abstract: We present the first official release of CAAL, a web-based tool for modelling and verification of concurrent processes. The tool is primarily designed for  educational purposes and it supports the classical process algebra CCS together with its timed extension TCCS. It allows to compare processes with respect to a range of strong/weak and timed/untimed equivalences and preorders (bisimulation, simulation and traces) and supports model checking of CCS/TCCS processes  against recursively defined formulae of Hennessy-Milner logic. The tool offers a graphical visualizer for displaying labelled transition systems, including their minimization up to strong/weak bisimulation, and process behaviour can be examined by playing (bi)simulation and model checking games or via the generation  of distinguishing formulae for non-equivalent processes. We describe the modelling and analysis features of CAAL, discuss the underlying verification algorithms  and show a typical example of a use in the classroom environment.


Martin Zimmermann, Reactive Systems Group, Saarland University, Germany.
Wednesday 26.8.2015 at 14:30 in 0.2.90.

How Much Lookahead is Needed to Win Infinite Games?

Abstract: Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent’s moves. For omega-regular winning conditions it is known that such games can be solved in doubly-exponential time and that doubly- exponential lookahead is sufficient. We improve upon both results by giving an exponential time algorithm and an exponential upper bound on the necessary lookahead. This is complemented by showing EXPTIME-hardness of the solution problem and tight exponential lower bounds on the lookahead. Both lower bounds already hold for safety conditions. Furthermore, solving delay games with reachability conditions is shown to be PSPACE-complete. For winning conditions expressed in weak monadic second order logic with the unbounding quantifier, which is able to express (un)boundedness properties, we show that it is decidable whether the delaying player is able to win such a game with bounded lookahead, i.e., if she only skips a finite number of moves. This is complemented by showing that any unbounded lookahead is sufficient. Finally, we present some general determinacy results for delay games with Borel winning conditions and discuss what a strategy in a delay game is, a surprisingly non-trivial question. Based (partially) on joint work with Felix Klein (Saarland University).


K. Subramani, LDCSEE, West Virginia University, USA.
Thursday 6.8.2015 at 14:30 in 0.2.90.

Fast algorithms for checking linear and integer feasibility in Horn polyhedra

Abstract: In this talk, I will discuss various issues concerning the linear and integer feasibility problems in Horn polyhedra. A Horn polyhedron is a linear system of the form: A x <= b, x >= 0, such that b is integral, each entry of A belongs to {-1,0,1} and at most one entry in each row of A is positive. It can be shown that Horn polyhedra generalize three classes of constraints, viz., difference constraint systems, satisfiable Unit Two Variable per Inequalty constraint systems and Horn clauses. These polyhedra arise in a number of application domains, including but not limited to Program verification (Abstract Interpretation), operations research and econometrics. A problem that is closely related to the feasibility problem in Horn polyhedra, is  the problem of optimizing a linear function over such polyhedra. While the feasibility problems are polynomial-time solvable, the optimization problem is NP-hard. On the algorithmic front, I will present two polynomial time algorithms for the feasibility problems. The first algorithm expolits the rewrite rule: x_i - x_j - x_k >= 3, x_i, x_j, x_k >= 0 --> x_i >= 3. The second algorithm expoits the rewrite rule: x_i- x_j - x_k >= 3, x_i, x_j, x_k >= 0 --> x_i - x_j >= 3, x_i - x_k >= 3, x_i, x_j, x_k >= 0. On the complexity front, I will show that the problem of maximizing a linear function over a Horn polyhedra is NP-hard.


Martin Zimmermann, Reactive Systems Group, Saarland University, Germany.
Tuesday 10.3.2015 at 10:00 in 0.2.13.

Parametric Linear Temporal Logics

Abstract: Linear-time Temporal Logic is the most popular logic for the specification and verification of reactive systems. However, it cannot express timing constraints and is not able two express all omega-regular properties. The first shortcoming was addressed by introducing parametric extensions like Prompt-LTL and Parametric LTL (PLTL) while there is a plethora of extensions of LTL with the full expressiveness of omega-regular languages. I will report on the model-checking and the synthesis problem for such logics: first, I consider PLTL, which extends LTL by bounded temporal operators that are for example able to express that every request is answered within some arbitrary, but fixed time. Then, I introduce PLDL, a novel parameterized logic that is able to express all omega-regular languages, i.e., a logic that simultaneously overcomes both shortcomings of LTL. Finally, I will consider the quantitative synthesis problem for a certain type of LTL formulas, so called request-response properties. Based on joint work with Peter Faymonville, Florian Horn, Wolfgang Thomas, and Nico Wallmeier.


Daniel Gebler, VU University Amsterdam, Netherlands.
Wednesday 21.1.2015 at 14:30 in 0.2.12.

Robust compositional specification of probabilistic processes

Abstract: Probabilistic transition systems are the fundamental structure in order to provide operational semantics to probabilistic nondeterministic systems and languages. For those systems, boolean notions of behavioural equivalences and logical satisfaction are too fragile. Over the last decade it became clear that metrics measuring degrees of behavioural (bi)similarity and degrees of logical satisfaction are the appropriate notion to allow for robust reasoning. In this talk I will present recent results that explore which operators of probabilistic process calculi allow for compositional reasoning with respect to bisimulation metric semantics. We consider various compositionality properties proposed in the literature and argue that the modulus of continuity of the compositionality property defines the maximal process replication behavior that is allowed for process combinators. Combining these results, we demonstrate how compositional reasoning about systems specified by continuous process algebra operators allows for metric assume-guarantee like performance validation.


Falak Sher Vira, RWTH Aachen University, Germany.
Tuesday 13.1.2015 at 13:00 in 0.2.90.

Tight Game Abstractions of Probabilistic Automata

Abstract: We present a new game-based abstraction technique for probabilistic automata (PA). The key idea is to use distribution-based abstraction – preserving novel distribution-based (alternating) simulation relations – rather than classical state-based abstraction. These abstractions yield (simple) probabilistic game automata (PGA), turn-based two-player stochastic games with – as opposed to classical stochastic games – equal decision power for both players. As distribution-based (alternating) simulation relations are pre-congruencies for composite PGA, abstraction can be done compositionally. Our abstraction yields tighter upper and lower bounds on (extremal) reachability probabilities than state-based abstraction. This shows the potential superiority over state-based abstraction of PA and Markov decision processes (restricted PA).


Marco Muniz, University of Freiburg, Germany.
Monday 8.12 at 13:00 in 0.2.12

Model Checking for Time Division Multiple Access (TDMA) Systems

Abstract: In this talk we present a number of techniques that make the model checking of TDMA systems with a large number of components possible. First, we formalize key principles of TDMA systems using the new semantic-based notions of periodic cyclic timed automata, disjoint activity, sequentialisability, and concatenation for sequentialisable periodic cyclic timed automata. The concatenation operator produces a system that is bisimilar to the one obtained by parallel composition. Application of the concatenation operator removes unnecessary edges and locations leading to quadratic speed ups. Next, in order to increase the applicability of model checking for industrial TDMA systems, we present the syntax-based class of sequential timed automata and a sequential composition operator. The sequential composition operator produces a system that is weakly bisimilar to the one obtained by parallel composition. Application of the sequential composition operator reduces the time complexity from exponential to linear in the number of components. Finally, we address another aspect of real timed systems: clocks that have different values in a run (i.e. in a sequence of states in the interleaving semantics of a network of timed automata) only for a period of zero time duration. We call these clocks quasi-equal clocks. Systems with such clocks can be simplified, yielding a much smaller equivalent system. Before a simplification can take place, the presence of quasi-equal clocks needs to be detected. We provide an efficient abstraction based analysis method for detecting quasi-equal and equal clocks.


Please contact Giorgio Bacci for information on the seminars in this series, and to be added to the mailing list for seminar announcements.

Giorgio Bacci (Assistant Professor)
Department of Computer Science, 1.2.59
Selma Lagerlofs Vej 300 
9220 Aalborg Øst, DK
Phone: +45 99 40 98 59