arXiv subjects

Erik P. de Vink

Publications and source records attributed to Erik P. de Vink.

8 recordsLinked to original sources

arXiv2026

A Comprehensive History of $μ$CRL and mCRL2

This article gives a historical overview of the background, motivation and development of μCRL and its successor mCRL2, from the inception to the present. Both mCRL2 and μCRL are similar, compact, but very expressive formalisms based on process algebra, term rewriting, and the modal mu-calculus. They are developed to model and analyse the behaviour of interacting systems, i.e., systems that communicate by exchange of messages, among each other and with the outside world. Every contemporary computer system can be viewed as such an interacting system and their communication schemes are difficult to design correctly. By sticking to the mathematical foundations, but being led by the desire to be practically relevant, the formalism has grown to become very versatile. In particular, mCRL2 does not only foster the development of theory and the formulation of correctness proofs, but it is also the basis of a large set of automatic tools that help to provide insight in the behaviour of complex computer controlled systems.

cs.LO↗

arXiv2026

Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity

Spatial models are of increasing interest in traditional computer science domains and beyond. Spatial minimisation procedures are crucial for efficient model checking of such models that are often large in size. For the recent notion of spatial bisimilarity for quasi-discrete closure models, called `Compatible Paths' (CoPa) bisimilarity, an effective minimisation method is proposed, and shown to be correct. Reasoning about space represented by quasi-discrete closure models involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality, representing the fact that a point can be reached from another point, under certain conditions. The core of our minimisation method is the encoding of closure models as labelled transition systems, enabling minimisation algorithms for branching bisimilarity to compute CoPa equivalence classes. A prototype toolchain, VoxMinX, is proposed to validate the minimisation method. VoxMinX preserves the relationship between equivalence classes and sets of pixels in the original image. Experimental validation of the toolchain via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size.

cs.LO↗

arXiv2026

Weak Simplicial Bisimilarity and Minimisation for Polyhedral Model Checking

The work described in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking on polyhedral models using the logical language SLCS$η$, a weaker version of SLCS. In this work we show that the mapping from polyhedral models to cell poset models preserves and reflects SLCS$η$. We also propose weak simplicial bisimilarity on polyhedral models and weak $\pm$-bisimilarity on cell poset models, where by ``weak'' we mean that the relevant equivalence is coarser than the corresponding one for SLCS, leading to a greater reduction of the size of models and thus to more efficient model checking. We show that the proposed bisimilarities enjoy the Hennessy-Milner property, i.e. two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS$η$. Similarly, two cells are weakly $\pm$-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS$η$. Furthermore we present a model minimisation procedure and prove that it correctly computes the minimal model with respect to weak $\pm$-bisimilarity, i.e. with respect to logical equivalence of SLCS$η$. The procedure works via an encoding into LTSs and then exploits branching bisimilarity on those LTSs, exploiting the minimisation capabilities as included in the mCRL2 toolset. Various examples show the effectiveness of the approach.

cs.LO↗

arXiv2025

On Bisimilarity for Quasi-discrete Closure Spaces

Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of neighborhood akin to that of topological spaces that build on open sets. For closure models and quasi-discrete closure models, in this paper we present three notions of bisimilarity that are logically characterised by corresponding modal logics with spatial modalities: (i) CM-bisimilarity for closure models (CMs) is shown to generalise topo-bisimilarity for topological models and to be an instantiation of neighbourhood bisimilarity, when CMs are seen as (augmented) neighbourhood models. CM-bisimilarity corresponds to equivalence with respect to the infinitary modal logic IML that includes the modality ${\cal N}$ for ``being near to''. (ii) CMC-bisimilarity, with `CMC' standing for CM-bisimilarity with converse, refines CM-bisimilarity for quasi-discrete closure spaces, carriers of quasi-discrete closure models. Quasi-discrete closure models come equipped with two closure operators, Direct ${\cal C}$ and Converse ${\cal C}$, stemming from the binary relation underlying closure and its converse. CMC-bisimilarity, is captured by the infinitary modal logic IMLC including two modalities, Direct ${\cal N}$ and Converse ${\cal N}$, corresponding to the two closure operators. (iii) CoPa-bisimilarity on quasi-discrete closure models, which is weaker than CMC-bisimilarity, is based on the notion of compatible paths. The logical counterpart of CoPa-bisimilarity is the infinitary modal logic ICRL with modalities Direct $ζ$ and Converse $ζ$, whose semantics relies on forward and backward paths, respectively. It is shown that CoPa-bisimilarity for quasi-discrete closure models relates to divergence-blind stuttering equivalence for Kripke models.

cs.LO↗

arXiv2024

Weak Simplicial Bisimilarity for Polyhedral Models and SLCS_eta -- Extended Version

In the context of spatial logics and spatial model checking for polyhedral models -- mathematical basis for visualisations in continuous space -- we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of $\pm$-bisimilarity on cell-poset models, a discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their repesentations are weakly $\pm$-bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral models, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCS_eta, a weaker version of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS_eta. Similarly, two cells are weakly $\pm$-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS_eta. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS.

cs.LO↗

arXiv2016

Towards a Feature mu-Calculus Targeting SPL Verification

The modal mu-calculus mu-L is a well-known fixpoint logic to express and model check properties interpreted over labeled transition systems. In this paper, we propose two variants of the mu-calculus, mu-Lf and mu-Lf', for feature transition systems. For this, we explicitly incorporate feature expressions into the logics, allowing operators to select transitions and behavior restricted to specific products and subfamilies. We provide semantics for mu-Lf and mu-Lf' and relate the two new mu-calculi and mu-L to each other. Next, we focus on the analysis of SPL behavior and show how our formalism can be applied for product-based verification with mu-Lf as well as family-based verification with mu-Lf'. We illustrate by means of a toy example how properties can be model checked, exploiting an embedding of mu-Lf' into the mu-calculus with data.

cs.LO↗

arXiv2015

Rooted branching bisimulation as a congruence for probabilistic transition systems

We propose a probabilistic transition system specification format, referred to as probabilistic RBB safe, for which rooted branching bisimulation is a congruence. The congruence theorem is based on the approach of Fokkink for the qualitative case. For this to work, the theory of transition system specifications in the setting of labeled transition systems needs to be extended to deal with probability distributions, both syntactically and semantically. We provide a scheduler-free characterization of probabilistic branching bisimulation as adapted from work of Andova et al. for the alternating model. Counter examples are given to justify the various conditions required by the format.

cs.LO↗

arXiv2015

Coherent branching feature bisimulation

Progress in the behavioral analysis of software product lines at the family level benefits from further development of the underlying semantical theory. Here, we propose a behavioral equivalence for feature transition systems (FTS) generalizing branching bisimulation for labeled transition systems (LTS). We prove that branching feature bisimulation for an FTS of a family of products coincides with branching bisimulation for the LTS projection of each the individual products. For a restricted notion of coherent branching feature bisimulation we furthermore present a minimization algorithm and show its correctness. Although the minimization problem for coherent branching feature bisimulation is shown to be intractable, application of the algorithm in the setting of a small case study results in a significant speed-up of model checking of behavioral properties.

cs.LO↗