Reasoning about Regular Properties:
A Comparative Study

Tomáš Fiedor Lukáš Holík Martin Hruška

Adam Rogalewicz Juraj Síč Pavol Vargovčík

Brno University of Technology

Several new algorithms for deciding emptiness of Boolean combinations of regular languages and of languages of alternating automata (AFA) have been proposed recently,
especially in the context of analysing regular expressions and in string constraint solving.
The new algorithms demonstrated a significant potential,
but they have never been systematically compared,
neither among each other nor with the state-of-the art implementations of existing (non)deterministic automata-based methods.
In this paper, we provide the first such comparison as well as an overview of the existing algorithms and their implementations.

We collect a diverse benchmark mostly originating in or related to practical problems from string constraint solving, analysing LTL properties, and regular model checking, and evaluate collected implementations on it.
The results reveal the best tools and hint on what the best algorithms and implementation techniques are. Roughly, although some advanced algorithms are fast, such as antichain algorithms and reductions to IC3/PDR, they are not as overwhelmingly dominant as sometimes presented and there is no clear winner. The simplest NFA-based technology may be actually the best choice, depending on the problem source and implementation style.
Our findings should be highly relevant for development of these techniques as well as for related fields such as string constraint solving.

§ INTRODUCTION

Efficient representation of regular properties of finite words has been the subject of research for a long time, with applications and results spanning much of the field of formal reasoning,
including regular expression matching, verification, testing, modelling, or general decision procedures of logics.

When regular properties are combined or generated using Boolean and similar operations,
interesting decision problems are PSPACE-complete.
This includes the most essential problem of language emptiness (further just emptiness),
The textbook approaches that use deterministic automata are in practice plagued by state space explosion.
Determinisation and complementation is done by exponential subset construction and conjunction is quadratic.
This motivated the research on efficient algorithms for non-deterministic
and alternating automata.
Using nondeterminism and alternation, one can gain one or two levels of exponential savings in the size of automata, respectively.
Alternation, which adds conjunctive branching to the disjunctive non-deterministic branching, allows to avoid the blow-up in the automata size completely. However, from the perspective of the worst case complexity, the gained succinctness is payed back by the PSPACE-completeness of language emptiness. Still, the more succinct the representation gives more opportunities for clever heuristics that combat the worst case complexity and work in practical cases, essentially by avoiding re-creation of the entire (non)deterministic representation.

Several very promising techniques and their implementations were proposed during the recent years.

The latest advances in testing AFA emptiness appeared in the context of analysing
combinations of regular expressions and in string solving.
A group of these
techniques is based on reducing AFA emptiness to a reachability in a
Boolean transition systems and using existing implementations of model-checking algorithms, most notably of IC3/PDR [43, 15], such as ABC [17], nuXMV [20], or IC3Ref [16],
to solve it
[25, 24, 44, 72].
The most recent contribution from [66] extends the SMT-solver Z3 with symbolic derivatives, a generalisation of Antimirov derivatives of regular expressions. Z3 uses them to convert a combination of regular expressions into an alternating/Boolean automaton and on the fly tests its language emptiness through the classical de-alternation and a search for an accepting configuration.

Slightly older algorithm for testing equivalence of AFA (convertible to an emptiness test) is based on computing bisimulation up-to congruence [27]. It generalizes the original NFA-equivalence test of [11].

The congruence closure algorithms were preceded by the antichain algorithms that optimise the subset construction by the subsumption pruning [74, 38], and by the first attempt to use the model checking algorithms, namely the algorithm Impact of [57], to emptiness of combinations of regular properties [37].

Lastly, the area of string constraint solving gave rise to a large variety of string constraint solvers.

They approach combinations of regular properties through a spectrum of clever techniques based e.g. on automata, transformations to other types of constraints, reasoning on lengths of strings, Parikh images, etc. (e.g. Z3 [59, 66], CVC4/5 [7, 60], Z3Str4 [9], OSTRICH [22, 23], Trau [4, 3] to name a few).

These works demonstrate a significant promise,

but they are presented in specific, often narrow contexts and under varying views on state of the art. Consequently, they were never sufficiently compared against each other.

Even comparisons against the most efficient implementations of the more standard techniques based on (non)deterministic automata is rare.

String solvers were compared only against string solvers, advanced AFA-emptiness tests were compared only against the basic de-alternation.
A somewhat interesting comparison was done only between NFA-antichain and up-to congruence-based language inclusion and equivalence test in [11] and in [35], and between the basic antichain based AFA emptiness and a version that uses abstract interpretation [38]. A number of works also take as their baseline implementations of automata

or string solvers

which, even though being respectable tools in their own right,

are currently not the fastest solvers of combinations of regular properties in either category.

On top of that, all the mentioned works on solving combinations of regular properties use only narrow benchmarks, often mutually exclusive.

Systematic comparisons of tools and algorithms on meaningful benchmarks is obviously
needed to answer the questions `What to use?' and `What to compare with?',
and generally for the field of reasoning about regular properties and automata to progress.

We thus present a comparison of implementations of major algorithms.

We compare the tools on a large benchmark of problems that we have collected from other works,

from string constraint solving problems, analysis of regular expressions,
regular model checking, and analysing LTL properties of systems.

We believe that it is currently the most comprehensive benchmark in existence.

Our main focus is on examples around string solving and analysis of regular expressions,
which is also where the most of the recent developments has happened.

These benchmarks mostly allow for a relatively simple representations of automata transition functions.

Even though the alphabets in examples coming form this are large (e.g. UNICODE with up to $2^{32}$ symbols),
the alphabet size can, in most cases, be reduced to few symbols by working with alphabet minterms (classes of indistinguishable symbols) instead of individual symbols.

The issue of effective symbolic representation of transition relations with large alphabets then does not dominate the evaluation, although it would be critical in other application areas, such as deciding WS1S or arithmetic formulae.

We have obtained results that paint the basic landscape of the available techniques and tools. They identify tools and approaches which are likely to work well and should be used as the baseline in comparisons.

We also provide a relatively diverse and large benchmark to be used in comparisons.

The results broadly confirm that the new algorithms represent a leap in efficiency compared to the technology of DFA and also make a reduction of a problem to language emptiness of alternating automaton an attractive  option.

On the other hand, they challenge some folklore knowledge and conclusions implied elsewhere.

For instance, reductions to IC3/PDR, although yielding one of the fastest algorithm, are not as vastly superior as sometimes presented.

Some practically relevant benchmark categories are best solved by a combination of an antichain algorithm with a SAT solver. Others, surprisingly many in fact, by a simple efficiency oriented implementation of basic algorithms for nondeterministic automata.

Our results also underscore that there is no universal silver bullet.
The particular kind of the problem, determined to a large degree by its source, is a decisive factor that should be taken into account when choosing and tuning a solver.

§ PRELIMINARIES

A (nondeterministic) finite automaton (NFA) over $\Sigma$ is a tuple
$\aut= (Q,\Delta,I,F)$
where $Q$ is a finite set of states,
$\Delta$ is a set of transitions of the form $\move q  a  r$ with $q,r\in
%Q$ and $ a \in\Sigma\cup\{\epsilon\}$, $I\subseteq Q$ is the set of \emph{initial states}, and $F\subseteq Q$
Q$ and $ a \in\Sigma$, $I\subseteq Q$ is the set of initial states, and $F\subseteq Q$
is the set of final states.
A run of $\aut$ over a word $w \in \Sigma^*$ is
a sequence
$\move{p_0}{ a _1}{p_1}
\move{}{ a _2}{}
\ldots
%$p_{n-1},  a _n, p_n$
\move{}{ a _n}{p_n}$
where for all $1\leq i \leq n$, it holds that $ a _i \in \Sigma \cup
\{\epsilon\}$, $w =  a _1
\concat  a _2 \concats  a _n$, and either $\move{p_{i-1}} { a _i} {p_i}\in\Delta$ or $p_{i-1} = p_i$, $a_i=\epsilon$.

The run is accepting if $p_0 \in I$ and $p_n\in F$, and the language
$\langof{\aut}$ of $\aut$ is the set of all words for which $\aut$ has an accepting run.

The automaton is deterministic (DFA) if for every state $q$ and symbol $a$, $\delta$ has at most one transition $\move q a r$.
Any NFA can be determinised by the subset construction, which creates the DFA
$A' = (2^Q,\Delta',\{I\},\{S\mid S\cap F\neq \emptyset\})$ where $\move S a S'\in \Delta'$ iff $S' = {\{s' \mid s\in S \land \move s a {s'}\in\delta\}}$.

The basic automata constructions implementing Boolean operations with languages are
$\aut\cap\aut' = (Q\times Q',\Delta^\times,I\times I',F\times F')$ where
$\move {(q,q')}{ a }{(r,r')}\in\Delta^{\times}$ iff
$\move{q}{ a }{r}\in\Delta$ and
$\move{q'}{ a }{r'}\in\Delta'$, non-deterministic union $\aut\cup\aut' = (Q\cup Q',\Delta\cup\Delta',I\cup I',F\cup F')$, deterministic union by product which is the same as $\cap$ up to that the final states are $F\times Q \cup Q\times F$, and complementation which consists of determinization and complementing the final states.

Alternating automata.
An alternating finite automaton (AFA) in the most general form would be a tuple
$\M = (\Sigma,\alphapred, Q,\delta,I,F)$ where, when denoting $\boolform X$ the Boolean predicate formulae over variables $X$:

* $\Sigma$ is a finite alphabet;

* $\alphapred$ is a set of unary symbol predicates with a free variable $\symbvar$;

* $Q$ is a finite set of states;

* $\delta: Q \rightarrow \boolform{Q \cup \alphapred}$ is a
transition function where states of $Q$ have only positive occurrences

* $I \in \boolform{Q}$ is a positive initial condition; and

* $F\in\boolform{Q}$ is a negative final/accepting condition.

It can be interpreted as the forward NFA $\fwnfa A = (\Sigma, \pow Q,\fw \Delta, I',  F')$ with states $\conf\subseteq Q$ called configurations of $A$.

