Anders Schlichtkrull, Dept. Computer Science, Aalborg University, DK
Tuesday 29.11.2022 at 13:00 in 0.2.12

Isabelle-verified correctness of Datalog programs for program analysis

Abstract: Static analysis has become an intrinsic part of the development process for developers seeking to avoid bugs and security vulnerabilities; even more so for high-assurance critical applications requiring formal verification. In this paper we use Isabelle to formalise and prove correct a Datalog formulation of the classical bit-vector framework, thus showing that Datalog-based analyses subsume bit-vector analyses, the first such formalized proof to the best of our knowledge. In order to do this we formalise the semantics of stratified Datalog, the first such formalisation in Isabelle to the best of our knowledge, and formally establish the existence of least solutions for any stratified Datalog program. Lastly, we illustrate the usefulness and applicability of our framework by further formalising four concrete classic analyses and proving them correct.

Scott Buckley, University of New South Wales (UNSW Sydney), Sydney, Australia. Monday 31.10.2022 at 14:00, in 0.2.13

A broad overview of seL4, its verification, and the verification of time protection

Abstract: In this talk, we give a brief overview of what seL4 is and how we verify seL4 (and what that means). We discuss how we conceptually verify time protection, and how we are adding time protection proofs to seL4's verification framework. In particular, we discuss micro-architectural timing channels which are well-known mechanisms for information leakage. Time protection has recently been demonstrated as an operating-system mechanism able to prevent them. However, established theories of information-flow security are insufficient for verifying time protection, which must distinguish between (legal) overt and (illegal) covert flows. We provide a machine-checked formalization of time protection via a dynamic, observer relative, intransitive non-leakage property over a careful model of the state elements that cause timing channels. We instantiate and prove our property over a generic model of OS interaction with its users, demonstrating for the first time the feasibility of proving time protection for OS implementations.

Alexander L. Robayo, Dept. Computer Science, Aalborg University, DK.
Wednesday 28.09.2022 at 14:00, in 0.2.13

Efficient Estimation of Agent Networks

Abstract: In this talk, I will present a framework to formally estimate global dynamics of nonlinear systems under all possible parameterizations. The approach contains two steps: estimation and reduction. The estimation step replaces the dependencies between variables by external parameters (decoupling). The decoupled system is then solved using estimation equivalence. This is an estimation-preserving reduction technique that uses a partition refinement algorithm and is of polynomial time complexity. We demonstrate the framework on a multi-class SIRS model from epidemiology and obtain a speed-up factor that is proportional to the number of population classes.

Christian Schilling, Dept. Computer Science, Aalborg University, DK
Tuesday 06.09.2022 at 10:00 in NOVI9-1.112

Synthesis of hybrid automata from time-series data

Abstract: I will present an algorithmic framework for synthesizing a hybrid automaton from time-series data. The key feature of the framework is that the automaton is guaranteed to capture the data up to some precision error epsilon, in the following sense: for each time series, the automaton contains an execution that is epsilon-close to the data points. I will discuss several algorithms with different feature sets such as online and offline synthesis, different classes of dynamics, or the choice of the value epsilon.

Sarah Winter, Dept. Computer Science, Université libre de Bruxelles, Belgium. Wednesday 24.08.2022 at 14:00, in 0.2.13

Unambiguity in Transducer Theory

Abstract: This talk surveys some introductory results regarding unambiguity in transducer theory. Transducers are automata with output; they recognize relations. A transducer is unambiguous if for each word u from its domain there is a unique accepting run with input u. In more detail, we show that the classes of functions recognized by functional transducers and unambiguous transducers coincide. We also show that unambiguity, while necessary for one-way transducers, can be traded for determinism at the price of two-wayness.

Samitha Samaranayake, School of Civil and Environmental Engineering, Cornell University. Friday 1.07.2022 at 10:30, in 0.2.90

Algorithmic foundations for demand-responsive transit systems

Abstract: Affordable, equitable and efficient access to personal mobility is a fundamental societal need---with broad implications for personal well-being, economic mobility, education, and public health. Emerging mobility services have disrupted the urban transportation ecosystem and instilled hope that new data-driven mobility solutions can improve personal mobility for all. While these apps provide a valuable service, as evident by their popularity, there are many questions regarding their scalability, efficiency, impact on equity, and negative externalities (e.g. congestion). On the other hand, traditional public transit systems provide affordable and community-oriented access to personal mobility, but have their own operational limitations. This talk will focus on some algorithmic foundations for integrating public transit operations with agile, demand-responsive services with the goal of enabling personal mobility for all.

