* The last session ends at 12 noon on Feb 4th.
Talk titles and abstracts
- Nathalie Bertrand: Controlling a population of NFA (slides)
Abstract: We consider a family of identical NFA, and view it as a 2-player game: the first player chooses which action to play, and the second one resolves the non-determinism in each copy of the NFA. The objective for the first player is to synchronize all copies to a target state. In this talk, we will report on decidability and complexity of the following parameterized problem: for every family size, does the first player have a winning strategy? We will also discuss memory requirements and cutoffs.
- Supratik Chakraborty: Hashing-based Methods for Approximate Sampling and Counting (slides)
Abstract: Constrained counting and sampling are two fundamental problems in artificial intelligence with a diverse range of applications from probabilistic reasoning to constrained random verification. While the theory of these problems have been thoroughly investigated in the 1980s, prior work either did not scale to real-life problem instances, or gave up theoretical guarantees to achieve scalability. Recently, we have proposed an approach that combines universal hashing with SAT/SMT solving to address this problem. This has resulted in algorithms that scale to formulas with hundreds of thousands of variables, while preserving strong theoretical guarantees. In this talk, we discuss the key ingredients of this approach and discuss challenges that lie ahead.
- Martin FrΓ€nzle: Multi-Objective Parameter Synthesis in Probabilistic Hybrid Systems (slides)
(joint work with Alessandro Abate, Sebastian Gerwinn, Joost-Pieter katoen, and Paul KrΓΆger)
Abstract: Technical systems interacting with the real world can be modelled elegantly using probabilistic hybrid automata (PHA). Parametric probabilistic hybrid automata are dynamical systems featuring hybrid discrete-continuous dynamics and parametric probabilistic branching, thereby generalizing PHA by capturing a family of PHA within a single model. Such system models have a broad range of applications, from control systems over network protocols to biological components. We present a novel method to synthesize parameter instances (if such exist) of PHA satisfying a multi-objective bounded horizon specification over expected rewards. Our approach combines three techniques: statistical model checking of model instantiations, a symbolic version of importance sampling to handle the parametric dependence, and SAT-modulo-theory solving for finding feasible parameter instances in a multi-objective setting. The method provides statistical guarantees on the synthesized parameter instances. To illustrate the practical feasibility of the approach, we present experiments showing the potential benefit of the scheme compared to a naive parameter exploration approach.
- Blaise Genest: Languages of Markov Chains (slides)
Abstract: (Discrete Time) Markov Chains are the simplest formalisms describing stochastic systems. While some verification questions (namely PCTL* ones) are well-understood with very efficient algorithms, there are questions which are very fundamental and yet for which we dont have a clear undestanding of the most efficient solution. In this talk, we start from a simple biological system (a population of yeasts) modeled as a Markov Chain. We will visit several verification questions about this system, as well as the state of the art algorithmic results we have to solve them.
This is a joint work with: Manindra Agrawal, S Akshay, Nathalie Bertrand, Hugo Gimbert, Bruno Karelovic, P.S. Thiagarajan, and Nikhil Vyas.
- Holger Hermanns: Markov Automata - The State of Affairs (slides)
Abstract: Markov Automata have been coined as a compositional continuous-time formalism for stochastic timed systems back in 2010. Initiallly, research on this model was dominated by foundational semantic questions, but over the years techniques and tools have been assembled to perform model construction, model simplification, and model checking of Markov automata, possibly extended with costs, rewards, or parameters.
After reviewing the basic motivation for the interest in this model, the talk provides an overview of the state of affairs in Markov automata modelling, analysis, and application. We close with presenting a collection of challenging open problems.
- Joost-Pieter Katoen: Probabilistic Programming is Intricate (slides)
Abstract: Probabilistic programs are used in different application areas, ranging from machine learning to security and quantum computing. In this talk, I'll discuss semantic issues of probabilistic programming languages and present several nuances of termination: whereas ordinary program termination is about whether a program has an infinite run or not, the termination of probabilistic programs is much more delicate. I'll show that almost-sure termination is "more undecidable" than ordinary termination, and I will argue that whether a program almost surely terminates in a finite expected amount of time is the most interesting notion of termination, and even "more undecidable". Finally, I'll show how to establish the expected run-time of a program --- and thus whether this is finite or not --- using weakest precondition calculus.
- Pushmeet Kohli: Where Machine Learning meets Quantitative Verification
- Jan Kretinsky: Learning to use learning in verification (slides)
Abstract: Recently, a considerable effort has been spent on employing machine learning techniques in diverse areas, including verification. We survey some of the applications, focusing on quantitative verification, e.g., using reinforcement learning for verification of large or complex systems. On the examples we discuss the different approaches to combine verification and machine learning methodologies. We hope to stimulate a discussion about the desiderata for such combinations.
- S N Krishna: Stochastic Timed Games (slides)
Abstract: Stochastic timed games---as introduced by Bouyer and Forejt---are a natural
generalization of the two-player extension of continuous-time Markov chains with
Alur-Dill style clock variables. In their seminal paper, Bouyer and Forejt studied the reachability problem for stochastic timed games and showed that the qualitative reachability problem is decidable for $1\frac{1}{2}$-player one-clock STGs, while the quantitative reachability problem is undecidable for $2\frac{1}{2}$-player three-clock STGs.
In this talk, we explore the horizon of decidability for the qualitative and quantitative reachability problems in stochastic timed games.
- Kim Larsen: Real Time Model Checking, Performance Evaluation, Synthesis and Optimization
Abstract: Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. During the last 20 years the real-time model checker UPPAAL has been developed allowing for efficient verification of hard timing constraints of timed automata. Moreover a number of significant branches exists, e.g. UPPAAL CORA providing efficient support for optimization, UPPAAL TIGA allowing for automatic synthesis of strategies for given safety and liveness objectives, and UPPAAL SMC offering a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata. Most recently the branch UPPAAL STRATEGO has been released supporting synthesis (using machine learning) and evaluation of near-optimal strategies for stochastic priced timed games. The lecture will review the various branches of UPPAAL and indicate their concerted applications to a range of real-time and cyber-physical examples.
- Pavithra Prabhakar: Algorithmic Verification of Stability of Hybrid Systems (slides)
Abstract: Hybrid systems refer to systems exhibiting mixed discrete-continuous behaviors and arise as a natural byproduct of the interaction of a network of embedded processors with physical systems. Stability is a fundamental property in control system design and captures the notion that small perturbations to the initial state or input to the system result in only small variations in the eventual behavior of the system. We present foundations and practical methods for approximation based analysis of stability including quantitative versions of predicate abstraction and counter-example guided abstraction refinement that are based on finite state abstractions, as well as novel hybridization techniques that construct infinite state hybrid system abstractions. In contrast to the well-known methods for automated verification of stability based on Lyapunov functions, which are deductive, we present algorithmic techniques for stability analysis.
- Sriram Rajamani: Probabilistic Programming
Abstract: Recent years have seen a huge shift in the kind of programs that most programmers write. Programs are increasingly data driven instead of being algorithm driven. They use various forms of machine learning techniques to build models from data, for the purpose of decision making. Indeed, search engines, social networks, speech recognition, computer vision, and applications that use data from clinical trials, biological experiments, and sensors, are all examples of data driven programs. We use the term "probabilistic programs" to refer to data driven programs that are written using higher-level abstractions. Though they span various application domains, all data driven programs have to deal with uncertainty in the data, and face similar issues in design, debugging, optimization and deployment. In this talk, we describe connections this research area called "Probabilistic Programming" has with programming languages and software engineering β this includes language design, static and dynamic analysis of programs, and program synthesis. We survey current state of the art and speculate on promising directions for future research.
- Mahesh Viswanathan: Translating LTL to Probabilistic Automata (slides)
Abstract: Starting with the seminal work of Sistla, Vardi, and Wolper (1985), there has been a lot of interest in discovering efficient translations of Linear Temporal Logic (LTL) formulae into small automata. The reason for this is that logic to automata translations directly impact the complexity of runtime monitoring, verification, and synthesis of systems. While much of the work has focused on translations from LTL to nondeterministic and deterministic automata, in this talk we will present new constructions of probabilistic automata for LTL. We will discuss the consequences of this translation to the asymptotic complexity of problems in monitoring and verification of stochastic systems.
Joint work with Dileep Kini.
- Igor Walukiewicz: Reachability problem in timed automata: abstractions, bounds, and search order (slides)
Abstract: The reachability problem for timed automata is probably the most basic
and the most studied problem for this model. We consider zone-based algorithms with explicit state representation. In forward reachability algorithms, zone abstractions are crucial not only to guarantee termination but also for efficiency. Zone based algorithms are also sensitive to order of exploration, experience showing that BFS often gives better results than DFS.
In this talk we will see three recent proposals for improving efficiency of zone based algorithms. We will present efficient methods for using non-convex abstractions, for inferring better clock bounds, and for improving the search order.
PhD student talks
- Ratul Saha: Quantitative analysis of distributed probabilistic systems (slides)
Abstract: We would discuss about a class of communicating probabilistic agents which can be viewed as a succinct and distributed presentation of a large global Markov chain. The model incorporates the interplay among concurrency and stochasticity within reasonable assumptions to perform efficient analysis. In this talk we will give a brief overview of the model and the relevant quantitative reachability analysis, and discuss at length about application domains such as business processes and cloud computing.
- Khushraj Madnani: Metric Temporal Logic with Counting (slides)
Abstract: Ability to count number of occurrences of events within a specified time interval is very useful in specification of resource bounded real time computation. In this paper, we study an extension of Metric Temporal Logic (π¬π³π«) with two different counting modalities called π’ and π΄π³ (until with threshold), which enhance the expressive power of π¬π³π« in orthogonal fashion. We confine ourselves only to the future fragment of π¬π³π« interpreted in a pointwise manner over finite timed words. We provide a comprehensive study of the expressive power of logic π’π³π¬π³π« and its fragments using the technique of EF games extended with suitable counting moves. Finally, as our main result, we establish the decidability of π’π³π¬π³π« by giving an equisatisfiable reduction from π’π³π¬π³π« to π¬π³π«. The reduction provides one more example of the use of temporal projections with oversampling introduced earlier for proving decidability. Our reduction also implies that π¬π¨π³π« extended with π’ and π΄π³ modalities is elementarily decidable.
- Amit Gurung: XSpeed: A Tool for Parallel Reachability Analysis of Continuous Systems on Multi-core Processors (slides)
Abstract: We present a tool XSpeed, a parallel state-space exploration algorithm for continuous systems with linear dynam- ics and nondeterministic inputs. We have exploited the computational power of multicore processors to speed-up the reachability analysis. We have presented two variants of parallelization. In our first approach, we propose a parallel implementation of the support function (SF) algorithm by sampling the SFs in parallel. Secondly, we propose a parallel state-space exploration by slicing the time horizon and computing the reachable states in the time slices in parallel. The second method can be however applied only to a class of linear systems with invertible dynamics and fixed input set. We have also embedded a GPU implementation in XSpeed, presenting a lazy evaluation strategy on SFs. We evaluated the performance on two benchmarks models, a five dimensional linear continuous system and a 28 dimensional Helicopter controller model. Comparison with the sequential counterpart shows a maximum speed-up of almost 7Γ on a 6 core, 12 thread Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up of 12Γ over the sequential implementation and 53Γ over SpaceEx (LGG scenario), the state of the art tool for reachability analysis of linear hybrid systems. Experimental results shows that our parallel algorithm with time slicing not only speeds-up performance but also improves precision.
- Prakash Saivasan: Acceleration in Multi-Pushdown Systems (slides)
Abstract: Model checking of concurrent recursive programs is an interesting and a hard problem. Multi pushdown systems (MPDS) naturally model such programs . However without any restriction, this model is turing powerful. One well known technique used in verification of infinite state systems is that of loop acceleration. The idea is to consider loop of transitions (finite sequence of transitions leading from a control state back to same control state ) and determine the effect of iterating such a loop on finite representations of configurations of a system. We will in this talk study the effect of iterating loops on different representations of configurations of MPDS.