\begin{document}

\date{\today} 

\title{Language Inclusion for \Finite Prime Event Structures
	hanks{
This work has received funding from the Electronic Component
Systems for European Leadership Joint Undertaking under grant
agreement No 737459 (project Productive4.0), which receives support from the European Union Horizon 2020
research and innovation program and Germany, Austria, France,
Czech Republic, Netherlands, Belgium, Spain, Greece, Sweden,
Italy, Ireland, Poland, Hungary, Portugal, Denmark, Finland, Luxembourg, Norway, Turkey, 
from the by ECSEL Joint Undertaking
under the project H2020 737469 AutoDrive --- Advancing failaware,
fail-safe, and fail-operational electronic components, systems, and
architectures for fully automated driving to make future mobility
safer, affordable, and end-user acceptable,
from the LogiCS doctoral program W1255-N23 of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund
(WWTF) through the projects Heisenbugs project VRG11-005.
}

\begin{abstract}

We study the problem of language inclusion between finite, labeled prime event structures.

Prime event structures are a formalism to compactly represent concurrent behavior of discrete systems.

A labeled prime event structure induces a language of sequences of labels produced by the represented system.

We study the problem of deciding inclusion and membership for languages encoded by finite prime event structures and provide complexity results for both problems.

We provide a family of examples where prime event structures are exponentially more succinct than formalisms that do not take concurrency into account. 
We provide a decision algorithm for language inclusion that exploits this succinctness.

Furthermore, we provide an implementation of the algorithm and an evaluation on a series of benchmarks.

Finally, we demonstrate how our results can be applied to mutation-based test case generation.

\keywords{Event Structures, Language Inclusion, Concurrency, Mutation-based Test Case Generation}
\end{abstract}

$\cdot 10^3$ection{Introduction}

Language inclusion is a fundamental problem in computer science which
arises in numerous application domains. In its most familiar form
the problem is instantiated with regular languages and finite
automata \cite{automata_book}; an incarnation frequently occurring
in formal verification and model checking is language inclusion
(and intersection, respectively) for $\omega$-regular languages
and B\"uchi automata \cite[Chapter 7]{modelchecking_book}.
In the latter application, the goal is to check whether a
transition system conforms to a specification given in
linear temporal logic. 
One challenge arising in automata-based model checking is that the
verification of concurrent systems relies on the explicit construction 
of a product automaton whose size can be exponential
in the number of processes. Partial Order Reduction 
(POR, see \cite{Valmari1989,Godefroid1996} and
\cite[Chapter 12]{modelchecking_book}, for instance)
addresses this problem by exploiting independence between
transitions to avoid the construction of the full
product automaton: the reduction identifies
equivalence classes of words in the language (i.e., executions)
obtained by reordering commutative edges/transitions \cite{Mazurkiewicz1986}
and restricts the exploration to representative members of these classes. 
POR in its simplest form can be used to check reachability and deadlock problems; 
for checking temporal logic properties only transitions
whose labels are ``invisible'' to the property are assumed to be
independent \cite[Chapter 12]{modelchecking_book}.
This renders the approach impractical for language
inclusion if the alphabets of both languages are the same, e.g., when
checking whether a modification is language-preserving --
a question arising in the applications that motivated our work (see below).

In this paper, we focus on language inclusion for finite, labeled prime
event structures, a representation of bounded executions of
concurrent systems in which dependence (and independence) of
transitions is made explicit.

This representation can be exponentially more
succinct than finite automata, as shown in \cref{sec:algorithm}:
there are event structures with $n$ events, 
such that the smallest NFA expressing the same language has at
least $2^n$ states.

We provide an analysis of the computational complexity of checking
language membership as well as inclusion between two event structures,
showing that the former is NP-complete and the latter is $\Pi^p_2$-complete
(\cref{sec:complexity}).
\review{
While a similar results to the former was proven earlier for
trace languages \cite{bertoni1989membership}, to the best of our knowledge, 
the latter result is novel even in the related domains of bounded trace languages and bounded labeled Petri nets.

}

\review{Besides showing the complexity of the decision problems, 
we provide a practical decision algorithm for solving event structure language inclusion in \cref{sec:algorithm}.}
By finding suitable embeddings of one event structure in another, the algorithm
determines whether the language of the former is included in the language
of the latter. The algorithm iteratively refines the event structure
whenever two labels occur unordered in the former structure 
but ordered in the latter. Moreover, the algorithm can provide
counterexamples to inclusion encoded as event
structures representing words that occur in the former language but
not in the latter.

\Cref{sec:experiments} provides a qualitative analysis of our
representation and an experimental evaluation that highlights
advantages and disadvantages of event structures
in comparison to an automaton-based representation (for which
language inclusion is PSPACE-complete). 

\review{Our inclusion algorithm decides whether two systems, represented as
event structures, have the same behavior in terms of bounded
words over a common vocabulary.} This scenario arises in a range of
applications: refinement or model checking, where an implementation is
compared against a specification; upgrade or regression checking,
where a fixed version of a software is compared against the original
version; or mutation-based test case generation, where a small
modification (or bug) is introduced in code to obtain a ``mutant''
of the original program, and the counterexample to inclusion then
represents a test case which discriminates between mutant and
original. 

We use the latter scenario, which motivated our research on
language inclusion, as an exemplary application
of our approach in our experiments (\cref{sec:experiments}).

\endinput

\afsays{copy - pasted the applications part here:}

$\cdot 10^3$ubsection{Other uses}

We envision numerous other applications that we did not investigate in depth. 

\paragraph*{Regression checking and version comparison}

Since many concurrent system can be concisely represented as an event structure comparison of these structures makes sense to find semantic differences between two versions of a software. This can, for example, be used to find regressions if between two versions the observable behavior of the system changed.

\paragraph*{Bounded model checking}

Model checking basically involves checking if a system exhibits the same behavior as a model. 
It differs from MBMT in that for MBMT tests are generated from the model and later run against the implementation. 
For model-checking, the implementation has to exist. 
Therefore one event system would be built from the model and one from the implementation. 
The language inclusion check can then verify that the implementation operates within the specification of the model.

\begin{figure}
\caption{Event structure comparison algorithm in context}
\label{fig:overview}
\end{figure}

In this work, we present a method to compare labeled event structures.
We use this technique to efficiently detect behavioral inconsistencies between event structures obtained from different sources.
We assume that the two sources label events with a common vocabulary, but might order events differently and assign independence of events differently.
Our method checks whether the two event structures allow the same interleavings of such event labels.

The main advantage of this technique is to find such inconsistencies without needing to check every single interleaving of events separately.
In case the systems includes concurrent events, i.e. events that happen independently of each other, this results in an exponential speedup.

We use this technique in the context of mutation driven, model based test case generation.
A model of a system is described as a labeled event structure.
Likewise, a mutated version of the model is described as a labeled event structure.
By mutated version, we mean a version that is obtained from the original by introducing a small, syntactic alternation.
The two resulting event structures are compared for interleaving equivalence.
In case we find that they are found to be inconsistent, we can obtain a test case from the result.

For example, a simple model of a train station might have two tracks, where only one track can be active at the same time.
Furthermore, there is a button to switch back and forth between the tracks, and a monitor showing which track currently is active.
The model allows to observe the monitor and whether the tracks are currently being switched.
The model does not specify an order whether first the track switch or the monitor value is observed.

One implementation of the system might order the events, such that always first the track switch is observed and the monitor value is only shown when the switch is over.
Such an implementation is conformant according to our check.
Another implementation might first show the track on the monitor, then make the track switch observable, and then show the final track on the monitor.
This implementation is not conformant according to our check.

Figure \ref{fig:overview} shows the event structure comparison in context of its use cases.
Event structures can be obtained from different sources, such as concurrent programs, abstract models or specifications, and abstract Petri nets.
We want to compare such event structures to counterparts of it.
Such counterparts could be different versions of the same artifact, or an artifact that was obtained by introducing faults to it.

Our comparison algorithm can efficiently decide, whether the two event structures represent the same behavior in terms of traces over a common language.
The main advantage of our algorithm is that it can decide this without the need to go over each trace individually, but infer (non)- conformance based on the structure of the event structures.
As such, we obtain an exponential speedup over a trace based comparison in certain cases.

The result of the comparison algorithm can be interpreted in different ways.
First of all, it is a verdict of (non)- conformance of the two event structures.
In addition, for non-conformant event structures, we obtain an event structure that represents all non-conformant behavior.
Such an event structure can be used to obtain test cases for implementations of the system under investigation.
If the event structures were obtained from the system or program directly, it can serve as debug information to locate the fault in the implementation quicker.

$\cdot 10^3$ection{Preliminaries}

In this section we introduce labeled prime event structures.

Throughout this work, we assume that every set of labels $\mathcal{E}label$ contains a distinct label $\varepsilon$, 
which denotes the empty symbol.
Concatenation of $\varepsilon$ to a word does not change the word.

\begin{definition}[FLES]
Given a set of labels $\mathcal{E}label$, a finite, $\mathcal{E}label$-labeled prime event structure (FLES) is a tuple $\mathcal{E} := \mathcal{L}le E, <, \#, h\rangle$
where $E$ is a finite set of events, $<\, $\cdot 10^3$ubseteq E \times E$ is a strict partial order on $E$, called \emph{causality relation},
$h: E \rightarrow \mathcal{E}label$ labels every event with an element of $\mathcal{E}label$, 
and $\# $\cdot 10^3$ubseteq E\times E$ is the symmetric, irreflexive \emph{conflict relation} \review{that is \emph{closed under} $<$, i.e.}
for all $e,e',e'' \in E$, if $e \# e'$ and $e' < e''$, then $e \# e''$.

\end{definition}

For an event $e$, we use $\hist e$ to denote the history of $e$ as the set of events that must happen before $e$ according to $<$, formally $\hist e := \{e' \in E \mid e' < e\}$. 

We require that there is a special event $\bot \in E$, such that $\hist\bot = \emptyset$, for all events $e \in E:\ \bot < e$, and $h(\bot) = \varepsilon$.
We define the direct successors $\kw{dsucc}$ of event $e$ as the set of events that depend on $e$ without there being another event in-between, formally $\kw{dsucc}(e)=\{e'\in E \mid e < e' \wedge \nexists e'':\ e < e'' < e'\}$.
We say that two events $e, e' \in E$ are \emph{concurrent} if $e \neq e'$, not $(e < e')$, not $(e > e')$, and not $(e \# e')$.

A central concept in assigning event structures a semantic is the notion of configurations:

\begin{definition}[Configuration]
\review{
For a FLES $\mathcal{E} := \mathcal{L}le E, <, \#, h\rangle$, a
\emph{configuration} of $\mathcal{E}$ is a set of events
$C~=~\{e_1,\ldots,e_n\}~$\cdot 10^3$ubseteq~E$ that is both
}
\begin{itemize}
	\item Left closed: $\forall e \in C: \forall e' \in E $ such
          that $e' < e \implies e' \in C$, and
	\item Conflict free: $\forall e,e' \in C: \neg (e \# e')$
\end{itemize}

\end{definition}

A configuration $C$ is \emph{maximal}, if there is no configuration $C'$ such that \review{$C $\cdot 10^3$ubseteq C'$ and $C \neq C'$}.
We denote by $\mathcal{MC}(\mathcal{E})$ the set of all maximal configurations of an event structure $\mathcal{E}$.

A \emph{trace} $\trace$ of $C$ is a sequence of events $\mathcal{L}le e_1,\ldots,e_n \rangle$, where every event $e\in C$ occurs exactly once in the sequence and for all $e_i,e_j\in \trace:\  e_i<e_j\implies i < j$.
We denote the set of all traces of a configuration $C$ with $T(C)$.
Let $f: C \rightarrow X$ be a mapping on $C$ to some set $X$.
For a trace $\trace$ of $C$, we denote by $f(\trace)$ the sequence resulting from point-wise application of $f$ on the elements of $\trace$.

Finally, we extend $T$ to event structures by defining it as the union
of traces over all maximal configurations.
That is, $T(\mathcal{E}) := \bigcup_{C \in \mathcal{MC}(\mathcal{E})} T(C)$.

A finite, labeled prime event structure $\mathcal{E}$ represents a finite set of bounded words over an alphabet $\mathcal{E}label$, where 
the bound for the length of words is given by the size of the largest maximal configuration.
We call this set the language $\mathcal{L}(\mathcal{E})$. 

\begin{definition}[Language of $C$ and $\mathcal{E}$]
The language of configuration $C$ of $\mathcal{E}$ is $\mathcal{L}(C) := \{ h(\trace) \mid \trace \in T(C)\}$. 
The language of $\mathcal{E}$ is $\mathcal{L}(\mathcal{E}) := \{h(\trace) \mid \trace \in T(\mathcal{E})\}$.
\end{definition}

To illustrate this definition we give a small example.

\begin{figure}
\caption{LES with one maximal configuration}
\label{fig:ex-noconf}

\caption{Event structure with conflicts}
\label{fig:ex-conf}

\caption{Event structures}
\label{fig:ex-simple}
\end{figure}

\begin{example}[Event structure and configurations]
We show two event structures in \cref{fig:ex-noconf,fig:ex-conf}. 
Boxes depict events.
Inside every box is its event's identifier, above or below the box is its event's label. If there is no label we implicitly assume the label to be $\varepsilon$.
Solid arrows depict direct successors of an event.
Dashed lines depict immediate conflicts.
Two events $e,e'$ are in immediate conflict if $e\# e'$ and there are no $e_1,e_2 \in E$ such that $e_1 < e \wedge e_1 \# e'$ or $e_2 < e' \wedge e\#e_2$.
For better readability, we omit all other causalities and conflicts.

\Cref{fig:ex-noconf,fig:ex-conf} both represent the language $\{AB,BA\}$. The event structure in \cref{fig:ex-noconf} has a single maximal configuration consisting of events $\{\bot,e_1,e_2\}$. The event structure in \cref{fig:ex-conf} has two maximal configurations: $\{\bot,e_1,e_2\}$ and $\{\bot,e_3,e_4\}$ (due to the conflict between $e_1$ and $e_3$ these two events cannot appear in the same configuration).
\end{example}

$\cdot 10^3$ection{Language Inclusion Problem and Complexity Results}
\label{sec:complexity}

\begin{figure}
\caption{$\mathcal{E}
\label{fig:ex-three}
\end{figure}

The language inclusion problem for two event structures $\mathcal{E}_1,  \mathcal{E}_2$ is to decide whether $\mathcal{L}(\mathcal{E}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_2)$.

In this section we prove a complexity bound for the language inclusion problem. 
As an intermediate step we look at the membership problem.

$\cdot 10^3$ubsection{Language Membership is NP-complete}

The \emph{finite prime event structure language membership problem} for word $w$ and FLES $\mathcal{E}$ is the problem of deciding whether $w \in \mathcal{L}(\mathcal{E})$.
Surprisingly, deciding membership is NP-complete. 
In contrast, trace membership $\trace \in T(\mathcal{E})$ can be decided in polynomial time.
Trace membership can be decided simply by verifying that the set of events of $\trace$ forms a maximal configuration of $\mathcal{E}$, 
which requires to verify left-closure, conflict-freedom, and maximality.
All of those can be checked in polynomial time (\review{linear time, assuming linear conflict lookup}).

Intuitively, the hardness of language membership comes from the fact that the labeling function does not need to be injective and the role of conflicts, 
which together rule out a greedy algorithm that consumes the word in question symbol by symbol in a unique way.

\begin{theorem}
\label{thm:membership_in_np}

Finite prime event structure language membership is in NP.

\end{theorem}

\begin{proof}

Let $\mathcal{E} = \mathcal{L}le E, <, \#,h \rangle$ be an $\mathcal{E}label$-labeled FLES and $w = \mathcal{L}le $\cdot 10^3$igma_1,\ldots,$\cdot 10^3$igma_n \rangle \in \mathcal{E}label^*$ be a word.
A trace $\trace$ is a polynomially sized certificate for $w \in \mathcal{L}(\mathcal{E})$.
Checking that $\trace\in T(\mathcal{E})$ can be done in polynomial time, and 
checking whether $h(\trace) = w$ can be done in linear time.
\qed

\end{proof}

To prove NP-hardness we reduce the Hamiltonian cycle (HC) problem  to the membership problem. 
HC is known to be NP-hard~\cite{karp1972reducibility}. It is the problem of deciding whether for a directed graph there exists a path that visits all vertices once and that ends in the vertex it started.
We use $$\cdot 10^3$ource{f}$ and $\target{f}$ to denote the source and target of a directed edge $f$.

\begin{restatable}{theorem}{membershipnphard}
\label{lem:cycle_red}
\label{thm:membership_np_hard}
Finite prime event structure language membership is NP-hard.
\end{restatable}

\begin{proof}
\review{
For a directed graph $G=(\{v_1,\ldots,v_n\},\{f_1,\ldots,f_k\})$ we construct an event structure $\mathcal{E}^G$, such that $x^n \in \mathcal{L}(\mathcal{E}^G)$ iff $G$ has a Hamiltonian cycle. $\mathcal{E}^G$ is shown in \cref{fig:ex-three} and we present the main arguments why this reduction is correct here. 
A detailed, formal proof is given in \cref{sec:langincproof}.

Configurations of the event structure encode a sequence of $n$ edges.
If event $e_{f,i}$ is included in the configuration it means that edge $f$ is at position $i$ in the sequence of edges. 
To ensure that every vertex is visited, edges with the same target are in conflict. 
Since $n$ edges need to be selected, there are $n$ vertices, and every vertex is a target of some selected edge, every vertex is visited once by the selected edges.
To ensure that the sequence of edges actually forms a cycle they need to be connected. 
Events $e_{f,i}$ and $e_{f',{i+1} \mathsf{mod} n}$ for which the target of $f$ is the source of $f'$ cause an $x$-labeled event $e_{f,f',i}$.
Therefore, only configurations that represent a cycle form the word $x^n$.

In summary, checking the membership of $x^n$ 
amounts to checking whether there exists a Hamiltonian cycle in $G$.
The reduction clearly is polynomial.
}

\qed
\end{proof}

$\cdot 10^3$ubsection{Language Inclusion is $\Pi^p_2$-complete}

The \emph{finite prime event structure language inclusion problem} for FLES $\mathcal{E}_1$ and $\mathcal{E}_2$ is the problem of deciding whether $\mathcal{L}(\mathcal{E}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_2)$.

$\Pi^p_2$ is a complexity class from the polynomial hierarchy. It intuitively represents a $\forall\exists$ quantifier alternation.

To show inclusion, we use the definition of $\Pi^p_2$ given by Wrathall~\cite{wrathall1976complete},
providing semantics for the complexity class in terms of formal languages.
These languages should not be confused with the particular type of languages we discuss in this work.
In contrast, such languages encode problem instances and candidate witnesses.

Formally, a language $L$ is in $\Pi^p_2$ iff there exists a polynomially decidable language $L'$, such that $x\in L \Leftrightarrow \forall y_1 \exists y_2 [\mathcal{L}le x,y_1,y_2\rangle \in L']$.
A language $L'$ is polynomially decidable if $w \in L'$ can be decided in polynomial time.
The $x$ represents an encoding of the problem instance as a string.
The $y_1$ and $y_2$ represent string encodings of witnesses to a sub-problem.

We fix two $\mathcal{E}label$-labeled FLES $\mathcal{E}_1 = \mathcal{L}le E_1, <_1, \#_1, h_1\rangle$ and $\mathcal{E}_2 = \mathcal{L}le E_2, <_2, \#_2, h_2\rangle$.

\begin{theorem}
\label{thm:inclusion_in_pip2}

Finite prime event structure language inclusion is in $\Pi^p_2$.

\end{theorem}

\begin{proof}

Language inclusion $\mathcal{L}(\mathcal{E}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_2)$ amounts to checking whether $\forall w\in \mathcal{L}(\mathcal{E}_1)\Rightarrow w \in \mathcal{L}(\mathcal{E}_2)$.
In terms of traces this can be expressed as
$\forall \trace_1 \in T(\mathcal{E}_1) .\ \exists \trace_2 \in T(\mathcal{E}_2) .\ h_1(\trace_1)=h_2(\trace_2)$, meaning that for every trace in $\mathcal{E}_1$ there has to be a trace in $\mathcal{E}_2$ corresponding to the same word in the common alphabet $\mathcal{E}label$.

We define $L := \{\mathcal{L}le \mathcal{E}_1, \mathcal{E}_2 \rangle \mid \mathcal{L}(\mathcal{E}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_2)\}$ and $L' := \{\mathcal{L}le \mathcal{L}le \mathcal{E}_1, \mathcal{E}_2 \rangle,\trace_1,\trace_2\rangle \mid \trace_1 \in T(\mathcal{E}_1) \Rightarrow \big( h_1(\trace_1)=h_2(\trace_2) \wedge \trace_2 \in T(\mathcal{E}_2) \big)\}$.
By the argument above, we obtain the desired form $x\in L$ iff $\forall y_1 \exists y_2 [\mathcal{L}le x,y_1,y_2\rangle \in L']$ to show $\Pi^p_2$ inclusion.
Furthermore, $L'$ can be decided deterministically in polynomial time, because trace membership, as well as label equality, can be decided in polynomial time.
\qed
\end{proof}

To show $\Pi^p_2$ hardness, we present a reduction from the Dynamic Hamiltonian Cycle (DHC) problem to the finite prime event structure language inclusion problem.
Given an undirected graph $G=(V,F)$ and a set $B $\cdot 10^3$ubseteq F$, graph $G$ and $B$ form a DHC if for every set $D $\cdot 10^3$ubseteq B$ with $|D| \leq |B|/2$, the graph $G_D=(V,F$\cdot 10^3$etminus D)$ has a Hamiltonian cycle. We define $n:=|V|$, $k:=|F|$, $m:=|B|$, and $bh:=\lfloor |B|/2 \rfloor$.
Essentially DHC, in comparison to HC, has an additional universal quantifier over subsets of $B$.
DHC is known to be $\Pi^p_2$-complete \cite{ko1995complexity}.

\begin{restatable}{theorem}{lemdyncycle}
\label{lemma:dyn_ham_cycle}
\label{thm:inclusion_pip2-hard}
Finite prime event structure language inclusion is $\Pi^p_2$-hard.
\end{restatable}

\begin{figure}
\caption{$\mathcal{E}
\label{fig:ex-g1}

\caption{$\mathcal{E}
\label{fig:ex-g2}

\caption{Event structures for the language inclusion hardness proof. We use $\ldots$ to indicate omitted events.}
\label{fig:ex-hardness}
\end{figure}

\begin{proof}
\review{

For an undirected graph $G=(V,F)$ and set $B= \{b_1,\ldots,b_m\} $\cdot 10^3$ubseteq F$ we construct event structures $\mathcal{E}^{G,B}_1$ and $\mathcal{E}^{G,B}_2$, such that $\mathcal{L}(\mathcal{E}^{G,B}_1)$\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}^{G,B}_2)$ iff $G, B$ satisfy DHC. 
$\mathcal{E}^{G,B}_1$ and $\mathcal{E}^{G,B}_2$ are shown in \cref{fig:ex-hardness} and we present the main arguments why this reduction is correct here.
A detailed, formal proof, as well as an example, are given in \cref{sec:langincproof}.

The idea of the proof is to encode subsets $D$ of $B$ via events $ein_i$ and $eout_i$ with $i \in [1,m]$ in both $\mathcal{E}^{G,B}_1$ and $\mathcal{E}^{G,B}_2$.
Events $ein_i$ are labeled with $lb_i$ and represent $b_i \in D$, whereas $eout_i$ are labeled with $\varepsilon$ and represent $b_i \notin D$.
Furthermore, the cardinality of $D$ is encoded in $\mathcal{E}^{G,B}_1$ via $y$-labeled events $eD_i$.
In contrast $y$-labeled events $eD_i$ in $\mathcal{E}^{G,B}_2$ are not used to count $|D|$, but to differentiate whether or 
not a Hamiltonian cycle is required to show DHC (i.e. whether $|D| \leq \frac{|B|}{2}$).
For every $i \in [1,m]$, event $\mathit{efix}_i$ is used to guarantee the existence of maximal configurations in $\mathcal{E}^{G,B}_2$ with $i$ $y$-labeled events.
In case a Hamiltonian cycle is required to show DHC for some set $D$, 
we encode $G_D$ using the same event structure as in the proof of \cref{thm:membership_np_hard}, 
excluding edges from $D$ via conflicts of events $ein_i$.

Our Hamiltonian cycle encoding used in the proof of \cref{thm:membership_np_hard}
operates on directed edges, but DHC is defined for undirected graphs.
Therefore, we replace every edge $f$ in $G$ with two edges in opposing directions,
 denoted by $\vec{f}$ and $\cev{f}$.
Clearly, every Hamiltonian cycle in the directed version corresponds to a Hamiltonian cycle in the undirected graph.
In order to faithfully represent restricted graphs $G_D$, 
we make sure always to exclude all directed edges corresponding to edges in $D$ 
when looking for a Hamiltonian cycle in $G_D$.

Every subset $D$ of $B$ is encoded by some word in $\mathcal{L}(\mathcal{E}^{G,B}_1)$ via labels $lb_i$ of events $ein_i$.
Since $ein_i$ is in conflict with $eout_i$ maximal configurations can only include one or the other.
That is, words exactly enumerate all subsets $D$ of $B$. Furthermore, similarly as for the proof of \cref{thm:membership_np_hard}, every $w \in \mathcal{L}(\mathcal{E}^{G,B}_1)$ contains $n$ times the label $x$.

Membership of words of $\mathcal{L}(\mathcal{E}^{G,B}_1)$ in $\mathcal{L}(\mathcal{E}^{G,B}_2)$ only depends on whether the encoded subset $F$\cdot 10^3$etminus D$ induces a Hamiltonian cycle:
Words that encode a $D$ such that $|D| > \frac{|B|}{2}$ are always
in $\mathcal{L}(\mathcal{E}^{G,B}_2)$, because they are trivially accepted by events $ev_i$. 
In contrast, for $D$ such that $|D| \leq \frac{|B|}{2}$ the event $\mathit{efix}_{|D|}$ is in concflict with $ev_1$, 
thereby preventing a trivial acceptance of words in $\mathcal{L}(\mathcal{E}^{G,B}_1)$.
Therefore, $x$ labels of words in $\mathcal{L}(\mathcal{E}^{G,B}_2)$ that encode $D$ such that $|D| \leq \frac{|B|}{2}$ 
must be of events caused by $es$.
The events caused by $es$ exactly encode Hamiltionian cycles in $G_D$, similarly to the proof of \cref{thm:membership_np_hard}.

Since the two cases are exhaustive and cover every subset $D$ of $B$, 
we get $\mathcal{L}(\mathcal{E}^{G,B}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}^{G,B}_2)$ iff $G$ and $B$ satisfy DHC.
The reduction is polynomial as can be easily observed by the event structures in \cref{fig:ex-hardness}.
}
\qed
\end{proof}

$\cdot 10^3$ection{Deciding Language Inclusion}
\label{sec:algorithm}

In this section, we introduce a decision algorithm for the FLES language inclusion problem.
Furthermore, we provide a language preserving translation of event structures into non-deterministic finite automata (NFAs), which allows us to compare our algorithm to NFA language inclusion.

We start by introducing necessary concepts for our decision algorithm.

\paragraph*{Configuration as an event structure}
Given an event structure $\mathcal{E} = \mathcal{L}le E, <, \#, h\rangle$ and a configuration $C$, 
we denote its corresponding event structure as 
$\mathcal{E}^C := \mathcal{L}le C, <_{\lceil C\times C}, \emptyset, h_{\lceil C} \rangle $, 
where $X_{\lceil Y}$ denotes the restriction of $X$ to $Y$.
For ease of presentation, when describing our algorithms, 
we abuse notation and do not differentiate between a configuration and its corresponding event structure.
Furthermore, in the following presentation of the algorithms, we assume that the causality relations and 
labeling functions of configurations $C_i$ for $i \in \{1,2\}$ are implicitly given by the event structure interpretation over $\mathcal{E}_i$.

\review{
\paragraph*{$\varepsilon$-free configurations}
For every configuration $C$, there is a configuration with the same language whose only $\varepsilon$-labeled event is $\bot$.
This $\varepsilon$-free configuration can be obtained simply by removing all $\varepsilon$-labeled events besides $\bot$ 
from its corresponding event structure, in particular from $C$ and $<_{\lceil C\times C}$.
The resulting $\varepsilon$-free configuration has the same language as the initial configuration, 
because the causality relation is transitive.
Furthermore, $\varepsilon$-labeled events do not modify the words and 
thus removing them does not influence the language of the configuration.
Therefore, in order to improve readability, 
from hereon we assume without loss of generality that configurations are $\varepsilon$-free.
We keep the $\bot$ event to improve readability, even though for our purpose this event is not required neither.
Note that $\varepsilon$-labeled events are useful during the construction phase of the event structure representing, for example, 
hidden transitions or non-deterministic choices.
}

\paragraph*{Embeddings}

\begin{figure}
\caption{Necessary and sufficient embeddings.\\
$\varphi: \bot \mapsto \bot; e_1 \mapsto e_4; e_2 \mapsto e_5; e_3\mapsto e_6$ is a necessary embedding (dotted arrows).\\
$\varphi: \bot \mapsto \bot; e_7 \mapsto e_4; e_8 \mapsto e_5; e_9 \mapsto e_6$ is a sufficient embedding (dash-dotted arrows).
}
\label{fig:ex-str1}
\label{fig:ex-str2}
\label{fig:ex-str3}
\label{fig:ex-necessary}
\end{figure}

An embedding is a structure-preserving one-to-one mapping between events of two configurations from different event structures. 
We consider two different types of embeddings that vary in their strictness in terms of structure preservation.
\review{Since embeddings are defined between configurations, conflicts do not play a role in these considerations.}
In order to use these embeddings for deciding language inclusion between two FLES, 
we assume that in a step prior to searching for embeddings, the maximal configurations of both $\mathcal{E}_1$ and $\mathcal{E}_2$ are computed.
This can, for example, be achieved with the algorithm presented in \cite{Rodriguez2015}.

In the following we consider two configurations $C_1$ and $C_2$ of two $\mathcal{E}label$-labeled FLES $\mathcal{E}_1=\mathcal{L}le E_1, <_1, \#_1, h_1\rangle$ respectively
 $\mathcal{E}_2=\mathcal{L}le E_2, <_2, \#_2, h_2\rangle$.

\begin{definition}[Necessary Embedding]
A mapping $\varphi: C_1 \rightarrow C_2$ is a \emph{necessary embedding} if
A) $\varphi$ is bijective, B) $\forall e \in C_1: h_1(e) = h_2(\varphi(e))$, and C) $\forall e \in C_1: \neg \big( e (<_1 \cup <_2^\varphi)^+ e \big)$, 

where $.^+$ denotes transitive closure and $<_2^\varphi$ denotes the relation $<_2$ mapped to the events of $C_1$.
Formally $<_2^\varphi:=\{(\varphi^{-1}(e_1),\varphi^{-1}(e_2)) \mid \exists e_1,e_2 \in C_2.\ e_1 <_2 e_2 \}$.
For a necessary embedding $\varphi$ from $C_1$ to $C_2$, we write $C_1~$\cdot 10^3$im^\varphi_N~C_2$.
We write $C_1~$\cdot 10^3$im_N~C_2$ if there exists a necessary embedding $\varphi$ such that $C_1~$\cdot 10^3$im^\varphi_N~C_2$.
\end{definition}

A necessary embedding implies that the two configurations have a common word, 
by requiring they have the same number of events with the same labels and 
that their partial orders are not contradicting each other.
\review{Note that the relation $$\cdot 10^3$im_N$ is symmetric, since for a necessary embedding 
$\varphi: C_1 \rightarrow C_2$, $\varphi^{-1}$ is a necessary embedding from $C_2$ onto $C_1$
}
\begin{example}
Consider the configurations in \cref{fig:ex-str1,fig:ex-str2}. 
There are only two label-preserving bijections between the configurations:
$\varphi_1: \bot \mapsto \bot; e_1 \mapsto e_6; e_2 \mapsto e_5; e_3\mapsto e_4$ and 
$\varphi_2: \bot \mapsto \bot; e_1 \mapsto e_4; e_2 \mapsto e_5; e_3\mapsto e_6$.

The mapping $\varphi_1$ is not a necessary embedding, since $e_2 (<_1 \cup <_2^\varphi) e_2$, which violates C).
To see this, consider the chain of events $e_2<_1 e_3 <_2^\varphi e_2$, where $e_3 = \varphi^{-1}(e_4), e_2 = \varphi^{-1}(e_5),$ and $e_4 <_2 e_5$.

