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.

# Seminars

## Seminars

## List of Seminars

Mathias R. Pedersen, Dept. of Computer Science, Aalborg University, Denmark.

Tuesday 24.04.2018 at 14:00 in 0.2.90.

*Timed Comparisons of Semi-Markov Processes*

Abstract: Semi-Markov processes are Markovian processes in which the firing time of transitions is modelled by probabilistic distributions over positive reals interpreted as the probability of firing a transition at a certain moment in time. In this paper we consider the trace-based semantics of semi-Markov processes, and investigate the question of how to compare two semi-Markov processes with respect to their time-dependent behaviour.

To this end, we introduce the relation of being "faster than" between processes and study its algorithmic complexity. Through a connection to probabilistic automata we obtain hardness results showing in particular that this relation is undecidable. However, we present an additive approximation algorithm for a time-bounded variant of the faster-than problem over semi-Markov processes with slow residence-time functions, and a coNP algorithm for the exact faster-than problem over unambiguous semi-Markov processes.

Shyamlal Karra, Dept. of Computer Science, Aalborg University, Denmark.

Tuesday 28.03.2018 at 14:00 in 0.2.11.

*Petri Games are Monotonic but difficult to Decide*

Abstract: We shall look at two-player games played on infinite but monotonic game structures. We concentrate on coverability games, a natural subclass of reachability games in the context of monotonic game structures. On the negative side, we show that surprisingly, and contrary to the one-player case, coverability is undecidable on two-player mono- tonic game structures. We shall focus on the undecidability results of these monotonic game structures by looking into the proofs of reducing the two counter machine reachability problem to the strategy synthesis problem on these games. On the positive side, we identify an interesting subclass of two-player monotonic game structures, for which coverability is decidable and for which we can effectively construct winning strategies. Furthermore, we show how to define two-player game structures that belong to that subclass with Petri nets. The results of this paper are compared to recent results obtained independently by Abdulla, Bouajjani and d’Orso on similar game structures where they identify another subclass of monotonic game structures with decidable results.

Peter Gjøl Jensen, Dept. of Computer Science, Aalborg University, Denmark.

Tuesday 27.03.2018 at 14:00 in 0.2.11.

*PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing*

Abstract: Sets and their efficient implementation are fundamental in all of computer science, including model checking, where sets are used as the basic data structure for storing (encodings of) states during a state-space exploration. In the quest for fast and memory efficient methods for manipulating large sets, we present a novel data structure called PTrie for storing sets of binary strings of arbitrary length. The PTrie data structure distinguishes itself by compressing the stored elements while sharing the desirable key characteristics with conventional hash-based implementations, namely fast insertion and lookup operations. We provide the theoretical foundation of PTries, prove the correctness of their operations and conduct empirical studies analysing the performance of PTries for dealing with randomly generated binary strings as well as for state-space exploration of a large collection of Petri net models from the 2016 edition of the Model Checking Contest (MCC'16). We experimentally document that with a modest overhead in running time, a truly significant space-reduction can be achieved. Lastly, we provide an efficient implementation of the PTrie data structure under the GPL version 3 license, so that the technology is made available for memory-intensive applications such as model-checking tools.

Shiyan Hu, Chair of Cyber-Physical Systems, Linnaeus University, Sweden.

Friday 09.03.2018 at 11:00 in 0.2.90.

*Smart Energy Cyber-Physical System Security: Threat Analysis and Defense Technologies*

Abstract: The massive deployment of advanced metering infrastructures and smart energy systems has mandated a transformative shift of the classical grid towards a more reliable smart grid. Despite its importance, such a cyber-physical system is vulnerable to various cyberattacks. In this talk, I will describe a systematic data analytics framework, which is based on partially observable Markov decision process, orthogonal matching pursuit, and empirical mode decomposition, to detect anomaly energy usage behavior through analyzing the massive smart meter data in a community. I will also discuss how this framework can be used for detecting smart grid cyberattacks such as energy theft. I will conclude the talk with some of the ongoing research in this direction.

Adrien Le Coent, Dept. of Computer Science, Aalborg University, Denmark.

Thursday 01.03.2018 at 13:30 in 0.2.90.

*Set-based simulation of dynamical systems using the Euler method*

Abstract: Computing the solution at discrete times of a linear ordinary differential equation when the initial condition is given as a box can be easily done using polytopes, and this, because we know exactly the solution of the ODE, which can be written as an affine transformation. Yet, generally, the exact solution of nonlinear differential equations cannot be obtained, and a numerical integration scheme is used to approximate the state of the system. With the objective of synthesizing guaranteed controllers for switched dymamical systems and ensuring continuous time properties, the computation of a reachability tube is mandatory.

To this end, we propose an extremely fast approach based on the Euler method. Associated to the hypothesis that the vector fields are one-sided Lipschitz (OSL), we establish a new error bound for the Euler method. An appropriate way to exploit this new bound is balls of Rn, and the formula established is available for all time in the switching period. It allows us to compute reachability tubes in an extremely fast way compared to Runge-Kutta methods, although it can lack accuracy for certain values of the OSL constant. The method is implemented in a symbolic control synthesis tool, and we propose some other possible applications. We illustrate the approach on several examples of the literature and the results are compared with a previous method based on the Runge-Kutta integration method.

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.

## See also ...

## Contact

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