arXiv subjects

Jan Friso Groote

Publications and source records attributed to Jan Friso Groote.

At least 19 recordsLinked to original sources

arXiv2026

A Comprehensive History of $\mu$CRL and mCRL2

This article gives a historical overview of the background, motivation and development of {\mu}CRL and its successor mCRL2, from the inception to the present. Both mCRL2 and {\mu}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↗

arXiv2025

A formal specification of the desired software behaviour of the Princess Marijke lock complex

The Princess Marijke lock complex is a large lock and water-protection installation in the Netherlands between the river Rhine and the Amsterdam-Rijnkanaal -- a large waterway connecting the Rhine to the port of Amsterdam. The lock complex consists of two independent locks and a moveable flood-protection barrier. Ensuring safe control of the lock complex is of utmost importance to guarantee both flood-protection and reliable ship operations. This paper gives a precise, formal description of the software control of the lock complex in less than 400 lines of mCRL2 code. This description can act as a blueprint on how the software of this lock complex needs to be constructed. Moreover, using model checking, 53 software requirements are shown to be valid, ensuring that the formal description of the behaviour is correct with regard to these properties and is unlikely to contain mistakes and oversights.

eess.SY↗

arXiv2025

The Autonomous Data Language -- Concepts, Design and Formal Verification

Nowadays, the main advances in computational power are due to parallelism. However, most parallel languages have been designed with a focus on processors and threads. This makes dealing with data and memory in programs hard, which distances the implementation from its original algorithm. We propose a new paradigm for parallel programming, the data-autonomous paradigm, where computation is performed by autonomous data elements. Programs in this paradigm are focused on making the data collaborate in a highly parallel fashion. We furthermore present AuDaLa, the first data autonomous programming language, and provide a full formalisation that includes a type system and operational semantics. Programming in AuDaLa is very natural, as illustrated by examples, albeit in a style very different from sequential and contemporary parallel programming. Additionally, it lends itself for the formal verification of parallel programs, which we demonstrate.

cs.PL↗

arXiv2025

A Complete Formal Specification and Verification of the BESW software control system of the Maeslant Storm Surge Barrier

The Maeslant Barrier is a storm surge barrier that protects Rotterdam and its harbour from storm surges in the North Sea. Its software control consists of three major components, one of which is BesW. BesW is responsible for all the movements of the barrier except for pushing and pulling it. In this document, we report on the complete formal specification of BesW in mCRL2. All its behaviour has been specified, including manual and testing modes. Furthermore, all fault situations have been taken into account. The formalisation allows formal verification of all behavioural properties, formulated in the modal $\mu$-calculus, with the constraints that water levels only have a restricted number of values and not all combinations of failures of pumps and valves are allowed.

cs.LO↗

arXiv2025

A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice

This paper proposes a notion of branching bisimilarity for non-deterministic probabilistic processes. In order to characterize the corresponding notion of rooted branching probabilistic bisimilarity, an equational theory is proposed for a basic, recursion-free process language with non-deterministic as well as probabilistic choice. The proof of completeness of the axiomatization builds on the completeness of strong probabilistic bisimilarity on the one hand and on the notion of a concrete process, i.e. a process that does not display (partially) inert $\tau$-moves, on the other hand. The approach is first presented for the non-deterministic fragment of the calculus and next generalized to incorporate probabilistic choice, too.

cs.LO↗

arXiv2024

A Quadratic Lower Bound for Simulation

We show that deciding simulation equivalence and simulation preorder have quadratic lower bounds assuming that the Strong Exponential Time Hypothesis holds. This is in line with the best know quadratic upper bounds of simulation equivalence. This means that deciding simulation is inherently quadratic. A typical consequence of this result is that computing simulation equivalence is fundamentally harder than bisimilarity.

cs.LO↗

arXiv2024

On Woolhouse's Cotton-Spinning Problem

In 1864 W.S.B. Woolhouse formulated the Cotton-Spinning problem. This problem boils down to the following. A piecer works at a spinning mule and walks back and forth to repair broken threads. The question is how far the piecer is expected to walk when the threads break at random. This problem can neatly be solved using process modelling and quantitative model checking, showing that Woolhouse's model led to an overestimation of the walking distance.

cs.LO↗

arXiv2024

Formal Modelling and Analysis of Slot Machines

Slot machines can have fairly complex behaviour. Determining the RTP (return to player) can be involved, especially when a player has an influence on the course of the game. In this paper we model the behaviour of slot machines using probabilistic process specifications where the intervention of players is modelled using non-determinism. The RTP is formulated as a quantitative modal formula which can be evaluated fully automatically on the behavioural specifications of these slot machines. We apply the method on an actual slot machine provided by the company Errèl Industries B.V. The most useful contribution of this paper is that we show how to describe the behaviour of slot machines both concisely and unequivocally. Using quantitative modal logics there is an extra bonus, as we can quite easily provide valuable insights by a.o. computing the exact RTP and obtaining the optimal player strategies.

cs.LO↗

arXiv2024

Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment

Rijkswaterstaat, the National Dutch body responsible for infrastructure, recognised the importance of formal modelling and set up a program to model the control of road tunnels. This is done to improve the standardisation of tunnel control and make communication with suppliers smoother. A subset of SysML is used to formulate the models, which are substantial. In an earlier paper we have shown that these models can be used to prove behavioural properties by manually translating the models to mCRL2. In this paper we report on an automatic translation to mCRL2. As the results of the translation became unwieldy, we also investigated modelling tunnel control in the specification language Dezyne which has built-in verification capabilities and compared the results.

cs.LO↗

arXiv2023

Tool interoperability for model-based systems engineering

Supervisory control design of cyber-physical systems has many challenges. Model-based systems engineering can address these, with solutions originating from various disciplines. We discuss several tools, each state-of-the-art in its own discipline, offering functionality such as specification, synthesis, and verification. Integrating such mono-disciplinary tools in a multi-disciplinary workflow is a major challenge. We present Analytics as a Service, built on the Arrowhead framework, to connect these tools and make them interoperable. A seamless integration of the tools has been established through a service-oriented architecture: The engineer can easily access the functionality of the tools from a single interface, as translation steps between equivalent models for the respective tools are automated.

cs.SE↗

arXiv2023

A Cancellation Law for Probabilistic Processes

We show a cancellation property for probabilistic choice. If distributions mu + rho and nu + rho are branching probabilistic bisimilar, then distributions mu and nu are also branching probabilistic bisimilar. We do this in the setting of a basic process language involving non-deterministic and probabilistic choice and define branching probabilistic bisimilarity on distributions. Despite the fact that the cancellation property is very elegant and concise, we failed to provide a short and natural combinatorial proof. Instead we provide a proof using metric topology. Our major lemma is that every distribution can be unfolded into an equivalent stable distribution, where the topological arguments are required to deal with uncountable branching.

cs.LO↗

arXiv2023

Real Equation Systems with Alternating Fixed-points (full version with proofs)

We introduce the notion of a Real Equation System (RES), which lifts Boolean Equation Systems (BESs) to the domain of extended real numbers. Our RESs allow arbitrary nesting of least and greatest fixed-point operators. We show that each RES can be rewritten into an equivalent RES in normal form. These normal forms provide the basis for a complete procedure to solve RESs. This employs the elimination of the fixed-point variable at the left side of an equation from its right-hand side, combined with a technique often referred to as Gauß-elimination. We illustrate how this framework can be used to verify quantitative modal formulas with alternating fixed-point operators interpreted over probabilistic labelled transition systems.

cs.LO↗

arXiv2023

Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable

We study the problem of computing minimal distinguishing formulas for non-bisimilar states in finite LTSs. We show that this is NP-hard if the size of the formula must be minimal. Similarly, the existence of a short distinguishing trace is NP-complete. However, we can provide polynomial algorithms, if minimality is formulated as the minimal number of nested modalities, and it can even be extended by recursively requiring a minimal number of nested negations. A prototype implementation shows that the generated formulas are much smaller than those generated by the method introduced by Cleaveland.

cs.LO↗

arXiv2023

Lowerbounds for Bisimulation by Partition Refinement

We provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is $Ω((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu n)$ and for parallel algorithms this is $Ω(n)$, where $n$ is the number of states and $m$ is the number of transitions. The lowerbounds are obtained by analysing families of deterministic transition systems, ultimately with two actions in the sequential case, and one action for parallel algorithms. For deterministic transition systems with one action, bisimilarity can be decided sequentially with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that this approach is not of help to develop a faster generic algorithm for deciding bisimilarity. For parallel algorithms there is a similar situation where these techniques may be applied, too.

cs.LO↗

arXiv2021

Fair Mutual Exclusion for N Processes (extended version)

Peterson's mutual exclusion algorithm for two processes has been generalized to $N$ processes in various ways. As far as we know, no such generalization is starvation free without making any fairness assumptions. In this paper, we study the generalization of Peterson's algorithm to $N$ processes using a tournament tree. Using the mCRL2 language and toolset we prove that it is not starvation free unless weak fairness assumptions are incorporated. Inspired by the counterexample for starvation freedom, we propose a fair $N$-process generalization of Peterson's algorithm. We use model checking to show that our new algorithm is correct for small $N$. For arbitrary $N$, model checking is infeasible due to the state space explosion problem, and instead, we present a general proof that, for $N \geq 4$, when a process requests access to the critical section, other processes can enter first at most $(N-1)(N-2)$ times.

cs.LO↗

arXiv2021

Infinite Choice and Probability Distributions. An Open Problem: The Real Hotel

We sketch a process algebra with data and probability distributions. This allows to combine two very powerful abstraction mechanisms namely non-deterministic choice and probabilities. However, it is not clear how to define an appropriate semantics for the generalised choice over data in combination with probability density functions. The real hotel is a puzzle that exemplifies the core of the problem.

cs.LO↗

arXiv2021

A Set Automaton to Locate All Pattern Matches in a Term

Term pattern matching is the problem of finding all pattern matches in a subject term, given a set of patterns. Finding efficient algorithms for this problem is an important direction for research [19]. We present a new set automaton solution for the term pattern matching problem that is based on match set derivatives where each function symbol in the subject pattern is visited exactly once. The algorithm allows for various traversal patterns over the subject term and is particularly suited to search the subject term in parallel.

cs.FL↗