Ander Gray, Advanced Computing, United Kingdom Atomic Energy Authority, and University of Liverpool, UK. Wednesday 11.05.2022 at 14:30, in 0.2.90

Rigorous enclosures of probabilities in reachability analysis

Abstract: Reachability Analysis studies the rigorous time evolution of sets in non-linear dynamical systems. One is often interested verification problems, where we wish to guarantee that a future state U of the system is not reached. The analysis returns three possible probabilities: P(U) = 0 (guaranteed to be safe), P(U) = 1 (guaranteed to be unsafe), and the interval probability P(U) = [0, 1] (unknown safety). The last of these options is a drawback of the method, that it may not be possible to prove or disprove the safety of the system. We combine Reachability Analysis and Probability Bounds Analysis, which in addition to intervals, allows for an imprecisely known random variable (a probability box) to be specified as the initial states of the dynamical system, returning more general interval probabilities for verification problems. The methodology places no constraints on the input probability distribution and can handle dependencies generally in the form of copulas.

Luca Ferranti, University of Vaasa, Finland
Wednesday 11.05.2022 at 14:30, in 0.2.90

Solving systems of linear equations with interval methods and application to engineering problems

Abstract: Solving linear systems is central in most computational domains, from mathematics to engineering applications. This talk will introduce IntervalLinearAlgebra.jl: a package written in Julia to solve linear systems, with interval or real coefficients, rigorously. That is, producing a set guaranteed to contain the true solution of the original problem. This can be applied to solve problems involving uncertainty propagation or perform self-validated computations.

Marcelo Forets, Universidad de la República, Montevideo, Uruguay
Wednesday 11.05.2022 at 14:30, in 0.2.90

Applying reachability to transient dynamics problems

Abstract: In this talk we review a novel approach for time integration with applications to heat transfer and structural dynamics problems in mechanical engineering and related disciplines. The procedure is based on set-based reachability analysis techniques and finite element methods (FEM), and it is implemented in our SOTA open-source toolkits JuliaReach and ONSAS, the former developed in collaboration with Christian Schilling.

Anna Lukina & Emir Demirović, Dept. of Software and Computer Technology, TU Delft, The Netherlands. Tuesday 19.04.2022 at 10:00, in 0.2.90

Optimal Decision Trees, Controllers, and Formal Methods