In contrast, $\varphi_2$ is a necessary embedding and a witness to the common word ABA of both configurations.
\end{example}

\begin{restatable}{lemma}{lemmasimempty}
\label{lem:simempty}

Let $C_1$ and $C_2$ be maximal configuration of FLES $\mathcal{E}_1$ respectively $\mathcal{E}_2$.\\
$C_1~$\cdot 10^3$im_N~C_2$ if and only if $\mathcal{L}(C_1) \cap \mathcal{L}(C_2) \neq \emptyset$.

\end{restatable}

The following corollary gives rise to a termination criterion of the decision algorithm.
If we find a configuration $C$ in $\mathcal{E}_1$, such that there exists no configuration in $\mathcal{E}_2$ that shares a word with $C$, 
we can abort the search and report non-inclusion.

\begin{corollary}

Let $C,C_1,\ldots,C_n$ be configurations \review{such that $C\neq \emptyset$}.
If $(\forall i = 1, \ldots, n : C_i~\nsim_N C)$ then $\mathcal{L}(C) \nsubseteq \bigcup_{i=1}^n \mathcal{L}(C_i)$.

\end{corollary}

The second type of embedding has a stronger requirement on structure preservation.
Intuitively, it requires that the source of such an embedding is at least as strict in terms of causality as the target.

