Events at MF 6.132

In the setting of an elementary probabilistic process language we consider branching bisimilarity for distributions. In earlier work its axiomatization included a semantic condition for the probabilistic counterparts of the B-axiom. In this talk we introduce the syntactic notion of probabilistic inclusion. We further discuss how to replace the semantic condition by the requirement of …continue reading

Morphic sequences form a natural class of infinite sequences, most times defined by fixed points of morphisms. They cover well-known examples like the Thue- Morse sequence and the Fibonacci sequence. In this talk we focus on the following three aspects of morphic sequences: 1. Equivalent characterizations of the class of morphic sequences. These include characterizations …continue reading

Abstract by Michel Reniers: We propose a method to show how model checking may be used to verify that a synthesized supervisor indeed is safe (w.r.t. safety requirements used in the synthesis procedure), nonblocking and controllable. To achieve this we propose a method for transforming networks of extended finite automata that interact through shared events, …continue reading

Strong apartness has been proposed as a relation for distinguishing states in a labelled transition system. Prior work has shown that there is a clear connection between Hennessy-Milner logic, strong bisimilarity and strong apartness. In this talk, I discuss the connection between apartness and bisimulation games. In particular, I show that in a bisimulation game, …continue reading

Configurable systems enables customization of features to alter system functionalities. However, feature modifications have the potential to impact security, safety or usability of the configured system. In many cases, configuration spaces tend to be exponential w.r.t. the number of features, hampering detection and explanation of behaviors of interest. Recent works have introduced the notion of …continue reading

The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. We propose a new explicit-state model checking algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae that is aimed at running on such devices. We prove its correctness and termination guarantee, …continue reading

Decision tree classifiers (DTs) provide an effective machine-learning model, well-known for its intuitive interpretability. However, they still miss opportunities well-established in software engineering that could further improve their explainability: separation of concerns, encapsulation, and reuse of behaviors. To enable these concepts, we recently introduced templates in decision diagrams (DDs) as an extension of multi-valued DDs. …continue reading

The Autonomous Data Language (AuDaLa) is a recently introduced programming language and is supported by an operational semantics. I this talk I will present a new operational semantics for AuDaLa with relaxed memory consistency and incoherent memory, with the goal of allowing more compiler optimisations. Under certain conditions, the new semantics are equivalent to the …continue reading

The notion of 𝛼-equivalence between πœ†-terms is used to identify terms that are considered equal modulo renaming bound variables. Using De Bruijn indices we can give a unique representation for closed πœ†-terms modulo 𝛼-equivalence. Equating terms that have the same De Bruijn representation falls short when comparing subterms occurring within a larger context: it may …continue reading