AuDaLa is a recently introduced programming language that follows the new data autonomous paradigm. In this paradigm, small pieces of data execute functions autonomously. Considering the paradigm and the design choices of AuDaLa, it is interesting to determine the expressivity of the language. In this paper, we implement Turing machines in AuDaLa and prove that implementation correct. This proves that AuDaLa is Turing complete, giving an initial indication of AuDaLa's expressivity. Additionally, we give examples of how to add extensions to AuDaLa to increase its practical expressivity and to better match conventional parallel languages, allowing for a more straightforward and performant implementation of algorithms.

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 AuDaLais 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.

When describing the behavior of systems, state variables are typically modeled using complex data types. This use of data types allows for concise models that are easy to read. However, model checking tools that aim to automatically establish the correctness of such models use static analyses of state variables to improve their performance. Therefore, the use of complex data types in behavioral models negatively affects the performance of model checking tools. To address this, in this article we revisit a technique by Groote and Lisser that can be used to replace a single state variable of a complex data type by multiple state variables of simpler data types. We introduce and study several extensions in the context of the process algebraic specification language mCRL2, and establish their correctness. We demonstrate that our technique typically reduces the verification times when using symbolic model checking, and show that sometimes it enables static analysis to reduce the underlying state space from infinite to finite.

We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices.

Abstract Automata learning is a technique to infer an automaton model of a black-box system via queries to the system. In recent years it has found widespread use both in industry and academia, as it enables formal verification when no model is available or it is too complex to create one manually. In this paper we consider the problem of learning the individual components of a black-box synchronous system, assuming we can only query the whole system. We introduce a compositional learning approach in which several learners cooperate, each aiming to learn one of the components. Our experiments show that, in many cases, our approach requires significantly fewer queries than a widely-used non-compositional algorithm such as $$\mathtt {L^*}$$ L ∗ .

Abstract This special issue contains six revised and extended versions of tool papers that appeared in the proceedings of TACAS 2021, the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. The issue is dedicated to the realization of algorithms in tools and the studies of the application of these tools for analysing hard- and software systems.

Abstract In model checking, reduction techniques can be helpful tools to fight the state-space explosion problem. Partial-order reduction (POR) is a well-known example, and many POR variants have been developed over the years. However, none of these can be used in the context of model checking stutter-sensitive temporal properties. We propose POR techniques for parity games, a well-established formalism for solving a variety of decision problems, including model checking. As a result, we obtain the first POR method that is sound for the full modal $$\upmu $$ μ -calculus. We show how our technique can be applied to the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments with our implementation indicate that substantial reductions can be achieved.

One of the most popular state-space reduction techniques for model checking is partial-order reduction (POR). Of the many different POR implementations, stubborn sets are a very versatile variant and have thus seen many different applications over the past 32 years. One of the early stubborn sets works shows how the basic conditions for reduction can be augmented to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a stronger reduction condition and provide extensive new correctness proofs to ensure the issue is resolved. Furthermore, we analyse in which formalisms the problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory.

Abstract In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is sufficient to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a solution together with an updated correctness proof. Furthermore, we analyse in which formalisms this problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory.

Abstract Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal $$\mu $$ -calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.

Reasoning about the correctness of parallel and distributed systems requires automated tools. By now, the mCRL2 toolset and language have been developed over a course of more than fifteen years. In this paper, we report on the progress and advancements over the past six years. Firstly, the mCRL2 language has been extended to support the modelling of probabilistic behaviour. Furthermore, the usability has been improved with the addition of refinement checking, counterexample generation and a user-friendly GUI. Finally, several performance improvements have been made in the treatment of behavioural equivalences. Besides the changes to the toolset itself, we cover recent applications of mCRL2 in software product line engineering and the use of domain specific languages (DSLs).