\begin{definition}[Sufficient Embedding]
A mapping $\varphi: C_1 \rightarrow C_2$ is a \emph{sufficient embedding} if
A) $\varphi$ is bijective, B) $\forall e \in C_1:\ h_1(e) = h_2(\varphi(e))$, and C) $\forall e_1,e_2 \in C_1:\ \varphi(e_1) <_2 \varphi(e_2) \implies e_1 <_1 e_2$.

If there exists a sufficient embedding $\varphi$ from $C_1$ to $C_2$, we write $C_1~$\cdot 10^3$qsubset^{\varphi}_S~C_2$.
We write $C_1~$\cdot 10^3$qsubset_S~C_2$ if there exists sufficient embedding $\varphi$, such that $C_1~$\cdot 10^3$qsubset^{\varphi}_S~C_2$.

\end{definition}

A sufficient embedding is a witness to language inclusion between configurations.
The reason to work with two kinds of embeddings is that we can construct necessary embeddings
using a backtracking algorithm.
It is easy to check whether a necessary embedding is also sufficient, 
whereas it is not straight forward to construct a sufficient embedding from scratch.

\begin{example}
Consider the configurations in \cref{fig:ex-str2,fig:ex-str3}. 
The mapping $\varphi_1: \bot \mapsto \bot; e_7 \mapsto e_4; e_8 \mapsto e_5; e_9 \mapsto e_6$ is a sufficient embedding.
The only non-trivial causality to check is $e_4 <_2 e_5$, for which we have $\varphi_1^{-1}(e_4) = e_7 <_3 e_8 = \varphi_1^{-1}(e_5)$.

In contrast, $\varphi_2: \bot \mapsto \bot; e_7 \mapsto e_6; e_8 \mapsto e_5; e_9 \mapsto e_4$ is not a sufficient embedding,
since in this case $e_4 <_2 e_5$ and $\varphi_1^{-1}(e_4) = e_9 \nless_3 e_8 = \varphi_1^{-1}(e_5)$.

This shows that the language of the event structure in \cref{fig:ex-str3} is included in language of the event structure in \cref{fig:ex-str2}.
\end{example}

The following Lemma provides a connection between sufficient embeddings and language inclusion.
In case there exists a sufficient embedding, the respective languages are included.

\begin{restatable}{lemma}{lemmasufficient}
\label{lem:sufficient}

Let $C_1$ and $C_2$ be maximal configurations of FLES $\mathcal{E}_1$ and $\mathcal{E}_2$ respectively.
If $C_1~$\cdot 10^3$qsubset_S~C_2$ then $\mathcal{L}(C_1) $\cdot 10^3$ubseteq \mathcal{L}(C_2)$.

\end{restatable}

