An Overview of the mCRL2 Toolset and its Recent Advances
---
paper_title: Parameterised Boolean Equation Systems

paper_content:

Boolean equation system are a useful tool for verifying formulas from modal μ-calculus on transition systems (see [Mader, Lecture Notes in Computer Science, Vol. 1019, 1995, pp. 72-88] for an excellent treatment). We are interested in an extension of boolean equation systems with data. This allows to formulate and prove a substantially wider range of properties on much larger and even infinite state systems. In previous works [Groote and Mateescu, Lecture Notes in Computer Science, Vol. 1548, 1999, pp. 74-90; Groote and Willemse, Sci. Comput. Program., 2005] it has been outlined how to transform a modal formula and a process, both containing data, to a so-called parameterised boolean equation system, or equation system for short. In this article we focus on techniques to solve such equation systems. We introduce a new equivalence between equation systems, because existing equivalences are not compositional. We present techniques similar to GauB elimination as outlined in [Mader, Lecture Notes in Computer Science, Vol. 1019, 1995, pp. 72-88] that allow to solve each equation system provided a single equation can be solved. We give several techniques for solving single equations, such as approximation (known), patterns (new) and invariants (new). Finally, we provide several small but illustrative examples of verifications of modal μ-calculus formulas on concrete processes to show the use of the techniques.
---
paper_title: Relating levels of the mu-calculus hierarchy and levels of the monadic hierarchy

paper_content:

As is already known from the work of D. Janin & I. Walukiewicz (1996), the mu-calculus is as expressive as the bisimulation-invariant fragment of monadic second-order logic. In this paper, we relate the expressiveness of levels of the fixpoint alternation depth hierarchy of the mu-calculus (the mu-calculus hierarchy) with the expressiveness of the bisimulation-invariant fragment of levels of the monadic quantifiers alternation-depth hierarchy (the monadic hierarchy). From J. van Benthem's (1976) results, we know already that the fixpoint free fragment of the mu-calculus (i.e. polymodal logic) is as expressive as the bisimulation-invariant fragment of monadic /spl Sigma//sub 0/ (i.e. first-order logic). We show that the /spl nu/-level of the mu-calculus hierarchy is as expressive as the bisimulation-invariant fragment of monadic /spl Sigma//sub 1/ and that the /spl nu//spl mu/-level of the mu-calculus hierarchy is as expressive as the bisimulation-invariant fragment of monadic /spl Sigma//sub 2/, and we show that no other level /spl Sigma//sub k/ (for k>2) of the monadic hierarchy can be related similarly with any other level of the mu-calculus hierarchy. The possible inclusion of all the mu-calculus in some level /spl Sigma//sub k/ of the monadic hierarchy, for some k>2, is also discussed.
---
paper_title: Parameterised Boolean Equation Systems

paper_content:

Boolean equation system are a useful tool for verifying formulas from modal μ-calculus on transition systems (see [Mader, Lecture Notes in Computer Science, Vol. 1019, 1995, pp. 72-88] for an excellent treatment). We are interested in an extension of boolean equation systems with data. This allows to formulate and prove a substantially wider range of properties on much larger and even infinite state systems. In previous works [Groote and Mateescu, Lecture Notes in Computer Science, Vol. 1548, 1999, pp. 74-90; Groote and Willemse, Sci. Comput. Program., 2005] it has been outlined how to transform a modal formula and a process, both containing data, to a so-called parameterised boolean equation system, or equation system for short. In this article we focus on techniques to solve such equation systems. We introduce a new equivalence between equation systems, because existing equivalences are not compositional. We present techniques similar to GauB elimination as outlined in [Mader, Lecture Notes in Computer Science, Vol. 1019, 1995, pp. 72-88] that allow to solve each equation system provided a single equation can be solved. We give several techniques for solving single equations, such as approximation (known), patterns (new) and invariants (new). Finally, we provide several small but illustrative examples of verifications of modal μ-calculus formulas on concrete processes to show the use of the techniques.
---
paper_title: Verification of reactive systems via instantiation of Parameterised Boolean Equation Systems

