|Rayna Dimitrova (CISPA), Invited Talk
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.
|Christoph Ohrem (Universität Münster)
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.
|Jens Oliver Gutsfeld (TU Braunschweig)
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.
|Ernst-Rüdiger Olderog (Universität Oldenburg)
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.
|Lara Stoltenow (Universität Duisburg Essen)
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.
|Lukas Panneke (DLR)
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.
|Paul Hannibal (Universität Oldenburg)
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.
|Tobias Schüler (Universität Siegen)
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.
|Ira Fesefelt (RWTH Aachen)
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.
|Benjamin Bisping (TU Berlin)
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.
|Barbara König (Universität Duisburg Essen), Invited Talk
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.
|Roman Lakenbrink (Universität Münster)
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.
|Nadine Karsten (TU Berlin)
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.
|Lara Bargmann (Universität Oldenburg)
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.
|Jacob Tepe (TU Braunschweig)
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.