The converse statement is not always true.
To see this, consider a configuration $C_1 = \{\bot,e_1,e_1'\}$ such that $e_1$ and $e_1'$ are concurrent and $h(e_1) = h(e_1') = A$.
Furthermore, consider a configuration $C_2 = \{\bot,e_2,e_2'\}$ such that $e_2$ and $e_2'$ are sequential and $h(e_2) = h(e_2') = A$.
Clearly, the configurations have the same language $\{AA\}$.
However, there is no sufficient embedding from $C_1$ to $C_2$.

Our decision algorithm performs an additional refinement step in such a case and concludes language inclusion only after checking the refined configurations.

In \cref{app:detailed}, we provide a proof that in the case of unique labels, the converse statement also holds.

\paragraph*{Splits}

Our language inclusion decision algorithm continuously performs configuration refinement steps that we call splits.
To be precise, we refine the causality relation of its corresponding event structure.

\begin{definition}[Split]
Let $C$ be a configuration of event structure $\mathcal{L}le E,<,\#,h\rangle$ and let $e_1,e_2\in C$ be two concurrent events.
The \emph{split} of $C$ on $e_1$ before $e_2$ is 
$C_{e_1<e_2}:=\mathcal{L}le C,(<\cup\{(e_1,e_2)\})^+_{\lceil C\times C},\emptyset,h_{\lceil C}\rangle $ where ${.}^+$ denotes transitive closure. 

\end{definition}

\review{
A split on two concurrent events $e_1$ and $e_2$ simply adds an additional ordering constraint between the two events.
In our algorithm, we always split both ways, creating two new configurations that order concurrent events $e_1$ and $e_2$ one way and the other.
Note that in order to avoid duplication of events, in practice splits can be implemented via additional, optional causalities on the event structure.
The following lemma states that splitting a configuration in both ways produces two new configurations with languages whose union is the original language.

\begin{restatable}{lemma}{lemmasplitlang}
\label{lemma:splitlang}

Let $C$ be a configuration and $e_1, e_2 \in C$ be concurrent events, then 
$\mathcal{L}(C)~=~\mathcal{L}(C_{e_1<e_2})~\cup~\mathcal{L}(C_{e_2<e_1})$.
If $h$ is injective (labels are unique), then $\mathcal{L}(C_{e_1<e_2})~\cap~\mathcal{L}(C_{e_2<e_1})~=~\emptyset$.

\end{restatable}
}

The following lemma guarantees progress of our algorithm.
It states that if we find a necessary, but not sufficient embedding, 
there are events that can be used to split $C_1$.
The goal is that after a finite number of splits 
a sufficient embedding can be established.

\begin{restatable}{lemma}{lemmasplitwitness}
\label{lemma:splitwitness}

Let $C_1, C_2$ be maximal configuration of FLES $\mathcal{E}_1$ respectively $\mathcal{E}_2$.\\
Furthermore, let $C_1 $\cdot 10^3$im^{\varphi}_N C_2$ and $C_1 \nsqsubset^{\varphi}_S C_2$.
Then there are concurrent events $e,e' \in C_1$, such that $\varphi(e) <_2 \varphi(e')$.

\end{restatable}

$\cdot 10^3$ubsection{Language Inclusion Decision Algorithm}

\begin{algorithm}
\SetAlgoLined\DontPrintSemicolon

\SetKwFunction{FCheck}{Check}
\SetKwProg{Fn}{Function}{:}{}

\SetKwFunction{FSufficient}{SuffOrSplit}
\SetKwProg{Fn}{Function}{:}{}

\KwIn{Finite, labeled Prime Event Structures $\mathcal{E}_1$ and $\mathcal{E}_2$}

\KwResult{$\mathcal{L}(\mathcal{E}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_2)$}

$\{C_1^1,\ldots,C_1^n\}, \{C_2^1,\ldots,C_2^m\} \gets $ all maximal configurations of $\mathcal{E}_1$ respectively $\mathcal{E}_2$\;

\Return $\bigwedge_{C_1 \in \{C_1^1,\ldots,C_1^n\}}$ \FCheck{$C_1,\{C_2^1,\ldots,C_2^m\}$}\;

\Fn{\FCheck{$C_1$, $\{C_2^{i_1},\ldots,C_2^{i_l}\}$}}{
\KwResult{$\mathcal{L}(C_1) $\cdot 10^3$ubseteq \bigcup_{j=1}^l \mathcal{L}(C_2^{i_j})$}
$\var{Candidates} \gets \{C_2^{i_1},\ldots,C_2^{i_l}\}$\;
\ForEach{$C_2 \in \{C_2^{i_1},\ldots,C_2^{i_l}\}$}{
	\If{$\exists\varphi: C_1\rightarrow C_2.\ C_1~$\cdot 10^3$im^\varphi_{N}~C_2$\label{line:nembed}} {
		\Return \FSufficient{$C_1,C_2,\varphi,Candidates$}\;
	}
	\Else{
		$Candidates \gets Candidates $\cdot 10^3$etminus \{C_2\}$\;
	}
}
\Return $\mathtt{false}$\Comment*[f]{counter-example $C_1$}\; \label{line:no_necessary}
}
\Fn{\FSufficient{$C_1,C_2,\varphi,Candidates$}}{
\If{$C_1 ~$\cdot 10^3$qsubset^\varphi_{S}~C_2$}{
	\Return $\mathtt{true}$\;
} 
Let $e,e' \in C_1$ be concurrent and $\varphi(e) <_2 \varphi(e')$\Comment*[f]{always exist (\cref{lemma:splitwitness})}\;
\Return \FSufficient{$C_{e < e'},C_2,\varphi,Candidates$} $\wedge$ \FCheck{$C_{e' < e},Candidates$}\; \label{line:sufficient_recursive}
}

\caption{Language inclusion decision algorithm}
\label{algo:comparison}

\end{algorithm}

We present our decision algorithm in \cref{algo:comparison}. 
Inputs to the algorithm are finite, labeled prime event structures $\mathcal{E}_1$ and $\mathcal{E}_2$.

The first step of the algorithm is to \review{calculate the maximal configurations of the event structure}, 
which can be done with the algorithm described in \cite{Rodriguez2015}.
For every maximal configuration $C_1$ of $\mathcal{E}_1$, the function \FCheck{} attempts to show that $\mathcal{L}(C_1)$ is a subset of $\mathcal{L}(\mathcal{E}_2)$.
This is achieved by searching for sufficient embeddings from (refined versions of) $C_1$ to maximal configurations of $\mathcal{E}_2$.

In order to construct candidate sufficient embeddings, 
in \cref{line:nembed} the algorithm attempts to construct necessary embeddings, using \cref{algo:necessary}.
In the following line, function \FSufficient{} checks whether a necessary embedding $\varphi$ is also sufficient.
This can be done by checking $\forall e \in C_2: \forall e' \in \kw{dsucc}(e): \varphi^{-1}(e) $ is not concurrent with $\varphi^{-1}(e')$.
In case $\varphi$ is not a sufficient embedding, such a pair of events is guaranteed to exist by \cref{lemma:splitwitness}.
For efficiency, this check can already be done during construction of the necessary embedding.

In case $\varphi$ is not sufficient, \cref{lemma:splitwitness} guarantees the existence of a pair of concurrent events that can be split.
The resulting split configurations are recursively checked for language inclusion in \cref{line:sufficient_recursive}.
\cref{lemma:splitwitness} guarantees us that $\varphi$ is a necessary embedding for one of the splits (say $C_{e < e'}$).
Therefore, for $C_{e < e'}$ we do not need to construct a new necessary embedding again, 
but can immediately check whether $\varphi$ is a sufficient embedding for $C_{e < e'}$.

In case no necessary embedding can be found for some configuration $C_1$ and its candidates, according to \cref{lem:simempty}, 
we can conclude $\mathcal{L}(C_1) \cap \mathcal{L}(\mathcal{E}) = \emptyset$, i.e. all words in $C_1$ are counter-examples to language inclusion.
Once \cref{line:no_necessary} is reached we know that $C_1$ does not share any word with any $\{C_2^{1},\ldots,C_2^{m}\}$, therefore $C_1$ is a counter-example to language inclusion.

The algorithm terminates, because the notions of necessary and 
sufficient embedding collapse in case the configuration contains only a single trace,
which is the case when the causality relation is a total order on the events of the configuration (see \cref{lemma:totalorder}).

As the algorithm recursively searches for sufficient embeddings, 
for efficiency, we can reduce the set of candidate configurations, 
because in case there is no necessary embedding between two configurations, 
there is clearly also no necessary embedding between any of their split configurations.

\begin{algorithm}[tb]
\SetAlgoLined\DontPrintSemicolon

\SetKwFunction{FContainsCycle}{ContainsCycle}
\SetKwProg{Fn}{}{:}{}

\SetKwFunction{FNEmbedding}{NEmbedding}

\KwIn{Configurations $C_1,C_2$}
\KwResult{$\varphi:C_1\rightarrow C_2$ if $C_1$\cdot 10^3$im^\varphi_N C_2$, $\mathtt{None}$ otherwise}

\If{$\exists x\in\mathcal{E}label.\ |\{e\in C_1 \mid h_1(e)=x\}| \neq |\{e\in C_2 \mid h_2(e)=x\}|$\label{line:trivialfalse}}{
\Return $\mathtt{false}$\;
}
\Return \FNEmbedding{$\{\bot_1\}, \{\bot_1 \mapsto \bot_2\}$}\;

\Fn{\FNEmbedding{$\var{frontier}, \varphi$}}{
\KwIn{$\var{frontier}$ stack of events $C_1$}
\KwIn{$\varphi:C_1 \rightarrow C_2$ (partial mapping)}
\KwResult{$\varphi:E_1\rightarrow E_2$ if $C_1$\cdot 10^3$im^\varphi_N C_2$, $\mathtt{None}$ otherwise}

\If{$\var{frontier}=\emptyset$\label{line:frontierempty}}{
  \Return $\varphi$\;
}
$e \gets \var{frontier}.\var{pop}()$\;
\ForEach(\Comment*[f]{direct successors of $e$ in $C_1$}){$e'\in \kw{dsucc}_{\mathcal{E}^{C_1}}(e)$\label{line:addfrontier}}{
	$\var{frontier}.\var{push}(e')$\;
}
\ForEach{$e''\in C_2$ such that $h_1(e)=h_2(e'')\wedge e''\notin \var{range}(\varphi)$}{
  $\varphi' \gets \varphi\cup\{e\mapsto e''\}$\;
  \If(\Comment*[f]{check for cycle}){$\nexists e_1,e_2\in E_1.\ e_1 <_1 e_2 \wedge \varphi'(e_2) <_2 \varphi'(e_1)$\label{line:cycle}}{
    $\varphi''\gets\FNEmbedding{$\var{frontier}, \varphi'$}$\;\label{line:recursion}
    \If{$\varphi''\neq \mathtt{None}$}{
      \Return $\varphi''$\;
    }
  }
}
\Return $\mathtt{None}$\;
}

\caption{$$\cdot 10^3$im_N$ decision algorithm}
\label{algo:necessary}

\end{algorithm}

We present the algorithm to construct necessary embeddings in \cref{algo:necessary}.
Intuitively, the algorithm is a combined depth first search over the causality relation, 
as well as the space of possible bijective, label-preserving mappings.

The algorithm starts by dismissing configurations that can never have a necessary embedding because the number of events with the same label differs (\cref{line:trivialfalse}).
The actual embedding is established with the recursive function \FNEmbedding{}. The recursion maintains a frontier of events that are yet to be explored and a partial mapping of already explored events. It ends if the frontier becomes empty (\cref{line:frontierempty}). The exploration is done on $C_1$ by adding the successors of the current event $e$ to the frontier (\cref{line:addfrontier}). Then for every event $e''$ in $C_2$ with the same label as $e$ a mapping $\varphi'$ is created and a cycle check performed. If this mapping does not introduce a cycle we recurs on it (\cref{line:recursion}). The first valid (not $\mathtt{None}$) mapping that is returned by a recursion is returned. If no such mapping is found, then $\mathtt{None}$ is returned.
The cycle check in \cref{line:cycle} basically checks if the two causality relations $<_1$ and $<_2$ are compatible for the mapped events, 
in the sense that the events can be brought in an order that respects both causality relations. 
The procedure can be implemented using any of the well known cycle detection algorithms over the graph with nodes being events of $C_1$ and edges being 
causalities $<_1 \cup <^{\varphi}_2$.

The worst-case runtime of the decision algorithm is exponential in $O(2^{2n})$, 
where $n = |E_1| + |E_2|$, which is not surprising for an algorithm solving a $\Pi^p_2$ hard problem.
There are two dominant factors of the exponential complexity.

First, the number of maximal configurations can be exponential in $n$ and 
\cref{algo:comparison} potentially has to compare all pairs of maximal configurations.
The CCNFS benchmark in \cref{sec:experiments} is an example for an event structure with an exponential number of maximal configurations in $n$.

Second, the number of mappings between configurations that need to be considered as candidates for necessary embeddings can be exponential in $n$.
That is, algorithm \cref{algo:necessary} has worst case runtime exponential in $n$.
Note that for a fixed mapping, the algorithm performs a linear search over the configuration and the combined causality relation.

Note that the number of possible embeddings decreases with the number of calls to \mbox{\FCheck} and 
the size of maximal configurations decreases relative to $n$ with the number of maximal configurations.
Therefore, the amortized runtime should be much better than the worst case complexity.

$\cdot 10^3$ubsection{Automaton Based Language Inclusion}
\label{sec:automaton}
We provide a language preserving encoding of event structures into non-deterministic finite automata (NFA).
The encoding allows us to compare our algorithm to well researched language inclusion algorithms in our evaluation (\cref{sec:experiments}).

The encoding has a state for every configuration of the event structure.
There is a transition between two states, if the difference between the corresponding configurations is just one event.
The transition is labeled with the label of that event.
In essence, the encoding is an automaton representation of what is known as the configuration structure of a prime event structure \cite{Glabbeek2009}.

\begin{definition}[Automaton Encoding]
Let $\mathcal{E} = \mathcal{L}le E, <, \#, h\rangle$ be a finite prime event structure with labels $\mathcal{E}label$.
We define the non-deterministic finite automaton $\mathcal{A}^{\mathcal{E}} =  \mathcal{L}le Q^{\mathcal{E}},\Omega^{\mathcal{E}},\delta^{\mathcal{E}},q^{\mathcal{E}}_0,F^{\mathcal{E}}\rangle$ as 
$Q^{\mathcal{E}} = \{q^{\mathcal{E}}_C \mid C \text{ is a configuration of } \mathcal{E}\}$, $\Omega^{\mathcal{E}} = \mathcal{E}label$, $(q^{\mathcal{E}}_{C_1},$\cdot 10^3$igma,q^{\mathcal{E}}_{C_2}) \in \delta^{\mathcal{E}}$ iff there is $e \in E$, such that $C_1 \cup \{e\} = C_2$ and $h(e) = $\cdot 10^3$igma$, $q^{\mathcal{E}}_0 := q^{\mathcal{E}}_{\{\bot\}}$, and $F^{\mathcal{E}} = \{q^{\mathcal{E}}_C \mid C \text{ is maximal}\}$.

\end{definition}

\begin{restatable}{lemma}{lemmapreserving}
\label{lemma:preserving}

Let $\mathcal{E}$ be a labeled, finite prime event structure, then
$\mathcal{L}(\mathcal{E}) = \mathcal{L}(\mathcal{A}^{\mathcal{E}})$.

\end{restatable}

The provided encoding is not optimal in general due to conflicts and 
the fact that events of prime event structures are caused in a unique way, 
which is a well known caveat of prime event structures \cite{Winskel1988}.
However, for the family of event structures that consists of the $\bot$ event and $n$ concurrent events (c.f. the proof of \cref{lem:words} in \cref{app:detailed}), 
our encoding contains exactly $2^n + 1$ states, which is one state more than the provably optimal NFA accepting the language of the event structure.
Furthermore, in our experiments, we apply optimized NFA reduction techniques~\cite{mayr2013advanced} before checking language inclusion on automata.

\begin{restatable}{theorem}{exponentialsuccinctness}
\label{lem:words}
There is a family of event structures $\mathcal{E}_n$ with events $E_n$, such that $|E_n| = n + 1$, $|\mathcal{L}(\mathcal{E}_n)| = n!$, and $|Q^{\mathcal{E}}| = 2^n + 1$.
Every NFA $\mathcal{A}$ with $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\mathcal{E}_n)$ has at least $2^n$ states.
\end{restatable}

\label{sec:applications}

Language inclusion of prime event structures is useful whenever two systems can be expressed as prime event structures. It is particularly beneficial for systems with inherent concurrency, where prime event structures are very succinct.

$\cdot 10^3$ubsection{Mutation-based test case generation}

Our motivation to investigate event structures and language inclusion was model-based mutation testing. 
The goal of \emph{model-based testing} (MBT) is to derive test-cases from a model of a system. 
The model may, for example, be a UML state machine and the test may be a sequence of inputs and outputs of the system. The simplest way of obtaining such test cases would be to randomly explore the state machine and record the produced input/output (IO) sequences. 
These tests can then be run against an implementation at a later point.

\emph{Model-based mutation testing} (MBMT) compares the original model to a mutated version of it. 
A mutation is a small change in the model, such as removing or adding a transition. 
Then a test case is only generated if it shows a difference between the original and the mutated model. 
This test case generation can be easily expressed using language inclusion between the two versions of the system: 
The test is exactly the word that is a member of the mutant, but not of the original.

The use of event structures is motivated by two factors. Firstly, models often use parallely running state machine that synchronize rarely. Secondly, for the test case generation we only consider the part until the input is required by the model, which is typically finite. This is motivated by the IO conformance~\cite{tretmans1996test}, which roughly-speaking allows the mutant to accept different inputs, but not to produce different outputs.

We implemented this approach and present the results in \cref{sec:experiments}.

$\cdot 10^3$ubsection{Other uses}

We envision numerous other applications that we did not investigate in depth. 

\paragraph*{Regression checking and version comparison}

Since many concurrent system can be concisely represented as an event structure comparison of these structures makes sense to find semantic differences between two versions of a software. This can, for example, be used to find regressions if between two versions the observable behavior of the system changed.

\paragraph*{Bounded model checking}

Model checking basically involves checking if a system exhibits the same behavior as a model. 
It differs from MBMT in that for MBMT tests are generated from the model and later run against the implementation. 
For model-checking, the implementation has to exist. 
Therefore one event system would be built from the model and one from the implementation. 
The language inclusion check can then verify that the implementation operates within the specification of the model.

$\cdot 10^3$ection{Application and Evaluation}
\label{sec:experiments}

Our motivation to investigate event structures and language inclusion was model-based mutation testing. 
The goal of \emph{model-based testing} (MBT) is to derive test-cases from a model of a system. 
The model may, for example, be a UML state machine and the test may be a sequence of inputs and outputs of the system. The simplest way of obtaining such test cases would be to randomly explore the state machine and record the produced input/output (IO) sequences. 
These tests can then be run against an implementation at a later point.

\emph{Model-based mutation testing} (MBMT) compares the original model to a mutated version of it, where 
a mutation is a small change in the model, such as removing or adding a transition. 
A test case is only generated if an \review{observable} difference between the original and the mutated model can be witnessed. 
This form of test case generation can be easily expressed using language inclusion between the two versions of the system: 
The test is exactly the word that is a member of the mutant, but not of the original.

The application of finite prime event structures to this problem is motivated by three factors.
Firstly, models often use concurrent state machine that synchronize rarely. 
Secondly, mutation analysis on reactive models can be performed by exploring models in bounded segments \cite{Fellner:2019:MMT:3305158.3289256}, 
where a bounded segment refers to all events occurring between two consecutive inputs.
These bounded segments can be represented as finite event structures.
Thirdly, it is desirable express independence in test cases in order to produce minimal test suites 
that do not need to list all variations of a test that differ only in terms of independent events.
Such test cases can be obtained as counter-examples to language inclusion, as discussed in \cref{sec:algorithm}.

To this end, we implemented the presented prime event structure language inclusion algorithm 
in the model-based mutation testing tool MoMuT~\cite{Fellner:2019:MMT:3305158.3289256}.
MoMuT accepts models written as object-oriented action systems (OOAS).
The models can be understood as labeled transition systems, where labels are either observable, controllable or hidden ($\varepsilon$).
OOAS models can model highly concurrent systems.
In order to construct test cases for such concurrent models efficiently, 
we need to apply partial order reduction during model exploration.
In \cite{Rodriguez2015} a partial order reduction based algorithm for 
constructing labeled prime event structures from transition systems is given.
We implemented this algorithm, using a static dependency relation based on variable reads and writes, 
and use it during model exploration, obtaining finite labeled event structures representing bounded segments of the model.
Each segment corresponds to all output or hidden transitions following some input until either a new input is required 
by the model to progress further or the model is in a terminating state.
We operate on models that exclude infinite sequences of outputs or hidden transitions.
Thus, the discussed segments are indeed bounded in our case.

The event structures constructed during partial order reduction are labeled with (potentially hidden) transitions of the explored model.
However, for mutation analysis, we want to find observable differences between event structures for given controllable inputs, 
in contrast to any difference in transition labels.
Therefore, in addition to using transition labels during partial order reduction, 
we use projected, visible (input \& output) labels and 
perform language inclusion on the languages over the latter kind.

During model exploration, which is described in detail in \cite{Fellner:2019:MMT:3305158.3289256}, 
we construct event structures $\mathcal{E}_B$ of the original model and $\mathcal{E}_A$ of mutants, representing 
bounded segments (as described above) following the same sequence of inputs.
We perform language inclusion checks $\mathcal{L}(\mathcal{E}_A) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_B)$ using \cref{algo:comparison} 
to decide whether the corresponding mutant is killed by the sequence of inputs 
and a test case can be produced.

In our experimental evaluation, we report measurements of these language inclusion checks 
during test case generation on a sequence of benchmark models.
For comparison and in addition to event structure based language inclusion, 
we perform language inclusion via automaton encoding, as described in \cref{sec:automaton}.
To this end, we encode the produced event structures as NFAs and check language inclusion using the tool RABIT~\cite{mayr2013advanced}. 

$\cdot 10^3$ubsection{Benchmarks and Results}

We use the following benchmarks for our experimental evaluation.
All benchmark models, scripts to instantiate the models for any parameter value, 
and the version of MoMuT used in the experiments can be found in the publicly available artifact of this paper \cite{andreas_fellner_2019_3514619}, 
which can be run with the virtual machine provided in \cite{dietsch_daniel_2019_3533104}.

\begin{itemize}
	\item The \textbf{Paxos$(n,m,k)$} benchmark models the Paxos distributed consensus protocol \cite{Lamport2001} with $n$ proposers, $m$ acceptors, and $k$ learners.
	The protocol specifies how the different actors can exchange certain messages to achieve consensus on some proposed value.
	The actions of the actors are largely independent of each other, which introduces lots of concurrency to the model.
	Furthermore, test cases extracted from our method should be interesting to concertize and run against implementations of the Paxos algorithm.
	\item The \textbf{Semaphore$(n)$} benchmark models $n$ threads that are synchronized by a semaphore. 
	Exactly $n-1$ threads are allowed to enter and compute in a critical section at the same time. 
	The amount of parallelism of this model is proportional to $n$.
	Furthermore, the model exhibits lots of conflicts, 
	as all operations on the semaphore are in conflict with each other.
	\item The \textbf{ParSum$(n)$} benchmark models a parallel summation algorithm.
	The sequence $0,\ldots,n^2{-}1$ is split into $n$ equally sized chunks, which are summed up concurrently. Then the partial results are summed up centrally when all parallel threads are finished.

	\item The \textbf{CCNFS$(n)$} benchmark models a system with $n$ events and unique labels, such that the $2i'th$ event is in conflict exactly with the $2i{+}1 'th$ event.
	Every set of independent events induces an event resetting the state.
	This benchmark is interesting, because its number of maximal configurations $2^{\lfloor\frac{n}{2}\rfloor}$ 
	(each configuration contains either $2i$ or $2i{+1}$ for each $i = 1 \ldots \lfloor\frac{n}{2}\rfloor$)
	is exponential in the number of events $n$.
	Due to the high number of maximal configurations, this benchmark is challenging for our algorithm.
	\item The \textbf{AllPar$(n)$} benchmark models a system with $n$ independent events and unique labels.

	The benchmark is the ideal case for our algorithm, because its event structure consists of only one maximal configuration with all events in parallel.
	In contrast, the benchmark is a very bad case for NFA language inclusion, as the smallest NFA to encode all permutations of $n$ symbols is exponential in $n$ (\cref{lem:words}).
	\item The \textbf{Sharing$(n,m)$} benchmark models a system that has $n$ different prefixes that all share the same suffix of length $m$.
	The benchmark particularly exhibits the well known shortcoming of event structures not being able to encode shared causes.
	The NFA is able to express the common suffix more succinct in comparison to the event structure.
\end{itemize}

\newcommand{\ms}{}
\newcommand{$\cdot 10^3$}{$\cdot 10^3$}
\newcommand{TO}{TO}

\newcommand{-}{-}
\newcommand{TOO}{TO & TO}
\newcommand{TOOOO}{TOO & TOO}
\newcommand{TOOOOO}{TO & TOOOO}

	 

	         

\newcommand{\textbf{Inclusion}}{\textbf{Inclusion}}
\newcommand{\textbf{Non-Incl.}}{\textbf{Non-Incl.}}
\newcommand{\mbox{Time}}{\mbox{Time}}
\newcommand{\mbox{Num}}{\mbox{Num}}
\begin{table}[tb]
	\captionsetup{justification=centering}
	\centering
	\begin{tabular}{l | r r r r r r | r r r r r}
	\textbf{Name} & $\mathbf{|\mathcal{E}_B|}$ & \textbf{PC} & \multicolumn{2}{r}{\textbf{Inclusion}} & \multicolumn{2}{r}{\textbf{Non-Incl.}} & $\mathbf{|\mathcal{A}^{\mathcal{E}_B}|}$ & \multicolumn{2}{r}{\textbf{Inclusion}} & \multicolumn{2}{r}{\textbf{Non-Incl.}}  \\
	 & & & \mbox{Time} & \mbox{Num} & \mbox{Time} & \mbox{Num} & &  \mbox{Time} & \mbox{Num} & \mbox{Time} & \mbox{Num} \\
  \midrule
  Paxos(2,3,1)& 80 & 4.1 & - & 0& 4.1$\cdot 10^3$ & 65&  23469& TOOOO \\
	Paxos(3,6,1)& 716 & 4.1 & - & 0& 4.0$\cdot 10^3$ & 94&  TOOOOO \\
	Semaphore(3)& 9 & 1.2 & - & 0& 23.8\ms & 78&  5& - & 0& 324.0\ms & 78\\
	Semaphore(11)& 25 & 2.3 & 3.5\ms & 2& 48.9\ms & 84&  9& - & 0& 564.2\ms & 80\\
	ParSum(3)& 18 & 2.2 & 1.1\ms & 80& 170.5\ms & 92&  218& 2.5$\cdot 10^3$ & 80& 9.3$\cdot 10^3$ & 84\\
	ParSum(5)& 38 & 3.8 & 342.0\ms & 84& 67.6\ms & 94& TOOOOO \\
  ParSum(10)& 123 & 8.2 & - & 0& 12.6\ms & 23& TOOOOO \\
  CCNFS(3)& 15 & 1.7 & 3.9\ms & 88& 1.2\ms & 88&  9& 262.7\ms & 88& 610.9\ms & 88\\
	CCNFS(6)& 77 & 2.7 & 501.8\ms & 108& 84.0\ms & 92&   65& 379.7\ms & 108& 1.2$\cdot 10^3$ & 92\\
  CCNFS(10)& 1045 & 4.0 & 303$\cdot 10^3$ & 98& 17$\cdot 10^3$ & 102& 59050 & TOOOO \\
  AllPar(10) & 12 & 4.0 & 1.4\ms & 56& 8.6\ms & 144&  1025& 10$\cdot 10^3$ & 56& 82$\cdot 10^3$ & 144\\
  AllPar(50) &  52 & 17.3 & 3.2\ms & 44& 93.3\ms & 156& TOOOOO \\
  AllPar(500) & 502 & 167.3 & 361.9\ms & 40& 7.7$\cdot 10^3$ & 160&  TOOOOO \\
  Sharing(5,20)& 111 & 1.0 & 7.2\ms & 26& 4.2\ms & 174&  23& 338.1\ms & 26& 1.1$\cdot 10^3$ & 174\\
  Sharing(50,50)&2601 & 1.0 & 1.9$\cdot 10^3$ & 38& 527.2\ms & 162&  53& 255.4\ms & 38& 1.5$\cdot 10^3$ & 162\\
	\end{tabular}
	\centering
  \caption{Benchmark results for language inclusion checks \\
	         $\mathcal{L}(\mathcal{E}_A) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_B)$ respectively $\mathcal{L}(\mathcal{A}^{\mathcal{E}_A}) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{A}^{\mathcal{E}_B})$.}
	\label{tab:results}

\end{table}

We present the results of our experimental evaluation in \cref{tab:results}. 
For every benchmark, we report measurements of language inclusion checks for the largest bounded segment encountered during model exploration.
As described above, every such bounded segment corresponds to all output and hidden transitions following some input transition.
We report measurements of event structure based language inclusion $\mathcal{L}(\mathcal{E}_A) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_B)$ and 
automaton based language inclusion $\mathcal{L}(\mathcal{A}^{\mathcal{E}_A}) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{A}^{\mathcal{E}_B})$.
We separate the results into the cases where language inclusion holds (\textbf{Inclusion}) respectively does not hold (\textbf{Non-Incl.}).
Column $\mathbf{|\mathcal{E}_B|}$ shows the size of $\mathcal{E}_B$ in terms of the number of its events.
Column $\mathbf{|\mathcal{A}^{\mathcal{E}_B}|}$ shows the size of $\mathcal{A}^{\mathcal{E}_B}$ in terms of the number of its states.
Columns \mbox{Num}~show the number of inclusion checks performed 
on the respective bounded segment (which is the number of mutants relevant in the segment). 
Columns \mbox{Time}~show the average time for the inclusion checks in milliseconds.
Finally, column \textbf{PC} shows a measurement of the degree of concurrency.
For a single configuration $C$, the measurement is defined as $|C|/max_{e\in C}depth(e)$ and 
we report the average measurement of all maximal configurations in the respective event structure.

The reported time for language inclusion of event structures is the time for calculation of the maximal configurations plus the time for the actual language inclusion check. 
The reported time for language inclusion of automata is the time for the language inclusion check on a pre-reduced automaton. 
The construction and minimization of the NFAs is not included.

The results show that our language inclusion algorithm performs well on models with a lot of concurrency, i.e. those with high ParCoeff.
Furthermore, the automaton translation clearly fails in cases with lots of concurrency that are easy for our method (c.f. the \textbf{AllPar} benchmark).
For these examples our algorithm is very useful.
This result is not surprising, since our method exploits concurrency, whereas the NFA encoding does not include any notion of concurrency.
\review{Nevertheless, the result demonstrates that the benefits of exploiting concurrency with our method outweigh  
optimizations and fine-tuning of a well established language inclusion algorithm that has no notion of concurrency.}

However, as the \textbf{Sharing} benchmark shows, the inability of prime event structures to encode shared causes of events is a limitation of the approach.
In contrast, the reduced automaton representation can be significantly more compact than the event structure representation, 
rendering the automaton-based language inclusion superior.

$\cdot 10^3$ection{Related Work}

Prime event structures are a widely used formalism to express concurrency of discrete systems \cite{Winskel1988}
that can be obtained from transition systems via the method presented in 
\cite{Rodriguez2015}, or its extended version in \cite{Nguyen2018}.
There are multiple other variants of event structures, 
such as stable event structures \cite{Winskel1988} and flow event structures \cite{Boudol1990}.
Studying language inclusion for these event structure variants is interesting future work.

\review{
Event structure containment based on causality and conflict refinement is considered in \cite{Winskel1988,Winskel2016}.
However, as we demonstrate in our work, causality preservation is not necessary for language inclusion.
In \cite{Glabbeek1989,VanGlabbeek2001a} equivalence of event structures under action refinement is investigated.
This line of research is orthogonal to our approach, as it considers refinement of event structures,
while we compare event structures that can be obtained in multiple different ways.
Moreover, there is almost never language inclusion between an event structure and the event structure with refined actions by design.

Model checking over particular types of event structures has been studied in \cite{Penczek1997} for event structures labeled with atomic propositions and 
in \cite{Madhusudan2003} for event structures labeled with trace languages.
However, the proposed model-checking methods are not based on language inclusion,
which is one of the interesting future directions for our research.
Instead, formulas are directly interpreted over the event structure.

Several formalisms to express concurrency of discrete systems have been proposed and their relationships have been worked out in \cite{Winskel:1995:MC:218623.218630}.
In particular, trace languages and Petri nets are formalisms closely related to event structures, for which languages and language related problems have been studied.
}

The theory of trace languages \cite{Mazurkiewicz1986,Mazurkiewicz1995} studies closure of string languages under independence relations.
\cite{Cerny2017} presents an efficient method to show trace language inclusion over languages defined by 
non-deterministic finite automata.
\review{
In \cite{diekert1997partial} decidability results of rational trace languages are studied.
In particular, it is shown that language inclusion of rational (closed under union, concatenation, and Kleene-star) trace languages is decidable 
if and only if the common independence relation is transitive.
Language membership for context free and regular trace languages was shown to be NP-complete in \cite{bertoni1989membership}.
In \cite{Bouajjani2017}, comparison of concurrent programs via trace languages is studied.
The suggested trace languages abstract the program executions by considering statement ordering, 
as well as read and write accesses on a subset of relevant variables and synchronization primitives.
Trace language refinement is then reduced to assertion checking.
Interestingly, for Boolean programs this refinement check has complexity $\Delta^P_2$ 
for bounded abstraction precision and $\Sigma^P_2$ for unbounded abstraction precision.
In contrast to arbitrary event labels considered in our work, 
the authors of \cite{Bouajjani2017} consider refinement on languages of a more concrete program and dependency model.
}

Our problem is orthogonal to trace language inclusion in three aspects.
Firstly, we do not assume the independence relations of the compared systems to be equal.
Secondly, we do not require the independence relation to be defined over labels.
That is, we can study systems where two labels occur concurrently in one place, 
while the labels occur sequentially in another. This can occur because different events can have the same label.
Finally, in contrast to automata, which are often used to define trace languages, event structures are acyclic.
Therefore, event structures are less expressive than automata.
However, the price of the additional expressivity is that 
trace language inclusion over automata is undecidable in general \cite{Bertoni1982},
whereas our problem is decidable.

\review{
Petri nets are a formalism for concurrent systems that is closely related to event structures \cite{Nielsen1981}.
A manifold of complexity questions have been studied for Petri nets, see \cite{Jones1977,Esparza1996,DBLP:journals/eatcs/EsparzaN94} for surveys.
In particular, language related problems of labeled Petri nets have been studied, 
see \cite{peterson2019petri,Gaubert1999} for an overview over the types of considered languages and complexity results.
Since Petri nets typically describe languages on infinite words and many Petri net related problems are undecidable,
complexity results on language related Petri nets problems focus on establishing the boundary between decidability and undecidability.
Language inclusion and equivalence were shown to be undecidable for a wide range of types of Petri nets \cite{Grabowski1979,Jancar2001,DBLP:journals/eatcs/EsparzaN94}.
Language inclusion is decidable for languages of firing of regular Petri nets \cite{Valk1981} and 
certain types of deterministic Petri nets \cite{Gaubert1999}.
In contrast, language membership is decidable for a large class of Petri nets and language types \cite{peterson2019petri,Hack1976}.

Similarly to trace languages, the additional expressivity of Petri nets 
over finite prime event structures manifests in increased complexity of solving language inclusion.
However, as we demonstrated with our application, finite prime event structures are sufficient for interesting practical problems.
}

Finite asynchronous automata \cite{Fates2013} express concurrent systems succinctly 
in the same spirit as prime event structures.
Furthermore, asynchronous automata accept trace languages \cite{Zielonka1987}.
However, to the best of our knowledge, there is neither an algorithm, 
nor a tool to check language inclusion for (loop free) finite asynchronous automata.

Language inclusion of regular languages is a classic problem of computer science \cite{automata_book,meyer1972equivalence,Friedman1976,stearns1985equivalence}.
Algorithms for the problem are well studied and highly optimized \cite{mayr2013advanced,abdulla2010simulation,Cerny2017}.
However, as we demonstrate in the evaluation section, 
our procedure can outperform these algorithms in the realm of highly concurrent systems.
Adapting methods for classic automaton based language inclusions to event structures is interesting future work.

$\cdot 10^3$ection{Conclusion and Future Work}
\label{sec:future}

In this paper we showed that the language inclusion problem between two event structures is computationally hard, 
but our application and evaluation show that there are numerous benchmarks where the use of event structures and their comparison is beneficial.
However, the experiments also manifested a well known shortcoming of prime event structures, namely their inability to succinctly encode shared causes of events.

Interesting future work includes adapting our language inclusion method to different variants of event structures that do not suffer this problem.
Furthermore, we want to study whether our language inclusion procedure can be used to perform model checking over event structures.
Finally, we want to further study the test cases generated for the Paxos distributed consensus algorithm.
Concertizing the resulting test cases and running them against an implementation of the protocol might yield interesting results.

\appendix
\crefalias{section}{appsec}

$\cdot 10^3$ection{Lemmas and Proofs}
\label{app:detailed}

\begin{lemma}
\label{lemma:totalorder}
Let $C$ be a configuration.
$|T(C)| = 1$ if and only if $|C| = 1$ or for all events $e,e' \in C$ either $(e < e')$ or $(e' < e)$.

\end{lemma}
\begin{proof}

The claim is trivial for $|C| = 1$.

$\Rightarrow$\\
Let $T(C) = \{\mathcal{L}le e_1,\ldots,e_n \rangle\}$.
Since $\mathcal{L}le e_2,e_1,\ldots,e_n \rangle \notin T(C)$, we have that $e_1 < e_2$.
Likewise, we can show that $e_i < e_{i+1}$ for all $i \in [1,n-1]$.
Therefore, $e_i < e_j$ for $i < j$.
Since $C = \{e_1,\ldots,e_n\}$ have shown the claim.

$\Leftarrow$\\
Since $<$ is irreflexive, we immediately get that $|T(C)| > 0$.
From the definition of $T(C)$ follows that $e < e'$ then $e$ appears earlier in any trace in $T(C)$ than $e'$.
Since we assume that every pair of events is ordered by $<$, we have that the order in any trace is fully fixed.
In other words, there can only be a single trace. 
\qed

\end{proof}

\begin{corollary}
$|T(C)| > 1$ if and only if there are concurrent events $e,e' \in C$.
\end{corollary}

\lemmasimempty*

\begin{proof}
$\Rightarrow:$

There is a label preserving bijection $\varphi$, such that $<_1 \cup <_2^\varphi$ is a partial order.
Thus, via a depth first search over the events of $C_1$ with the order $<_1 \cup <_2^\varphi$, we can find a sequence of events $\mathcal{L}le e_1,\ldots,e_n\rangle$, such that
$e_j (<_1 \cup <_2^\varphi) e_i$ implies $j < i$.
It follows that $e_j <_1 e_i$ implies $j < i$, i.e. $\mathcal{L}le e_1,\ldots,e_n\rangle \in T(C_1)$.
Likewise it is the case that $e_j (<_2^{\varphi}) e_i$ implies $j < i$ and by the definition of $<^{\varphi}$, we get $\varphi(e_j) <_2 \varphi(e_i)$, i.e. $\varphi(\mathcal{L}le e_1,\ldots,e_n\rangle) \in T(C_2)$.
Since $\varphi$ is label-preserving, $h(\mathcal{L}le e_1,\ldots,e_n\rangle) = h(\varphi(\mathcal{L}le e_1,\ldots,e_n\rangle)) =: w$, which implies $w \in \mathcal{L}(C_1)$ and $w \in \mathcal{L}(C_2)$.

$\Leftarrow:$

Let $t_1 = \mathcal{L}le e_1,\ldots,e_n \rangle$ and $t_2 = \mathcal{L}le e'_1,\ldots,e'_n \rangle$ be traces of $C_1$ and $C_2$ respectively, such that $h(t_1) = h(t_2) \in \mathcal{L}(C_1) \cap \mathcal{L}(C_2)$.
We show that the mapping $\varphi: e_i \mapsto e'_i$ is a necessary embedding.
Clearly $\varphi$ is bijective and label-preserving.
We need to show $\forall e \in C_1: \neg e (<_1 \cup <_2^\varphi) e$.
Assume the contrary, i.e. $\exists e \in C_1:  e (<_1 \cup <_2^\varphi) e$.
In order to close the cycle and since $<_1$ and $<_2$ are order relations, there must exist an event $e' \in C_1$, such that $e' <_1 e$ and $e <_2^{\varphi} e'$, i.e. $\varphi(e) <_2 \varphi(e')$.
This implies, that for all $t \in T(C_1)$ we have that $e'$ appears earlier than $e$ and all traces $t\in T(C_2)$ are such that $\varphi(e)$ appears earlier than $\varphi(e')$.
This is a contradiction to $t_1 \in T(C_1), t_2 \in T(C_2)$ and $t_2 = \varphi(t_1)$. 
\qed