paper_content:

Verification problems for finite- and infinite-state processes, like model checking and equivalence checking, can effectively be encoded in Parameterised Boolean Equation Systems (PBESs). Solving the PBES then solves the encoded problem. The decidability of solving a PBES depends on the data sorts that occur in the PBES. We describe a pragmatic methodology for solving PBESs, viz., by attempting to instantiate them to the sub-fragment of Boolean Equation Systems (BESs). Unlike solving PBESs, solving BESs is a decidable problem. Based on instantiation, verification using PBESs can effectively be done fully automatically in most practical cases. We demonstrate this by solving several complex verification problems using a prototype implementation of our instantiation technique. In addition, practical issues concerning this implementation are addressed. Furthermore, we illustrate the effectiveness of instantiation as a transformation on PBESs when solving verification problems involving systems of infinite size.
---
paper_title: A cure for stuttering parity games

paper_content:

We define governed stuttering bisimulation for parity games, weakening stuttering bisimulation by taking the ownership of vertices into account only when this might lead to observably different games. We show that governed stuttering bisimilarity is an equivalence for parity games and allows for a natural quotienting operation. Moreover, we prove that all pairs of vertices related by governed stuttering bisimilarity are won by the same player in the parity game. Thus, our equivalence can be used as a preprocessing step when solving parity games. Governed stuttering bisimilarity can be decided in $\mathcal{O}(n^2m)$ time for parity games with n vertices and m edges. Our experiments indicate that governed stuttering bisimilarity is mostly competitive with stuttering equivalence on parity games encoding typical verification problems.
---
paper_title: Model-checking processes with data

paper_content:

We propose a procedure for automatically verifying properties (expressed in an extension of the modal µ-calculus) over processes with data, specified in µCRL. We first briefly review existing work, such as the theory of µCRL and we discuss the logic, called first order modal µ-calculus in more detail. Then, we introduce the formalism of first order boolean equation systems and focus on several lemmata that are at the basis of the soundness of our decision procedure. We discuss our findings on three non-trivial applications for a prototype implementation of this procedure. The results show that our prototype can deal with quite complex and interesting properties and systems, showing the efficacy of the approach.
---
paper_title: Linearization in parallel pCRL

paper_content:

Abstract We describe a linearization algorithm for parallel pCRL processes similar to the one implemented in the linearizer of the μCRL Toolset. This algorithm finds its roots in formal language theory: the `grammar' defining a process is transformed into a variant of Greibach Normal Form. Next, any such form is further reduced to linear form , i.e., to an equation that resembles a right-linear, data-parametric grammar. We aim at proving the correctness of this linearization algorithm. To this end we define an equivalence relation on recursive specifications in μCRL that is model independent and does not involve an explicit notion of solution.
---
paper_title: Abstraction in Parameterised Boolean Equation Systems

paper_content:

We present a general theory of abstraction for a variety of verification problems. Our theory is set in the framework of parameterized Boolean equation systems. The power of our abstraction theory is compared to that of generalised Kripke modal transition systems (GTSs). We show that for model checking the modal µ-calculus, our abstractions can be exponentially more succinct than GTSs and our theory is as complete as the GTS framework for abstraction. Furthermore, we investigate the completeness of our theory for verification problems other than the modal µ-calculus. We illustrate the potential of our theory through case studies using the first-order modal µ-calculus and a real-time extension thereof, conducted using a prototype implementation of a new syntactic transformation for equation systems.
---
paper_title: Bridging the Semantic Gap: Visualizing Transition Graphs with User-Defined Diagrams

paper_content:

Analysts of computer-based systems often face large data sets, such as those represented in state transition graphs, in which the organizational structure is clear but interpreting the data is not. This new method lets users generate interactive visualizations that help them analyze systems more easily, accurately, and quickly. Computer scientists and engineers use state transition graphs to model and study the behavior of computer-based systems. These graphs describe sets of system states and sets of transitions. Transitions are source-action-target triples in which the execution of an action triggers a transition from a source to a target state.
---
paper_title: Equivalence checking for infinite systems using parameterized boolean equation systems

paper_content:

In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove correctness, and illustrate the approach with an unbounded queue example. We also provide some adaptations to obtain similar transformations for weak bisimulation and simulation equivalence.
---
paper_title: Modal Abstractions in µCRL

paper_content:

We describe a framework to generate modal abstract approximations from process algebraic specifications, written in the language μCRL. We allow abstraction of state variables and action labels. Moreover, we introduce a new format for process specifications called Modal Linear Process Equation (MLPE). Every transition step may lead to a set of abstract tates labelled with a set of abstract actions. We use MLPEs to characterize abstract interpretations of systems and to generate Modal Labelled Transition Systems, in which transitions may have two modalities may and must. We prove that the abstractions are sound for the full action-based μ-calculus. Finally, we apply the result to check some safety and liveness properties for the bounded retransmission protocol.
---
paper_title: LTSMIN: distributed and symbolic reachability

paper_content:

In model checking, analysis algorithms are applied to large graphs (state spaces), which model the behavior of (computer) systems These models are typically generated from specifications in high-level languages The LTSmin toolset provides means to generate state spaces from high-level specifications, to check safety properties on-the-fly, to store the resulting labelled transition systems (LTSs) in compressed format, and to minimize them with respect to (branching) bisimulation.
---
paper_title: Visualization of state transition graphs

paper_content:

A new method for the visualization of state transition graphs is presented. Visual information is reduced by clustering nodes, forming a tree structure of related clusters. This structure is visualized in three dimensions with concepts from cone trees and emphasis on symmetry. The resulting visualization makes it easier to relate features in the visualization of the state transition graph to semantic concepts in the corresponding process and vice versa.
---
paper_title: Static Analysis Techniques for Parameterised Boolean Equation Systems

paper_content:

Parameterised Boolean Equation Systems (PBESs) can be used to encode and solve various types of model checking and equivalence checking problems. PBESs are typically solved by symbolic approximation or by instantiation to Boolean Equation Systems (BESs). The latter technique suffers from something similar to the state space explosion problem and we propose to tackle it by static analysis techniques, which we tailor for PBESs. We introduce a method to eliminate redundant parameters and a method to detect constant parameters. Both lead to a better performance of the instantiation and they can sometimes even reduce problems that are intractable due to the infinity of the underlying BES to tractable ones.
---
paper_title: Invariants for Parameterised Boolean Equation Systems

paper_content:

The concept of invariance for Parameterised Boolean Equation Systems (PBESs) is studied in greater detail. We identify a weakness with the associated theory and fix this problem by proposing a stronger notion of invariance called global invariance. A precise correspondence is proven between the solution of a PBES and the solution of its invariant-strengthened version; this enables one to exploit global invariants when solving PBESs. Furthermore, we show that global invariants are robust w.r.t. all common PBES transformations and that the existing encodings of verification problems into PBESs preserve the invariants of the processes involved. These traits provide additional support for our notion of global invariants, and, moreover, provide an easy manner for transferring (e.g. automatically discovered) process invariants to PBESs. Several examples are provided that illustrate the advantages of using global invariants in various verification problems.
---
paper_title: Tree automata, mu-calculus and determinacy

paper_content:

It is shown that the propositional mu-calculus is equivalent in expressive power to finite automata on infinite trees. Since complementation is trivial in the mu-calculus, the equivalence provides a radically simplified, alternative proof of M.O. Rabin's (1989) complementation lemma for tree automata, which is the heart of one of the deepest decidability results. It is also shown how mu-calculus can be used to establish determinacy of infinite games used in earlier proofs of complementation lemma, and certain games used in the theory of online algorithms. >
---
paper_title: Bisimulation Minimisations for Boolean Equation Systems

paper_content:

Boolean equation systems (BESs) have been used to encode several complex verification problems, including model checking and equivalence checking. We introduce the concepts of strong bisimulation and idempotence-identifying bisimulation for BESs, and we prove that these can be used for minimising BESs prior to solving these. Our results show that large reductions of the BESs may be obtained efficiently. Minimisation is rewarding for BESs with non-trivial alternations: the time required for solving the original BES mostly exceeds the time required for quotienting plus the time for solving the quotient. Furthermore, we provide a verification example that demonstrates that bisimulation minimisation of a process prior to encoding the verification problem on that process as a BES can be arbitrarily less effective than minimising the BES that encodes the verification problem.
---
paper_title: Reo: A Channel-based Coordination Model for Component Composition

paper_content:

Apparatus for mixing together milk, a fluoride solution and a flavoring solution to produce a pleasant-tasting fluordiated beverage, comprises two sets each of three vessels for containing the respective liquids to be mixed. The volumes of the three vessels are in the proportions in which the liquids are to be mixed and inlet flows from supply tanks of the three liquids are metered to fill the three vessels simultaneously. A common inlet valve shuts off the three supplies simultaneously and operation of the inlet valve automatically opens the outlet and mixing valve. As one set of vessels is filled, the other is emptied to provide a substantially continuous flow of the beverage.
---
paper_title: The Petri Net Markup Language

paper_content:

The Petri Net Markup Language (PNML) is an XML-based interchange format for Petri nets. PNML supports any version of Petri net since new Petri net types can be defined by so-called Petri Net Type Definitions (PNTD).
---
paper_title: Supervisory machine control by predictive-reactive scheduling

paper_content:

A translator comprising a light receiving unit including three kinds of photocells having spectral sensitivities to red, green and blue colors respectively for receiving light from the optical projecting system of an enlarger equipped with color correction filters, arithmetic units for calculating ratios between the outputs of the photocells by taking one of the outputs as denomenators and the other two outputs as numerators respectively, comparison output setting units having their outputs determined only by the conditions of a negative previously memorized for comparison with the outputs from the arithmetic units respectively, and comparison units for comparing the outputs from the arithmetic units with the corresponding comparison outputs individually to indicate the differences therebetween, whereby the amount of color correction given only by the conditions of the negative is adjusted for the enlarger actually used for color printing.
---
paper_title: SMI++ object-oriented framework for designing and implementing distributed control systems

paper_content:

In the SMI++ framework, the real world is viewed as a collection of objects behaving as finite state machines. These objects can represent real entities, such as hardware devices or software tasks, or they can represent abstract subsystems. A special language (SML) is provided for the object description. The SML description is then interpreted by a logic engine (coded in C++) to drive the control system. This allows rule based automation and error recovery. SMI++ objects can run distributed over a variety of platforms, all communication being handled transparently by an underlying communication system - DIM. This framework has been first used by the DELPHI experiment at CERN for the experiment control. BaBar experiment at SLAC has adopted this framework for the design and implementation of their run control system. For this purpose the framework was significantly upgraded. The BaBar run control and the underlying SMI++ framework has been in production since the beginning of 1999. SMI++ has recently been adopted at CERN by all LHC experiments for their detector control systems as recommended by the Joint Controls Project. The main features of the framework and in particular of SML language as well as recent and near future upgrades will be discussed. SMI++ has, so far, been used only by large particle physics experiments. It is, however, equally suitable for any other control applications.
---
paper_title: Higher-level synchronising devices in Meije-SCCS

paper_content:

Abstract In an algebraic setting for parallelism and synchronisation due to R. Milner, we define a wide variety of synchronising operators on processes. We introduce them by the semantical conditional rules they obey. We prove they are higher-level nonprimitive operators from the original SCCS calculus, showing how to meet their behaviours with primitive expressions. Our purposes are: study of expressiveness—either ‘semantic’, in the realm of transition systems, or ‘syntaxic’, through translation of other formalisms in the calculus. Such operators allow one to specify formally sophisticated synchronisation modes dealing with (operational) products and transformations of transition systems, and still not lose their informal appealing intuition; for we then forget the realisation working with Meije -SCCS elementary synchronisation mechanisms (the mechanics below the hood). The defining rules are syntactically given, except for the allowed relations on the components' actions monoids. This ‘semantical’ aspect allows us to treat many ‘calculability’ issues. This is especially true of closed terms, where we may claim constructive ‘universality’ amongst transition systems. The case of operators seems slightly more intricate. The proof of our main result has led us to a technical shaping of equivalence proofs for open expressions which shows to be interesting in its own right.
---
paper_title: Transforming SOS Specifications to Linear Processes

paper_content:

This paper describes an approach to transform Structural Operational Semantics, given as a set of deduction rules, to a Linear Process Specification. The transformation is provided for deduction rules in De Simone format, including predicates. The Linear Process Specifications are specified in the syntax of the mCRL2 language, that, with help of the underlying (higher-order) re-writer/tool-set, can be used for simulation, labeled transition system generation and verification of behavioral properties. We illustrate the technique by showing the effect of the transformation from the Structural Operational Semantics specification of a simple process algebra to a Linear Process Specification.
---
paper_title: Automatic validation of protocol narration

paper_content:

We perform a systematic expansion of protocol narrations into terms of process algebra in order to make precise some of the detailed checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice for identifying a number of authentication flaws in symmetric key protocols such as Needham-Schroeder, Otway-Rees, Yahalom and Andrew Secure RPC.
---
paper_title: Syntax and consistent equation semantics of hybrid Chi

paper_content:

Abstract The hybrid χ (Chi) formalism integrates concepts from dynamics and control theory with concepts from computer science, in particular from process algebra and hybrid automata. It integrates ease of modeling with a straightforward, structured operational semantics. Its ‘consistent equation semantics’ enforces state changes to be consistent with delay predicates, that combine the invariant and flow clauses of hybrid automata. Ease of modeling is ensured by means of the following concepts: (1) different classes of variables: discrete and continuous, of subclass jumping or non-jumping, and algebraic; (2) strong time determinism of alternative composition in combination with delayable guards; (3) integration of urgent and non-urgent actions; (4) differential algebraic equations as a process term as in mathematics; (5) steady-state initialization; and 6) several user-friendly syntactic extensions. Furthermore, the χ formalism incorporates several concepts for complex system specification: (1) process terms for scoping that integrate abstraction, local variables, local channels and local recursion definitions; (2) process definition and instantiation that enable process re-use, encapsulation, hierarchical and/or modular composition of processes; and (3) different interaction mechanisms: handshake synchronization and synchronous communication that allow interaction between processes without sharing variables, and shared variables that enable modular composition of continuous-time or hybrid processes. The syntax and semantics are illustrated using several examples.
---
paper_title: LTSMIN: distributed and symbolic reachability

paper_content:

In model checking, analysis algorithms are applied to large graphs (state spaces), which model the behavior of (computer) systems These models are typically generated from specifications in high-level languages The LTSmin toolset provides means to generate state spaces from high-level specifications, to check safety properties on-the-fly, to store the resulting labelled transition systems (LTSs) in compressed format, and to minimize them with respect to (branching) bisimulation.
---
paper_title: Formalizing a domain specific language using SOS: An industrial case study

paper_content:

This paper describes the process of formalizing an existing, industrial domain specific language (DSL) that is based on the task-resource paradigm. Initially, the semantics of this DSL is defined informally and implicitly through an interpreter. The formalization starts by projecting the existing concrete syntax onto a formal abstract syntax that defines the language operators and process terms. Next, we define the dynamic operational semantics at the level of individual syntactical notions, using structural operational semantics (SOS) as a formal meta-language. Here, the impact of the formalization process on the DSL is considered in terms of disambiguation of underlying (semantic) language design decisions.
---
paper_title: Using model checking to analyze the system behavior of the LHC production grid

paper_content:

DIRAC (Distributed Infrastructure with Remote Agent Control) is the grid solution designed to support production activities as well as user data analysis for the Large Hadron Collider ''beauty'' experiment. It consists of cooperating distributed services and a plethora of light-weight agents delivering the workload to the grid resources. Services accept requests from agents and running jobs, while agents actively fulfill specific goals. Services maintain database back-ends to store dynamic state information of entities such as jobs, queues, or requests for data transfer. Agents continuously check for changes in the service states and react to these accordingly. The logic of each agent is rather simple; the main source of complexity lies in their cooperation. These agents run concurrently and communicate using the services' databases as a shared memory for synchronizing the state transitions. Despite the effort invested in making DIRAC reliable, entities occasionally get into inconsistent states. Tracing and fixing such behaviors is difficult, given the inherent parallelism among the distributed components and the size of the implementation. In this paper we present an analysis of DIRAC with mCRL2, process algebra with data. We have reverse engineered two critical and related DIRAC subsystems, and subsequently modeled their behavior with the mCRL2 toolset. This enabled us to easily locate race conditions and livelocks which were confirmed to occur in the real system. We further formalized and verified several behavioral properties of the two modeled subsystems.
---
paper_title: Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games

paper_content:

Parameterised Boolean Equation Systems (PBESs) are sequences of Boolean fixed point equations with data variables, used for, e.g., verification of modal mu-calculus formulae for process algebraic specifications with data. ::: Solving a PBES is usually done by instantiation to a Parity Game and then solving the game. Practical game solvers exist, but the instantiation step is the bottleneck. ::: We enhance the instantiation in two steps. First, we transform the PBES to a Parameterised Parity Game (PPG), a PBES with each equation either conjunctive or disjunctive. Then we use LTSmin, that offers transition caching, efficient storage of states and both distributed and symbolic state space generation, for generating the game graph. To that end we define a language module for LTSmin, consisting of an encoding of variables with parameters into state vectors, a grouped transition relation and a dependency matrix to indicate the dependencies between parts of the state vector and transition groups. ::: Benchmarks on some large case studies, show that the method speeds up the instantiation significantly and decreases memory usage drastically.
---
paper_title: Model checking the FlexRay startup phase

paper_content:

The FlexRay protocol is an upcoming standard in automotive industry. Its specification is finalised and maintained by ISO. It is a time-triggered protocol that uses a fault-tolerant clock synchronisation mechanism. During a startup phase that should be resilient to certain faults, the clocks in the network are synchronised and the protocol is initialised. This paper presents a model of the startup phase of the protocol in the mCRL2 modelling language, and shows how model checking techniques can be used to check that the startup protocol fulfills the requirements. A previously unknown scenario is uncovered in which a single failing node can cause another node, or even the entire network, not to start up.
---
paper_title: Dogfooding the Formal Semantics of mCRL2

paper_content:

The mCRL2 language is a formal specification language that is used to specify, model, analyze and verify behavioral properties for distributed systems and protocols. The semantics of the mCRL2 language is defined formally using Structural Operational Semantics (SOS). In previous work, we propose an approach that takes the SOS of a formal language, along with a concrete model, that serves as an initialization, and transforms it to a Linear Process Specification (LPS). In this paper we extend the approach and show that it can be applied to a formal language that in practice is used to specify and model discussed systems. Hence, we take mCRL2's own operational semantics and transform it into an mCRL2 specification. In essence, this means that we are feeding the mCRL2 toolset its own formal language definition. This semantic dogfooding approach validates the implemented behavior for the mCRL2 language against its formal definition. By performing this exercise we revealed gaps between the defined and implemented semantics. These gaps have subsequently been resolved.
---
paper_title: Stuttering mostly speeds up solving parity games

paper_content:

We study the process theoretic notion of stuttering equivalence in the setting of parity games. We demonstrate that stuttering equivalent vertices have the same winner in the parity game. This means that solving a parity game can be accelerated by minimising the game graph with respect to stuttering equivalence. While, at the outset, it might not be clear that this strategy should pay off, our experiments using typical verification problems illustrate that stuttering equivalence speeds up solving parity games in many cases.
---
paper_title: PAT: Towards Flexible Verification under Fairness

paper_content:

Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Current practice of system analysis is, however, deficient under fairness. In this work, we present PAT, a toolkit for flexible and efficient system analysis under fairness. A unified algorithm is proposed to model check systems with a variety of fairness effectively in two different settings. Empirical evaluation shows that PAT complements existing model checkers in terms of fairness. We report that previously unknown bugs have been revealed using PAT against systems functioning under strong global fairness.
---
paper_title: The SPIN Model Checker: Primer and Reference Manual

paper_content:

The SPIN Model Checker is used for both teaching software verification techniques, and for validating large scale applications. The growing number of users has created a need for a more comprehensive user guide and a standard reference manual that describes the most recent version of the tool. This book fills that need. SPIN is used in over 40 countries. The offical SPIN web site, spinroot.com receives between 2500 and 3000 hits per day. It has been estimated that up to three-quarters of the $400 billion spent annually to hire programmers in the United States is ultimately spent on debugging
---
paper_title: LTSMIN: distributed and symbolic reachability

paper_content:

In model checking, analysis algorithms are applied to large graphs (state spaces), which model the behavior of (computer) systems These models are typically generated from specifications in high-level languages The LTSmin toolset provides means to generate state spaces from high-level specifications, to check safety properties on-the-fly, to store the resulting labelled transition systems (LTSs) in compressed format, and to minimize them with respect to (branching) bisimulation.
---
paper_title: Abstraction in Parameterised Boolean Equation Systems

paper_content:

We present a general theory of abstraction for a variety of verification problems. Our theory is set in the framework of parameterized Boolean equation systems. The power of our abstraction theory is compared to that of generalised Kripke modal transition systems (GTSs). We show that for model checking the modal µ-calculus, our abstractions can be exponentially more succinct than GTSs and our theory is as complete as the GTS framework for abstraction. Furthermore, we investigate the completeness of our theory for verification problems other than the modal µ-calculus. We illustrate the potential of our theory through case studies using the first-order modal µ-calculus and a real-time extension thereof, conducted using a prototype implementation of a new syntactic transformation for equation systems.
---
paper_title: JITty: A rewriter with strategy annotations

paper_content:

We demonstrate JITty, a simple rewrite implementation with strategy annotations, along the lines of the Just-In-Time rewrite strategy, explained and justified in [4]. Our tool has the following distinguishing features: ::: ::: ::: It provides the flexibility of user defined strategy annotations, which specify the order of normalizing arguments and applying rewrite rules. ::: ::: ::: Strategy annotations are checked for correctness, and it is guaranteed that all produced results are normal forms w.r.t. the underlying TRS. ::: ::: ::: The tool is “light-weight” with compact but fast code. ::: ::: ::: A TRS is interpreted, rather than compiled, so the tool has a short start-up time and is portable to many platforms.
---

Title: An Overview of the mCRL2 Toolset and its Recent Advances

Section 1: Introduction
Description 1: This section provides an introduction to distributed systems, the challenges in their design, and the purpose of the mCRL2 toolset.

Section 2: mCRL2: approach, applications and challenges
Description 2: This section introduces the mCRL2 language, its sublanguages, the underlying data theory, process behaviours, property language, and the related challenges in automation.

Section 3: The mCRL2 toolset
Description 3: This section details the components of the mCRL2 toolset, its internal objects, linear processes, parameterised boolean equation systems (PBESs), and recent advancements in the toolset.

Section 4: Interfacing with other languages
Description 4: This section discusses the mCRL2 toolset's capabilities in interfacing and transforming various specification languages into mCRL2, and the challenges faced in maintaining these transformations.

Section 5: Architecture and implementation
Description 5: This section covers the architecture and implementation of the mCRL2 toolset, code organization, recent development efforts, and the toolset's interface capabilities.

Section 6: Applications and case studies
Description 6: This section provides an overview of various application domains and case studies exemplifying the use of mCRL2 in real-world scenarios and the effectiveness of its latest advancements.

Section 7: Related work
Description 7: This section positions the mCRL2 toolset within the broader context of verification tooling, comparing it with other similar toolsets, including CADP, FDR2, PAT, SPIN, and others.

Section 8: Closing remarks
Description 8: This section concludes the paper with a discussion on the future directions, ongoing developments, challenges, and the importance of continual improvements in the mCRL2 toolset.