Probabilistic Hyperproperties of Markov Decision Processes

Probabilistic temporal logics such as PCTL and PCTL*, which extend branching temporal logics with a probabilistic quantifier, are an established formalism for specifying performance and reliability requirements of concurrent probabilistic systems. They are, however, not capable of expressing many interesting requirements, such as, for example, probabilistic noninterference. More generally, they cannot capture probabilistic hyperproperties, which relate multiple executions of a system. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements, like symmetry, partial observation, robustness, and fault tolerance.
In this talk, I will present a temporal logic for the specification of hyperproperties of Markov decision processes (MDPs), called Probabilistic Hyper Logic (PHL). PHL extends classic probabilistic logics with quantification over schedulers and traces. It can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference and differential privacy, as well as novel applications in areas such as planning. A consequence of the generality of the logic is that the model-checking problem for PHL is undecidable. I will present methods both for proving and for refuting formulas from a fragment of the logic that includes many probabilistic hyperproperties of interest.

Deciding Asynchronous Hyperproperties for Recursive Programs

We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same complexity of the model checking problem for finite state models. Beyond this, we study the model checking problem of our logic for pushdown models. We argue that the combination of asynchronicity and a non-regular model class studied in this paper constitutes the first suitable approach for hyperproperty model checking against recursive programs.

Temporal Team Semantics for Asynchronous Hyperproperties

In this talk, we study a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We present three logics: TeamLTL, TeamCTL and TeamCTL*  which are obtained by adding quantification over so-called time evaluation functions controlling the asynchronous progress of traces. We discuss expressivity, decidability and complexity for these logics and also analyze them using Alternating Asynchronous Büchi Automata (AABA), a subclass of a recently introduced automata model.

Concurrent Hyperproperties

Trace properties, which are sets of execution traces, are often used to analyze systems, but their expressiveness is limited. Clarkson and Schneider defined hyperproperties as a generalization of trace properties to sets of sets of traces. Typical applications of hyperproperties are found in information flow security. We introduce an analogous definition of concurrent hyperproperties, by generalizing traces to concurrent traces, which we define as partially ordered multisets. We take Petri nets as the basic semantic model. Concurrent traces are formalized via causal nets. To check concurrent hyperproperties, we define may and must testing of sets of concurrent traces in the style of DeNicola and Hennessy, using the parallel composition of Petri nets. In our approach, we thus distinguish nondeterministic and concurrent behavior. We discuss examples where concurrent hyperproperties are needed.

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions

We study graph conditions à la Pennemann (essentially first-order logic for graphs, e.g. testing for occurrence of certain subgraphs etc.) and develop an algorithm to check unsatisfiability, or find and output finite models if they exist, or (in some cases) also detect certain types of infinite models. We also generalize these results to certain other categories.

Symbolic Unfoldings of High-level Petri Nets

Unfoldings are a well known partial-order semantics of P/T (low-level) Petri nets that can be applied to various model checking or verification problems. For colored (high-level) Petri nets, the so-called symbolic unfolding generalizes this notion. A finite complete prefix of a P/T Petri net's unfolding contains all information to verify, e.g., reachability of markings. Würdemann et. al. unite these two concepts and define finite complete prefixes of the symbolic unfolding of colored Petri nets. We evaluate this extended algorithm through a prototype implementation on four novel benchmark families. We find that our approach is effective and is applicable for a class of nets where previous unfolding based approaches are cannot be applied.

Petri Games: Synthesis of Distributed Systems with Causal Memory

Petri games are a game model for the synthesis of distributed, reactive systems. The players are represented as tokens on a Petri net and are grouped into system players and environment players. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the entire causal history of the other players. The system players decide on which transitions to take next based on their causal history, which grows infinitely in a Petri net with loops. The synthesis problem for Petri games asks whether there exists a strategy for the system players that satisfies a given safety property against all possible behaviours of the adversarial environment players. The talk will cover recent results, in particular the undecidability of the synthesis problem for 6-player Petri games and a new approach to finding winning strategies with bounded memory.

Concurrent Database Manpulating Processes

Database manipulating systems (DMS) formally specify a labeled transition system whose states denote relational database instances and whose transitions denote actions. Actions evolve those instances due to change operations applied to the current database instance. However, in most recent DMS models, there is no explicit notion of process semantics to control sequencing, conflicts and concurrency of action occurrences such that any action may be applied to an instance whenever it is enabled. Accordingly, those approaches lack a formally founded notion of behavioral equivalence for database manipulating processes. These open issues are particularly challenging due to the delicate properties of the underlying labeled transition system being not only infinite state but also infinitely branching.  In my talk, I tackle this problem by introducing a collection of abstract domains for DMS. Enabling abstract interpretation for DMS. Thereupon, I propose an additional control layer to DMS based on the process algebra ACP. The operational semantics of the calculus enables us to investigate equivalence notions for DMS processes as well as further crucial properties like reachability properties, concurrency, confluence and parallel independence.

Expectation-based Reasoning in Concurrent Probabilistic Programs

Expectation-based reasoning about probabilistic programs has given rise to various new techniques in recent years. On of these allows the reasoning about lower bounds of probabilities for concurrent probabilistic programs. However, these results open the way to two more questions: (1) reasoning about (lower bounds of) expected values instead of probabilities and (2) upper bounds of both probabilities and expected values. In my presentation, I will give ideas how proof systems for each of these problems may look like.  

