Abstract µCRL [13] is a language for specifying and verifying distributed systems in an
algebraic fashion. It targets the specification of system behaviour in a process-algebraic …

A distributed system is driven by separate components that are executed in parallel, and
protocols for such systems form a major aspect of system design in today's world of wireless …

We present a modular method for on-the-fly state space reduction. The theoretical
foundation of the method is a new confluence notion for labeled transition systems. The …

Markov automata are a novel formalism for specifying systems exhibiting nondeterminism,
probabilistic choices and Markovian rates. Recently, the process algebra MAPA was …

This paper demonstrates the modeling and deductive verification of out-of-order
microprocessors of varying complexities using a logic of Counter Arithmetic with Lambda …

We present a probabilistic leader election algorithm for anonymous, bidirectional,
asynchronous rings. It is based on an algorithm from Franklin 22, augmented with random …

The formal methods approach to develop reliable and efficient safety-or performance-critical
systems is to construct mathematically precise models of such systems on which properties …

Abstract τ-confluence is a reduction technique used in enumerative model-checking of
labeled transition systems to avoid the state explosion problem. In this paper, we propose a …

This paper presents a novel technique for state space reduction of probabilistic
specifications, based on a newly developed notion of confluence for probabilistic automata …

Quantitative model checking is concerned with the verification of both quantitative and
qualitative properties over models incorporating quantitative information. Increases in …