Thomas Henzinger: Two Successes, Two Failures, and Two Predictions

Rajeev Alur: Time for Temporal Logic

Tom Henzinger’s early work developed theoretical foundations of real-time temporal logics. One of his first papers, co-authored with me and published at FOCS 1989, was titled “A really temporal logic”. Research on real-time temporal logics remains vibrant even today motivated by applications to robotics and cyber-physical systems and the new opportunities to translate informal requirements to formal specifications. In this talk, I will first reminisce about our joyful and productive collaboration on real-time temporal logics. I will then give an overview of current research in my group which explores why and how temporal logic can be used to specify task requirements in reinforcement learning.

Christel Baier: From classical to non-classical stochastic shortest path problems

The classical stochastic shortest path (SSP) problems asks to find a policy for traversing a weighted stochastic graph until reaching a distinguished goal state that minimizes the expected accumulated weight. The underlying graph model is a finite-state Markov decision process (MDP) with integer weights for its state-action pairs. Prominent results are the existence of optimal memoryless deterministic policies together with linear programming techniques and value and policy iteration to compute such policies and their values. These results rely on the assumption that the minimum under all proper policies that reach the goal state almost surely exists. Early work on the SSP problems goes back to the 1960s-1990s and makes additional assumptions. Complete algorithms that only require the existence of proper policies combine these techniques with a pre-analysis of end components, an elegant graph-theoretic concept for MDPs that has been introduced by de Alfaro in the late 1990s. The talk will start with a summary of these results. The second part of the talk presents more recent results for variants of the classical SSP. The conditional and partial SSP drop the assumption that the goal state must be reached almost surely and ask to minimize the expected accumulated weight under the condition that the goal will be reached (conditional SSP) resp. assign value 0 to all paths that do not reach the goal state (partial SSP). Other variants take into account aspects of risk-awareness, e.g., by studying the conditional value-at-risk or the variance-penalized expected accumulated weight. While the classical SSP problem is solvable in polynomial time, such non-classical SSP problems are computationally much harder. For the general case, the decidability status of such non-classical SSP problems is unknown, but they have been shown to be at least as hard as the Skolem problem (and even as the positivity problem). However, for non-positive weights, the conditional, partial and variance-penalized SSP problem are solvable in exponential time with a PSPACE lower bounds for acyclic MDPs.

Javier Esparza: Back to the Future: A Fresh Look at Linear Temporal Logic

In the late 1970s, Amir Pnueli introduced Linear Temporal Logic (LTL) into computer science as a framework for specifying and verifying concurrent programs. During the 1980s, in collaboration with Zohar Manna and others, he designed a deductive verification framework for LTL, based on a key Normalization Theorem for LTL.

In 1985 Vardi and Wolper introduced an automata-theoretic approach to model checking LTL. Its success took the logical approach of Manna and Pnueli out of the limelight, and “demoted“ LTL to a specification language, a sort of syntax for automata.

In the last years, together with Jan Kretinsky, Salomon Sickert and Ruben Rubio, we have shown that logic techniques, and in particular a new normalization algorithm, help to translate LTL into smaller and better automata for modern applications, like probabilistic verification and automatic program synthesis. The talk will present some highlights of this work.

Edward Lee: Generalizing Logical Execution Time

In the Logical Execution Time (LET) principle, concurrent software components interact deterministically, reading their inputs atomically at the start of a task and producing outputs atomically after a fixed elapsed logical time. In addition to deterministic concurrency, LET programs yield more deterministic timing when they interact with their physical environment through sensors and actuators. This talk shows through a series of examples that the LET principle can be realized flexibly and generalized using the Lingua Franca coordination language.

Joel Ouaknine: What’s Decidable about Discrete Linear Dynamical Systems?

Discrete linear dynamical systems are an important and fundamental class of infinite-state systems and are ubiquitous in mathematics, physics, engineering, and computer science. They play a key role, among others, in the formal analysis and verification of program loops, probabilistic and weighted automata, control systems, etc. In this talk, I will present an overview and survey of the state of the art on the algorithmic analysis of discrete linear dynamical systems, focussing in particular on reachability and model-checking problems.

Shaz Qadeer: A discipline of verified program construction

I have worked on program verification for many years. In this time, I invented many techniques and built a variety of tools, running the gamut from static to dynamic verification. I also had the privilege of doing my work in the setting of the software industry, which allowed me to make credible attempts to convince software engineers to use these tools in their everyday programming. 

Automatic program verification, as broadly understood by the research community, is the goal of analyzing software artifacts automatically with no involvement from the programmer. Over time, my assessment of the theory of program verification and the practice of software construction led me to a devastating conclusion: progress towards automatic program verification, by itself, is unlikely to enable productive deployment of verification methods at scale. This conclusion forced me to consider a different goal—verified program construction.

I will talk about the basis for my conclusion and the difference between verified program construction and program verification. I will illustrate the discipline of verified program construction by discussing a few research efforts whose goals are similar in spirit. Finally, I will talk about Civl, a verifier that could help with the construction of verified concurrent and distributed systems.