Assume many sorted interpretation of formulae over variables $Q$ of the type Boolean (values $0$ and $1$) and the variable $\alpha$ of the type $\Sigma$.
A set of states $\conf\subseteq Q$ is understood as an assignment $Q\rightarrow \{0,1\}$ in which $\conf(q)=1$ corresponds to $q\in \conf$.
A pair $(\conf,a)$, $a\in\Sigma$ is understood as the same assignment extended with $\alpha \mapsto a$. The satisfaction relation $\models$ between a formula and a configuration $\conf$ or a pair $(\conf,a)$ is defined as usual.

The transition relation $\fw \Delta$ then contains a transition $\move \conf a {\conf'}$ iff
$(\conf',a) \models \bigwedge_{q\in\conf} \Delta(q)$, and
$I'$ and $F'$ are the sets of configurations that satisfy $I$ and $F$, respectively.

It is common to define $\fw \Delta$ to contain only the smallest transitions, that is, for a given $\conf$ and $a$,
only the transitions $\move \conf a {\conf'}$ with the $\subseteq$-minimal target $\conf'$ are in $\Delta$.[A state in a configuration is understood as a constraint. The less constraints, the more can be accepted from the configuration. Transitions to more constrained configurations are useless.]

The language of $A$, $L(A)$, is the language of $\fwnfa A$.

The AFA can equivalently be interpreted as the backward NFA, the automaton $\bwnfa A = (\Sigma, \pow Q,\bw \Delta, I', F')$ where
$\move \conf a {\conf'} \in \bw \Delta$ if
$(\conf,a)\models \Delta(q)$ for each $q\in \conf$.
Here it is enough to take, for a given $\conf'$ and $a$, only the transition with the $\subseteq$-largest source $\conf$[Going backward, larger configurations are more permissive. Transitions from the same target with smaller configurations are useless.]

(this makes the transition relation backward deterministic).

Boolean automata.
Alternating automata may be extended to Boolean finite automata (BFA) by allowing any Boolean combination in the initial, final, and transition formulae
(states in the initial and transition formulae may occur negatively, states in the final formula may occur positively).

Note that the extension of AFA to BFA is not dramatic, as a BFA is easily encoded as an AFA with only double the size, by the following steps:

1) for each $q\in Q$, add state $\bar q$ with $\Delta(\bar q) = \neg\Delta(q)$,
2) transform all formulas in $I,F,\Delta$ to NNF,
3) replace all literals $\neg q$ by $\bar q$ in $\Delta$ and $I$ and replace literals $q$ by $\neg \bar q$ in $F$.

Restricted forms of AFA transition relation.

The general form of AFA, as defined above, is the most succinct. It provides space for most optimizations, such as in [69]. Automata in this form are generated from LTL conversions of [31] used in [27, 69]. On the other hand, only a small subset of algorithms and tools support AFA in this most liberal form.

A common restriction (used e.g. in [27]) is to separate symbols from states in the transition formulae, that is, having $\Delta(q)$ in the form  $\symbolf \land \statef$ with $\symbolf\in\boolform{\alphapred},\statef\in\boolform{Q}$. We call such AFA separated.

The transition relation can then be seen as a function $Q\rightarrow \boolform\alphapred \times \boolform Q$.

Separated AFA are often considered with the state formula $\statef$ in the disjunctive normal form (e.g. in [33, 38]), which we call the  DNF form, and $\Delta$ then may be seen as a set of transitions of the form $\move q \symbolf c$ where $\bigwedge c$ is a (positive) clause of $\statef$.

The decision problems.
We will concentrate on two decision problems:

(1) AFA emptiness asks whether the language of the given AFA is empty.

(2) Emptiness of Boolean combinations of regular properties (BRE), asks whether a Boolean combination of regular languages, given as automata or regular expressions, is empty (languages can be combined with $\cap$, $\cup$, and complement wrt. $\Sigma^*$, which also covers testing inclusion and equivalence[$L'\subseteq L$ is emptiness of $L'\cap \overline L$ and equivalence is emptiness of  $(L'\cap \overline L)\cup(\overline{L'}\cap L)$.]).

§ EXISTING ALGORITHMS AND TOOLS

In this section, we will overview the existing approaches and tools implementing AFA and BRE emptiness.

§.§ Representation of Automata Transition Relations

In the simplest form, a predicate on a automata transition represents a single letter from the alphabet.
This is called an explicit transition. Explicit automata are simple, allow for low level optimizations, and implementation of complex algorithms for them is manageable (such as advanced algorithms for computing simulations [62, 47, 21]).

The technique of a-priori mintermization, that replaces the alphabet by the alphabet of minterms, classes of indistinguishable symbols, makes explicit automata usable also when alphabets are large.

However, when the number of minterms tends to explode, explicit automata do not scale.

Various implementations of automata have been using transition predicates implemented as BDDs, Boolean formulae, formulae over SMT-theory of bit-vectors, intervals of numbers, etc.

This has been systematized in the works on symbolic automata [71, 28, 30], where the symbol predicates may be taken from any effective Boolean algebra (and the automata are in the separated form).

Even more compact than symbolic automata are representations of the transition relation used in the WS1S solver or in some of the implementations of AFA, which in a way drop the restriction to the separated form.

We will discuss the concrete implementations below.

§.§ (Non)deterministic Finite Automata

The baseline approach to solve BRE is to use DFA or NFA.
Boolean operations are implemented as the classical construction listed in <ref>.
Automata may be kept deterministic,

or they are kept non-deterministic whenever possible and determinised only before complementing.

An important ingredient of achieving efficiency is usually to minimize automata at least once every few operations (important e.g. in applications such as regular model checking [12] or some approaches to string solving [10, 22, 3]).
The deterministic approaches construct the minimal DFA by the Hopcroft, Moore, Brzozowski, or the Huffman algorithm [49, 58, 18, 50],

the non-deterministic approach may use simulation [62, 21, 42, 51, 47] or bisimulation [68, 61, 45] based reduction methods.
Simulation reduces significantly more but is much costlier.
DFA/NFA are implemented in many libraries. Here we select a representative sample.

First, is the simplest tool, our own implementation of NFA. It uses explicit automata with mintermization. It is implemented in , with efficiency in mind, but with no extensive optimizations (roughly, transitions from a state stored in a two layered data structure, the first layer divided and ordered by symbols, and the second layer ordered by the target state). It uses
an off the shelf implementation of one of the newest generation algorithms for computing simulation [62, 21, 47] (that achieve good efficiency through a usage of the partition-relation data structure) taken from tree automata library [53] (implementing namely [47]).[In our experiment, simulation is only used after parsing and has minimal overall impact.]

The automata library [6], written in Java, is often considered a baseline in comparisons [6]. It uses primarily deterministic automata and symbolic representation of transition relation using character ranges. It is written in Java and is relatively optimized.

The library  [70], made in C#, implements symbolic NFA/DFA  parametrized by an effective Boolean algebra. We use it with the default algebra of BDDs. has been long developed and has accumulated many optimizations and novel techniques for handling symbolic automata

[41], written in C, is the most influential and optimized implementation of deterministic automata.

It specialises in deciding WS1S formulae, which besides Boolean combinations includes also quantification. The decision procedure generates DFA with complex transition relations over large alphabets of bit-vectors. For this purpose, uses a compact representation of the transition relation: a single MTBDD for all transitions originating in a state, with the target states in its leaves. can represent only a DFA, hence it always implicitly determinizes.

[53], written in , is a library implementing non-deterministic tree automata.
As NFA are a special case of tree automata, we can use it as an implementation of the basic constructions for explicit NFA. It is relatively optimised. We include it into the comparison for its fast implementation of the antichain inclusion checking [12, 46], which for NFA boils down to the inclusion check of [33].

§.§ Alternating Automata

The basic approach to AFA emptiness is de-alternation, transformation to an NFA, either the forward $\fwnfa A$ or the backward $\bwnfa A$, followed by testing the emptiness of the resulting NFA.
Both NFAs are constructed by a variation on the NFA subset construction.
We are not aware of any tool using pure de-alternation,
and we believe that it would not be competitive.

The forward algorithm is however the basis of [65] used in where it is run on the fly with a novel symbolic derivative construction (discussed also in the paragraph on string constraint solvers).

Interpolation based abstraction refinement.
Attempts to harness model checking algorithms to AFA emptiness appeared in the context of string solving and processing of regular expressions.

To our best knowledge, the earliest attempt was [37], where conjunctions of regular constraints were solved using the interpolation-based algorithm of [56].

The interpolation-based abstraction refinement, namely the algorithm Impact of [57], was also used in [52]. This work concentrated on more general problem, solving emptiness of AFA over data words with an infinite data domain (that can relate past and current values of data variables). Their tool [2] (in Java), that we include into our comparison, can be run on our benchmark too.

Reduction to reachability and IC3/PDR.

The work of [72] presented the first translation of string constraints (mostly BRE) into reachability in a Boolean transition system (circuit) that was then solved  by the model checker nuXmv [20]. This was de facto the first reduction of AFA emptiness to reachability in a Boolean transition system (BTS).

Let us briefly overview the basic principle of the reduction.
The forward BTS for an AFA $A$ has configurations that are Boolean assignments to $Q$,
initial and final configurations satisfy $I$ and $F$, respectively,
and transitions are given by the formula
$\fw \Phi_\Delta : \bigwedge_{q\in Q}q\rightarrow [\Delta(q)]'$.
Here we use $[\varphi]'$ to denote the formula obtained from $\varphi$ by substituting every state $q$ by its primed version $q'$,
and we will also denote by $[\conf]'$ the primed version $\{q' \mid q \in \conf\}$ of a configuration $\conf$.
A successor of a configuration $\conf$ is any configuration $\bar \conf$ such that
$[\bar \conf]'$ satisfies
$\exists Q\exists \symbvar  \, \fw \Phi_\Delta \land \bigwedge_{q\in C} q$ (the symbol variable alpha is of the bit-vector sort).
Reachability is then the transitive and reflexive closure of the successor relation and the reachability problem asks whether a final configuration is reachable from an initial one. It is the case if and only if $A$ is not empty.
[72] used the forward reduction.

Alternatively, the backward BTS for $A$ has
the initial configurations satisfying $F$, final configurations satisfying $I$, and the successor relation given by the formula