Abstract: The talk is part of our research visit, where our aim is to explore the connection between (optimal) decision trees, controllers, and formal methods! For this reason we divided the talk into two parts.
In the first part of the talk, we motivate our discussion with applications of decision tree learning in verification of neural-network based controllers. Revisiting verification of decision trees distilled from such controllers, we explore scalability of this approach with respect to the tree size. This discussion is based on "Formal Methods with a Touch of Magic" (FMCAD'20) and recent experiments.
In the second part, we provide an overview of our approaches to global optimisation of decision trees for classification problems. This is in contrast to traditional decision tree algorithms, which are based on heuristics. Our novel methods are based on dynamic programming and search, support constraints on the depth of the tree and number of nodes, and optimise accuracy and nonlinear metrics such as the F1-score. The success of our approach is attributed to a series of specialised techniques that exploit properties unique to classification trees. Our detailed experimental study demonstrates that our approach uses only a fraction of the time required by the state-of-the-art and can handle datasets with tens of thousands of instances, providing several orders of magnitude improvements. These results are based on two recent papers: "MurTree: Optimal Decision Trees via Dynamic Programming and Search" (JMLR'22) and "Optimal Decision Trees for Nonlinear Metrics" (AAAI'21).

Christian Schilling, Dept. of Compurer Science, Aalborg University, DK.
Thursday 03.02.2022 at 14:00, in 0.2.13

Verification of neural-network control systems

Abstract: We study the verification problem for closed-loop dynamical systems with neural-network controllers (NNCS). This problem is commonly reduced to computing the set of reachable states. When considering dynamical systems and neural networks in isolation, there exist established approaches for that task based on various set representations. However, the combination of these approaches to NNCS is non-trivial because, when converting between the set representations, dependency information gets lost in each control cycle and the accumulated approximation error quickly renders the result useless. We present an algorithm to chain approaches based on Taylor models and zonotopes, yielding a precise reachability algorithm for NNCS. Our implementation delivers state-of-the-art performance and is the first to successfully analyze all benchmark problems of an annual reachability competition for NNCS.

Nikolaj Jensen Ulrik, Dept. of Compurer Science, Aalborg University, DK.
Tuesday 11.01.2022 at 14:00, in 0.2.13 (and Teams: )

Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking

Abstract: In LTL model checking, a system model is synchronized using the product construction with Büchi automaton representing all runs that invalidate a given LTL formula. The existence of a run with infinitely many occurrences of an accepting state in the product automaton then provides a counter-example to the validity of the LTL formula. Classical partial order reduction methods for LTL model checking allow to considerably prune the searchable state space, however, the majority of published approaches do not use the information about the current Büchi state in the product automaton. We demonstrate that this additional information can be used to significantly improve the performance of existing techniques. In particular, we present a novel partial order method based on stubborn sets and a heuristically guided search, both driven by the information of the current state in the Büchi automaton. We implement these techniques in the model checker TAPAAL and an extensive benchmarking on the dataset of Petri net models and LTL formulae from the 2021 Model Checking Contest documents that the combination of the automata-driven stubborn set reduction and heuristic search improves the state-of-the-art techniques by a significant margin.

Alvaro Torralba, Dept. Computer Science, Aalborg University, DK.
Monday 29.11.2021 at 13:00, in 0.2.13

Dominance Analysis in AI Planning

Abstract: AI Planning is a model-based approach to intelligent sequential decision making. Given a model of the environment, a rational agent can automatically decide what actions to perform to achieve its goals with minimal cost. The aim is to decouple the description of the problem and the mechanism to make intelligent decisions, so that the same algorithm can be applied to solve any domain (e.g. logistics, space exploration, chemistry, natural language generation). In classical planning, this is formally represented as finding a path in the state space: a graph implicitly given by the model that describes the outcome of all possible actions of the agent. However, this graph is often exponential in the size of the model, so it is unfeasible to explore it completely. The key is to exploit the structure of the task, finding its individual properties.
This talk introduces dominance analysis, a novel technique to unveil the structure of a planning task in the form of a relation that compares pairs of states, proving that one of them is preferable to achieve the agent's goal. This can be used in different ways, e.g., to eliminate states that are dominated by others, or identify actions leading to better states. This provides a speed-up of up to several orders of magnitude on tasks where dominance can be discovered.

Marcel Baunach & Leandro B. Ribeiro, EAS, TU Graz, Austria.
Tuesday 24.08.2021 at 14:00, in 0.1.95

The Embedded Automotive Systems Group and its Work with UPPAAL

Abstract: In the first part of the presentation, Prof. Baunach introduces the Embedded Automotive Systems Group at Graz University of Technology and current research projects on Compositional Embedded Automotive Hardware and Software, Dependable Internet of Things, and the group’s embedded operating system and reconfigurable processor architecture.
In the second part, Leandro Batista Ribeiro covers his current work on modeling and verifying embedded software stacks with UPPAAL. Details of the EAS Group's research operating system (MCSmartOS) are presented along with an overview of the OS model. It is shown how to model application modules that run on top of the OS and how compositional application software can be verified by combining the OS model and the application model. The goal of the verification is to, e.g., guarantee the consistency of OS data structures, prove the absence of potential deadlocks, starvation, and deadline violations.

Martin Zimmermann, Dept. Computer Science, Aalborg University, DK.
Monday 16.08.2021 at 14:30, in 0.1.95

Logics, Automata, and Synthesis

Abstract: This talk is an invitation for collaboration: I will introduce myself and my work, both trying to give a general overview and to present some details on projects I am currently working on:   HyperLTL and HyperCTL* are temporal logics for the specification and verification of information-flow properties, crucial for security and privacy. They generalize classical temporal logics, i.e., LTL and CTL* by trace quantification, which allows to reason about multiple executions of a system simultaneously. I will give a gentle introduction to these logics and discuss some of my own results on satisfiability and connections to first-order logic. (2) Good-for-games pushdown automata have recently been introduced as a novel class of nondeterministic pushdown automata for which both universality and solving games are decidable (while it is undecidable for general nondeterministic pushdown automata). I will discuss some results and many open problems. (3) Reactive synthesis asks to automatically generate a correct-by-construction system from its specification. I argue that synthesis has to be treated as a multidimensional optimization problem and present some results for combinations of these dimensions.

Michele Albano, Dept. Computer Science, Aalborg University, DK.
Monday 14.12.2020 at 14:00, virtually on Zoom

AoI-based Multicast Routing over Voronoi Overlays with Minimal Overhead

Abstract: The increasing pervasive and ubiquitous presence of devices at the edge of the Internet is creating new scenarios for the emergence of novel services and applications. This is particularly true for location and context-aware services.  These services call for new decentralized, self-organizing communication schemes that are able to face issues related to demanding resource consumption constraints while ensuring efficient locality-based information dissemination and querying. Voronoi-based communication techniques are among the most widely used solutions in this field. However, when used for forwarding messages inside closed areas of the network (called Areas of Interest, AoIs), these solutions generally require a significant overhead in terms of redundant and/or unnecessary communications. This fact negatively impacts both the devices' resource consumption levels, as well as the network bandwidth usage. In order to eliminate all unnecessary communications, this talk presents the MABRAVO (Multicast Algorithm for Broadcast and Routing over AoIs in Voronoi Overlays) protocol suite. MABRAVO allows to forward information within an AoI in a Voronoi network using only local information, reaching all the devices in the area, and using the lowest possible number of messages, i.e., just one message for each node included in the AoI.

Peter G. Jensen, Dept. Computer Science, Aalborg, DK.
Wednesday 09.12.2020 at 13:00, virtually on Zoom

Teaching Stratego to Play Ball - Optimal Synthesis for Continuous Space MDPs

Abstract: Formal models of cyber-physical systems, such as priced timed Markov decision processes, require a state space with continuous and discrete components. The problem of controller synthesis for such systems then can be cast as finding optimal strategies for Markov decision processes over a Euclidean state space. We develop two different reinforcement learning strategies that tackle the problem of continuous state spaces via online partition refinement techniques. We provide theoretical insights into the convergence of partition refinement schemes. Our techniques are implemented in Uppaal Stratego. Experimental results show the advantages of our new techniques over previous optimization algorithms of Uppaal Stratego.

Anders Schlichtkrull, Dept. Computer Science, Aalborg (Copenhagen), DK. Friday 04.12.2020 at 14:00, virtually on Zoom

Formal Formal Methods with Isabelle/HOL

Abstract: With formal methods, we use computer programs to conclude that systems live up to their specification. However, formal-methods computer programs are also systems that should live up to their specification and give correct results. If they do not, then there is a risk that we may use them to draw wrong conclusions about other systems, or that they are not able to draw all the conclusions that we expect them to. In this talk, I suggest that we apply formal methods to formal methods and overcome this. We can call this Formal Formal Methods. Specifically, I show how Isabelle/HOL can be used to prove the soundness and completeness of a resolution theorem prover. In addition to revealing several mistakes in the literature, Isabelle/HOL helps us clear up theory, gives the literature a formal companion, and creates an explicit link between the theory and the running software. In the talk, I also suggest a number of possibilities for applying Formal Formal Methods to the research done in DEIS. Here, suggestions from the audience will be very welcome!

Charif Mahmoudi, University Paris-Est Créteil, France & Siemens Corporate Technology, US. Friday 20.11.2020 at 15:00, virtually on Zoom

Towards a Verified Enhancement of Embedded Cyber-Physical Platforms

Abstract: The enhancement of legacy code with more performant components faces challenges regarding the compatibility of the newly integrated components with the rest of the system. Formal verification is a key to provide a developer-accessible capability for piece-by-piece enhancement of software components with new verified code that is both correct-by-construction and compatible-by-construction. This talk describes a methodology that leverages formal methods to build verified connections between a functional Domain-Specific Language (DSL) and the actual running code to enable an end-to-end verification of the correctness and compatibility of the enhanced components with the rest of the system.

Andrej Kiviriga, Dept. of Computer Science, Aalborg University, DK.
Monday 2.11.2020 at 14:00, virtually on Zoom 

Randomized Refinement Checking of Timed I/O Automata

Abstract. To combat the state-space explosion problem and ease system development, we present a new refinement checking (falsification) method for Timed I/O Automata based on random walks. Our memoryless heuristics Random Enabled Transition (RET) and Random Channel First (RCF) provide efficient and highly scalable methods for counterexample detection. Both RET and RCF operate on concrete states and are relieved from expensive computations of symbolic abstractions. We compare the most promising variants of RET and RCF heuristics to existing symbolic refinement verification of the Ecdar tool. The results show that as the size of the system increases our heuristics are significantly less prone to exponential increase of time required by Ecdar to detect violations: in very large systems both “wide” and “narrow” violations are found up to 600 times faster and for extremely large systems when Ecdar timeouts, our heuristics are successful in finding violations.

Marco Muñiz, Dept. of Computer Science, Aalborg University, DK.
Friday 16.10.2020 at 14:00, virtually on Zoom

Urgent Partial Order Reduction for Extended Timed Automata

Abstract. We propose a partial order reduction method for reachability analysis of networks of timed automata interacting via synchronous channel communication and via shared variables. Our method is based on (classical) symbolic delay transition systems and exploits the urgent behaviour of a system, where time does not introduce dependencies among actions. In the presence of urgent behaviour in the network, we apply partial order reduction techniques for discrete systems based on stubborn sets. We first describe the framework in the general setting of symbolic delay time transition systems and then instantiate it to the case of timed automata. We implement our approach in the model checker Uppaal and observe a substantial reduction in the reachable state space for case studies that exhibit frequent urgent behaviour and only a moderate slowdown on models with limited occurrence of urgency.
This is a joint work with Kim G. Larsen, Marius Mikucionis, and Jiri Srba

Andrea Vandin, Dept. of Applied Mathematics and Computer Science, DTU Compute, DK. Friday 22.11.2019 at 14:00 in 0.2.90.

Speeding up the simulation of large-scale dynamical systems by aggregation

Abstract: Dynamical systems across many branches of science and engineering can be described in terms of massively many entities, possibly interacting over large-scale networks. Examples are social networks involving spreading (or diffusion) of rumours, opinions, epidemics, malware, or technologies, as well as models of protein-interaction networks, and distributed computing systems. Mathematically, these models can often be described as stochastic processes or differential equations which, in all but special cases, do not enjoy analytical solutions. This requires computationally-expensive analysis based on stochastic simulators and numerical solvers, hindering our capability of dealing with complex large-scale real-world models. This talk will overview an array of recent techniques and tools of mine that tame the complexity of complex large-scale models by aggregating their constituting systems of equations while preserving the models' intelligibility and dynamics.

Stefano Chessa, Department of Computer Science, University of Pisa, Italy. Tuesday 19.11.2019 at 13:30 in 0.2.90.

Scheduling tasks  in energy harvesting IoT

Abstract: Internet of Things (IoT) applications can exploit energy harvesting systems to guarantee virtually uninterrupted operations. However, the use of energy harvesting poses issues concerning the optimization of the utility of the application while guaranteeing energy neutrality of the devices. The talk will present a dynamic programming algorithm for the optimization of the scheduling of the tasks in IoT devices that harvest energy by means of a solar panel. The scheduling problem is NP-hard and the algorithm can find the optimum solution in pseudo-polynomial time. Nevertheless, the algorithm can be executed with a small overhead even on low-power IoT platforms.

Imran Hasrat, Dept. of Computer Science, Aalborg University, DK.
Friday 15.11.2019 at 14:00 in 0.2.90.

Formal Specification and Analysis of Termination Detection by Weight-throwing Protocol

Abstract: Termination detection is a critical problem in distributed systems. A distributed computation is called terminated if all of its processes become idle and there are no in-transit messages in communication channels. A distributed termination detection protocol is used to detect the state of a process at any time, i.e., terminated, idle or active. A termination detection protocol on the basis of the weight-throwing scheme is described in Yu-Chee Tseng, “Detecting Termination by Weight-throwing in a Faulty Distributed System”, JPDC, 15 February 1995. We apply model checking techniques to verify the protocol and for formal specification and verification, the tool-set UPPAAL is used. Our results show that the protocol fails to fulfil some of its functional requirements.

Nicolas Schnepf, Dept. of Computer Science, Aalborg University, DK.
Thursday 14.11.2019 at 14:00 in 0.2.90.

Orchestration and verification of security functions for smart devices

Abstract: Smart environments, in particular smartphones, are the target of multiple security attacks. Moreover, the deployment of traditional security mechanisms is often inadequate due to their highly constrained resources. In that context, we propose to use chains of security functions which are composed of several security services, such as firewalls or antivirus, automatically configured and deployed in the network. Chains of security functions are known as being error-prone and hard to validate. This difficulty is caused by the complexity of these constructs that involve hundreds and even thousands of configuration rules. 
During my PhD thesis, I proposed the architecture of an orchestrator, exploiting the programmability brought by software-defined networking, for the automated configuration and deployment of chains of security functions. It is important to automatically ensure that these security chains are correct, before their deployment in order to avoid the introduction of security breaches in the network. To do so, my orchestrator relies on methods of automated verification and synthesis to ensure the correctness of the chains. My work also considers the optimization of the deployment of chains of security functions in the network, in order to maintain its resources and quality of service.

Muhammad Naeem, Dept. of Computer Science, Aalborg University, DK.
Friday 08.11.2019 at 14:00 in 0.2.90.

Modelling and Analysis of Cooperative Packet Recovery Protocol

Abstract: Real-time audio/video transmission through Internet media is an important part of communication. Due to bandwidth limitation and noisy environment, delivery of multimedia contents to a remote location is not 100% guaranteed. These limitations are the basic cause of missing packets which eventually affect the Quality of Service (QoS). A protocol for the recovery of lost packets is described in [Maxemchuk, Nicholas F., K. Padmanabhan, and S. Lo. “A cooperative packet recovery protocol for multicast video.” Network Protocols, 1997. International Conference on. IEEE.]. This protocol claims a significant improvement in QoS. We formally specify the protocol as a network of timed automata. By model-checking, we find that packet recovery is not always there. We report the scenarios of malfunctioning in the protocol when the size of multimedia contents is unknown (e.g., live broadcasting) and the middle-level server has a different rate of data sending and receiving. Moreover, we formulate the effects of inter-packet delay and transmission speed upon the packet recovery mechanism.

Mikkel Hansen, Dept. Computer Science and DEIS, Aalborg University, DK. Thursday 05.09.2019 at 14:00 in 0.2.90.

Model Checking Constrained Markov Reward Models with Uncertainties

Abstract: We study the problem of analysing Markov reward models (MRMs) in the presence of imprecise or uncertain rewards. Properties of interests for their analysis are (i) probabilistic bisimilarity, and (ii) specifications expressed as probabilistic reward CTL formulae.
We consider two extensions of the notion of MRM, namely (a) constrained Markov reward models, i.e., MRMs with rewards parametric on a set variables subject to some constraints, and (b) stochastic Markov reward models, i.e., MRMs with rewards modelled as real-valued random variables as opposed to precise rewards. Our approach is based on quantifier elimination for linear real arithmetic. Differently from existing solutions for parametric Markov chains, we avoid the manipulation of rational functions in favour of a symbolic representation of the set or parameter valuations satisfying a given property in the form of a quantifier-free first-order formula in the linear theory of the reals.
Our work finds applications in model repair, where parameters need to be tuned so as to satisfy the desired specification, as well as in robustness analysis in the presence of stochastic perturbations.
This is a joint work with Giovanni Bacci and Kim G. Larsen.

André Platzer, Department of Computer Science, Carnegie Mellon University, USA. Wednesday 19.06.2019 at 14:00 in 0.2.90.

Safe AI for CPS

Abstract: Autonomous cyber-physical systems are systems that combine the physics of motion with advanced cyber algorithms to act on their own without close human supervision. The present consensus is that reasonable levels of autonomy, such as for self-driving cars or autonomous drones, can only be reached with the help of artificial intelligence and machine learning algorithms that cope with the uncertainties of the real world. That makes safety assurance even more challenging than it already is in cyber-physical systems (CPSs) with classically programmed control, precisely because AI techniques are lauded for their flexibility in handling unpredictable situations, but are themselves harder to predict.
This talk identifies the logical path toward autonomous cyber-physical systems. With the help of differential dynamic logic (dL) do we provide a logical foundation for developing cyber-physical system models with the mathematical rigor that their safety-critical nature demands. Its ModelPlex technique provides a logically correct way to tame the subtle relationship of CPS models to CPS implementations. The resulting logical monitor conditions can then be exploited to safeguard the decisions of learning agents, guide the optimization of learning processes, and resolve the nondeterminism frequently found in verification models. Overall, logic leads the way in combining the best of both worlds: the strong predictions that formal verification techniques provide alongside the strong flexibility that the use of AI provides.

Max Tschaikowski, Institute of Computer Engineering, TU Wien, Austria.
Wednesday 29.05.2019 at 13:00 in 0.2.90.

Lumpability for Uncertain Continuous-Time Markov Chains

Abstract: In the first part of the talk, we will discuss a submitted work that focuses on uncertain CTMCs where rates are assumed to vary non-deterministically with time. This leads to a semantics which associates each state with the reachable set of its probability under all possible choices of the uncertain rates. We will develop a notion of lumpability as a partition of the states such that the reachable set of a state in the lumped chain is equal to the reachable set of the sum of the probabilities of the original states belonging to that partition block, thus lifting the well-known CTMC ordinary lumpability to the uncertain setting. Similarly to CTMCs, we will provide a polynomial time and space algorithm for the minimization of an uncertain CTMC by partition refinement. Finally, we will show that lumpability of uncertain CTMCs preserves model checking of uncertain CTMCs. (This is joint work with L. Cardelli, R. Grosu, M. Tribastone, and A. Vandin.)

Shyam Lal Karra, Department of Computer Science, Aalborg University, DK. Tuesday 28.05.2019 at 14:00 in 0.2.90.

Safe and Time-Optimal Control for Railway Games

Abstract: Railway scheduling is a complex and safety-critical problem that has recently attracted attention in the formal verification community. We provide a formal model of railway scheduling as a stochastic timed game and using the tool UPPAAL STRATEGO, we synthesize the most permissive control strategy for operating the lights and points at the railway scenario such that we guarantee system's safety (avoidance of train collisions). Among all such safe strategies, we then select (with the help of reinforcement learning) a concrete strategy that minimizes the time needed to move all trains to their target locations. This optimizes the speed and capacity of a railway system and advances the current state-of-the-art where the optimality criteria were not considered yet.

Mikkel Thorup, Department of Computer Science, University of Copenhagen, DK. Friday 03.05.2019 at 14:00 in 0.2.13.

Unleashing the Power of Hashing

Abstract: Hash functions are used everywhere in computing. Originally, hashing was invented to store and look up elements in computer memory, but more recently it has become a crucial component in the analysis of Big Data applications. We think of a hash function as a random function, assigning random hash values to elements; thus if we use hash values to place elements in computer memory then we expect them to spread out nicely.  At the same time, the hash function has to be fixed as soon as we start using it; otherwise can't find the elements again. In the context of Big Data, we use hash functions to create small sketches of large sets, allowing us to quickly measure how similar they are, and if they are similar, what exactly are the differences. The sets can be processed independently as long as we use the same hash function to create the sketch. 
I will talk about some of these applications of random hash functions, about the probabilistic properties they are required to have, and about how they can be generated to work efficiently on huge data sets.

Stefan Schmid and Klaus-Tycho Förster, Department of Computer Science, University of Vienna, Austria.
Tuesday 02.04.2019 at 14:30 in 0.2.90.

Emerging Communication Networks: A Case for Automation – and Formal Methods?

Abstract: Communication networks have become a critical infrastructure of our digital society. However, today’s communication networks are complex and inflexible to operate and manage. In this talk, I will argue that in order to meet the stringent dependability and performance requirements of emerging applications, communication networks need to become more automated. To this end, I will discuss two case studies: (1) fast failover in MPLS networks and (2) consistent network policy updates. For the first case study, I will present an automata-theoretic approach to design a polynomial-time what-if analysis tool, and for the second case study, I will provide an overview of challenges. Finally, I will discuss my vision of “Self-Driving Networks”.

 

Sibylle Schupp, Head of Institute STS, Technische Universität Hamburg, Germany.
Wednesday 06.02.2019 at 14:00 in 0.2.90.

Reasoning about Software in an Unreasonable World

Abstract: The degree of dependability increases, and so does the need to provide formal guarantees about the workings of a software system. But what if the gap between model and reality is too big or if reality cannot be modeled at all? Reporting from recent collaborations with engineers from medical technology and social scientists from law school I exemplify in this talk with underspecified, incomplete, or informally specified systems which problems one encounters from a verification point of view and show some of the approaches and prototypes we currently develop in the STS group ("Software, Technology, Systems") group at TUHH.

 

Lars Moltsen, Chief Science Officer and Founder of 2Operate, Denmark.
Friday 02.11.2018 at 14:00 in 0.2.11.

Getting access to data from 5G networks through standardised interfaces

Abstract: 2operate is a local company (Aalborg, Denmark) providing network management software for mobile network operators. As an independent management systems provider, 2operate relies on data interfaces from equipment vendors (Ericsson, Nokia, Huawei, etc.). Lars Moltsen, one of the founders of 2operate, will talk about the various types of data and interfaces from early days when everything was proprietary interfaces, to the 3G specifications of management layer (ETSI/3GPP, from around 2000 - and used today), to the latest, ongoing ETSI/3GPP specification of service-oriented interfaces in upcoming 5G (REST, JSON). Lars will also talk about how 2operate has developed a feature for automated diagnostics of network faults using Bayesian networks. Lars is currently leading a project, MegaMan, which aims to push the same interfaces for satellite constellations networks.

 

Frederik M. Bønneland, Dept. Computer Science, Aalborg University, DK.
Wednesday 20.06.2018 at 15:00 in 0.2.90.

Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems

Abstract: Partial order reduction for timed systems is a challenging topic due to the dependencies among events induced by time acting as a global synchronization mechanism. So far, there has only been a limited success in finding practically applicable solutions yielding significant state space reductions. We suggest a working and efficient method to facilitate stubborn set reduction for timed systems with urgent behaviour. We first describe the framework in the general setting of timed labelled transition systems and then instantiate it to the case of timed-arc Petri nets. The basic idea is that we can employ classical untimed partial order reduction techniques as long as urgent behaviour is enforced. Our solution is implemented in the model checker TAPAAL and the feature is now broadly available to the users of the tool. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.

 

Lukas Esterle, Aston Lab for Intelligent Collectives Engineering, Aston University, United Kingdom.
Monday 11.06.2018 at 14:00 in 0.2.13.

Self-organised team affiliation in collectives of mobile and autonomous IoT devices

Abstract: Collaboration in teams can be essential in collectives, in order to achieve goals, individual devices would otherwise not be able to accomplish. This problem becomes more important when the individual teams pursue tasks that are complimentary to each other. In a distributed and highly dynamic system, a global coordination might not be possible. In this talk, we look into the multi-task k-assignment problem where tasks arise dynamically at runtime and require multiple devices to be completed. Since operators might not be able to determine all dynamic aspects of the given environment at the time of deployment, I present a novel, goal-aware approach to affiliate each device with a team at runtime. In this novel approach, devices only operate on aggregated information from the network which is constantly changes during runtime. Finally, I will also present an approach to select a team affiliation during runtime using machine learning techniques.

 

Peter Gjøl Jensen, Dept. of Computer Science, Aalborg University, Denmark.
Thursday 07.06.2018 at 14:30 in 0.2.13.

Simplification of CTL Formulae for Efficient Model Checking of Petri Nets

Abstract: We study techniques to overcome the state space explosion problem in CTL model checking of Petri nets. Classical state space pruning approaches like partial order reductions and structural reductions become less efficient with the growing size of the CTL formula. The reason is that the more places and transitions are used as atomic propositions in a given formula, the more of the behaviour (interleaving) becomes relevant for the validity of the formula. We suggest several methods to reduce the size of CTL formulae, while preserving their validity. By these methods, we significantly increase the benefits of structural and partial order reductions, as the combination of our techniques can achieve up to 60 percent average reduction in formulae sizes. The algorithms are implemented in the open-source verification tool TAPAAL and we document the efficiency of our approach on a large benchmark of Petri net models and queries from the Model Checking Contest 2017.

 

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.
Wednesday 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 dynamical 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 Inequality 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 exploits the rewrite rule: x_i - x_j - x_k >= 3, x_i, x_j, x_k >= 0 --> x_i >= 3. The second algorithm exploits 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.