Events at MF 6.132

–

In the MACHINAIDE project we verify Cordis models by means of mCRL2. Cordis models are UML-like models developed, tested and simulated in the Cordis SUITE. In this presentation I will take you along on our journey towards verification of Cordis models in three parts: Description of the structure and semantics of Cordis models Peculiarities in the …continue reading

–

It is a natural question to find a DFA or NFA for which a given set of words should be accepted and another given set should not be accepted. In this presentation we investigate how to find a smallest automaton for both types by means of SMT solving, and compare the results.

–

In my previous talk I described the unfolding of process parameters in mCRL2, as it is done by lpsparunfold. This technique requires extending data specifications with new operations and equations. As part of the correctness, we need to reason about properties of the data specification. Working on these proofs triggered questions about the mCRL2 data …continue reading

–

In this talk we will consider deterministic finite automata(DFAs) with a singleton as alphabet. These rather restrictive machines have a strong connection with a very specific field of word combinatorics. In particular we will show how the periodicity of the bouncing DVD logo[1](or a billiard ball) is related to these automata and generate so-called Fibonacci words. …continue reading

–

During our work on the asynchronous communication of OIL components, we started to wonder what the impact would be of changing the communication model. In this presentation I will present our current findings. I will shortly explain related work from Engels, Mauw and Reniers on the hierarchy of communication models that served as the basis …continue reading

–

We present a way to implement term rewriting on a GPU. We do this by letting the GPU repeatedly perform a massively parallel evaluation of all subterms. We experimentally compared inner-most term rewriting with a relaxed form of inner-most rewriting, and designed and experimented with two different garbage collection mechanisms, to remove terms that are …continue reading

–

A key challenge in the synthesis and subsequent analysis of supervisory controllers is the impact of state-space explosion caused by concurrency. The main bottleneck is often the memory needed to store the composition of plant and requirement automata and the resulting supervisor. Partial-order reduction (POR) is a well-established technique that alleviates this issue in the …continue reading

–

In a previous talk I presented an efficient pattern matching algorithm based on the notion of set automaton. This matching algorithm can be exploited to implement efficient term rewriting procedures. These procedures interleave pattern matching steps and rewriting steps, and thus smoothly integrate redex discovery and subterm replacement. In particular this method is suitable to …continue reading