\end{proof}

\begin{restatable}{lemma}{lemmamaxtransfer}
\label{lemma:maxtransfer}

An event $e$ is \emph{maximal} in $C$, if there is no event $e' \in C$, such that $e < e'$.
Let $C_1$ and $C_2$ be configurations such that $C_1~$\cdot 10^3$qsubset^{\varphi}_S~C_2$.
If $e$ is maximal in $C_1$ then $\varphi(e)$ is maximal in $C_2$.

\end{restatable}

\begin{proof}

Assume there exists $e'$, such that $\varphi(e) <_2 \varphi(e')$.
Since $\varphi$ is a sufficient embedding, we have that $e <_1 e'$, which is a contradiction to $e$ being maximal in $C_1$.
Therefore, no such $e'$ exists.
Since $\varphi$ is bijective, $\varphi(e)$ is maximal in $C_2$. 
\qed

\end{proof}

\begin{restatable}{lemma}{lemmasubconf}
\label{lemma:subconf}

Let $e$ be maximal in configuration $C$, then
$C$\cdot 10^3$etminus \{e\}$ is a configuration and
for every $\mathcal{L}le e_1,\ldots,e_n \rangle \in T(C$\cdot 10^3$etminus \{e\})$ it is the case that $\mathcal{L}le e_1,\ldots,e_n,e \rangle \in T(C)$.

