Olav Bunte: Dynamic systems of communicating OIL components


Event Details


In the previous presentation, I showed how we can model asynchronously communicating OIL components in mCRL2. Since then, we have added a “new” operator in OIL which enables users to create new instances of components dynamically. I show how we model the addition of this operator in mCRL2, which required significant changes. Also, I show how the notion of confluence can help with reducing the time to generate the state space in our context.