$\bw \Phi_\Delta : \bigwedge_{q\in Q}q'\rightarrow \Delta(q)$.

Works of [25, 24] applied IC3/PDR [43, 15], implemented in IC3Ref [16], together with the backward BTS reduction to solve emptiness of BRE and obtained very encouraging results.
Their implementation is, however, proprietary and not publicly available.

Similar approach was taken by [44], where a string constraint was translated to a multi-tape AFA and then to a BTS by the forward translation, and given to IC3/PDR to solve through tools nuXmv [20] or ABC [17].

Results of [69] seem to indicate that the backward translation is better and the same is suggested by the comparison in [25, 24] in which the string solver Sloth [44], based on the forward reduction, was much slower that Qzy, based on the backward reduction. In this comparison, we include our own  implementation of the backward reduction based on

Antichain algorithms presented in [74] were the first breakthrough in solving BRE. They use subsumption relations between the states of the automata constructed by variations of the subset construction to prune the constructions.
They were used to test language universality and inclusion of NFAs and AFA emptiness.
The AFA emptiness namely is based on an on-the-fly search for an accepting state of the $\fwnfa A$ or for an initial state of the $\bwnfa A$.
Subsumption prunes discovered states that are larger (smaller for the backward algorithm) than others.

The antichain algorithms were enhanced and generalized in a number of works, e.g. with a more aggressive pruning by the simulation-based subsumption [5, 33], or by counterexamples guided abstraction refinement in [38].

In this comparison, we include the NFA inclusion check implemented in the tree automata library

We also experimented with a student-made implementation of the antichain AFA emptiness check of [38]  that uses abstraction refinement (the original implementation is no longer maintained and we were not able to run it). However, not being  able to achieve a competitive performance, we excluded it from the comparison. One reason of the poor performance may be that simplest form of AFA, explicit DNF form (used in the original version [38]), might be too inefficient and costly to construct in our examples, partly due to a large number of minterms induced by the AFA emptiness benchmark.

We implemented (in ) the antichain AFA emptiness test of [33] that integrates tightly with a SAT solver to handle the general form of AFA with large alphabets. We will refer to it as .

We will briefly explain its principle.

It essentially implements the reachability test for the backward BTS discussed in the previous paragraph.

A configuration $\conf$ is represented by the conjunction $\phi_\conf = \bigwedge_{q \in Q \setminus \conf} \neg q$.

Note that $\phi_\conf$ is satisfied by the downward closure of $\conf$, which are all configurations included in (subsumed by) $\conf$.

To compute predecessors of configurations represented by $\phi_\conf$,
the SAT solver (namely MiniSAT [34]) is called on the formula

$\Phi: \bw \Psi_\Delta \land \phi_\conf \land \psi_{\ach}$.

Here, $\psi_{\ach}$ excludes all already discovered configurations from the solution. It is a conjunction of clauses $\overline{\phi_\conf} : \bigvee_{q\in Q\setminus \conf} q$ for every previously discovered configuration $\conf$.

