Social networks can be formally modeled to take advantage of distributed systems and concurrency results, while still holding empirical validity and relevance towards social issues. In this talk, an asynchronous model of opinion will be introduced, where social consensus and fairness properties play a key role. This presentation will be based on a CONCUR 2024 …continue reading

Decision diagrams form a cornerstone of many model checkers, but understanding the information they contain can be difficult. In this talk we introduce our new visualization tool developed to tackle this problem. The purpose and capabilities of this tool are presented by exploring a simple use-case in circuit verification.

Labelled transition systems can be a great way to visualize the complex behavior of parallel and communicating systems. However, if, during a particular timeframe, no synchronization or communication between processes occurs, then multiple parallel sequences of actions can interleave arbitrarily, and the resulting LTS quickly becomes too complex for the human eye to understand easily. …continue reading

According to my gut feeling the last algorithm for branching bisimulation on labelled transition systems is too complicated and should be simplified. This talk will present a new algorithm that — although definitely simpler — is still quite complex. The gut feeling also told me that memory use and speed should both be better in …continue reading

A business process is defined as a set of tasks executed in a certain order to achieve a specific goal. BPMN has become the standard modelling language for describing and developing business processes. One of the main challenges in the business process management area is to provide techniques and tools for analyzing processes, which is …continue reading

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