\end{restatable}

\begin{proof}

$C$\cdot 10^3$etminus \{e\}$ is conflict free, because $C$ is conflict free.
$C$\cdot 10^3$etminus \{e\}$ is left closed, because $e$ is maximal, therefore there is no event $e'$ such that $e < e'$.
Note that traces in $T(.)$ contain all events of the configuration.
Therefore, from $\mathcal{L}le e_1,\ldots,e_n \rangle \in T(C$\cdot 10^3$etminus \{e\})$ follows $\{e_1,\ldots,e_n,e\} = C$.
Furthermore, for every $e' \in C$, such that $e' < e$, we have that $e' \in \{e_1,\ldots,e_n\}$, which implies $\mathcal{L}le e_1,\ldots,e_n,e \rangle \in T(C)$.
\qed
\end{proof}

\begin{restatable}{lemma}{lemmasubconf2}
\label{lemma:subconf2}

Let $C$ be a configuration.
$\mathcal{L}le e_1,\ldots,e_n \rangle \in T(C)$ implies that $e_n$ is maximal in $C$.

\end{restatable}

\lemmasufficient*

\begin{proof}

We show the claim by induction on $|C_1| = |C_2| = n$.

In the base case we have $C_1 = \{\bot\}$ and $C_2 = \{\bot\}$.
For these configurations the claim is trivially fulfilled.

Let the induction hypothesis be that the claim holds for all configurations of size $n$.

Assume that $C_1$ and $C_2$ are configurations of size $n+1$, such that $C_1~$\cdot 10^3$qsubset^{\varphi}_S~C_2$.
We show $T(C_1) $\cdot 10^3$ubseteq \varphi(T(C_2))$.
Since $\varphi$ is bijective and label-preserving, $T(C_1) $\cdot 10^3$ubseteq \varphi(T(C_2))$ is equivalent to $\mathcal{L}(C_1) $\cdot 10^3$ubseteq \mathcal{L}(C_2)$.

Let $t = \mathcal{L}le e_1,\ldots,e_{n+1} \rangle \in T(C_1)$.
We need to show that $\varphi(t) \in T(C_2)$. 

Since $e_{n+1}$ is the last event of a trace and we consider only traces that include all events of the configuration, clearly $e_{n+1}$ is maximal in $C_1$.
According to \cref{lemma:maxtransfer,lemma:subconf}, we have that $C_1 $\cdot 10^3$etminus \{e_{n+1}\}$ and $C_2 $\cdot 10^3$etminus \{\varphi(e_{n+1})\}$ are configurations of size $n$.
Furthermore, $\varphi$ restricted to $C_1 $\cdot 10^3$etminus \{e_{n+1}\}$ is a witness for $C_1 $\cdot 10^3$etminus \{e_{n+1}\}~$\cdot 10^3$qsubset_S~C_2 $\cdot 10^3$etminus \{\varphi(e_{n+1})\}$.

From the induction hypothesis we get $ \varphi(\mathcal{L}le e_1,\ldots,e_n \rangle) \in T(C_2 $\cdot 10^3$etminus \{\varphi(e_{n+1})\})$.
Since $\varphi(e_{n+1})$ is maximal in $C_2$, from \cref{lemma:subconf} follows $\varphi(\mathcal{L}le e_1,\ldots,e_n,e_{n+1} \rangle) \in T(C_2)$.
\qed
\end{proof}

\begin{lemma}
\label{lem:sufficient_2}

Let $C_1$ and $C_2$ be maximal configuration of FLES $\mathcal{E}_1$ and $\mathcal{E}_2$ and for every $e_1 \in C_1$ and $e_2 \in C_2$ it is the case that $|\{e\in C_1 \mid h(e_1) = h(e)\}| = 1$ and $|\{e\in C_2 \mid h(e_2) = h(e)\}| = 1$\\
If $\mathcal{L}(C_1) $\cdot 10^3$ubseteq \mathcal{L}(C_2)$ then $C_1~$\cdot 10^3$qsubset_S~C_2$.

\end{lemma}

\begin{proof}

We show the claim by induction on $|C_1| = |C_2| = n$.

In the base case we have $C_1 = \{\bot\}$ and $C_2 = \{\bot\}$.
For these configurations the claim is trivially fulfilled.

Let the induction hypothesis be that the claim holds for all configurations of size $n$.

Let $e_{n+1}$ be a maximal event of $C_1$.
Let $M_{e_{n+1}} := \{e \in C_2 \mid e $ is maximal and $h(e_{n+1}) = h(e)\}$.

We start by showing $\exists e \in M_{e_{n+1}}$, such that
$\mathcal{L}(C_1 $\cdot 10^3$etminus \{e_{n+1}\}) $\cdot 10^3$ubseteq \mathcal{L}(C_2 $\cdot 10^3$etminus \{e\})$.

Assume the contrary.
That is, for every maximal event $e \in M_{e_{n+1}}$ it is the case that $\mathcal{L}(C_1 $\cdot 10^3$etminus \{e_{n+1}\}) \nsubseteq \mathcal{L}(C_2 $\cdot 10^3$etminus \{e\})$.
Then $\mathcal{L}(C_1 $\cdot 10^3$etminus \{e_{n+1}\}) \nsubseteq \bigcup_{e\in M_{e_{n+1}}} \mathcal{L}(C_2 $\cdot 10^3$etminus \{e\})$.
That is, there is a word $w \in \mathcal{L}(C_1 $\cdot 10^3$etminus \{e_{n+1}\})$ such that $w \notin \bigcup_{e\in M_{e_{n+1}}} \mathcal{L}(C_2 $\cdot 10^3$etminus \{e\})$.
Since $e_{n+1}$ is maximal $w \circ h(e_{n+1}) \in \mathcal{L}(C_1)$ ($\circ$ denotes concatenation).
Let us define language $\mathcal{L}^{\circ} := \bigcup_{e\in M_{e_{n+1}}} \mathcal{L}(C_2 $\cdot 10^3$etminus \{e\}) \circ h(e_{n+1})$ ($\circ$ is applied element-wise).
Clearly, $w \circ h(e_{n+1}) \notin \mathcal{L}^{\circ}$.

We claim that no word in $\mathcal{L}(C_2) $\cdot 10^3$etminus \mathcal{L}^{\circ}$ ends with $h(e_{n+1})$.
Assume there is such a word $w'$.
This word corresponds to a trace ending with some event $e'$ with label $h(e_{n+1})$.
Since $e'$ is the last event in a trace, and we only consider maximal configurations, it needs to be maximal.
Therefore, $e' \in M_{e_{n+1}}$, which is a contradiction to $w' \in \mathcal{L}(C_2) $\cdot 10^3$etminus \mathcal{L}^{\circ}$.
Since $w \circ h(e_{n+1})$ ends with $h(e_{n+1})$, we have $w \circ h(e_{n+1}) \notin \mathcal{L}(C_2) $\cdot 10^3$etminus \mathcal{L}^{\circ}$.

However, clearly $\mathcal{L}(C_2) = \mathcal{L}^{\circ} \cupdot (\mathcal{L}(C_2) $\cdot 10^3$etminus \mathcal{L}^{\circ})$.
In summary, we found $w \circ h(e_{n+1}) \in \mathcal{L}(C_1)$ such that 
$w \circ h(e_{n+1}) \notin \mathcal{L}(C_2)$, which is a contradiction to $\mathcal{L}(C_1) $\cdot 10^3$ubseteq \mathcal{L}(C_2)$.

Therefore, we can apply the induction hypothesis to $C_1 $\cdot 10^3$etminus \{e_{n+1}\}$ and $C_2 $\cdot 10^3$etminus \{e\}$ for the existing $e \in M_{e_{n+1}}$.
That is, $C_1 $\cdot 10^3$etminus \{e_{n+1}\} ~$\cdot 10^3$qsubset^{\varphi}_S~ C_2 $\cdot 10^3$etminus \{e\}$.
We extend $\varphi$ to $C_1$ by setting $\varphi(e_{n+1}) := e$.
Clearly, $\varphi$ is bijective and label-preserving.
Furthermore, causality preservation for events other than $e_{n+1}$ carries over from $C_1 $\cdot 10^3$etminus \{e_{n+1}\}$ to $C_1$.
What remains to show is that for all $e\in C$ with $\varphi(e) < \varphi(e_{n+1})$ we have $e < e_{n+1}$.
Since $e_{n+1}$ is maximal, clearly it is not the case that $e_{n+1} < e$.
Assume that $e$ and $e_{n+1}$ are concurrent.
Then there is a word, in which $h(e_{n+1})$ appears earlier than $h(e)$.
Since events are uniquely labeled and $\varphi(e) < \varphi(e_{n+1})$, this word is not in $\mathcal{L}(\mathcal{E}_2)$,
which is a contradiction to $\mathcal{L}(\mathcal{E}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}_2)$.
Therefore, $e < e_{n+1}$ and $\varphi$ is a sufficient embedding.
\qed

\end{proof}

\begin{lemma}
\label{lemma:splits}

Let $C$ be a configuration and $e_1, e_2 \in C$ be concurrent events, then
$T(C) = T(\mathcal{E}^C_{e_1<e_2}) \cup T(\mathcal{E}^C_{e_2<e_1})$ and $T(\mathcal{E}^C_{e_1<e_2}) \cap T(\mathcal{E}^C_{e_2<e_1})=\emptyset$.

\end{lemma}

\begin{proof}

From $t \in T(C_{e_1<e_2})$ directly follows $t \in T(C)$, since there is simply one less constraint to fulfill.
Thus, we have $T(C_{e_1<e_2}) $\cdot 10^3$ubseteq T(C)$.
Symmetrically we can show $T(C_{e_2<e_1}) $\cdot 10^3$ubseteq T(C)$, thus showing $T(C_{e_1<e_2}) \cup T(C_{e_2<e_1}) $\cdot 10^3$ubseteq T(C)$.