The SAT solver discovers a satisfying assignment $e$, which is turned into a new configuration $c' = Q \cap e$ (that is, the values of the symbol bits constituting the bit-vector $\symbvar$ are omitted from $e$). Unless $c'$ is initial, it is queued for further predecessor computation and is immediately added to $\phi_\ach$ through the interface of incremental SAT solving as the clause $\overline{\phi_{c'}}$.

Finally, only maximal predecessors of $c$ are of interest, as the non-maximal ones are subsumed by them. We enforce the maximality of $c$ through working directly with the internal SAT solver structures: at decision points, the SAT solver is forced to give priority to decisions that assign 1 to state variables.

Bisimulation up-to congruence.

A later class of algorithms, here refered to as up-to algorithms, checks equivalence as a bisimulation between configurations of AFA, and utilises the up-to congruence technique to prune the search space.
The first algorithm on NFA equivalence [11] was extended to alternating automata emptiness check in [27].
These algorithms are close to antichains. [11] shows that the pruning potential of the up-to techniques is in theory the same or larger than that of antichain.

A disadvantage of the up-to congruence technique is the need for expensive evaluation of congruence closures.

The more extensive experiments of [35] shows antichain algorithms as faster, with an exception of randomly generated automata with small alphabets and very dense transition relations.
We include into the comparison the Java implementation of the AFA-emptiness of [27] (emptiness reduces to equivalence with a trivial empty AFA), that we refer to as . The other implementations of up-to algorithms we are aware of, from [36] and [11], are single-purpose programs that decide equivalence of two NFAs, hence we would be able to run them on a very small fraction of .

§.§ String Constraints Solvers

There are dozens of string constraint solvers that implement, to a various degree, a support for deciding combinations of regular properties. String languages are rich and BRE are not the absolute priority of the solvers, hence they perform on them generally worse than specialised tools. However, string solvers implement a wide scale of unique techniques and pragmatic heuristics that may work in specific instances. Representatives of the solvers with the most mature implementations (also used in most comparisons in the literature) are [59, 65] and [60, 7]. solves BRE mostly through rewriting rules.

Recently [65] extended with an approach based on the Antimirov derivative automata construction generalised to symbolic automata and extended regular expressions. Essentially, the construction produces a symbolic AFA/BFA and checks its emptiness on the fly while running the forward de-alternation.
[65] shows that it is significantly more efficient in solving BRE than other SMT solvers (including ).

§.§ Other Approaches and Tools

Although we believe that we have collected a representative subset of existing algorithms and tools, we have not collected all interesting specimens. Some were not available, some were difficult to run or prepare the inputs for, some seemed covered by experimentation in other works. Including these tools and algorithms into the comparison could still be interesting and we leave it for the future work (we plan to keep extending the tool base as well as the benchmark set). Namely, the tool DPRLE [48], used in the comparison in [25], seemed to be mostly outperformed by the IC3/PDR approach implemented in Qzy, however, not absolutely consistently. The implementation of NFA antichain and up-to congruence techniques used in [35] seems efficient, with its NFA antichain inclusion twice as fast as that of . The up-to congruence NFA equivalence checking of [11] could be fast too ([11] and [35] report somewhat conflicting results). There are numerous NFA/DFA libraries, e.g. the C alternative of [55] or the Java implementation of symbolic NFA of [26]. ALASKA [32] might contain interesting implementations of antichain algorithms but is no longer maintained and available. Our comparison is missing a basic implementation of antichain-powered de-alternation for explicit AFA in the DNF form, which, if not overwhelmed by a large number of minterms, could reach a good performance through simple fast data structures, similarly to our .

§ BENCHMARKS

We collected as comprehensive benchmark as possible, harvesting examples used in previous works as well as generating some of our own. It is available at [1].
Our main focus is the areas where the most of the development in solving AFA and BRE emptiness happened recently, which is string constraint solving and analysis of regular expressions used in analysing and filtering texts.

Atomic regular properties are here mostly given in the form of regular expressions over UNICODE character classes. The alphabet is large but the number of minterms is mostly small or moderate.

This is true also for our examples from regular model checking.

Symbolic handling of complex transition relations over large alphabets is thus not absolutely crucial and the experiment can stay focused on the main algorithms for emptiness check.

For that reason, we do not include benchmarks from solving WS1S [19], the primary target of ,
or Presburger arithmetic with automata [13, 73], where the techniques of handling symbolic alphabet are indispensable.

Techniques specialising at this kind of problems would deserve their own study.

Our benchmarks where the symbolic alphabet representation is still rather important are AFA coming from (combinations of) LTL properties, with alphabets of sets of atomic propositions, and from translations of string constraint problems to AFA with complex multi-track alphabets.

[We did not attempt to generate purely random problems. First, purely random automata generated e.g. by [67] seem to have different characteristics than automata coming from practical problems (e.g. in [12, 35]). Second, although generating random NFA is possible with a generator controlled by three simple parameters which give a manageable parameter-value space covering all NFA, it is not clear how to similarly generate random AFA or BRE. On the other hand, we do include a benchmark based on randomly generated LTL formulae, which we consider relatively close to realistic LTL specifications.]

*Boolean combinations of regular expressions.
This group of BRE contains benchmarks on which we can run all tools, including those based on NFA and DFA. They have small to moderate numbers of minterms (about 30 in average, at most over a hundred).

contains 330 string constraints from the Norn and SyGuS-qgen, collected in SMT-LIB benchmark [8], that fall in BRE. These were also used to compare SMT-solvers in [66].

has 56 difficult handwritten problems from [66] containing membership in regular expressions extended with intersection and complement. They encode
(1) date and password problems,
(2) problems where Boolean operations interact with concatenation and iteration, and
(3) problems with exponential determinization.

contains 171 language inclusion problems from runs of abstract regular model checking tools (verification of the bakery algorithm, bubble sort, and a producer-consumer system) of [12]. These examples were used also in [35, 11].

contains 500 problems, obtained analogously as in [27, 69], of the form $r_1 \land r_2 \land r_3 \land r_4 = r_1 \land r_2 \land r_3 \land r_4 \land r_5$, where each $r_i$ is one of the 75 regexes[<https://github.com/lorisdanto/symbolicautomata/blob/master/benchmarks/src/main/java/regexconverter/pattern%4075.txt>] from RegExLib [63] selected so that $r_1 \land r_2 \land r_3 \land r_4 \land r_5$ is not empty.
This benchmark is inspired by spam filtering, where we want to test whether a new filter $r_5$ adds anything to existing filters.
We transformed this problem into the inclusion $r_5 \subseteq r_1 \land r_2 \land r_3 \land r_4$, and kept the original form for which expects an equivalence.

has 8 parametric problems. Four are from [37]:

(1) $\regex{[a-c]a[a-c]}\{n+1\} \cap \regex{[a-c]a[a-c]}\{n\}$ (long strings),

(2) $\bigcap_{i=1}^n\regex{([0-1]}\{i-1\}\regex{0[0-1]}\{n-1\}\regex{0[0-1]}\{n-i\}\alpha_i\regex{)|([0-1]}\{i-1\}\regex{1[0-1]}\{n-1\}\regex{1[0-1]}\{n-i\}\alpha_i\regex{)}$ (exponential branching),

(3) $\bigcap_{i=1}^n\regex{.*(.}\{p_{10+i}\}\regex{)+}\alpha_i$ (exponential paths 1), and

(4) $\bigcap_{i=1}^n\regex{.+}\alpha_i\regex{0(.}\{p_{10+i}\}\regex{)+}$ (exponential paths 2), where $\alpha_1,\ldots,\alpha_n$ are disjoint character classes and $p_j$ is the $j$-th prime number.

Another four are from [25]:

(5) $\verb|^.[01]*.1.[01]{n}.$| \setminus \verb|^.[01]*.0.[01]{n-1}.$|$ (sat. difference),

(6) $\verb|^.[01]*.1.1.[01]{n}.$| \setminus \verb|^.[01]*.0.[01]{n+1}.$|$ (unsat. difference),

(7) $\verb|^.[01]*.1.[01]{n}.$| \cap \verb|^.[01]*.0.[01]{n-1}.$|$ (sat. intersection) and

(8) $\verb|^.[01]*.1.[01]{n}.$| \cap \verb|^.[01]*.0.[01]{n}.$|$ (unsat. intersection).

For (1) we chose $n \in \{50,100,\dots,500\}$, for (2)-(4) we chose $n \in \{2,3,\dots,60\}$ and for (5)-(8) we chose $n \in \{50,100,\dots,100\}$.

§.§ AFA benchmark

The second group of examples contains AFA not easily convertible to BRE. Here we can run only tools that handle general AFA emptiness. Some of these benchmarks also have large sets of minterms (easily reaching to thousands) and complex formulae in the AFA transition function, hence converting them to restricted forms such such as separated DNF or explicit may be very costly. This also seems to be the main reason for which our implementation of [38] could not compete.

comes from transformation of linear temporal logic formulae over finite traces () to AFA [31]. The 1699 formulae are from [54][<https://drive.google.com/file/d/1eOYGvm3C8sQ-9iyfZ8qx42K54hgrFNTC>] and they represent common patterns which can be divided into two groups: (1) 7 parametric patterns (100 each) and (2) randomly generated conjunctions of simpler patterns (999 formulae).

contains 300 formulae obtained with the random generator of [69]. The generator traverses the syntactic tree of the LTL grammar, and is controlled by the number of variables, probabilities of connectives, maximum depth, and average depth.
We have set the parameters empirically in a way likely to generate examples difficult for the compared  solvers (the formulae have 6 atomic propositions and maximum depth 16).

has a pair of hand-made parametric formulae (160 formulae each) used in [27, 69]: Lift [40] describes a simple lift operating on a parametric number of floors and Counter [64] describes a counter incremented modulo the parameter.

[54] contains 62 formulae that specify realistic systems, used by Boeing [14] and NASA [39].
The formulae represent specifications used for designing Boeing AIR 6110 wheelbraking system and for designing NASA NextGen air traffic control (ATC) system.

4062 AFA emptiness problems to which the string solver Sloth reduced string constraints [44]. The AFA have complex multi-track transitions encoding Boolean opetarations and transductions, and a special kind of synchronization of traces requiring complex initial and final conditions.

13840 AFA emptiness problems that correspond to certain sub-problems solved within the string solver Noodler in [10]. The AFA were created similarly as those of , but encode a different particular set of  operations over different input automata.

§ THE COMPARISON

We ran our experiments on Debian GNU/Linux 11, with Intel Core 3.4GHz
processor, 8 CPU cores, and 20 GB RAM. All experiments were run with the timeout of 60 seconds (increasing the timeout did not have a significant impact). Additional details as well as the virtual machine with the entire benchmark are available at [1].

Benchmarking infrastructure.
The initial difficulty is that the tools expect different input formats and forms of automata and the benchmarks come in different formats as well.

We converted all benchmarks to our internal AFA format, from which we generated formats supported by the AFA handling tools , , , and , or we extend the tools with a parser.

The BRE benchmarks come from various sources. We first convert them into a master file which specifies the Boolean combination of atomic  NFA,
each atomic NFA stored in a separate file.
The SMT-lib format is generated for $\zthree$ and $\cvc$.
In the case of $\bhand$, $\bparam$, and $\bcsmtlib$,
the atomic automata are translated from regular expressions using the parser of , while in the case of , where the regexes contain features not supported by , we use the parser from .
$\bcsmtlib$ and $\bhand$ requires first translating from SMT-lib to a regular expression.
In the case of , the atomic automata come directly as NFAs, and
are converted into formats of the individual BRE solvers (we again wrote parsers for some of the solvers), and to our AFA format for the AFA solvers. Every BRE solver was extended by an interpreter of the master file that reads the NFA/DFA from the generated solver-specific files (except the SMT solvers, which read SMT-lib).
We note that due to some difficulties with internal structures,
we currently cannot run on , and due to the lack of a converter frm complex regular expressions and from pure NFA to the SMT format, we do not run and on and on .

Measured data.
We will present the results obtained  with BRE (where we run all the tools) and with AFA emptiness (where we run , , , and ) separately.
We also separate the results on examples from applications from results on parametric hand-made examples.

Table <ref> summarizes
the statistics from evaluating the benchmarks.

The table lists: (i) the average time, (ii) the median time, and (iii) the number
of timeouts and number of errors (mostly, a tool ran out of the memory, made a bad alloc or ran into a segmentation fault).
A few errors, e.g. in or , were due to the
unsupported features in the inputs.
The tools' performance is then visualised on cactus plots in
For each tool, the plot shows the progress of the tool on each
benchmark: the $y$ axis is the cumulative time taken on the benchmark, with the individual examples on the $x$ axis ordered by the runtime taken by the tool. Timeouts are omitted.
In the appendix, we also show a set of scatter-plots that compare for every benchmark the three best performing tools.

Summary of AFA and BRE benchmarks. Table list (i) the average, (ii) the median, and (iii) the number of timeouts and errors (in brackets). Winners are highlighted in bold.

Cactus plots of AFA and BRE benchmarks. The $y$ axis is the cumulative time taken on the benchmark in logarithmic scale, benchmark on the $x$ axis are ordered by the runtime of each tool.

Finally, we compared the tools on the parametric benchmarks and
. We illustrate the results in Fig. <ref>. Each graph shows
the times for the increasing value of the specific parameter on the $x$ axis.

Models of runtime on parametric benchmarks based on specific parameter $k$ with timeout 60s. The sawtooths represent the tool failed on the benchmark for some $k$ while solving benchmarks for $k-1$ and $k+1$. For brevity, we draw the models only until they start continually failing.

§.§ Discussion

Based on the measurements, we make several observations.

Firstly, the tool which combines universality (it can be run on AFA as well as on BRE emptiness) with the most consistent good performance is . It dominates most of the AFA emptiness benchmark, shows great or a very good performance on the BRE benchmark, and often stands out on the parametric examples. Moreover, the measurements reported in [25] suggest that the backward BTS reduction has even more potential. This is visible namely from the comparison of our results on the parametric benchmarks , , , and .
Our implementation matched the result of [25] on and partially on , saw a worse trend on and much worse trend on .
A likely culprit is a different underlying model-checker, ABC [17] in our implementation versus ICRRef [16] in [25].
[25] however did not use IC3Ref out of the box,

Secondly, the results on application related BRE (all BRE except the parametric examples in ) quite surprisingly favour the tools based mostly on relatively basic NFA algorithms. The overall best is the simplest tool of all, our implementation  of basic NFA constructions. It should be emphasised that, despite being made with efficiency in mind, it is not optimised, and its simplicity allows for much further optimization. Close to the performance of is , which uses the antichain inclusion checking on and (the fact that explicit complementation of is faster than the antichain of suggests that the inclusion benchmarks are not particularly hard). specialises to the more general tree automata, which probably causes unnecessary overhead. also performs well. It uses slightly more advanced algorithms than (such as lazy evaluation of difference, though, without antichain pruning). Its symbolic representation of transition functions with BDDs probably does not provide much advantage here.
This result challenges the view that translating complex problems, arising for instance in string constraint solving, into AFA in order to use the sophisticated machinery of AFA solvers is an obvious silver bullet. Organizing the computation into smaller NFA operations, where, moreover, partial results can be minimised and re-used, and a simpler and hence more flexible NFA technology is used, might be a better strategy (this seems to work very well for instance in our recent prototype string constraint solver [10]).

Our AFA emptiness test based on the antichain algorithm and a SAT solver has an interesting performance. As can be seen on the cactus plots, besides its absolute domination on , it is significantly faster than other tools on a large portion of the other AFA emptiness benchmark, but struggles on the rest. The examples where it dominates are often

automata with the structure resembling a lasso (or several lassos) with a long handle. The other implementation of an antichain algorithm, NFA/NTA inclusion in , also shows a good performance.
This together points on the overall strength of antichain algorithms.

The SMT string constraint solvers are not among the best in the benchmark related to practical applications, but are competitive (especially ), and win on some parametric cases. This may be due to that various heuristics unique to SMT solvers, especially rewriting that reduces one type of a constraint to another, kicks in. For instance, seems to solve
with a help of rewriting to the sub-string constraint in the theory of sequences.
In general, the measurements on parametric examples underscore the fact that no algorithm is universally the best and their relative performance may vary drastically depending on the kind of an input.

Although the mediocre performance of the other tools can be partially explained by their focus on a different kind of a problem or a dated underlying technology, and each of them is respectable in its own right, a point can be made against relying on them as a baseline in comparisons of tools for solving our kind of problem.
, optimised for a different settings (complex alphabets of bit-vectors with many minterms), is held back by the implicit determinisation, and, in our case, probably by the overhead of the symbolic representation. It also frequently runs out of the 32-bit address space for BDD nodes. Similarly for , which also always determinises.
The low performance of is surprising relative to the good results of the up-to algorithms reported in [11, 27]. It is more consistent with [35] where up-to algorithms were not wining against antichains on the more practical examples. Our results however do not directly contradict the results of [27] itself, since it does not compare with the fast tools identified here and stands to a large degree on parametric and random benchmarks.

There is also always the possibility that we have prepared the input in a way not ideal for the tool. For instance, transformation to the separated AFA, required by , is not entirely trivial. Further investigation of this and a comparison with some other implementation of the up-to techniques seems to be needed. The lack of a raw speed of on BRE and AFA emptiness is expectable considering that it is meant for a different kind of systems, AFA over data words. The stable trends shown in the graphs suggest that an implementation of an interpolation-based abstraction refinement optimised for BRE and AFA emptiness might have a potential.

Main takeaways.
The backward reduction of AFA emptiness to BTS reachability in a combination with IC3 is very fast and extremely versatile, showing very good performance on almost all benchmarks. However, on BRE with a relation to a real world application, simple NFA algorithms actually tend to have the best raw performance, with the simplest implementation of NFA being the best.
Antichain algorithms work also well, even significantly better than other algorithms on specific kinds of AFA.
These seem to be the tools to use.
Reasonable implementations of the backward BTS reduction with IC3, of antichain, and of basic NFA should also be the baseline of comparisons.

and , based on DFA, as well as focused on data words rather then on pure regular properties, do no reach the performance of the best tools. Also did not confirm the power of up-to algorithms. SMT-solvers, especially, are competitive, but cannot be considered the top of state of the art.

Generally, the particular kind and source of benchmark is a decisive factor influencing the performance of tools, as especially visible on the parametric benchmark.

Threads to validity.
Our results must be taken with a grain of salt as the experiment contains an inherent room for error.

Although we tried to be as fair as possible, not knowing every tool intimately, the conversions between formats and kinds of automata, discussed at the start of <ref>, might have introduced biases into the experiment.

Tools are written in different languages and some have parameters which we might have used in sub-optimal way (we use the tools in their default settings), or, in the case of libraries, we could have used a sub-optimal combination of functions.

We also did not measure memory peaks, which could be especially interesting e.g. in when the tools are deployed on a cloud.

We are, however, confident that our main conclusions are well justified and the experiment gives a good overall picture. The entire experiment is available for anyone to challenge or improve upon [1].

[1]
Experiment replication package and additional material,

[2]
Jaltimpact, <https://github.com/cathiec/JAltImpact>

[3]
Abdulla, P.A., Atig, M.F., Chen, Y., Diep, B.P., Holík, L., Rezine, A.,
Rümmer, P.: Trau: SMT solver for string constraints. In: 2018 Formal
Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 -
November 2, 2018. pp. 1–5. IEEE (2018). 10.23919/FMCAD.2018.8602997,

[4]
Abdulla, P.A., Atig, M.F., Diep, B.P., Holík, L., Janku, P.: Chain-free
string constraints. In: Automated Technology for Verification and Analysis -
17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31,
2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp.
277–293. Springer (2019). 10.1007/978-3-030-31784-3_16,

[5]
Abdulla, P.A., Chen, Y.F., Holík, L., Mayr, R., Vojnar, T.: When simulation
meets antichains. In: TACAS'10. LNCS, vol. 6015, pp. 158–174. Springer

[6]
et al, A.M.: Brics automata library, <https://www.brics.dk/automaton/>

[7]
Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M.,
Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner,
M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and
industrial-strength smt solver. In: Tools and Algorithms for the Construction
and Analysis of Systems. pp. 415–442. Springer International Publishing,
Cham (2022)

[8]
Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories
Library (SMT-LIB). www.SMT-LIB.org (2016)

[9]
Berzish, Murphy: Z3str4: A Solver for Theories over Strings. Ph.D. thesis
(2021), <http://hdl.handle.net/10012/17102>

[10]
Blahoudek, F., Chen, Y.F., Chocholatý, D., Havlena, V., Holík, L.,
Lengál, O., Síč, J.: Word equations in synergy with regular
constraints. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Formal
Methods. pp. 403–423. Springer International Publishing, Cham (2023)

[11]
Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to
congruence. In: POPL'13. pp. 457–468. ACM Trans. Comput. Log. (2013)

[12]
Bouajjani, A., Habermehl, P., Holík, L., Touili, T., Vojnar, T.:
Antichain-based universality and inclusion testing over nondeterministic
finite tree automata. In: Implementation and Applications of Automata. pp.
57–67. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)

[13]
Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and
finite automata. In: Kirchner, H. (ed.) Trees in Algebra and Programming -
CAAP'96, 21st International Colloquium, Linköping, Sweden, April,
22-24, 1996, Proceedings. Lecture Notes in Computer Science, vol. 1059, pp.
30–43. Springer (1996). 10.1007/3-540-61064-2_27,

[14]
Bozzano, M., Cimatti, A., Fernandes Pires, A., Jones, D., Kimberly, G., Petri,
T., Robinson, R., Tonetta, S.: Formal design and safety analysis of AIR6110
wheel brake system. In: Kroening, D., Păsăreanu, C.S. (eds.)
Computer Aided Verification. pp. 518–535. Springer International Publishing,
Cham (2015)

[15]
Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of
counterexamples to induction. In: FMCAD'07. pp. 173–180. IEEE Computer
Society (2007)

[16]
Bradley, A.: Ic3 reference implementation: a short, simple, fairly competitive
implementation of ic3 (2015), <https://github.com/arbrad/IC3ref>

[17]
Brayton, R., Mishchenko, A.: Abc: An academic industrial-strength verification
tool. In: CAV'10. pp. 24–40. Springer (2010)

[18]
Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for
definite events. In: Proc. Symposium of Mathematical Theory of Automata. pp.
529–561 (1962)

[19]
Büchi, J.R.: On a decision method in restricted second order arithmetic.
In: Proc. of International Congress on Logic, Method, and Philosophy of
Science 1960. Stanford Univ. Press, Stanford (1962)

[20]
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A.,
Mover, S., Roveri, M., Tonetta, S.: The nuxmv symbolic model checker. In:
Computer Aided Verification. pp. 334–342. Springer International Publishing,
Cham (2014)

[21]
Cécé, G.: Foundation for a series of efficient simulation
algorithms. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. pp. 1–12. IEEE
Computer Society (2017). 10.1109/LICS.2017.8005069,

[22]
Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z.: What is decidable about
string constraints with the replaceall function. Proc. ACM Program. Lang.
2(POPL),  3:1–3:29 (2018). 10.1145/3158091,

[23]
Chen, T., Hague, M., Lin, A.W., Rümmer, P., Wu, Z.: Decision procedures
for path feasibility of string-manipulating programs with complex operations.
Proc. ACM Program. Lang.  3(POPL),  49:1–49:30 (2019).
10.1145/3290362, <https://doi.org/10.1145/3290362>

[24]
Cox, A.: Model Checking Regular Expressions.
url: <https://mosca19.github.io/slides/cox.pdf> (2019),
presented at MOSCA'19

[25]
Cox, A., Leasure, J.: Model checking regular language constraints. CoRR
abs/1708.09073 (2017)

[26]
D'Anthoni, L.: symbolicautomata,

[27]
D'Antoni, L., Kincaid, Z., Wang, F.: A symbolic decision procedure for symbolic
alternating finite automata. Electronic Notes in Theoretical Computer Science
336,  79–99 (2018).
the Thirty-third Conference on the Mathematical Foundations of Programming
Semantics (MFPS XXXIII)

[28]
D'Antoni, L., argus Veanes: Minimization of symbolic tree automata. In:
LICS'16. pp. 873–882. ACM Trans. Comput. Log. (2016)

[29]
D'Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proceedings of
the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
p. 541–553. POPL '14, Association for Computing Machinery, New York, NY,
USA (2014). 10.1145/2535838.2535849,

[30]
D'Antoni, L., Veanes, M.: The power of symbolic automata and transducers. In:
Computer Aided Verification. pp. 47–67. Springer International Publishing,
Cham (2017)

[31]
De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on
finite traces. In: IJCAI'13. pp. 854–860. ACM (2013)

[32]
De Wulf, M., Doyen, L., Maquet, N., Raskin, J.F.: Alaska. In: Cha, S.S., Choi,
J.Y., Kim, M., Lee, I., Viswanathan, M. (eds.) Automated Technology for
Verification and Analysis. pp. 240–245. Springer Berlin Heidelberg, Berlin,
Heidelberg (2008)

[33]
Doyen, L., Raskin, J.: Antichain algorithms for finite automata. In: Tools and
Algorithms for the Construction and Analysis of Systems, 16th International
Conference, TACAS 2010, Held as Part of the Joint European Conferences on
Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28,
2010. Proceedings. Lecture Notes in Computer Science, vol. 6015, pp. 2–22.
Springer (2010). 10.1007/978-3-642-12002-2_2,

[34]
Eén, N., Sörensson, N.: An extensible sat-solver. In: Theory and
Applications of Satisfiability Testing, 6th International Conference, SAT
2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers.
Lecture Notes in Computer Science, vol. 2919, pp. 502–518. Springer (2003).

[35]
Fu, C., Deng, Y., Jansen, D.N., Zhang, L.: On equivalence checking of
nondeterministic finite automata. In: Dependable Software Engineering.
Theories, Tools, and Applications - Third International Symposium, SETTA
2017, Changsha, China, October 23-25, 2017, Proceedings. Lecture Notes in
Computer Science, vol. 10606, pp. 216–231. Springer (2017).

[36]
Fu, C., Deng, Y., Jansen, D.N., Zhang, L.: On equivalence checking of
nondeterministic finite automata. In: Dependable Software Engineering.
Theories, Tools, and Applications. pp. 216–231. Springer International
Publishing, Cham (2017)

[37]
Gange, G., Navas, J.A., Stuckey, P.J., Søndergaard, H., Schachte, P.:
Unbounded model-checking with interpolation for regular language constraints.
In: TACAS 2013. Lecture Notes in Computer Science, vol. 7795, pp. 277–291.
Springer (2013). 10.1007/978-3-642-36742-7_20,

[38]
Ganty, P., Maquet, N., Raskin, J.: Fixed point guided abstraction refinement
for alternating automata. Theor. Comput. Sci.  411(38-39),
3444–3459 (2010)

[39]
Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., Rozier, K.Y.: Model checking
at scale: Automated air traffic control design space exploration. In:
Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification. pp. 3–22.
Springer International Publishing, Cham (2016)

[40]
Harding, A.: Symbolic strategy synthesis for games with LTL winning
conditions. Ph.D. thesis, University of Birmingham (2005)

[41]
Henriksen, J.G., Jensen, J.L., Jørgensen, M.E., Klarlund, N., Paige, R.,
Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In:
TACAS '95. LNCS, vol. 1019, pp. 89–110. Springer (1995)

[42]
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite
and infinite graphs. In: 36th Annual Symposium on Foundations of Computer
Science, Milwaukee, Wisconsin, USA, 23-25 October 1995. pp. 453–462. IEEE
Computer Society (1995). 10.1109/SFCS.1995.492576,

[43]
Hoder, K., Bjørner, N.: Generalized property directed reachability. In:
SAT'12. LNCS, vol. 7317, pp. 157–171. Springer (2012)

[44]
Holík, L., Janků, P., Lin, A.W., Rümmer, P., Vojnar, T.:
String constraints with concatenation and transducers solved efficiently.
Proc. ACM Program. Lang.  2(POPL) (2018)

[45]
Holík, L., Lengál, O., Síč, J., Veanes, M., Vojnar, T.:
Simulation algorithms for symbolic automata. In: Lahiri, S.K., Wang, C.
(eds.) Automated Technology for Verification and Analysis. pp. 109–125.
Springer International Publishing, Cham (2018)

[46]
Holík, L., Lengál, O., Simácek, J., Vojnar, T.: Efficient
inclusion checking on explicit and semi-symbolic tree automata. In: Bultan,
T., Hsiung, P. (eds.) Automated Technology for Verification and Analysis, 9th
International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011.
Proceedings. Lecture Notes in Computer Science, vol. 6996, pp. 243–258.
Springer (2011). 10.1007/978-3-642-24372-1_18,

[47]
Holík, L., Šimáček, J.: Optimizing an lts-simulation algorithm.
Computing and Informatics  2010(7),  1337–1348 (2010),

[48]
Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over
regular languages. In: Proceedings of the 30th ACM SIGPLAN Conference on
Programming Language Design and Implementation. p. 188–198. PLDI '09,
Association for Computing Machinery, New York, NY, USA (2009).
10.1145/1542476.1542498, <https://doi.org/10.1145/1542476.1542498>

[49]
Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite
automaton. Tech. rep., Stanford, CA, USA (1971)

[50]
Huffman, D.: The synthesis of sequential switching circuits. Journal of the
Franklin Institute  257(3),  161–190 (1954).

[51]
Ilie, L., Navarro, G., Yu, S.: On NFA Reductions, pp. 112–124. Springer Berlin
Heidelberg, Berlin, Heidelberg (2004). 10.1007/978-3-540-27812-2_11,

[52]
Iosif, R., Xu, X.: Abstraction refinement for emptiness checking of alternating
data automata. In: TACAS'18. pp. 93–111. Springer (2018)

[53]
Lengál, O., Simácek, J., Vojnar, T.: VATA: A library for
efficient manipulation of non-deterministic tree automata. In: Tools and
Algorithms for the Construction and Analysis of Systems - 18th International
Conference, TACAS 2012, Held as Part of the European Joint Conferences on
Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 -
April 1, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7214, pp.
79–94. Springer (2012). 10.1007/978-3-642-28756-5_7,

[54]
Li, J., Pu, G., Zhang, Y., Vardi, M.Y., Rozier, K.Y.: SAT-based explicit
LTLf satisfiability checking. Artificial Intelligence  289,
103369 (2020). https://doi.org/10.1016/j.artint.2020.103369,

[55]
Lutterkort, D.: libfa, <https://augeas.net/libfa/>

[56]
McMillan, K.L.: Interpolation and sat-based model checking. In: Computer Aided
Verification. pp. 1–13. Springer Berlin Heidelberg, Berlin, Heidelberg

[57]
McMillan, K.L.: Lazy abstraction with interpolants. In: CAV'06. LNCS,
vol. 4144, pp. 123–136. Springer (2006)

[58]
Moore, E.F.: Gedanken-Experiments on Sequential Machines, pp. 129–154.
Princeton University Press, Princeton (1956).

[59]
de Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Tools and
Algorithms for the Construction and Analysis of Systems. pp. 337–340.
Springer Berlin Heidelberg, Berlin, Heidelberg (2008)

[60]
Nötzli, A., Reynolds, A., Barbosa, H., Barrett, C., Tinelli, C.: Even
faster conflicts and lazier reductions for string solvers. In: Computer
Aided Verification. pp. 205–226. Springer International Publishing, Cham

[61]
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on
Computing  16(6),  973–989 (1987). 10.1137/0216062,

[62]
Ranzato, F., Tapparo, F.: An efficient simulation algorithm based on abstract
interpretation. Information and Computation  208,  1–22 (2010)

[63]
RegExLib.com: The Internet's first Regular Expression Library.

[64]
Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: SPIN'07. pp.
149–167. Springer (2007)

[65]
Stanford, C., Veanes, M., Bjørner, N.: Symbolic boolean derivatives for
efficiently solving extended regular expression constraints. In: Proceedings
of the 42nd ACM SIGPLAN International Conference on Programming Language
Design and Implementation. p. 620–635. PLDI 2021, Association for Computing
Machinery, New York, NY, USA (2021). 10.1145/3453483.3454066,

[66]
Stanford, C., Veanes, M., Bjørner, N.S.: Symbolic boolean derivatives for
efficiently solving extended regular expression constraints. In: PLDI '21.
pp. 620–635. ACM (2021). 10.1145/3453483.3454066,

[67]
Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata
constructions. In: Logic for Programming, Artificial Intelligence, and
Reasoning. pp. 396–411. Springer Berlin Heidelberg, Berlin, Heidelberg

[68]
Valmari, A.: Simple bisimilarity minimization in o(m log n) time. Fundam.
Informaticae  105(3),  319–339 (2010). 10.3233/FI-2010-369,

[69]
Vargovčík, P., Holík, L.: Simplifying alternating automata for
emptiness testing. In: Programming Languages and Systems. pp. 243–264.
Springer International Publishing, Cham (2021)

[70]
Veanes, M.: <https://github.com/AutomataDotNet>

[71]
Veanes, M., de Halleux, P., Tillmann, N.: Rex: Symbolic regular expression
explorer. In: Third International Conference on Software Testing,
Verification and Validation, ICST 2010, Paris, France, April 7-9, 2010. pp.
498–507. IEEE Computer Society (2010). 10.1109/ICST.2010.15,

[72]
Wang, H., Tsai, T., Lin, C., Yu, F., Jiang, J.R.: String analysis via automata
manipulation with logic circuit representation. In: CAV'16. LNCS,
vol. 9779, pp. 241–260. Springer (2016)

[73]
Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger
arithmetic constraints (extended abstract). In: Mycroft, A. (ed.) Static
Analysis, Second International Symposium, SAS'95, Glasgow, UK, September
25-27, 1995, Proceedings. Lecture Notes in Computer Science, vol. 983, pp.
21–32. Springer (1995). 10.1007/3-540-60360-3_30,

[74]
Wulf, M.D., Doyen, L., Henzinger, T.A., Raskin, J.: Antichains: A new
algorithm for checking universality of finite automata. In: CAV'06. LNCS,
vol. 4144, pp. 17–30. Springer (2006)

§ ONE TO ONE COMPARISON OF THE BEST TOOLS

Further, for each benchmark shown on <ref>, we have selected three best-performing tools
based on the rate of timeouts or their average times. We show their
comparison in Fig. <ref> in the form of scatter-plots. The triplets are distinguished by the color of the points and the position of each triplet corresponds to the position of the benchmark in <ref>.

Scatter-plots comparing the best tools one to one, by benchmark.


# Performance of a fine-sampling electromagnetic calorimeter prototype in the
energy range from 1 to 19 GeV

Yu.V.Kharlov  P.A.Semenov  Yu.A.Matulenko  O.P.Yushchenko  Yu.I.Arestov
G.I.Britvich  S.K.Chernichenko  Yu.M.Goncharenko  A.M.Davidenko
A.A.Derevschikov  A.S.Konstantinov  V.A.Kormilitsyn  V.I.Kravtsov  Yu.M.Melnik
A.P.Meschanin  N.G.Minaev  V.V.Mochalov  D.A.Morozov  A.V.Ryazantsev
I.V.Shein  A.P.Soldatov  L.F.Soloviev  A.V.Soukhikh  A.N.Vasiliev  M.N.Ukhanov
V.G.Vasilchenko  A.E.Yakutin corresponding author<EMAIL_ADDRESS>Institute for High Energy Physics, Protvino, Russia

###### Abstract

The fine-sampling electromagnetic calorimeter prototype has been
experimentally tested using the $1-19$ GeV/$c$ tagged beams of negatively
charged particles at the U70 accelerator at IHEP, Protvino. The energy
resolution measured by electrons is $\Delta{E}/E=2.8\%/\sqrt{E}\oplus 1.3\%$.
The position resolution for electrons is $\Delta{x}=3.1\oplus 15.4/\sqrt{E}$
mm in the center of the cell. The lateral non-uniformity of the prototype
energy response to electrons and MIPs has turned out to be negligible.
Obtained experimental results are in a good agreement with Monte-Carlo
simulations.

###### keywords:

Electromagnetic calorimeter , fine sampling , plastic scintillators , energy
resolution

###### PACS:

00.11.–aa

, , , , , , , , , , , , , , , , , , , , , , , , , , ††thanks: deceased

## Introduction

Electromagnetic calorimeters are based on the total energy deposition of
photons and electrons in the active medium of detectors. Energy deposited by
secondary particles of an electromagnetic shower is detected either as a
Cherenkov radiation of electrons and positrons, like in the lead-glass
calorimeters [1], or as a scintillation light emitted by the active medium
[2]. Sampling calorimeters constructed from alternating layers of organic
scintillator and heavy absorber, have been used in high energy physics over
last tens of years [3]. The sampling of such calorimeters is determined by the
required lateral size of electromagnetic shower, expressed by a Molière radius
$R_{M}$, and the light yield provided by scintillator plates. Scintillation
light is absorbed, re-emitted and transported to a photodetector by wave-
length shifting (WLS) optical fibers penetrating through the calorimeter
modules longitudinally (along the beam direction). Typical stochastic term of
the energy resolution of all large electromagnetic calorimeters of the
sampling type was about 10% [4, 5, 6].

Recently the improved electromagnetic calorimeter modules with a very fine
sampling have been developed for KOPIO experiment at BNL [7]. The energy
resolution of these modules, measured with photons of energy $220-350$ MeV,
was about $3\%/\sqrt{E~{}\mbox{(GeV)}}$ [8]. Details of the improved modules
tested in the energy range of $50-1000$ MeV, including mechanical
construction, selection of WLS fibers and photodetectors as well as
development of a new scintillator with improved optical and mechanical
properties are described in [9].

Similar high-performance electromagnetic calorimeters are now being considered
for PANDA and CBM experiments [10, 11] at the future FAIR facility, which is
under construction at GSI, Darmstadt in Germany. The both fixed target
experimental setups require an ability to measure single photons, $\pi^{0}$’s
as well as $\eta$’s in the wide energy range with excellent energy and
position resolutions. Fine-sampling calorimeters, not very expensive and
meanwhile covering wide areas like 3 m2 in PANDA and 100 m2 in CBM, were
chosen to meet the requirements. The energy range in PANDA and CBM experiments
will be extended up to 15 and 35 GeV, respectively. It is essential for these
projects to study parameters of a fine-sampling calorimeter in the wide energy
region, significantly wider than the one with the existing data (only up to 1
GeV).

In this paper, we describe a fine-sampling electromagnetic calorimeter
prototype with lead absorber plates, which thickness is significantly smaller
than radiation length $X_{0}$ of lead. Such a small thickness of the absorber
layers results in a small interaction probability of the secondary shower
particles. The design of this prototype is close to the KOPIO one including
the same lateral size of cells. The results of miscellaneous studies of the
prototype in the energy range from 1 to 19 GeV are presented in this paper.

##  1 Design of the modules

The electromagnetic calorimeter modules with fine sampling were constructed at
IHEP, Protvino. A module design was based on the electromagnetic calorimeter
for the KOPIO experiment, with additional modification to high-energy range.
Details of the mechanical design of the modules can be found in [9], but a few
modifications were applied to the prototype under study. The KOPIO experiment
was aimed to low-energy photons, and the total radiation length $16X_{0}$ was
enough for their purposes. The current prototype is being proposed for CBM and
PANDA, where the photon energy extends up to 30 GeV, and the requirement to
provide the total radiation length of $20X_{0}$ was put to the design. The
modules were assembled from 380 alternating layers of lead and scintillator
plates. Lead plates were doped by 3% of antimony to improve their rigidity.
Scintillator plates were made of polystyrene doped by 1.5% of paraterphenile
and 0.04% of POPOP. Scintillator was manufactured at the scintillator workshop
of IHEP with the use of molding technology. The physical properties of the
modules are presented in Table 1.

lead plate thickness | 0.275 mm
---|---
scintillator plate thickness | 1.5 mm
number of layers | 380
effective radiation length, $X_{0}$ | 34 mm
total radiation length | $20X_{0}$
effective Moliere radius, $R_{M}$ | 59 mm
module size | $110\times 110\times 675~{}\mbox{mm}^{3}$
module weight | 18 kg
Table 1: Physical properties of the module.

The WLS optical fibers BCF-91A with a diameter of 1.2 mm were used in the
modules. Each fiber penetrated through the module along its longitudinal axis
twice, forming a loop at the face end of the module. Radius of the loop was 28
mm. In total 72 such looped fibers formed a grid of $12\times 12$ fibers per
module with spacing of 9.3 mm. All 144 fiber ends were assembled into a bundle
of a diameter about 10 mm, glued, cut, polished and attached to the
photodetector at the downstream end of the module. No optical grease was used
to provide an optical contact between the bundle cap and the photodetector,
thus there was a natural air gap between them. A photomutiplier Hamamatsu
R5800 was used as a photodetector for the prototype. The diameter of the
photocathode is 25.4 mm, the number of dynodes is 10, the applied high voltage
was about 1100 V. Each photomultiplier was monitored by LED light guided to
the photocathodes by a clear polystyrene fiber.

##  2 Experimental setup for the prototype studies

The prototype of electromagnetic calorimeter consisted of 9 modules assembled
into $3\times 3$ matrix installed on the remotely controlled $x,y$-moving
support positioned the prototype across the beam with a precision of 0.4 mm.
The beam line 2B of the U-70 accelerator was used to study performance of the
calorimeter prototype. The secondary beam of negatively charged particles of
momenta from 1 to 19 GeV/$c$ contained more than 70% of electrons mixed with
muons and hadrons (mainly $\pi^{-}$ and $K^{-}$). Particle identification was
not available at this beam line. A momentum spread of the beam was at the
level of 1 to 5% at energies from 45 to 1 GeV, respectively. However, the
momentum tagging system[12] gave a beam momentum resolution from 0.13% to 2%
in the same momentum range. The tagging system illustrated in Fig.1 consisted
of the dipole magnet M and 4 sets of 2-coordinate drift chambers DC1–DC4. A
bending angle of the magnet was 55 mrad.

Figure 1: Beam tagging system for the calorimeter prototype studies.

A trigger of the experimental setup used the coincidence of scintillator
counters S1, S2 and S3 installed upstream before the first drift chamber DC1,
and a scintillator counter S4 installed after the last drift chamber DC4 in
front of the calorimeter prototype ECAL.

An amplitude out of each prototype cell was measured by the 15-bit charge
sensitive ADC modules LRS2285 over 150-ns gate with a sensitivity of 30
fC/count. To read out time information from the drift chamber stations TDC,
the LRS3377 CAMAC modules were used. Data acquisition system included a couple
of crates with ADC and TDC modules as well as control modules to synchronize a
read-out process. VME crate with CAMAC parallel branch driver and PCI-VME
bridge linked all the electronics into the complete system. Detailed
description of the data acquisition system and front-end electronics can be
found in [13].

##  3 Monte Carlo simulations

The relevant simulation tools were developed. These tools, at the first stage,
are intended mainly for cross-check of experimental results as well as for
tuning of the reconstruction algorithms.

Having proved the consistency of Monte Carlo and the real data, we plan to use
these tools for further optimization of module design and reconstruction
algorithms to provide better performance of the photons and $\pi^{0}$’s
reconstruction. Simulation studies were performed with GEANT3 as a Monte Carlo
engine with detailed description of materials and module geometry.

The developing shower produces light which originates from two different
sources:

  * •

scintillation in plastic plates due to continuous energy losses when charged
particles pass through the active calorimeter material,

  * •

Cherenkov radiation when charged particles pass through the WLS fibers.

The simplified technique consists of counting energy deposition in the active
material (with some corrections to take into account light attenuation in the
fibers) and ignoring Cherenkov radiation inside the fibers. This method is
very fast while can not reproduce all details of the calorimeter response such
as non-uniformity due to fibers and cell borders.

For these studies, the detailed light propagation was applied taking into
account the optical properties of the materials, internal reflections at plate
borders, light capture by fibers with double cladding and the Cherenkov light
production and propagation inside the fibers. It was assumed that attenuation
length was 70 cm in the scintillator and 400 cm in the fiber, scintillator
refraction index is 1.59, total internal reflection efficiency at large
scintillator faces is 0.97 and reflection of diffusion type was assumed at
side scintillator faces with the same probability. The mean deposited energy
for one optical photon production in the scintillator was assumed to be 100 eV
and the Cherenkov photons were generated by GEANT.

##  4 Results

###  4.1 Calibration of the modules

The modules were calibrated by a 19-GeV/$c$ beam. Each module was exposed to
the beam using an $x,y$-moving support. The energy spectrum from one module
(Fig.2, left plot)

Figure 2: Energy deposited by the 19-GeV/c beam in one module.

shows a peak at 19 GeV corresponding to the energy deposited by electrons.
Another peak at low energies is due to minimum ionizing particles (MIP). A
broad distribution in the energy specrtum between the two peaks is due to
hadrons. Calibration of the modules was possible using both electron and MIP
signals, but the best relative calibration coefficients were found by
equalizing MIP signals, while the absolute calibration was obtained by setting
the total measured energy in the $3\times 3$ matrix to 19 GeV. Events when
only one module has an energy above the threshold of 100 MeV were selected for
the MIP calibration. The energy distribution around the MIP peak (Fig.2, right
plot) has two contributions. One is caused by the Landau distribution of
ionization energy loss, and another one is due to the finite energy resolution
of the calorimeter at low energy. The MIP peak was fitted by the Gaussian, and
the mean value of the fitting function served for the relative calibration.

###  4.2 Energy and position resolution

After some dedicated calibration runs, when each module was exposed to the
19-GeV/$c$ beam, the ECAL prototype was fixed so that the beam hit the central
module. It was exposed to beam at momenta 1, 2, 3.5, 5, 7, 10, 14 and 19
GeV/$c$. For each beam momentum, magnetic field in the spectrometric magnet M
was adjusted to provide the same bending angle of the beam. The momentum of
the beam particle $p$ was measured by the magnetic spectrometer, and the
energy $E$ measured in the calorimeter prototype is linearly correlated with
the momentum $p$, as illustrated by Fig.3.

Figure 3: Correlation between the energy measured in the calorimeter and the
beam momentum measured in the magnetic spectrometer.

Therefore, in order to obtain a true energy resolution, the measured energy
should be corrected by the beam momentum, or the energy resolution can be
represented by the width of the distribution of the $E/p$ ratio (Fig.4).

Figure 4: Ratio of the energy $E$ measured in the calorimeter to the momentum
$p$ measured by the magnetic spectrometer at 19 GeV/$c$.

The energy resolution is obtained from the Gaussian fit of the right peak
around $E/p=1$. The energy resolution $\Delta E/E$ measured by electrons at
energies from 1 to 19 GeV are shown in Fig.5.

Figure 5: Measured energy resolution.

The black bullets represent the experimentally measured points. The solid
curve is a result of a fit of these experimental points, and the dashed curve
is a result of a fit of the Monte Carlo points. The fitting function can be
represented by the equation (1):

$\frac{\Delta
E}{E}=\sqrt{\left(\frac{a}{E}\right)^{2}+\frac{b^{2}}{E}+c^{2}},$ (1)

where parameters $a$, $b$ and $c$ for the experimental and Monte Carlo fits
are shown in Table 2.

|  $a$, $10^{-2}$ GeV |  $b$, $10^{-2}$ GeV1/2 |  $c$, $10^{-2}$
---|---|---|---
Experimental fit | $3.51\pm 0.28$ | $2.83\pm 0.22$ | $1.30\pm 0.04$
Monte Carlo fit | $3.33\pm 0.12$ | $3.07\pm 0.08$ | $1.24\pm 0.02$
Table 2: Fitting function parameters for the energy resolution.

A linear term $a$ of the energy resolution expansion is determined by a beam
spread rather than the calorimeter properties. As it was shown in previous
studies performed at this 2B beam channel [13], the main contribution to this
term comes from the electronics noise and the multiple scattering of the beam
particles on the beam pipe flanges and the drift chambers. The beam momentum
spread was introduced into Monte-Carlo simulations in order to fully reproduce
the experimental conditions. A simulated energy resolution is shown by the red
dashed line in Fig.5. The dotted line at this plot is a difference between the
experimental data fit and the Monte Carlo fit multiplied by 10. Thus a
deviation of the experimental result from the simulation one is less than
0.04%. The energy resolution obtained in Monte Carlo is in a good agreement
with the experimental data.

Position resolution has been determined by a comparison of the exact impact
coordinate of the beam particle, measured by the last drift chamber DC4, and
the center-of-gravity of electromagnetic shower developed in the calorimeter
prototype. Fig.6 shows a dependence of the measured coordinate $x_{\rm rec}$
on the true one $x_{0}$.

Figure 6: Center of gravity of the electromagnetic shower $X_{\rm rec}$ vs the
impact coordinate of the electron $x_{0}$.

A position resolution in the middle of the module is shown in Fig.7, where the
bullets represent the experimentally measured points, the solid curve is a
result of the experimental points fit, and and the red dashed curve is a
result of Monte Carlo points fit.

Figure 7: Measured position resolution.

The data were fitted by the function (2)

$\Delta x=\sqrt{a^{2}+\frac{b^{2}}{E}},$ (2)

where parameters $a$ and $b$ are given in Table 3.

|  $a$, mm |  $b$, mm GeV1/2
---|---|---
Experimental fit | $3.09\pm 0.16$ | $15.4\pm 0.3$
Monte Carlo fit | $3.40\pm 0.14$ | $14.5\pm 0.3$
Table 3: Fitting function parameters for the position resolution.

The dotted curve in Fig.7 stands for a deviation of the experimental data fit
results from the Monte Carlo fit results, which are consistent within 5% of
precision.

###  4.3 Lateral non-uniformity

Due to various mechanical inhomogeneities of the prototype one can expect to
observe the dependence of the energy $E$ deposited in the calorimeter on the
hit coordinates $(x,y)$. The “hot” zones, if any, should be seen at the WLS
fiber positions, at the steel strings, and at the boundaries between the
modules. A possible lateral non-uniformity of the energy response was studied
with the data collected in the 19-GeV/$c$-run. The last drift chamber DC4 was
used to measure the coordinate of the beam particle incidence onto the
calorimeter surface. As the beam contained several particle species which
interact differently with the calorimeter medium (see Fig.2), the mean
deposited energy was measured as a function of $(x,y$) for two energy
intervals, $E<0.5$ GeV and $16<E<22$ GeV corresponding to the MIP peak and
that of the electromagnetic shower, respectively. The relative energy response
profile for electrons vs $y$-coordinate at fixed $x$ is shown in Fig.8.

Figure 8: Relative energy response profile vs $y$-coordinate at fixed $x$.

As one can see, the fluctuations of the energy response do not exceed 1%, that
is no lateral non-uniformity of the energy response is observed within the
available statistics.

###  4.4 Light output measurement

Light output of the prototype modules, expressed as a number of photoelectrons
$N_{\rm p.e.}$, was evaluated with the highly stable LED pulses [14].
Fluctuations of the measured amplitude $A$ is determined by statistical
fluctuations of the number of detected photoelectrons and by fluctuations of
the photomultiplier gain $M$ [15]:

$\left(\frac{\sigma_{A}}{A}\right)^{2}=\frac{1}{N_{\rm
p.e.}}\left[1+\left(\frac{\sigma_{M}}{M}\right)^{2}\right].$ (3)

The gain fluctuation can be defined through the secondary emission factor of
the first dynode $\delta_{1}$ and the secondary emission factor of other
dynodes $\delta$:

$\left(\frac{\sigma_{M}}{M}\right)^{2}=\frac{\delta}{\delta_{1}}\cdot\frac{1}{\delta-1}.$
(4)

The total gain of the 10-dynode photomultiplier R5800 was equal to $10^{6}$
for the applied high voltage 1100 V, and the potential of the first dynode was
boosted to increase the secondary emission factor $\delta_{1}$ to
approximately 5. Thus, one can obtain the emission factor $\delta=3.9$ and the
equation (3) is derived to the number of the detected photoelectrons as a
function of the relative amplitude width:

$N_{\rm p.e.}\approx\frac{1.3}{(\sigma_{A}/A)^{2}}.$ (5)

A set of runs with six different LED amplitudes has been carries out. A
dependence of the number of photoelectrons on the LED amplitude for one cell
and a distribution of the light output for all 9 cells are shown in Fig.9.

Figure 9: Light output $N_{\rm p.e.}$ vs the LED amplitude for 1 modules
(left) and the light output distribution of all 9 modules (right).

These plots were fitted by the linear function, which slope represents the
number of photoelectrons per one ADC count. Being divided by the calibration
coefficient, one can obtain that the number of photoelectrons detected by the
the prototype modules is $4.8\pm 0.6$ p.e./MeV.

## Conclusion

The measurements of energy and position resolutions of the electromagnetic
calorimeter prototype of fine-sampling type for the PANDA and CBM experiments
at FAIR at Darmstadt have been carried out at the IHEP test beam facility at
the Protvino 70 GeV accelerator. The prototype consisted of a $3\times 3$
array with the cell sizes of $11\times 11$ cm2. Each cell had 380 layers with
1.5 mm scintillator and 0.3 mm lead. Scintillation light was collected by
optical fibers penetrating through the modules longitudinally along the beam
direction. The prototype was designed and assembled at the IHEP scintillator
workshop.

Studies were made in the electron beam energy range from 1 to 19 GeV. The
energy tagged has allowed us to measure the stochastic term in energy
resolution as $(2.8\pm 0.2)\times 10^{-2}~{}\mbox{GeV}^{1/2}$ which is
consistent with the one measured at BNL for the KOPIO project in the energy
range from 0.05 GeV to 1 GeV. Taking into account the effect of light
transmission in scintillator tiles and WLS fibers, photo statistics as well as
noise of the entire electronic chain resulted in good agreement between the
measured energy resolutions and the GEANT Monte Carlo simulations.

The stochastic term in the dependence of position resolution on energy in our
measurements is about $15.4\pm 0.3$ mm GeV1/2 which is in agreement with Monte
Carlo simulations. For 10 GeV electrons position resolution is 6 mm in the
center of the cell, and is 3 mm at a boundary between two cells.

The non-uniformity of the energy response of the prototype due to holes for
straight fibers studied with the use of electrons and MIPs has turned out to
be negligible. Monte-Carlo simulations are in a good agreement with the
obtained experimental results.

The characteristics experimentally determined for our calorimeter prototype
well meet the design goals of the PANDA and CBM experiments. However, the
final conclusion on lateral sizes of the cells as well as on Shashlyk
longitudinal sampling structure could be done only after studies of
reconstruction efficiency of $\pi^{0}$-mesons of different energies.

## Acknowledgment

This work was partially supported by the Rosatom grant with Ref. No.
N.4d.47.03.08.118, by the INTAS grants with Ref. No. 06-1000012-8845 and
06-1000012-8914, and by the RFBR grant 05-02-08009.

## References

  * [1] D.Alde et al., Nucl.Instr.Meth., A240(1985),343.
  * [2] O.V.Buyanov et al., Nucl.Instr.Meth., A349(1994),62.
  * [3] M.Beddo et al., The STAR Barrel Electromagnetic Calorimeter. Nucl.Instr.Meth. A499 (2003) 725-739
  * [4] “PHENIX calorimetrer”, L. Aphecetche et al., NIM A499 521-536 (2003)
  * [5] HERA-B collaboration, HERA-B Design Report, DESY-PRC 95/01 January 1995.
  * [6] LHCb Calorimeters Technical Design Report, CERN/LHCC 2000-0036, September 2000.
  * [7] I.-H.Chiang et al., AGS Experimental Proposal 926, 1996\.
  * [8] G.S.Atoian et al., Prepared for 11th International Conference on Calorimetry in High-Energy Physics (Calor 2004), Perugia, Italy, 28 Mar – 2 Apr 2004.
  * [9] G.S.Atoian et al., NIM A 584 (2008) 291.
  * [10] CBM technical status report, GSI, DOC-2005-Feb-447 (2005)
  * [11] M.Kotulla et al., Technical Progress Report PANDA ”Strong Interaction Studies with Antiprotons”, February 2005.
  * [12] V.A.Batarin et al., Development of a Momentum Determined Electron Beam in the 1-45 GeV Range, Nucl.Instr.Meth. A510 (2003) 211–218
  * [13] V.A.Batarin et al., Precision Measurement of Energy and Position Resolutions of the BTeV Electromagnetic Calorimeter Prototype, Nucl. Instrum. and Meth. A510(2003), 248–261.
  * [14] V.A.Batarin et al., LED monitoring system for the BTeV lead tungstate crystal calorimeter prototype. Nucl. Instrum. and Meth. A534(2004), 486–495.
  * [15] E.Kowalski, Nuclear Electronics. Springer, Berlin (1970).