Events at MetaForum MF 6.131

The toolset heavily relies on boolean equation systems, which are the workhorse to solve modal formulas. Boolean equation systems only permit truth values as solutions for variables. It would be nice to also extract quantitative information using modal formulas, such as probabilities, durations, or yields. For this purpose it would be nice to have real …continue reading

This thesis studies divergence and the extra complexity it adds to branching bisimilarity and axiomatizations with respect to branching bisimilarity. Aceto et al. provided sound and complete axiomatization with respect to rooted branching bisimilarity over basic CCS with the prefix iteration operator. Additionally, Spaninks, and Liu and Yu proposed sound and complete axiomatizations with respect …continue reading

Concise process models in mCRL2 can be obtained by the use of data types such as lists and structured sorts. However, the addition of structure in the process parameters negatively affects static analysis tools such as constant elimination, parameter elimination and sum elimination which consider process parameters as single units in their analysis. To address …continue reading

Image analysis using spatial model checking is a relatively recent approach that has promising applications in the medical field. We investigated whether it is possible to verify spatial proper- ties using the mCRL2 toolset, which was built to verify concurrent systems and protocols. This was achieved by translating Spatial Logic for Closure Spaces (SLCS) formulae …continue reading

The Unified Modeling Language (UML), proposed by the Object Management Group (OMG), is a general purpose modeling language which became the standard for modeling system’ structure and behaviour. A UML model offers different views of the system in the form of various diagrams. The talk’s focus are UML State Machine Diagrams, widely used to specify …continue reading

In an ongoing project on the complete axiomatization of branching probabilistic bisimulation, we are currently focusing on a cancellation property. We see a route of proving the property by means of topological arguments which seems a bit far-fetched. As a possible alternative approach we propose the notion of a stable process. A process is stable …continue reading