Let $t = \mathcal{L}le e'_1,\ldots,e'_n \rangle \in T(C)$.
There are $i \neq j$, such that $e'_i = e_1$ and $e'_j = e_2$.
In the case $i < j$, $t$ fulfills all constraints to be a trace of $C_{e_1<e_2}$, thus $t \in T(C_{e_1<e_2})$.
Likewise $j < i$ implies $t \in T(C_{e_2<e_1})$.
In any case $t \in T(C_{e_1<e_2}) \cup T(C_{e_2<e_1})$, showing $T(C) $\cdot 10^3$ubseteq T(C_{e_1<e_2}) \cup T(C_{e_2<e_1}) $.

Further, the $T(\mathcal{E}^C_{e_1<e_2})$ and $T(\mathcal{E}^C_{e_2<e_1})$ are disjoint because no trace can fulfill both constraints $e_1<e_2$ and $e_2<e_1$. 
\qed
\end{proof}
\review{
\lemmasplitlang*

\begin{proof}

$\mathcal{L}(C) = \mathcal{L}(C_{e_1<e_2}) \cup \mathcal{L}(C_{e_2<e_1})$ is a direct consequence of \cref{lemma:splits} and the definition of the language of prime event structures.
If $h$ is injective, i.e. labels are unique, then each word in $\mathcal{L}(C_{e_1<e_2})$ contains the sub sequence $\ldots h(e_1) \ldots h(e_2) \ldots$ whereas each word in $\mathcal{L}(C_{e_2<e_1})$ contains the different sub sequence $\ldots h(e_2) \ldots h(e_1), \ldots$, which shows that no word can be part of both languages.
\qed
\end{proof}
}
\lemmasplitwitness*

\begin{proof}

Since $\varphi$ is a label-preserving bijection, 
from $C_1 \nsqsubset^{\varphi}_S C_2$ follows that there are events 
$e,e'\in C$, such that $\varphi(e) <_2 \varphi(e')$ and $e \nless_1 e'$.
Towards contradiction assume $e' <_1 e$.
Then we have $e' (<_1 \cup <^{\varphi}_2) e'$, which is a contradiction to $\varphi$ being a necessary embedding.
Therefore, $e,e'$ are concurrent and a witness to the claim.
\qed
\end{proof}

\lemmapreserving*

\begin{proof}

Given a trace $\vec{e} = \mathcal{L}le e_1,\ldots,e_n \rangle$ we define $C^{\vec{e}}_l := \cup_{i=1}^l \{e_i\}$.

Let $w \in \mathcal{L}(\mathcal{A}^{\mathcal{E}})$, then by the definition of $\mathcal{A}^{\mathcal{E}}$, there is a trace  $\vec{e} = \mathcal{L}le e_1,\ldots,e_n \rangle$ such that $w = \mathcal{L}le h(e_1),\ldots, h(e_n) \rangle$, such that for every $l \leq n: C^{\vec{e}}_l$ is a configuration and $C^{\vec{e}}_n$ is a maximal configuration.
Since all $C^{\vec{e}}_l$ are configurations, we have $\mathcal{L}le e_1,\ldots,e_n \rangle \in T(C^{\vec{e}}_n)$.
Since $C^{\vec{e}}_n$ is maximal, we have $w \in \mathcal{L}(\mathcal{E})$.

Conversely, for every $w \in \mathcal{L}(\mathcal{E})$, there is a trace  $\vec{e} = \mathcal{L}le e_1,\ldots,e_n \rangle$ such that $w = \mathcal{L}le h(e_1),\ldots, h(e_n) \rangle$ and $\mathcal{L}le e_1,\ldots,e_n \rangle \in T(\mathcal{E})$.
From $\vec{e} \in T(\mathcal{E})$ follows that for every $l \leq n: C^{\vec{e}}_l$ is a configuration and that $C^{\vec{e}}_n$ is maximal.
By the definition of $\delta^{\mathcal{E}}$, we have for every $i = 1,\ldots,n-1: (q^{\mathcal{E}}_{C^{\vec{e}}_i},h(e_i),q^{\mathcal{E}}_{C^{\vec{e}}_{i+1}}) \in \delta^{\mathcal{E}}$.
Since $C^{\vec{e}}_n$ is maximal, $q^{\mathcal{E}}_{C^{\vec{e}}_{n}}$ is accepting.
Therefore, $w \in \mathcal{L}(Q^{\mathcal{E}})$.
\qed
\end{proof}

\exponentialsuccinctness*

\begin{proof}
The family is given by the $\mathcal{E}label$-labeled prime event structures $\mathcal{E}_n := \mathcal{L}le E_n, <_n, \emptyset, h_n \rangle$, where $\mathcal{E}label = \{\varepsilon\} \cup \{1,\ldots,n\}$, $E_n = \{\bot\} \cup \{e_1,\ldots,e_n\}$, $<_n := \{(\bot,e_i) \mid i = 1,\ldots,n\}$, and $h_n(e_i) := i$.
$\mathcal{E}_n$ encodes exactly all permutations of $\{1,\ldots,n\}$.
As shown in \cite{Ellul2005}, no NFA with less than $2^n$ states can accept the language of permutations of $n$ symbols,
showing that every $\mathcal{A}$ with $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\mathcal{E}_n)$ has at least $2^n$ states.

\noindent Furthermore, the number of all permutations of $n$ symbols is $n!$, showing that $|\mathcal{L}(\mathcal{E}_n)| = n!$.

\noindent Finally, every non-empty subset of $E_n$ is a configuration.
There are $2^n + 1$ such sets, which are all subsets of $\{e_1,\ldots,e_n\}$ together with $\bot$ plus the set $\{\bot\}$.
Since states of our encoding correspond one-to-one with configurations, we have $|Q^{\mathcal{E}}| = 2^n + 1$.
\qed
\end{proof}

$\cdot 10^3$ection{Detailed Proof of the Language Inclusion Reduction}

\membershipnphard*

\review{

\begin{proof}
We proof by reduction of HC to FLES language membership.

We use $s(f)$ and $t(f)$ to denote the respectively source and target vertices of directed edge $f$.

Let $G = (V,F)$ be a directed graph and define $n := |V|$.
We assume that $G$ does not contain any self loops, i.e. edges $f$ such that $s(f) = t(f)$, and that $n>1$.
Apart from a graph with only one vertex, a graph contains a Hamiltonian cycle if and only if the same graph without self-loops contains a Hamiltonian cycle.
The case $n=1$ can be trivially decided and is therefore not considered in our reduction.
A graph with self-loops can be converted into one without self-loops in linear time by removing self-loops from $F$.

Given an integer $j \in [1,n]$, we abbreviate $(j\ \mathsf{mod}\ n) + 1$ by $\jsucc{j}$.
We say that $f$ is connected to $f'$ if $t(f) = s(f')$.
We say that a sequence of edges $\mathcal{L}le f_1, \ldots, f_n \rangle$ is a cycle if for every $j \in [1,n]: f_j$ is connected to $f_{\jsucc{j}}$.
A Hamiltonian cycle of $G$ is a cycle $\mathcal{L}le f_1, \ldots, f_n \rangle$ of $F$, 
such that $\{t(f_j) \mid j \in [1,n]\} = V$.
The decision problem HC: "Does there exist a Hamiltonian cycle of $G$" is NP-hard \cite{karp1972reducibility}.

We provide a polynomially sized (in $|V|+|F|$) $\{\varepsilon,x\}$-labeled event structure $\mathcal{E}^G := \mathcal{L}le E,<,\#,h \rangle$, 
such that $x^n \in \mathcal{L}(\mathcal{E}^G)$ ($n$ times the letter $x$ concatenated) if and only if there exists a Hamiltonian cycle of $G$. 
The main idea is that configurations of the event structure translate to connected sequences of edges via events that each represent the assignment of an edge to a position in the sequence and events that express connectedness of two successive edges in the sequence.

\noindent The set of events $E$ contains exactly the following \textbf{events}:

\begin{itemize}
 \item The initial event $\bot$
 \item For every edge $f \in F$ and $j \in [1,n]$, there is an event $e_{f,j} \in E$ representing that $f$ is the $j$'th element of a sequence of edges.

 \item For every pair of edges $f,f' \in F$ with $t(f) = s(f')$ and $j\in [1,n]$ 