Concurrency formalisms as computer games

Participants of this session will play and judge small computer games built around the mechanics of well-known formalisms such as MDPs, process calculi, cellular automata, graph rewriting systems, and LTL. The games are a selection of the 26 student games created in our programming lab course at TU Berlin between 2019 and 2023 (https://pr.mtv.tu-berlin.de/). The talk also glances at the course design. The participant vote decides which student games deserve the “D-CON game awards.

Approximating Fixpoints of Approximated Functions

There is a large body of work on fixpoint theorems, guaranteeing the existence of fixpoints for certain functions and providing methods for computing them. This includes for instance Banachs’s fixpoint theorem, the well-known result by Knaster-Tarski that is frequently employed in computer science and Kleene iteration.
It is less clear how to compute fixpoints if the function whose (least) fixpoint we are interested in is not known exactly, but can only be obtained by a sequence of subsequently better approximations. This scenario occurs for instance in the context of reinforcement learning, where the probabilities of a Markov decision process (MDP) - for which one wants to learn a strategy - are unknown and can only be sampled. There are several solutions to this problem where the fixpoint computation (for determining the value vector and the optimal strategy) and the exploration of the model are interleaved. However, these methods work only well for discounted MDPs, that is in the contractive setting, but not for general MDPs, that is for non-expansive functions.
After describing and motivating the problem, we will in particular concentrate on the non-expansive case. There are many interesting systems who value vectors can be obtained by determining the fixpoints of non-expansive functions. Other than contractive functions, they do not guarantee uniqueness of the fixpoint, making it more difficult to approximate the least fixpoint by methods other than Kleene iteration. And also Kleene iteration fails if the function under consideration is only approximated.
We hence describe a dampened Mann iteration scheme for (higher-dimensional) functions on the reals that converges to the least fixpoint from everywhere. This scheme can also be adapted to functions that are approximated, under certain conditions.
We will in particular study the case of MDPs and consider a related problem that arises when performing model-checking for quantitative mu-calculi, which involves the computation of nested fixpoints.

A Navigation Logic for Recursive Programs with Dynamic Thread Creation

Dynamic Pushdown Networks (DPNs) are a model for multithreaded programs with recursion and dynamic creation of threads. In this talk, we propose a temporal logic called Navigation Temporal Logic for reasoning about the call- and return- as well as thread creation behaviour of  DPNs. Using tree automata techniques, we investigate the model checking problem for the novel logic and show that its complexity is not higher than that of LTL model checking against pushdown systems despite a more expressive logic and a more powerful system model. The same holds true for the satisfiability problem when compared to the satisfiability problem for a related logic for reasoning about the call- and return-behaviour of pushdown systems. Overall, this novel logic offers a promising approach for the verification of recursive programs with dynamic thread creation.

Store Locally, Prove Globally

The use of message-passing process calculi for the verification of distributed algorithms requires support for state-based reasoning that goes beyond their traditional action-based  style: knowledge about (local) states is at best provided implicitly. Therefore, we propose a distributed process calculus with locations, the units of distribution, which we equip with explicit state information in the form of memories. On top, we provide  a simple formal model for location failure and failure detection such that we can deal with the verification of fault-tolerant distributed algorithms. We exhibit the use of our calculus by formalizing a simple algorithm to solve Distributed Consensus and prove its correctness. The proof exploits global invariants by direct access to the local memories.

Lifting the Reasoning Level in Generic Weak Memory Verification

Weak memory models specify the semantics of concurrent programs on multi-core architectures. Reasoning techniques for weak memory models are often specialized to one fixed model and verification results are hence not transferable to other memory models. A recent proposal of a generic verification technique based on axioms on program behaviour expressed via weakest preconditions aims at overcoming this specialization to dedicated models. Due to the usage of weakest preconditions, reasoning however takes place on a very low level requiring the application of numerous axioms for deriving program properties, even for a single statement. In this talk, we lift reasoning in this generic verification approach to a more abstract level. Based on a view-based assertion language, we provide a number of novel proof rules for directly reasoning on the level of program constructs. We prove soundness of our proof rules and exemplify them on the write-to-read causality (WRC) litmus test. A comparison to the axiom-based low-level proof reveals a significant reduction in the number of required proof steps.

Making Programs Memory Safe

Safe Memory Reclamation (SMR) algorithms aid in writing fine-grained concurrent data structures in languages with manual memory management, e.g. C and C++. Some famous examples of SMR algorithms are Hazard Pointers (HP) and Epoch-Based Reclamation. However, using these SMR algorithms correctly is not trivial. In HP, for example, before safely accessing a pointer one must issue a protection to said pointer and also check whether the protection was successful. In this talk, we present a synthesis algorithm which correctly synthesizes calls to a given SMR algorithm. The synthesis algorithm has two stages: First, it conducts a proof of realizability using "Realizability Logic". From this proof it extracts a solution to the synthesis problem using "Realization Logic". Both, Realizability and Realization Logic, are novel approaches to solve synthesis problems and are not restricted to the domain of SMR algorithms.