there is an event $e_{f,f',j} \in E$ representing that $f$ and $f'$ are successive elements of a sequence of edges.

\end{itemize}

\noindent Formally, we define $E$ as follows:

$$E  := \{\bot\} \cup \bigcup_{j = 1}^n \left(\{e_{f,j} \mid f \in F\} \cup \{e_{f,f',j} \mid f,f' \in F \wedge  t(f) = s(f')\} \right)$$

Clearly, $|\mathcal{E}^G| = |E|$ is polynomial in $|F| \leq |G|$.
Note that causality, conflict relation, and labeling are always of at most quadratic size in $|E|$.

\noindent The causality relation $<$ is the smallest partial order relation containing the following \textbf{causalities}:

\begin{itemize}
 \item For every edge $f \in F$ and $j \in [1,n]$: $\bot < e_{f,j}$ representing that every assignment of a single edge to a position in a sequence of edges is allowed.

 \item For every pair of edges $f,f' \in F$ with $t(f) = s(f')$, and every $j \in [1,n]$: $e_{f,j} < e_{f,f',j}$ and $e_{f',\jsucc{j}} < e_{f,f',j}$ representing that successive edges assigned in the represented sequence are connected.

\end{itemize}

\noindent Formally, we define $<$ as follows, where $X^+$ denotes the transitive closure of relation $X$:

$$<  := \left(\bigcup_{j = 1}^n \left(\{(\bot,e_{f,j}) \mid f \in F\} \cup \{(e_{f,j},e_{f,f',j}), (e_{f',\jsucc{j}},e_{f,f',j}) \mid e_{f,f',j} \in E\} \right)\right)^+ $$

\noindent The conflict relation $\#$ is the smallest conflict relation closed under $<$ (i.e. $e \# e' \wedge e' < e'' \Rightarrow e\# e''$) containing the following \textbf{immediate conflicts}:

\begin{enumerate}[label=\textbf{C.\arabic*}]
 \item \label{conf1} For every edge $f \in F$ and $j, k \in [1,n], j \neq k$: $e_{f,j} \# e_{f,k}$ representing that every edge can only be assigned to one position in a sequence.

 \item \label{conf2} For every pair of edges $f, f' \in F, f \neq f'$ and every $j \in [1,n]$: $e_{f,j} \# e_{f',j}$ representing that every position in the sequence can only be assigned once.

 \item \label{conf3} For every pair of edges $f, f' \in F, f \neq f'$, such that $t(f) = t(f')$ and every $j,k \in [1,n]$: $e_{f,j} \# e_{f,k}$ representing that edges assigned to a sequence must have non-overlapping target vertices.

\end{enumerate}

\noindent Formally, $\#$ has the following set of immediate conflicts:

\begin{align*}
\#^i := \bigcup_{j = 1}^n \bigg(\bigcup_{i = 1, i \neq j}^n \Big(\{(e_{f,j},e_{f,i}) \mid f \in F\} &\cup \{(e_{f,j},e_{f',i}) \mid f,f'\in F \wedge f \neq f' \wedge t(f) = t(f')\} \Big) \\
&\cup \{ (e_{f,j},e_{f',j}) \mid f,f' \in F \wedge  f \neq f'\} \bigg)
\end{align*}

\noindent The \textbf{labeling function} $h$ is given as follows:

\begin{itemize}
 \item Every event of the form $e_{f,f',j}$ has label $h(e_{f,f',j}) := x$.
 \item Every other event in $E$ has label $\varepsilon$.
\end{itemize}

\noindent Foramlly, $h$ is defined as follows:
$$h(e) := \begin{cases} x & \mbox{for } e = e_{f,f',j} \in E \\
						  \varepsilon & \mbox{otherwise} \end{cases}$$

We say that a configuration of $\mathcal{E}^G$ represents a sequence of edge $\mathcal{L}le f_1,\ldots,f_m \rangle $ if it includes events $e_{f_1,i_1},\ldots,e_{f_m,i_m}$, where $\{i_1,\ldots,i_m\} $\cdot 10^3$ubseteq [1,n]$, for every $j \in [1,m-1]: i_j < i_{j+1}$.

\noindent\textbf{Configurations represent sequences of edges:}
We claim that every configuration (besides $\{\bot\}$) of $\mathcal{E}^G$ represents a sequence of $m \leq n$ edges with pairwise different targets.

The claim follows from the structure of the immediate conflicts:
Due to conflicts \ref{conf1}, a configuration cannot contain events $e_{f,j}$ and $e_{f,k}$ for $j \neq k$.
Therefore, for every edge, a configuration includes one such event or none.
Furthermore, the indices $j$ of events $e_{f,j}$ give rise to a sequence of represented edges.
Due to conflicts \ref{conf2}, every index can only be assigned to one position in the sequence.
There are at most $n$ possible positions.
Therefore, every configuration (besides $\{\bot\}$) represents a sequence of $m \leq n$ edges.
Furthermore, the edges must pairwise different targets due to conflicts \ref{conf3}.

\noindent\textbf{Configurations with events $e_{f,f',j}$ represent sequences of (partially) connected edges:} 

Due to the causes of events $e_{f,f',j}$, we have that a configuration contains $e_{f,f',j}$ 
if and only if it represents a sequence of edges $f_1,\ldots, f_j = f, f_{\jsucc{j}} = f',\ldots,f_m$.

\noindent\textbf{Hamiltonian cycle $\Rightarrow x^n \in \mathcal{L}(\mathcal{E}^G)$:}

Assume $G$ has a Hamiltonian cycle $\mathcal{L}le f_1,\ldots,f_n \rangle$.
We claim that the set of events $\bot \cup \{e_{f_j,j}, e_{f_j,f_{\jsucc{j}},j} \mid j \in [1,n]\}$ is a maximal configuration.
The set is causally closed, since the edges are connected.
The set is conflict free, because every position is assigned exactly once (no conflicts among \ref{conf1} and \ref{conf2}) and
since the sequence is a Hamiltonian cycle, the targets are not overlapping (no conflict among \ref{conf3}).
The configuration is maximal, since clearly no further event of the form $e_{f,i}$ can be added,
since the assignment of edges to positions is fixed, and no event of the form $e_{f,f',i}$ can be added, 
since these events are directly induced by the assignment of edges to positions in the sequence.
Furthermore, this maximal configuration contains exactly $n$ events labeled by $x$ 
and all other events are labeled by $\varepsilon$, showing $x^n \in \mathcal{L}(\mathcal{E}^G)$.

\noindent\textbf{$x^n \in \mathcal{L}(\mathcal{E}^G) \Rightarrow$ Hamiltonian cycle:}

If $x^n \in \mathcal{L}(\mathcal{E}^G)$, then $\mathcal{E}^G$ has a maximal configuration $C$ that includes $n$ events of the form $e_{f,f',j}$.

Assume that $C$ does not represent a Hamiltonian cycle.
That is, two successive edges in the represented sequence of edges that are not connected, or not all vertices are visited by the sequence.

The former case cannot be true, due to presence of events $e_{f,f',j}$ in $C$, showing that $f$ is connected to $f'$ and the causalities of such events ($e_{f,j}$ and $e_{f',\jsucc{j}}$), implying that $f$ and $f'$ are successive edges in the sequence of edges represented by $C$.

To see why the latter case cannot be true, consider that in order for a connected sequence of $n$ edges not to visit one of the $n$ vertices of the graph, it needs to visit some vertex twice.
That is, it needs to include edges that have the same target vertex.
$C$ can not represent two different edges with the same target due to conflicts \ref{conf3}.
Furthermore, $C$ can not represent the same edge twice, due to conflicts \ref{conf1}.
Therefore, the sequence of edges represented by $C$ can not contain two edges with the same target.

Therefore, the maximal configuration $C$ represents a Hamiltonian cycle in $G$.
\qed
\end{proof}

}
\review{

\label{sec:langincproof}
\lemdyncycle*

\begin{proof}
We prove the claim by reduction of DHC to FLES language inclusion.
Let $G = (V,F)$ be a finite, undirected graph and let $B $\cdot 10^3$ubseteq F$.
Let $V = \{v_1,\ldots,v_n\}$, $F = \{f_1,\ldots,f_k\}$, and $B = \{b_1,\ldots,b_m\}$.
Let $\mathit{bh} := \mathsf{floor}(\frac{|B|}{2})$.
Using the same arguments of generality as in the proof of \cref{thm:membership_np_hard}, 
we assume that $G$ does not contain any self loops, i.e. edges $f$ such that $s(f) = t(f)$, and that $n>1$.

For this proof, we will use the same method to encode Hamiltonian cycles of directed graphs into event structures as in the proof of \cref{thm:membership_np_hard}.
Therefore, the first step of our reduction is to encode $G$ as a directed graph 
$\vec{G} = (V,\vec{F})$ with $\vec{F} := \{\vec{f},\cev{f} \mid f = (u,v) \in F \wedge \vec{f} = \mathcal{L}le u,v \rangle \wedge  \cev{f} = \mathcal{L}le v,u \rangle \}$,
where $(u,v)$ and $\mathcal{L}le u,v \rangle$ denote undirected, respectively directed, edges between vertices $u$ and $v$.
A self loop-free graph $G$ has an undirected Hamiltonian cycle if and only if $\vec{G}$ has a directed Hamiltonian cycle. Intuitively this is true, because we introduce for each undirected edge an edge in each direction that connect the vertices in either direction, just as the undirected edge does.

We provide $\{\varepsilon, x,y,lb_1,\ldots, lb_m\}$-labeled event structures $\mathcal{E}^{G,B}_1 = \mathcal{L}le E_1, <_1, \#_1,h_1 \rangle$ and 
$\mathcal{E}^{G,B}_2 := \mathcal{L}le E_2, <_2, \#_2,h_2 \rangle$ such that 
$|\mathcal{E}label|$, $|\mathcal{E}^{G,B}_1| := |E_1|$, and $|\mathcal{E}^{G,B}_2| := |E_2|$ are polynomial in $|G| := |V| + |F|$ and
$G$, $B$ has a DHC if and only if 
$\mathcal{L}(\mathcal{E}^{G,B}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}^{G,B}_2)$. 
$X^+$ denotes the transitive closure of relation $X$.

We define the components of $\mathcal{E}^{G,B}_1$ as follows, where $\#^i_1$ denotes immediate conflicts:

\begin{align*}
	E_1 &:= \{\bot\}\cup \bigcup_{i=1}^n\{ev_i\} \cup \bigcup_{i=1}^m \{ein_i,eD_i,eout_i\}\\

	<_1 &:= \Big( \{(\bot,ev_1)\} \cup  \bigcup_{i=2}^n \{(ev_{i-1},ev_i)\} \cup  \bigcup_{i=1}^m \{(\bot,ein_i),(\bot,eout_i), (ein_i,eD_i)\} \Big)^+\\

	\#^i_1 &:= \bigcup_{i=1}^m \{(ein_i,eout_i) \}\\

  h_1(e) &:= \begin{cases} x & \mbox{for } e \in \{ev_1,\ldots,ev_n\} \\ lb_i & \mbox{for } e = ein_i \\ y & \mbox{for } e \in \{eD_1,\ldots,eD_m\} \\ \varepsilon & \mbox{otherwise} \end{cases}
\end{align*}

For the definition of $\mathcal{E}^{G,B}_2$, we make use of the event structure $\mathcal{E}^G$ 
encoding all Hamiltonian cycles in $\vec{G}$ defined in the proof of \cref{thm:membership_np_hard} and embed it into $\mathcal{E}^{G,B}_2$ using a new root event $es \in E_2$:
\begin{align*}
E^{HC}  := &\bigcup_{j = 1}^n \left(\{e_{f,j} \mid f \in \vec{F}\} \cup \{e_{f,f',j} \mid f,f' \in \vec{F} \wedge  t(f) = s(f')\}         \right)\\
<^{HC}  := &\bigcup_{j = 1}^n \left(\{(es,e_{f,j}) \mid f \in \vec{F}\} \cup \{(e_{f,j},e_{f,f',j}), (e_{f',\jsucc{j}},e_{f,f',j}) \mid e_{f,f',j} \in E^{HC}\} \right) \\
\#^{HC} := & \bigcup_{j = 1}^n \bigg(\bigcup_{i = 1, i \neq j}^n \Big(\{(e_{f,j},e_{f,i}) \mid f \in \vec{F}\} \cup \{(e_{f,j},e_{f',i}) \mid f,f'\in \vec{F} \wedge f \neq f' \wedge t(f) = t(f')\} \Big) \\
        & \phantom{\bigcup_{j = 1}^n \bigg(\bigcup_{i = 1, i \neq j}^n \Big(\{(e_{f,j},e_{f,i}) \mid f \in \vec{F}\}} \cup \{ (e_{f,j},e_{f',j}) \mid f,f' \in \vec{F} \wedge  f \neq f'\} \bigg)  \\
\end{align*}

Finally, we define the components of $\mathcal{E}^{G,B}_2$ as follows, where $\#^i_2$ denotes immediate conflicts:

\begin{align*}
  E_2 :=& \{\bot, es\} \cup \bigcup_{i=1}^n\{ev_i\} \cup \bigcup_{i=1}^m \{ein_i,eout_i,eD_i,\mathit{efix}_{i-1}\} \cup E^{HC}\\

  <_2 :=& \Big( \{(\bot,es),(\bot,ev_1),(\bot,\mathit{efix}_0),(\bot,eD_1)\} \cup  \bigcup_{i=2}^n \{(ev_{i-1},ev_i)\} \cup  \bigcup_{i=1}^m \{(\bot,ein_i),(\bot,eout_i)\} \\
  & \cup \bigcup_{i=1}^{m-1} \{(eD_i,\mathit{efix}_i),(eD_i,eD_{i+1})\} \cup <^{HC} \Big)^+\\

  \#^i_2 :=& \{(es,ev_1)\}\cup \bigcup_{i=1}^m \{(ein_i,eout_i), (eD_i,\mathit{efix}_{i-1}) \} \cup \bigcup_{i=1}^\mathit{bh} \{(\mathit{efix}_i,ev_1) \cup \#^{HC} \} \cup \\

  & \bigcup_{i=1}^m \bigcup_{j=1}^n \{(ein_i,e_{\vec{f_i},j}), (ein_i,e_{\cev{f_i},j}) \}\\

	h_2(e) :=& \begin{cases} x & \mbox{for } e = e_{f,f',j} \in E_2 \mbox{ for some } f,f' \in F \mbox{ and } j \in [1,n] \\ x & \mbox{for } e \in \{ev_1,\ldots, ev_n\}\\ y & \mbox{for } e \in  \{eD_1,\ldots,eD_m\} \\ lb_i & \mbox{for } e = ein_i \\ \varepsilon & \mbox{otherwise} \end{cases}
\end{align*}

From the definition of $\mathcal{E}^{G,B}_1$ and $\mathcal{E}^{G,B}_2$, we can immediately see that the reduction is polynomial.
Notice that the causality and the conflict relation, as well as the number of edges of the graph is always at most quadratic in the number of events and vertices in $G$.

Both event structures $\mathcal{E}^{G,B}_1$ and $\mathcal{E}^{G,B}_2$ encode subsets $D$ of $B$.
In particular, every word $w \in \mathcal{L}(\mathcal{E}^{G,B}_1) \cup \mathcal{L}(\mathcal{E}^{G,B}_2)$ encodes a subset $D(w) := \{b_i \mid lb_i \in w\}$ of $B$.

Consider an arbitrary word $w \in \mathcal{L}(\mathcal{E}^{G,B}_1)$.
We first gather some properties of its symbols and then proceed to show under which condition $w \in \mathcal{L}(\mathcal{E}^{G,B}_2)$ holds.
Firstly, $w$ must contain the symbol $x$ exactly $|V|$ times due to events $ev_i$.
Secondly, every event $ein_i$ of $\mathcal{E}_1$ causes an event $eD_i$ with label $y$.
Therefore, $w \in \mathcal{L}(\mathcal{E}^{G,B}_1)$ encodes the cardinality of $D(w)$ by the number of $y$ symbols in $w$.
Finally, since all events $ev_i$ are concurrent to all events $ein_j$ and all events $ein_j$ are pairwise concurrent, 
symbols $lb_i$ and $x$ can appear in any permutation.

To show under which conditions $w \in \mathcal{L}(\mathcal{E}^{G,B}_2)$ holds, we distinguish whether $y$ occurs in $w$ more often or less or equal than $\mathit{bh}$ times.

Firstly, consider the case that $w$ contains the symbol $y$ more often than $\mathit{bh}$.
That is, $w$ encodes $D(w)$ with $|D(w)| > \mathit{bh}$.
Since DHC does not require the existence of a Hamiltonian cycle in $G_{D(w)}$, the word should be contained in $\mathcal{L}(\mathcal{E}^{G,B}_2)$ for any graph $G$.
Consider the set of events $C_{D(w)} := \{\bot\} \cup \{ein_j \mid b_j \in D(w)\} \cup \{eout_j \mid b_j \notin D(w)\} \cup \lceil \mathit{efix}_{|D(w)|} \rceil \cup \{ev_1,\ldots,ev_n\}$. 
The set is a maximal configuration, since $\mathit{efix}_{|D(w)|}$ is not in conflict with $ev_1$, due to $|D(w)| > \mathit{bh}$. 
Furthermore, $w \in \mathcal{L}(C_{D(w)})$ because the $y$-labeled events $eD_i$ are pairwise concurrent with the $x$-labeled events $\{ev_1,\ldots,ev_n\}$ which are in turn pairwise concurrent with the $lb_i$-labeled $\{ein_j \mid b_j \in D(w)\}$ events.
Furthermore, the $lb_i$-labeled events $\{ein_j \mid b_j \in D(w)\}$ are pairwise concurrent to each other.
Therefore, $\mathcal{L}(C_{D(w)})$ includes exactly all permutations of these symbols, in particular $w \in \mathcal{L}(C_{D(w)})$.
In summary, for words $w$ which encode $D(w)$, such that $|D(w)| > \mathit{bh}$, we have $w \in \mathcal{L}(\mathcal{E}^{G,B}_2)$.

Secondly, consider the converse case that $w$ encodes a set $D(w)$ with $|D(w)| \leq \mathit{bh}$.
Any maximal configuration $C_{D(w)}$ such that $w \in \mathcal{L}(C_{D(w)})$ must include events
$\{\bot\} \cup \{ein_j \mid b_j \in D(w)\} \cup \{eout_j \mid b_j \notin D(w)\} \cup \lceil \mathit{efix}_{|D(w)|} \rceil$.

In contrast to the first case, the event $ev_1$ is in conflict with $\mathit{efix}_{|D(w)|}$, because $|D(w)| \leq \mathit{bh}$.
However, the event $es$ is not in conflict with $\mathit{efix}_{|D(w)|}$.
Hamiltonian cycles are encoded in the sub-event structure following $es$, which can be seen by the arguments presented in the proof of \cref{lem:cycle_red}.
However, due to conflicts of events $ein_i$ with $e_{\vec{f}_i,j}$ and $e_{\cev{f}_i,j}$, 
only events $e_{\vec{f},j}$ and $e_{\cev{f},j}$ can be included in $C_{D(w)}$ with $f \notin D(w)$, i.e. edges of the graph $G_{D(w)}$.
Thus, analogous to the proof of \cref{thm:membership_np_hard}, $C_{D(w)}$ include $|V|$ $x$-labeled events if and only if $G_{D(w)}$ has a Hamiltonian cycle.

In summary, for a word $w \in \mathcal{L}(\mathcal{E}_1)$, we have $w \in \mathcal{L}(\mathcal{E}_2)$ if and only if $|D(w)| > \mathit{bh}$ or $|D(w)| \leq \mathit{bh}$ and $G_{D(w)}$ contains a Hamiltonian cycle.
Furthermore, for every $D $\cdot 10^3$ubseteq B$, there is a word $w \in \mathcal{L}(\mathcal{E}_1)$, such that $D = D(w)$.

Therefore, we get $\mathcal{L}(\mathcal{E}^{G,B}_1) $\cdot 10^3$ubseteq \mathcal{L}(\mathcal{E}^{G,B}_2)$ if and only if $G$ and $B$ satisfy DHC.
\qed
\end{proof}

}

\begin{example}

Consider the graph shown in \cref{fig:dyn_ham_graph}.
The graph and the set of edges $\{b_1,b_2\}$ form a dynamic Hamiltonian cycle.

\Cref{fig:dyn_ham_struct1,fig:dyn_ham_conf} 
show the event structures $\mathcal{E}_1$ and $\mathcal{E}_2$ constructed according to the reduction in the proof of \cref{lemma:dyn_ham_cycle} on this example graph.

The bold events in \cref{fig:dyn_ham_struct1,fig:dyn_ham_conf} show the configurations
that correspond to the Hamiltonian cycle that can be obtained when $b_2$ is removed. 
The configuration where $b_1$ is removed is similar.

The remaining cases are removing none or both of $b_1$ and $b_2$.
In the case that both are removed, the number of $y$ labels is 2 and therefore $eD_2$ has to be part of the configuration, enabling $ev_1,\ldots,ev_4$ to generate 4 times $x$.
In case no $b_i$ is removed, the same configuration as in \cref{fig:dyn_ham_conf} can be used to show existence of a Hamiltonian cycle with small changes to accommodate for the different number of $y$ and the non-existence of $lb_2$.

\end{example}

\begin{figure}
\caption{Graph with dynamic Hamiltonian cycle.}

\caption{Cycle without $in_2$.}

\caption{Cycle without $in_1$.}

\caption{Graph}
\label{fig:dyn_ham_graph}
\label{fig:cycle1}
\label{fig:cycle2}
\end{figure}

\centering
\begin{figure}
\caption{Example Event structure $\mathcal{E}
\label{fig:dyn_ham_struct1}
\end{figure}

\centering
\begin{figure}
\caption{Example Event structure $\mathcal{E}
\label{fig:dyn_ham_conf}
\end{figure}

\end{document}