\documentclass[fleqn,runningheads]{llncs}
\newfont{\fsc}{eusm10}                                  % frenchscript letters
\newcommand{\pow}{\mbox{\fsc P}}                        % french P (powerset)
\usepackage{amssymb}
\usepackage{dsfont}
\usepackage{verbatim}
\usepackage[usenames]{color}

\definecolor{old}{cmyk}{0,0,0,0.7} % grey
\definecolor{new}{cmyk}{0,0,0,1}   % black

\bibliographystyle{plain}

\newcommand{\cterms}{T(\Sigma)}
\newcommand{\terms}{\mathds{T}(\Sigma)}
\newcommand{\ar}{{\it ar}}
\newcommand{\var}{{\it var}}
\newcommand{\dom}{{\it dom}}
\newcommand{\rhs}{{\it rhs}}
\newcommand{\lhs}{{\it lhs}}
\newcommand{\depth}{{\it depth}}
\newcommand{\diam}[1]{\langle#1\rangle}
\newcommand{\trans}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\ntrans}[1]{\hspace{4pt}\not\hspace{-4pt}\stackrel{#1\ }{\longrightarrow}}
\newcommand{\bis}{\;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\;}
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}}   % no vertical space

\renewcommand{\phi}{\varphi}
\renewenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill $\square$\end{trivlist}}

\title{Compositionality of Hennessy-Milner Logic by Structural Operational Semantics}
\titlerunning{Compositionality of Hennessy-Milner Logic}

\author{Wan Fokkink \inst{1,4} \and Rob van Glabbeek \inst{1,2,3} \and Paulien de Wind \inst{4}}
\institute{
CWI, Department of Software Engineering\\
PO Box 94079, 1090 GB Amsterdam, The Netherlands
\and
National ICT Australia\\
Locked Bag 6016, University of New South Wales, Sydney 1466, Australia      
\and
University of New South Wales, School of Computer Science and Engineering\\
Sydney 2052, Australia
\and
Vrije Universiteit Amsterdam, Department of Theoretical Computer Science\\
De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands\\[3ex]
\email{wanf@cs.vu.nl}, \email{rvg@cs.stanford.edu}, \email{pdwind@cs.vu.nl}\\
\texttt{http://www.cs.vu.nl/\homedir wanf/} \\
\texttt{http://theory.stanford.edu/\homedir rvg/} \\
\texttt{http://www.cs.vu.nl/\homedir pdwind/}
}

\begin{document}

\maketitle

\begin{abstract}
This paper presents a method for the decomposition of HML formulas. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulas, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is the extension of an earlier decomposition method for the De Simone format from the PhD thesis of Kim G. Larsen in 1986, to more general formats.
\end{abstract}


\section{Introduction}

In the past two decades, compositional methods have been developed for checking the validity of assertions in modal logics, used to describe the behaviour of processes. This means that the truth of an assertion for a composition of processes can be deduced from the truth of certain assertions for its components. Most research papers in this area focus on a particular process algebra. 

{\sc Barringer, Kuiper \& Pnueli} presented in \cite{BKP84} (a preliminary version of) a compositional proof system for concurrent programs, which is based on a rich temporal logic, including operators from process logic \cite{HKP82} and LTL \cite{Pnu81}. For modelling concurrent programs they defined a language including assignment, conditional and while statements. Parallel components interact via shared variables.

In \cite{Sti85-obs-eq}, {\sc Stirling} developed modal proof systems for subsets of CCS \cite{Mil80} (with and without silent actions) including only sequential and alternative composition, to decide the validity of formulas from Hennessy-Milner Logic (HML) \cite{HM85}. In \cite{Sti85-CCS,Sti85-SCCS}, {\sc Stirling} extended the results from \cite{Sti85-obs-eq}, creating proof systems for subsets of CCS and SCCS \cite{Mil83} including asynchronous and synchronous parallelism and infinite behaviour, using ideas from \cite{BKP84}. In \cite{Sti87}, {\sc Stirling} generalised the proposals from \cite{Sti85-CCS,Sti85-SCCS} in order to cope with the restriction operator.

{\sc Winskel} gave in \cite{Win86} a method to decompose formulas with respect to each operation in SCCS. The language of assertions is HML with infinite conjunction and disjunction. This decomposition provides the foundations of Winskel's proof system for SCCS with modal assertions. In \cite{Win90}, \cite{AW92} and \cite{ASW94} processes are described by specification languages inspired by CCS and CSP \cite{BHR84}. The articles describe compositional methods for deciding whether processes satisfy assertions from a modal $\mu$-calculus \cite{Koz83}. 

{\sc Larsen} developed in \cite{Lar86} a more general compositional method for deciding whether a process satisfies a certain property. Unlike the aforementioned methods, this method is not oriented towards a particular process algebra, but it is based on structural operational semantics \cite{Plo04}, which provides process algebras and specification languages with an interpretation. A transition system specification, consisting of an algebraic signature and a set of transition rules of the form $\frac{\rm premises}{\rm conclusion}$, generates a transition relation between the closed terms over the signature. An example of a transition rule, for alternative composition, is $$\frac{x_1\trans{a}y}{x_1+x_2\trans{a}y}$$ meaning for states $t_1$, $t_2$ and $u$ that if state $t_1$ can evolve into state $u$ by the execution of action $a$, then so can state $t_1+t_2$. Larsen showed how to decompose HML formulas with respect to a transition system specification in the De Simone format \cite{Sim85}. This format was originally put forward to guarantee that the bisimulation equivalence associated with a transition system specification is a congruence, meaning that bisimulation equivalence is preserved by all functions in the signature. In \cite{LX91}, {\sc Larsen and Xinxin} extended this decomposition method to HML with recursion (which is equivalent to the modal $\mu$-calculus).

Since modal proof systems for specific process algebras are tailor-made, they may be more concise than the ones generated by the general decomposition method of Larsen (e.g., \cite{Sti85-CCS,Sti85-SCCS,Sti87}). However, in some cases the general decomposition method does produce modal proof systems that are similar in spirit to those in the literature (e.g., \cite{Sti85-obs-eq,Win86}).

For systems consisting of parallel compositions of interacting components and specification logics based on the modal $\mu$-calculus, the efficacy of Larsen's compositional approach was demonstrated by {\sc Andersen} in \cite{And95}. {\sc Laroussinie \& Larsen} applied this approach in \cite{LaLa95} to real-time systems modelled as networks of timed automata.

{\sc Bloom, Fokkink \& van Glabbeek} presented in \cite{BFvG04} a method for decomposing formulas from a fragment of HML with infinite conjunction, with respect to terms from any process algebra that has a structural operational semantics in ready simulation format, which is the ntyft/ntyxt format \cite{Gro93} without lookahead. A rule in ntyft/ntyxt format may contain negative premises, the left-hand side of the conclusion contains at most one function symbol and no multiple occurrences of variables, and the right-hand sides of positive premises are variables that are all distinct and do not occur in the left-hand side of the conclusion. Such a rule has no lookahead if variables in the right-hand sides of premises do not occur in the left-hand sides of premises. This format is a generalisation of the De Simone format, and still guarantees that bisimulation equivalence is a congruence. The decomposition method is not presented in its own right, but is used in the derivation of congruence formats for a range of behavioural equivalences from {\sc van Glabbeek} \cite{vGl01}.

In the current paper, the decomposition method from \cite{BFvG04} is extended to full HML with infinite conjunction, for process algebras with a structural operational semantics in ntyft/ntyxt format without lookahead or in tyft/tyxt format \cite{GV92}. The latter format is the same as the ntyft/ntyxt format, but disallows negative premises. The rules in this format may contain lookahead, i.e.\ there may be a chain of premises such that the right-hand side of each premise occurs in the left-hand side of the next premise; if this chain is finite, we speak of bounded lookahead. We show that if a rule has unbounded lookahead, it can be replaced by a rule with bounded lookahead. This is needed because no HML formula can capture unbounded lookahead.

In \cite{Sim04}, {\sc Simpson} presented a proof system for
establishing the validity of HML formulas for processes in arbitrary
languages with a structural operational semantics in GSOS format
\cite{BIM95}, using a mixture of compositional and structural styles
of proof.  His method differs from ours, and from the work referenced
above, in that the validity of an assertion for a process term may be
inferred from statements about the dynamic behaviour of that process,
whereas we only allow modal assertions for subterms.

An earlier version of this paper, which featured only a compositionality result for ntyft/ntyxt format without lookahead, appeared as \cite{FvGdW03}.

The structure of the paper is as follows. Section \ref{sec:preliminaries} contains the preliminaries on modal logic and structural operational semantics. In Section \ref{sec:hml} we present the decomposition method for HML formulas. Finally, in Section \ref{sec:bisimulation} we show as an application of this method that the congruence theorem for the tyft/tyxt format from \cite{GV92,FvG96} is an immediate corollary of our decomposition result.


\section{Preliminaries}
\label{sec:preliminaries}

In this section we give the basic notions of Hennessy-Milner Logic and structural operational semantics that are needed to define our decomposition method.

\begin{definition}[LTS, transition relation]\label{def:lts}
A \emph{labelled transition system (LTS)} is a pair $(\mathds{P},\rightarrow)$ with $\mathds{P}$ a set of \emph{processes} and $\rightarrow\;\subseteq\mathds{P}\times A\times \mathds{P}$ for $A$ a set of \emph{actions}. The relation $\rightarrow$ is called the \emph{transition relation} and its elements are called \emph{transitions}. We write $p \trans{a} q$ for $(p,a,q)\in\;\rightarrow$ and $p\ntrans{a}$ for $\neg\exists q\in\mathds{P}:p\trans{a} q$.
\end{definition}
The elements of $\mathds{P}$ represent the processes we are interested in, and $p\trans{a} q$ means that process $p$ can evolve into process $q$ while performing the action $a$.

\subsection{Hennessy-Milner Logic}
Modal logic aims at formulating properties of processes, and to identify processes that satisfy the same properties. In \cite{HM85}, {\sc Hennessy \& Milner} defined a modal language, often called Hennessy-Milner Logic (HML), which characterises the bisimulation equivalence relation on processes, assuming that the transition relation is {\it image finite}, i.e.\ each process has finitely many outgoing $a$-transitions for each $a\in A$. This assumption can be discarded if infinite conjunctions are allowed; see \cite{Mil81,HS85}.

\begin{definition}[Hennessy-Milner Logic]\label{def:HML}
Assume an action set $A$. The set $\mathds{O}$ of \emph{potential observations} or \emph{modal formulas} is recursively defined by 
\[\phi ::= \bigwedge_{i\in I}\phi_i\mid\diam{a}\phi\mid\neg\phi\]
with $a\in A$ and $I$ some index set. 
\end{definition}

\begin{definition}[satisfaction relation]\label{def:sat}
Let $(\mathds{P},\rightarrow)$ be an LTS. The \emph{satisfaction relation} $\models\;\subseteq \mathds{P}\times \mathds{O}$ is defined as follows, with $p\in\mathds{P}$:
\[\begin{array}{@{}l@{\quad}l}
\displaystyle{p\models\bigwedge_{i\in I}\phi_i} & \mbox{iff }p\models\phi_i\mbox{ for all }i\in I\\
p\models\diam{a}\phi 
	& \mbox{iff there is a }q\in\mathds{P}\mbox{ such that }p\trans{a}q\mbox{ and }q\models\phi\\
p\models\neg\phi & \mbox{iff }p\not\models\phi \\
\end{array}\]
\end{definition}
We will use the binary conjunction $\phi_1\wedge\phi_2$ as an abbreviation of $\bigwedge_{i\in\{1,2\}}\phi_i$, whereas $\top$ is an abbreviation for the empty conjunction. We identify formulas that are logically equivalent using the laws $\top \wedge \phi \cong \phi$, $\bigwedge_{i \in I}(\bigwedge_{j \in J_i} \phi_j) \cong \bigwedge_{i\in I,\,j \in J_i}\phi_j$ and $\neg\neg\phi \cong \phi$. This is justified because $\phi \cong \psi$ implies $p \models \phi \Leftrightarrow p \models \psi$.

\begin{definition}[bisimulation]\label{def:bisimulation}
Let $(\mathds{P},\rightarrow)$ be an LTS. A binary relation $\mathcal{B}\subseteq\mathds{P}\times\mathds{P}$ is a \emph{bisimulation} if it is symmetric and $p\mathcal{B}q$ implies: if $p\trans{a}p'$ then there is a $q'$ such that $q\trans a q'$ and $p'\mathcal{B}q'$. For $p,q\in\mathds{P}$ we write $p\bis q$ if there is a bisimulation $\mathcal{B}$ such that $p\mathcal{B}q$.
\end{definition}

\begin{proposition}[\cite{Mil81,HS85}]\label{prop:O_characterizes_bis}
Let $(\mathds{P},\rightarrow)$ be an LTS. Then $p \bis q$ if and only iff $p \models \phi \Leftrightarrow q\models \phi$ for all $\phi\in \mathds{O}$.
\end{proposition}                                                               


\subsection{Structural Operational Semantics}

Structural operational semantics \cite{Plo04} provides a framework to give an operational semantics to programming and specification languages. In particular, because of its intuitive appeal and flexibility, structural operational semantics has found considerable application in the study of the semantics of concurrent processes.

Let $V$ be a set of variables.
If $S$ is any syntactic object, $\var(S)$ denotes the set of variables that occur in $S$.
A syntactic object $S$ is called \emph{closed} if it does not contain any variables from $V$, i.e.\ if $\var(S)=\emptyset$. 

\begin{definition}[signature]\label{def:signature}
A \emph{signature} is a collection $\Sigma$ of \emph{function symbols} $f\not\in V$, equipped with a function $ar:\Sigma\rightarrow\mathds{N}$. The set $\terms$ of \emph{terms} over a signature $\Sigma$ is defined recursively by:
\begin{itemize}
\item $V\subseteq\terms$,
\item if $f\in\Sigma$ and $t_1,\ldots,t_{ar(f)}\in\terms$, then $f(t_1,\ldots,t_{ar(f)})\in\terms$.
\end{itemize}
A term $c()$ is abbreviated as $c$. $\cterms$ is the set of closed terms over $\Sigma$.
A $\Sigma$-\emph{substitution} $\sigma$ is a partial function from $V$ to $\terms$. The domain of $\sigma$ is denoted by $\dom(\sigma)$. If $\sigma$ is a $\Sigma$-substitution and $S$ is any syntactic object, then $\sigma(S)$ denotes the object obtained from $S$ by replacing, for $x$ in the domain of $\sigma$, every occurrence of $x$ in $S$ by $\sigma(x)$. In that case $\sigma(S)$ is called a {\em substitution instance} of $S$. A $\Sigma$-substitution $\sigma$ is {\em closed} if $\sigma(x)\in\cterms$ for all $x\in V$.
\end{definition}
In the remainder, let $\Sigma$ denote a signature and $A$ a set of actions.

\begin{definition}[literal]\label{def:literal}
A \emph{positive $\Sigma$-literal} is an expression $t \trans{a} t'$ and a \emph{negative $\Sigma$-literal} an expression $t\ntrans{a}$ with $t,t'\in \terms$ and $a \in A$. For $t,t' \in \terms$ and $a\in A$, the literals $t \trans{a} t'$ and $t\ntrans{a}$ are said to \emph{deny} each other.
\end{definition}

\begin{definition}[transition rule]\label{def:transition_rule}
A \emph{transition rule} over $\Sigma$ is an expression of the form $\frac{H}{\alpha}$ with $H$ a set of $\Sigma$-literals (the \emph{premises} of the the rule) and $\alpha$ a positive $\Sigma$-literal (the \emph{conclusion}). With $\lhs(H)$ and $\rhs(H)$ we denote the sets of left- and right-hand sides of the premises in $H$, respectively. The left- and right-hand side of $\alpha$ are called the \emph{source} and the \emph{target} of the rule, respectively. A rule $\frac{H}{\alpha}$ with $H=\emptyset$ is also written $\alpha$. 
\end{definition}

\begin{definition}[transition system specification]\label{def:TSS}
A \emph{transition system specification (TSS)} is a pair $(\Sigma,R)$ with $R$ a collection of transition rules over $\Sigma$.
\end{definition}
The purpose of a TSS $(\Sigma,R)$ is to specify an LTS of the form
$(T(\Sigma),\rightarrow)$ with as processes the closed terms over
$\Sigma$ and as transition relation a set of closed positive literals
$\rightarrow\;\subseteq\cterms\times A\times\cterms$.
Hence we refer to a closed positive literal as a \emph{transition}.

\begin{definition}[proof]\label{def:proof}
Let $P=(\Sigma,R)$ be a TSS. An {\em irredundant proof} from $P$ of a transition rule $\frac{H}{\alpha}$ is a well-founded, upwardly branching tree whose nodes are labelled by $\Sigma$-literals, and some of the leaves are marked ``hypothesis'', such that:
\begin{itemize}
\item the root is labelled by $\alpha$,
\item $H$ is the set of labels of the hypotheses, and
\item if $\beta$ is the label of a node $q$ which is not a hypothesis and $K$ is the set of labels of the nodes directly above $q$, then $\frac{K}{\beta}$ is a substitution instance of a transition rule in $R$.
\end{itemize}
A {\em proof} from $P$ of $\frac{K}{\alpha}$ is an irredundant proof from $P$ of $\frac{H}{\alpha}$ with $H\subseteq K$. If an (irredundant) proof from $P$ of $\frac{K}{\alpha}$ exists, then $\frac{K}{\alpha}$ is {\em (irredundantly) provable} from $P$, notation $P\vdash\frac{K}{\alpha}$ (resp. $P\vdash_{\rm irr}\frac{K}{\alpha}$).
\end{definition}
The proof of $\frac{H}{\alpha}$ is called irredundant because $H$ must equal (instead of include) the set of labels of the hypotheses. The main advantage of irredundant proofs is that derived rules may inherit certain syntactic structure from the transition rules in the TSS from which they are derived; in standard proofs this syntactic structure is usually lost, because arbitrary literals can be added as premises of derived rules. In the current paper, irredundancy of proofs is not of immediate importance, but it can be essential in applications of our decomposition method for modal formulas. For instance, in \cite{BFvG04}, irredundancy is essential to guarantee that the syntactic restrictions of congruence formats for TSSs are also satisfied by the rules derived from those TSSs.

A TSS with only positive premises specifies a transition relation in a straightforward way as the set of all provable transitions. But it is much less trivial to associate a transition relation to a TSS with negative premises. Several solutions are proposed by {\sc Groote} in \cite{Gro93}, {\sc Bol \& Groote} in \cite{BG96}, and {\sc van Glabbeek} in \cite{vGl04}. From the last we adopt the notion of a well-supported proof and a complete TSS.

\begin{definition}[well-supported proof]\label{def:wsp}
Let $P=(\Sigma,R)$ be a TSS. A \emph{well-supported proof} from $P$ of a closed literal ${\alpha}$ is a well-founded, upwardly branching tree whose nodes are labelled by closed $\Sigma$-literals, such that:
\begin{itemize}
\item the root is labelled by $\alpha$, and
\item if $\beta$ is the label of a node $q$ and $K$ is the set of labels of the nodes directly above $q$, then
\begin{enumerate}
\item either $\frac{K}{\beta}$ is a closed substitution instance of a transition rule in $R$ 
\item or $\beta$ is negative and for every set $N$ of closed negative literals such that $P\vdash\frac{N}{\gamma}$ for $\gamma$ a closed literal denying $\beta$, a literal in $K$ denies one in $N$. 
\end{enumerate}
\end{itemize}
We say $\alpha$ is \emph{{\it ws}-provable} from $P$, notation $P\vdash_{\it ws}\alpha$, if a well-supported proof from $P$ of $\alpha$ exists.
\end{definition}
In \cite{vGl04} it was noted that $\vdash_{\it ws}$ is {\em consistent}, in the sense that no TSS admits well-supported proofs of two literals that deny each other.

\begin{definition}[completeness]\label{def:complete}
A TSS $P$ is {\em complete} if for any closed literal $p\ntrans{a}$ either $P\vdash_{\it ws} p\trans{a}p'$ for some closed term $p'$ or $P\vdash_{\it ws} p\ntrans{a}$.
\end{definition}
Now a TSS specifies a transition relation if and only if it is complete. The specified transition relation is then the set of all {\it ws}-provable transitions. For positive TSSs, the set of $\vdash_{\it ws}$-provable closed positive literals and the set of $\vdash$-provable closed literals are the same.

\begin{example}
\label{exa:well-supported}
Let $A=\{a,b\}$ and $P=(\Sigma,R)$, where $\Sigma$ consists of the constant $c$ and the unary function symbol $f$, and $R$ is:
$$
\frac{x\ntrans{a}}{f(x)\trans{b}c}
\qquad
\frac{c\ntrans{a}}{c\trans{a}c}
$$
There are well-supported proofs for the closed negative literals $f^{n+1}(c)\ntrans{a}$ for $n\geq 0$ and $c\ntrans{b}$.
In each case, the proof consists of a single node, labelled by the literal itself. Furthermore, there are well-supported
proofs for the closed positive literals $f^{n+2}(c)\trans{b}c$ for $n\geq 0$, where the proof consists of a tree of
two nodes: the root has as label the literal itself, and the node above it has label $f^{n+1}(c)\ntrans{a}$.
The TSS $P$ is not complete, since there is no well-supported proof for $c\ntrans{a}$ or $c\trans{a}p$ for $p\in\cterms$;
moreover, there is no well-supported proof for $f(c)\ntrans{b}$ or $f(c)\trans{b}p$ for $p\in\cterms$.
\end{example}

\subsection{Formats}

We recall the tyft/tyxt format \cite{GV92} and the ready simulation format \cite{BFvG04}. Both formats are restrictions of the ntyft/ntyxt format \cite{Gro93}, which was introduced as the most liberal format known to guarantee congruence properties for bisimulation equivalence.          

\begin{definition}[ntytt]\label{def:ntytt}
An \emph{ntytt rule} is a transition rule in which the right-hand sides of positive premises are variables that are all distinct, and that do not occur in the source. An ntytt rule is an \emph{ntyxt rule} if its source is a variable, and an \emph{ntyft rule} if its source contains exactly one function symbol and no multiple occurrences of variables. An ntytt rule is an \emph{nxytt rule} if the left-hand sides of its premises are variables. A \emph{tytt}, \emph{tyxt}, \emph{tyft} or \emph{xytt rule} is an ntytt, ntyxt, ntyft or nxytt rule, respectively, without negative premises. A \emph{xyft rule} is a tyft rule that is also an xytt rule.
\end{definition} 
Given a premise $t\trans{a}y$ of an ntytt rule, there is a dependency between each variable in $t$ and $y$. This is captured in the dependency graph of the rule. We will strive for rules in which there is neither infinite forward dependency between variables (bounded lookahead), nor infinite backward dependency between variables (well-foundedness).

\begin{definition}[lookahead, well-foundedness]\label{def:lookahead,well-foundedness}
Assume a set of positive $\Sigma$-literals $\{t_i\trans{a_i}t_i'\mid i\in I\}$. Its \emph{dependency graph} is a directed graph, with the collection of variables $V$ as vertices, and with as edges
\[
\{\langle x,y\rangle\mid x\mbox{ and }y\mbox{ occur in }t_i\mbox{ and }t_i'\mbox{ respectively, for some }i\in I\}.
\]
The dependency graph of a transition rule is the dependency graph of its positive premises. A transition rule is \emph{well-founded} if any backward chain of edges in its dependency graph is finite. A transition rule has \emph{lookahead} if there is a variable in the right-hand side of a premise that also occurs in the left-hand side of a premise; the lookahead is \emph{bounded} if any forward chain of edges in the dependency graph is finite. 
\end{definition}

\begin{definition}[pure]\label{def:pure}
A variable in a transition rule is \emph{free} if it occurs neither in the source nor in right-hand sides of positive premises of this rule. 
A rule is \emph{pure} if it is well-founded and does not contain free variables.
\end{definition}

\begin{definition}[depth]\label{def:depth}
If $r$ is a pure tytt rule of the form $\frac{\{v_k\trans{c_k}y_k\mid k\in K\}}{t\trans a u}$, then the \emph{depth} of terms $v$ with $\var(v)\subseteq\var(r)$ is defined by:
\[\begin{array}{l@{~~}l}
\depth_r(x)=0 & \textnormal{for }x\in\var(t)\\
\depth_r(y_k)=\depth_r(v_k)+1 & \textnormal{for }k\in K\\
\depth_r(v)={\it max}\{\depth_r(z)\mid z\in\var(v)\} & \textnormal{if }\var(v)\subseteq\var(r)\\
\end{array}\]
This is well-defined since the set of premises is well-founded. When clear from the context, the subscript $r$ will be omitted. For $d\geq 0$ we write $K_d$ for $\{k\in K\mid\depth(v_k)=d\}$.
\end{definition}
Each combination of syntactic restrictions on transition rules induces a corresponding syntactic format of the same name for TSSs. For example, a TSS is in \emph{tyft/tyxt format} if and only if it contains only tyft and tyxt rules.

\begin{definition}[ready simulation format]\label{def:ready_simulation_format}
A TSS is in \emph{ready simulation format} if it contains only ntyft and ntyxt rules without lookahead.
\end{definition}


\section{Decomposing HML Formulas}
\label{sec:hml}

In this section it is shown how one can decompose HML formulas with respect to process terms. Section \ref{sec:explain} explains what this means. The TSS defining the transition relation on these terms should be in ready simulation format or in tyft/tyxt format, i.e.\ in ntyft/ntyxt format and either without lookahead or without negative premises.

The decomposition method uses a collection of rules extracted from this TSS, called {\em ruloids}. These rules have the property that there is a well-supported proof of a transition \mbox{$p \trans{a}q$}, with $p$ a closed substitution instance of a term $t$, if and only if there exists a proof that uses at the root a ruloid with source $t$ (Theorems~\ref{thm:ruloid_ready_simulation} and \ref{thm:ruloid-tyft/tyxt}). We require our ruloids to be pure nxytt rules with bounded lookahead. Moreover, when dealing with a TSS without lookahead, the ruloids are required to be without lookahead as well, and when dealing with a TSS without negative premises, the ruloids likewise have to be xytt rules.

The construction of the ruloids for a TSS in ready simulation format stems from {\sc Bloom, Fokkink \& van Glabbeek} \cite{BFvG04} and is briefly recalled in Section \ref{sec:ready_simulation_format}.
In Section \ref{sec:tyft/tyxt_format} we construct ruloids for TSSs in tyft/tyxt format, applying the transformation from tyft/tyxt to pure xyft format from {\sc Fokkink \& van Glabbeek} \cite{FvG96}. An essential new step in the construction is the replacement of any pure nxytt rule by an equivalent rule with bounded lookahead.

The decomposition method is given in Section \ref{sec:decomposition_hml_formulas}, together with the proof that a term $t$ under closed substitution $\sigma$ satisfies a formula if and only if the variables in $t$ under substitution $\sigma$ satisfy the formulas given by the decomposition method.

Section \ref{sec:examples} contains two toy examples to illustrate the
method. Section \ref{sec:counter-examples} features two counterexamples; 
one to underline the importance that TSSs are complete, and one to
show why our two decomposition results for ready simulation and
tyft/tyxt format cannot be combined in a straightforward fashion.


\subsection{Some Intuition}\label{sec:explain}

To explain our decomposition method, we start with an example.
\begin{example}
Consider the TSS with rules
$$\begin{array}{c}
  a.x \trans{a} x ~~~~~\displaystyle
  \frac{x \trans{a} x'}{x \| y \trans{a} x'\|y}~~~~~
  \frac{y \trans{a} y'}{x \| y \trans{a} x\|y'}
\end{array}$$
for $a\in A$. The following rules describe all circumstances under
which a process $x\|y$ satisfies the modal formula $\diam{a}\diam{b}\top$:
$$\begin{array}{@{}c@{}}\displaystyle
\frac{x\models\diam{a}\diam{b}\top}
     {x\|y\models\diam{a}\diam{b}\top}~~~
\frac{x\models\diam{a}\top~~\,y\models \diam{b}\top}
     {x\|y\models\diam{a}\diam{b}\top}~~~
\frac{x\models\diam{b}\top~~\,y\models \diam{a}\top}
     {x\|y\models\diam{a}\diam{b}\top}~~~
\frac{y\models \diam{a}\diam{b}\top}
     {x\|y\models\diam{a}\diam{b}\top}
\end{array}$$
In this paper we show how to produce, for any modal formula $\phi$, a
complete set of rules for deriving $x\|y\models \phi$, whose premises
have the form $x\models\psi$ or $y\models\psi$. As the number of rules
we need grows dramatically in the size of $\phi$, we cannot simply
list these rules exhaustively. Instead we generate them with induction
on the structure of $\phi$. Let us start with proposing some notation.
The set of rules above, all of which share the conclusion
$x\|y\models\diam{a}\diam{b}\top$, is completely determined by their
sets of premises. Each set of premises can be given as a partial
function $\psi$ that associates modal formulas $\psi(x)$ to variables
$x$. The second rule, for instance, is given by the partial function
$\psi_2$, defined by $\psi_2(x)=\diam{a}\top$ and
$\psi_2(y)=\diam{b}\top$. For convenience, we extend these partial
functions to total ones---in the first rule above by defining
$\psi_1(y)=\top$. This is justified because the premise $y\models\top$
is vacuously true for any process $y$.  The set of the four mappings
$\psi_1$--$\psi_4$ characterising the four rules displayed above is
called the \emph{modal decomposition} of the formula
$\diam{a}\diam{b}\top$ with respect to the term $x\|y$ in the TSS
above. This model decomposition is denoted
$(x\|y)^{-1}(\diam{a}\diam{b}\top)$.
\end{example}
In general, for a given term $t$
and a modal formula $\phi$, the modal decomposition $t^{-1}(\phi)$ of
$\phi$ w.r.t.\ $t$ is a set of requirements $\psi_i$, one of which
must be satisfied in order for $t$ to satisfy $\phi$. Each requirement
$\psi_i$ is given as a mapping from variables to modal formulas; it
holds when for all $x\in\var(t)$ the process represented by $x$
satisfies $\psi_i(x)$.

The main contribution of this paper is the definition of $t^{-1}(\phi)$
for any HML formula $\phi$ and any term $t$, relative to a complete TSS
in ready simulation format or in
tyft/tyxt format (Definition~\ref{def:inverse}), together with the
theorem that states that this definition is correct
(Theorem~\ref{thm:decomposition}):
\begin{quote}\it For any closed substitution $\sigma$,
the process $\sigma(t)$ satisfies $\phi$ exactly
when there is a mapping $\psi$ in the modal decomposition
$t^{-1}(\phi)$ such that $\sigma(x)$ satisfies $\psi(x)$ for all
variables $x$ in $t$.
\end{quote}
This model decomposition result can be \emph{used} to infer the
validity of a statement $t\models \phi$ by structural induction on
$t$. However, the result is \emph{obtained} by structural induction on
$\phi$.


\subsection{Ruloids for the Ready Simulation Format}\label{sec:ready_simulation_format}

In the decomposition of modal formulas, we need an important result from \cite{BFvG04},
where for any TSS $P$ in ready simulation format
a collection of pure nxytt rules, called {\it $P$-ruloids}, is constructed.
We explain this construction on a rather superficial level;
the precise transformation can be found in \cite{BFvG04}.

First $P$ is converted to a TSS in pure ntyft format without lookahead. In this conversion from \cite{GV92},
free variables in a rule are replaced by closed terms, and if the source is of the form $x$ then this variable
is replaced by a term $f(x_1,\ldots,x_n)$ for each $f\in\Sigma$. Next, using a construction from \cite{FvG96},
left-hand sides of positive premises are reduced to variables.
Roughly the idea is, given a premise $f(t_1,\ldots,t_n)\trans{\alpha}y$ in
a rule $r$, and a rule $\frac{H}{f(x_1,\ldots,x_n)\trans{\alpha}t}$, to transform $r$ by replacing the
aforementioned premise by $H$, $y$ by $t$, and the $x_i$ by the $t_i$; this is repeated (transfinitely) until all
positive premises with a non-variable left-hand side have disappeared.
The same idea will be applied in the proof of the forthcoming Proposition~\ref{prop:pure_tyft}.
In the final transformation step, rules with a {\it negative} conclusion $t\ntrans\alpha$ are introduced.
The motivation is that instead of the notion of well-founded provability of Def.\ \ref{def:wsp}, we want
a more constructive notion, like the one of Def.\ \ref{def:proof}, in which proof step 2 is cast as a special case of proof step 1.
A rule $r$ with a conclusion $f(x_1,\ldots,x_n)\ntrans{\alpha}$ is obtained by picking
one premise from each rule with a conclusion \plat{$f(x_1,\ldots,x_n)\trans{\alpha}t$}, and including the denial of
each of the selected premises as a premise of $r$. For this last transformation it is essential that rules
do not have lookahead.

The resulting TSS, which is in pure ntyft format without lookahead, is denoted by $P^+$.
In \cite{BFvG04} it is established that $P^+\vdash\alpha\Leftrightarrow P\vdash_{\it ws}\alpha$ for all closed literals $\alpha$.
The notion of irredundant provability is adapted in a straightforward fashion
to accommodate rules with a negative conclusion. $P$-ruloids are the pure nxytt rules without lookahead that
are irredundantly provable from $P^+$. The following correspondence result from \cite{BFvG04} between
a TSS and its ruloids will play a crucial r\^ole in our decomposition
method. It says that, provided we have enough variables to build ruloids, there is a well-supported
proof from $P$ of a transition $p \trans{a}q$, with $p$ a closed substitution instance of a term $t$, if and only if there
is a proof of this transition that uses at the root a $P$-ruloid with source $t$.

\begin{theorem}[Lemma 8.2 from \cite{BFvG04}, which is Lemma 13 in the report version of \cite{BFvG04}]\label{thm:ruloid_ready_simulation}
Let the set $V$ of variables be infinite and satisfying $|V| \geq |A|$.
Let $P=(\Sigma,R)$ be a TSS in ready simulation format with $|\Sigma|\leq |V|$.
Then \plat{$P\vdash_{\it ws}\sigma(t)\trans a p$} for $t\in\terms$, $p\in\cterms$ and $\sigma$ a closed substitution, if and only if there are a $P$-ruloid $\frac{H}{t\trans a u}$ and a closed substitution $\sigma'$ with $P\vdash_{\it ws}\sigma'(\alpha)$ for $\alpha \in H$, $\sigma'(t)=\sigma(t)$ and $\sigma'(u)=p$.
\end{theorem}

\subsection{Ruloids for the Tyft/Tyxt Format}\label{sec:tyft/tyxt_format}

In this section we construct ruloids for TSSs in tyft/tyxt format (see Theorem~\ref{thm:ruloid-tyft/tyxt}). We proceed in three steps. First any TSS in tyft/tyxt format is converted into a TSS in pure xyft format, applying a result from \cite{FvG96} (Proposition~\ref{prop:IC96}). Then we show that the pure xytt rules irredundantly provable from the resulting TSS satisfy all properties of ruloids, except for having bounded lookahead (Proposition~\ref{prop:pure_tyft}). Finally we get rid of unbounded lookahead (Proposition~\ref{prop:replacement}).

\begin{proposition}[\cite{FvG96}, Section 4]\label{prop:IC96}
Let the set V of variables be infinite.
For each TSS $P$ in tyft/tyxt format there is a TSS $Q$ in pure xyft format, such that $P\vdash\alpha\Leftrightarrow Q\vdash\alpha$ for all closed positive literals $\alpha$.
\end{proposition}

\begin{proposition}\label{prop:pure_tyft}
Let the set $V$ of variables be infinite and satisfying $|V| \geq |A|$.
Let $P=(\Sigma,R)$ be a TSS in pure tyft format with $|\Sigma|\leq |V|$. Then $P\vdash\sigma(t)\trans a p$ for $t\in\terms$, $p\in\cterms$ and $\sigma$ a closed substitution, if and only if there are a pure xytt rule $\frac{H}{t\trans a u}$ and a closed substitution $\sigma'$ with $P\vdash_{\rm irr}\frac{H}{t\trans a u}$, $P\vdash{\sigma'(\alpha)}$ for $\alpha\in H$, $\sigma'(t)=\sigma(t)$ and $\sigma'(u)=p$.
\end{proposition}
Before giving the proof of this proposition, we simultaneously
illustrate Theorem~\ref{thm:ruloid_ready_simulation} and
Proposition~\ref{prop:pure_tyft} through a TSS in pure tyft format
without lookahead. It is based on an example in \cite{FvG96}.

\begin{example}{\bf (A fragment of CCS with replication)}\label{ccs}.
Let ${\cal A}$ be a set of {\em names}. The set
$\bar{\cal A}$ of {\em co-names} is given by $\bar{\cal A}=\{\bar{a}
\mid a\in {\cal A}\}$, and ${\cal L}={\cal A} \cup \bar{\cal A}$ is
the set of {\em visible actions}. The function $\bar{\cdot}$ is extended to
$\cal L$ by declaring $\bar{\bar{a}}=a$. Furthermore $A = {\cal L}\cup
\{\tau\}$ is the set of actions. Note that $\bar{\tau}$ is undefined.

The process algebra CCS has a constant $0$, a unary operator $a$ for $a \in A$,
binary operators $+$ and $|$, and a few constructs that are omitted here.
In addition we consider the unary {\em replication operator} $!$.
The TSS {\rm CCS!} is given by the pure tyft rules without lookahead
below; note that the rule for replication is not xyft.
These rules are actually schemata, where $a$ ranges over $A$.
$$\begin{array}{cccc}
ax \trans{a} x & \displaystyle\frac{x \trans{a} x'}{x+y \trans{a} x'} &
\displaystyle\frac{y \trans{a} y'}{x+y \trans{a} y'}\\[4ex]
\displaystyle\frac{x\trans{a} x'}{x\mid y \trans{a} x'\mid y} ~~~~ &
\displaystyle\frac{x\trans{a} x' ~~~ y \trans{\bar{a}} y'}
{x\mid y \trans{\tau} x'\mid y'} ~~~~ &
\displaystyle\frac{y \trans{a} y'}{x\mid y \trans{a} x\mid y'} ~~~~ &
\displaystyle\frac{!x \mid x \trans{a} x'}{!x \trans{a} x'}
\end{array}$$
We give an example application of Proposition~\ref{prop:pure_tyft},
with $t=!(a0+x)$, $\sigma(x)=\bar{a}0$ and $p=(a0+\bar{a}0)\mid 0 \mid 0$.
Note that $\sigma(t)\trans{\tau}p$ is part of the transition relation.

Below we depict the construction of an irredundant proof of the pure
xytt rule $\displaystyle \frac{x \trans {\bar{a}} x'}{!(a0+x) \trans
\tau \;!(a0+x)\mid 0 \mid x'}$. Labels of the proof tree are obtained
by applying $\rho$ to the conclusions of the rules in the structure
below. Definition~\ref{def:proof} of a proof tree does not specify the
identity of the nodes that occur in the tree; it merely poses
requirements on their labels. Following a convention from
\cite{FvG96}, we do not depict the hypothesis explicitly, and any 
other node we take to be an $\alpha$-conversion of the proof rule
applied in that node to obtain its label from the labels of the nodes
above it. By choosing the variables in all these rules to be disjoint,
we can unite the substitutions applied in each of these nodes into one
global substitution $\rho$.
\\
\unitlength 1.8cm
\begin{picture}(4,5.3)(-2,-.2)
\put(0,0){\makebox(0,0){$\displaystyle\frac{!z \mid z \trans \tau z'}
 {!z \trans \tau z'}$}}
\put(0,.65){\vector(0,-1){.3}}
\put(0,1){\makebox(0,0){$\displaystyle\frac{y_1 \trans a y_1' ~~ y_2 \trans
 {\bar{a}} y_2'}{y_1 \mid y_2 \trans \tau y_1' \mid y_2'}$}}
\put(.9,1.65){\vector(-1,-1){.3}}
\put(1,2){\makebox(0,0){$\displaystyle\frac{x_2 \trans {\bar{a}} x_2'}
 {x_1 + x_2 \trans {\bar{a}} x_2'}$}}
\put(-.9,1.65){\vector(1,-1){.3}}
\put(-1,2){\makebox(0,0){$\displaystyle\frac{!w \mid w \trans a w'}
 {!w \trans a w'}$}}
\put(-1,2.65){\vector(0,-1){.3}}
\put(-1,3){\makebox(0,0){$\displaystyle\frac{v_2 \trans a v_2'}
 {v_1 \mid v_2 \trans a v_1 \mid v_2'}$}}
\put(-1,3.65){\vector(0,-1){.3}}
\put(-1,4){\makebox(0,0){$\displaystyle\frac{u_1 \trans a u_1'}
 {u_1 + u_2 \trans a u_1'}$}}
\put(-1,4.65){\vector(0,-1){.3}}
\put(-1,4.85){\makebox(0,0){$\displaystyle as \trans a s$}}
\end{picture}
\hfill
$\begin{array}[b]{@{}lcl@{}}
\rho(s)&=&0\\
\rho(u_1)&=&a0\\
\rho(u_1')&=&0\\
\rho(u_2)&=&x\\
\rho(v_1)&=&!(a0+x)\\
\rho(v_2)&=&a0+x\\
\rho(v_2')&=&0\\
\rho(w)&=&a0+x\\
\rho(w')&=&!(a0+x) \mid 0\\
\rho(x_1)&=&a0\\
\rho(x_2)&=&x\\
\rho(x_2')&=&x'\\
\rho(y_1)&=&!(a0+x)\\
\rho(y_1')&=&!(a0+x) \mid 0\\
\rho(y_2)&=&a0+x\\
\rho(y_2')&=&x'\\
\rho(z)&=&a0+x\\
\rho(z')&=&!(a0+x) \mid 0 \mid x'\\
\end{array}$
\hfill\mbox{}\\[2ex]
Moreover, $\sigma'(x)=\bar{a}0$ and $\sigma'(x')=0$.
Note that $\sigma'(x\trans{\bar{a}}x')=\bar{a}0\trans{\bar{a}}0$ is part of the
transition relation.
\end{example}

\begin{trivlist} \item[\hspace{\labelsep}\bf Proof of Proposition~\ref{prop:pure_tyft}:]
\fbox{$\Leftarrow$} Suppose there are a pure xytt rule $\frac{H}{t\trans a u}$ and a closed substitution $\sigma'$, with $P\vdash_{\rm irr}\frac{H}{t\trans a u}$, $P\vdash{\sigma'(\alpha)}$ for $\alpha\in H$, $\sigma'(t)=\sigma(t)$ and $\sigma'(u)=p$. Let $\pi$ be an irredundant proof from $P$ of $\frac{H}{t\trans a u}$. Then a proof of $\sigma(t)\trans a p$ is obtained by taking $\sigma'(\pi)$ and replacing each $\sigma'(\alpha)$ for $\alpha\in H$ by a proof of $\sigma'(\alpha)$.

\fbox{$\Rightarrow$} Let $P\vdash\sigma(t)\trans a p$. First, suppose $t$ is a variable. Let $y$ be a different variable. By definition, the pure xytt rule $\frac{t\trans a y}{t\trans a y}$ is irredundantly provable from $P$. Let $\sigma'$ be a closed substitution with $\sigma'(t)=\sigma(t)$ and $\sigma'(y)=p$. Clearly, $P\vdash\sigma'(t\trans a y)$.

Next, suppose $t=f(t_1,\ldots,t_{\ar(f)})$. We apply structural induction on a closed proof $\pi$ from $P$ of $\sigma(t)\trans a p$. Let $r\in R$ be the pure tyft rule and $\rho$ with $\dom(\rho)=\var(r)$ be the closed substitution used at the bottom of $\pi$, where $r$ is of the form $\frac{\{v_k\trans{c_k}y_k\mid k\in K\}}{f(x_1,\ldots,x_{\ar(f)})\trans a v}$. Then $\rho(x_i)=\sigma(t_i)$ for $i\in\{1,\ldots,\ar(f)\}$, $\rho(v)=p$, and $\rho(v_k)\trans{c_k}\rho(y_k)$ for $k\in K$ are provable from $P$ by means of strict subproofs of $\pi$. 

We now show how to define two substitutions $\rho_\infty$ and $\sigma_\infty$, and a pure xytt rule
$\frac{H}{t\trans{a}\rho_\infty(v)}$ that is irredundantly provable from $P$, such that
$P\vdash\sigma_\infty(\alpha)$ for $\alpha\in H$ and
$\sigma_\infty(t\trans{a}\rho_\infty(v))=\sigma(t)\trans{a}p$.
The substitutions $\rho_\infty$ and $\sigma_\infty$ will be given as the ``limits" of sequences of
substitutions $\rho_d$ and $\sigma_d$, and the set $H$ will be defined in the process.
We begin by inductively defining substitutions $\rho_d$ and $\sigma_d$ for $d\in\mathds{N}$, such that
\begin{equation}\label{IH:dom_rho_d}
\dom(\rho_d)=\{z\in\var(r)\mid\depth(z)\leq d\},
\end{equation}
\begin{equation}\label{IH:var_rho_d}
\var(\rho_d(z))\subseteq\dom(\sigma_d) \textnormal{ for } z\in\dom(\rho_d),\textnormal{ and}
\end{equation}
\begin{equation}\label{IH:sigma_d_rho_d}
\sigma_d\rho_d(z)=\rho(z)\textnormal{ for }z\in\dom(\rho_d).
\end{equation}
Let $\rho_0$ and $\sigma_0$ be substitutions such that 
\begin{equation}\label{def:dom_rho_0}
\dom(\rho_0)=\{x_1,\ldots,x_{\ar(f)}\},
\end{equation}
\begin{equation}\label{def:dom_sigma_0}
\dom(\sigma_0)=\var(t),
\end{equation}
\begin{equation}\label{def:rho_0}
\rho_0(x_i)=t_i\textnormal{ for }i\in\{1,\ldots,\ar(f)\},\textnormal{ and}
\end{equation}
\begin{equation}\label{def:sigma_0}
\sigma_0(z)=\sigma(z)\textnormal{ for }z\in\var(t).
\end{equation}
Note that $\sigma_0(z)\in\cterms$ for $z\in\dom(\sigma_0)$.

Properties (\ref{IH:dom_rho_d})--(\ref{IH:sigma_d_rho_d}) hold for $d=0$: \mbox{$\dom(\rho_0)\stackrel{(\ref{def:dom_rho_0})}=\{z\in\var(r)\mid\depth(z)\leq 0\}$}, $\var(\rho_0(x_i))\hspace{-.2em}\stackrel{(\ref{def:rho_0})}=\hspace{-.2em}\var(t_i)\subseteq\var(t)\hspace{-.2em}\stackrel{(\ref{def:dom_sigma_0})}=\hspace{-.2em}\dom(\sigma_0)$ for $i\in\{1,\ldots,\ar(f)\}$, and $\sigma_0\rho_0(x_i)\stackrel{(\ref{def:rho_0})}=\sigma_0(t_i)\stackrel{(\ref{def:sigma_0})}=\sigma(t_i)=\rho(x_i)$ for $i\in\{1,\ldots,\ar(f)\}$.

Suppose $\rho_d$ and $\sigma_d$ have been defined for some $d\geq 0$. According to Definition~\ref{def:depth}, for $k\in K_d$ we have $\depth(v_k)=d$, so $P\vdash\sigma_d\rho_d(v_k)\stackrel{(\ref{IH:dom_rho_d}),(\ref{IH:sigma_d_rho_d})}=\rho(v_k)\trans{c_k}\rho(y_k)$ by means of a strict subproof of $\pi$. By induction on the structure of $\pi$ there are a pure xytt rule $\frac{H_k}{\rho_d(v_k)\trans{c_k}u_k}$ and a closed substitution $\sigma'_k$ with 
\begin{equation}\label{eq:P_irr_proves_rule}
P\vdash_{\rm irr}\frac{H_k}{\rho_d(v_k)\trans{c_k}u_k}, 
\end{equation}
\begin{equation}\label{eq:P_proves_premises}
P\vdash\sigma'_k(\alpha)\textnormal{ for }\alpha\in H_k, 
\end{equation}
\begin{equation}\label{eq:sigma'_k(rho_d(v_k))=sigma_d(rho_d(v_k))}
\sigma'_k\rho_d(v_k)=\sigma_d\rho_d(v_k),\textnormal{ and }
\end{equation}
\begin{equation}\label{eq:sigma_k(u_k)=rho(y_k)}
\sigma'_k(u_k)=\rho(y_k). 
\end{equation}
We define the substitution $\rho_{d+1}$ by:
\begin{equation}\label{def:dom_rho_d}
\dom(\rho_{d+1})=\dom(\rho_d)\cup\{y_k\in\var(r)\mid k\in K_d\},
\end{equation}
\begin{equation}\label{def:rho_d_old}
\rho_{d+1}(z)=\rho_d(z)\textnormal{ if }z\in\dom(\rho_d)\textnormal{, and}
\end{equation}
\begin{equation}\label{def:rho_d_new}
\rho_{d+1}(y_k)=u_k\textnormal{ for }k\in K_d.
\end{equation}
Owing to the assumption that $|\Sigma|\leq|V|$ and $|A|\leq |V|$, we can choose the sets $\rhs(H_k)$ for $k\in K_d$ pairwise disjoint, and disjoint from $\dom(\sigma_d)$ (cf. Lemma~6.4 in \cite{BFvG04}, which is Lemma~6 in the report version of \cite{BFvG04}). We define the substitution $\sigma_{d+1}$ by:
\begin{equation}\label{def:dom_sigma_d}
\dom(\sigma_{d+1})=\dom(\sigma_d)\cup\displaystyle{\bigcup_{k\in K_d}\hspace{-.5em}\rhs(H_k)},
\end{equation}
\begin{equation}\label{def:sigma_d_old}
\sigma_{d+1}(z)=\sigma_d(z)\textnormal{ if }z\in\dom(\sigma_d)\textnormal{, and}
\end{equation}
\begin{equation}\label{def:sigma_d_new}
\sigma_{d+1}(z)=\sigma'_k(z)\textnormal{ if }z\in\rhs(H_k)\textnormal{ for some }k\in K_d.
\end{equation}
Note that $\sigma_{d+1}(z)\in\cterms$ for $z\in\dom(\sigma_{d+1})$.

We proceed to prove (\ref{IH:dom_rho_d})--(\ref{IH:sigma_d_rho_d}) for $d+1$, assuming by induction that they hold for $d$. First, $\dom(\rho_{d+1})\stackrel{(\ref{def:dom_rho_d}),(\ref{IH:dom_rho_d})}=\{z\in\var(r)\mid\depth(z)\leq d+1\}$. Next, we prove that $\var(\rho_{d+1}(z))\subseteq\dom(\sigma_{d+1})$ for $z\in\dom(\rho_{d+1})$.
\begin{itemize}
\item Let $z\in\dom(\rho_d)$. Then $\var(\rho_{d+1}(z))\hspace{-.23em}\stackrel{(\ref{def:rho_d_old})}=\hspace{-.25em}\var(\rho_d(z))\hspace{-.22em}\stackrel{(\ref{IH:var_rho_d})}\subseteq\hspace{-.23em}\dom(\sigma_d)\hspace{-.27em}\stackrel{(\ref{def:dom_sigma_d})}\subseteq\hspace{-.27em}\dom(\sigma_{d+1})$.
\item Let $z=y_k$ for some $k\in K_d$. Then $\var(\rho_{d+1}(z))\stackrel{(\ref{def:rho_d_new})}=\var(u_k)\subseteq\var(\rho_d(v_k))\cup\rhs(H_k)$ by the pureness of $\frac{H_k}{\rho_d(v_k)\trans{c_k}u_k}$. We have $\var(v_k)\stackrel{(\ref{IH:dom_rho_d})}\subseteq\dom(\rho_d)$, so $\var(\rho_d(v_k))\stackrel{(\ref{IH:var_rho_d})}\subseteq\dom(\sigma_d)\stackrel{(\ref{def:dom_sigma_d})}\subseteq\dom(\sigma_{d+1})$. Further, $\rhs(H_k)\stackrel{(\ref{def:dom_sigma_d})}\subseteq\dom(\sigma_{d+1})$.
\end{itemize}
Finally, we prove that $\sigma_{d+1}\rho_{d+1}(z)=\rho(z)$ for $z\in\dom(\rho_{d+1})$.
\begin{itemize}
\item Let $z\in\dom(\rho_d)$. Then $\sigma_{d+1}\rho_{d+1}(z)\stackrel{(\ref{def:rho_d_old})}=\sigma_{d+1}\rho_d(z)\stackrel{(\ref{IH:var_rho_d}),(\ref{def:sigma_d_old})}=\sigma_d\rho_d(z)\stackrel{(\ref{IH:sigma_d_rho_d})}=\rho(z)$.
\item Let $z=y_k$ for some $k\in K_d$. Let $w\in\var(\rho_d(v_k))$. Then $w\stackrel{(\ref{IH:var_rho_d})}\in\dom(\sigma_d)$, and hence $\sigma_{d+1}(w)\stackrel{(\ref{def:sigma_d_old})}=\sigma_d(w)$. Since $\sigma'_k\rho_d(v_k)\stackrel{(\ref{eq:sigma'_k(rho_d(v_k))=sigma_d(rho_d(v_k))})}=\sigma_d\rho_d(v_k)$, it follows that $\sigma_d(w)=\sigma'_k(w)$. Hence
\begin{equation}\label{eq:sigma_d+1w=sigma'_kw}
\sigma_{d+1}(w)=\sigma'_k(w),\textnormal{ if }w\in\var(\rho_d(v_k)) \textnormal{ for some }k\in K_d.
\end{equation}
By the pureness of $\frac{H_k}{\rho_d(v_k)\trans{c_k}u_k}$, we have $\var(u_k)\subseteq\var(\rho_d(v_k))\cup\rhs(H_k)$, so $\sigma_{d+1}\rho_{d+1}(z)\stackrel{(\ref{def:rho_d_new})}=\sigma_{d+1}(u_k)\stackrel{(\ref{def:sigma_d_new}),(\ref{eq:sigma_d+1w=sigma'_kw})}=\sigma'_k(u_k)\stackrel{~(\ref{eq:sigma_k(u_k)=rho(y_k)})}=\rho(z)$.
\end{itemize}
Hence, (\ref{IH:dom_rho_d})-(\ref{IH:sigma_d_rho_d}) hold for $d+1$. 

Now we define a substitution $\rho_\infty$ with $\dom(\rho_\infty)=\var(r)$ as the limit of the $\rho_d$, so
\begin{equation}\label{def:rho_infty}
\rho_\infty(z)=\rho_d(z)\textnormal{ for }z\in\dom(\rho_d)\textnormal{ and }d\in\mathds{N}.
\end{equation}
Let $H=\bigcup_{k\in K}H_k$. We define a closed substitution $\sigma_\infty$ that behaves as the limit of the $\sigma_d$ on variables from $\var(t)\cup\rhs(H)$ and maps all other variables to arbitrary closed terms.
\begin{equation}\label{def:sigma_infty}
\sigma_\infty(z)=\sigma_d(z)\textnormal{ for }z\in\dom(\sigma_d)\textnormal{ and }d\in\mathds{N}.
\end{equation}
The substitutions $\rho_\infty$ and $\sigma_\infty$ are well-defined, owing to (\ref{def:rho_d_old}) and (\ref{def:sigma_d_old}). We verify that the rule $\frac{H}{t\trans a\rho_\infty(v)}$ together with the closed substitution $\sigma_\infty$ satisfies the desired properties.
\begin{itemize}
\item $\frac{H}{t\trans a\rho_\infty(v)}$ is pure xytt:

The right-hand sides of the positive premises in any $H_k$ are distinct variables. By construction, these sets of variables (one for every $k\in K$) are pairwise disjoint, and disjoint from $\var(t)$. Furthermore, the left-hand sides of the premises in any $H_k$ are variables. This makes $\frac{H}{t\trans a\rho_\infty(v)}$ an xytt rule. 

We prove that this rule does not contain free variables. We consider two cases:
\begin{itemize}
\item $z$ is the left-hand side of a premise in $H_k$ for some $k\in K$ and $z\not\in\rhs(H)$. Since $\frac{H_k}{\rho_\infty(v_k)\trans{c_k}u_k}$ is pure, $z\in\var(\rho_\infty(v_k))$.
\item $z\in\var(\rho_\infty(v))$.
\end{itemize}
Since $\var(\rho_\infty(w))\stackrel{(\ref{IH:var_rho_d})}\subseteq\dom(\sigma_\infty)\stackrel{(\ref{def:dom_sigma_0}),(\ref{def:dom_sigma_d})}=\var(t)\cup\rhs(H)$ for $w\in\var(r)$, in either case $z\in\var(t)\cup\rhs(H)$. 

We prove that $\frac{H}{t\trans a\rho_\infty(v)}$ is well-founded. Let $y\in\lhs(H_k)\cap\rhs(H_\ell)$ with $k\in K_d$, $\ell\in K_e$ and $k\neq\ell$. We prove that $e<d$. Since $\frac{H}{t\trans a\rho_\infty(v)}$ is xytt and $y\in\rhs(H_\ell)$, it follows that $y\not\in\rhs(H_k)$ and $y\not\in\var(t)$. Since $\frac{H_k}{\rho_\infty(v_k)\trans{c_k}u_k}$ is pure and $y\in\lhs(H_k)\backslash\rhs(H_k)$, we have $y\in\var(\rho_\infty(v_k))$. This implies that $y\in\var(\rho_d(v_k))\stackrel{(\ref{IH:var_rho_d})}\subseteq\dom(\sigma_d)\stackrel{(\ref{def:dom_sigma_0}),(\ref{def:dom_sigma_d})}\subseteq\var(t)\cup\hspace{-1em}\displaystyle{\bigcup_{k'\in K_{d-1}\cup\ldots\cup K_0}\hspace{-1.9em}\rhs(H_{k'})}$. Since $y\not\in\var(t)$ and $y\in\rhs(H_\ell)$ with $\ell\in K_e$ we have $e\in\{0,\ldots,d-1\}$ and thus $e<d$. Thus, if $\langle x,y\rangle$ and $\langle y,z\rangle$ are edges in the dependency graphs of respectively $H_\ell$ with $\ell\in K_e$ and $H_k$ with $k\in K_d$ and $k\neq\ell$, then $e<d$. Moreover, well-foundedness of the rules $\frac{H_k}{\rho_\infty(v_k)\trans{c_k}u_k}$ for $k\in K$ implies that their dependency graphs do not contain infinite backward chains. Hence, the dependency graph of $H$ does not contain an infinite backwards chain of edges either. Therefore, $\frac{H}{t\trans a\rho_\infty(v)}$ is well-founded.
\item $P\vdash_{\rm irr}\frac{H}{t\trans a\rho_\infty(v)}$:

Since $r\in R$, we have $P\vdash_{\rm irr}\rho_\infty(r)\stackrel{(\ref{def:rho_0}),(\ref{def:rho_d_new})}=\frac{\{\rho_\infty(v_k)\trans{c_k}u_k\mid k\in K\}}{t\trans a\rho_\infty(v)}$. Furthermore, $P\stackrel{(\ref{eq:P_irr_proves_rule})}{\vdash_{\rm irr}}\frac{H_k}{\rho_\infty(v_k)\trans{c_k}u_k}$ for $k\in K$. As $H=\bigcup_{k\in K}H_k$, it follows that $P\vdash_{\rm irr}\frac{H}{t\trans a\rho_\infty(v)}$.

\item $P\vdash\sigma_\infty(\alpha)$ for $\alpha\in H$:

Let $\alpha\in H$. Then there is a $k\in K$ such that $\alpha\in H_k$, so $k\in K_d$ for some $d\geq 0$. By the pureness of $\frac{H_k}{\rho_d(v_k)\trans{c_k}u_k}$, it follows that $\var(\alpha)\subseteq\var(\rho_d(v_k))\cup\var(\rhs(H_k))$, so $P\stackrel{(\ref{eq:P_proves_premises})}\vdash\sigma'_k(\alpha)\stackrel{(\ref{def:sigma_d_new}),(\ref{eq:sigma_d+1w=sigma'_kw})}=\sigma_{d+1}(\alpha))\stackrel{(\ref{def:sigma_infty})}=\sigma_\infty(\alpha)$. 

\item $\sigma_\infty(t)\stackrel{(\ref{def:sigma_0})}=\sigma(t)$.

\item $\sigma_\infty\rho_\infty(v)\stackrel{(\ref{IH:sigma_d_rho_d})}=\rho(v)=p$.
\hfill $\square$
\end{itemize}
\end{trivlist}
We have now obtained the required ruloids, except that we still
have to get rid of unbounded lookahead. We will do this by replacing
any ruloid by one with bounded lookahead.

\begin{definition}[replacement]\label{def:replacement}
We say that a transition rule $r$ \emph{can be replaced by} a transition rule $s$ if $r$ is a substitution instance of $s$ and for any closed substitution instance $\frac{K}{\alpha}$ of $s$ there is a closed substitution instance $\frac{H}{\alpha}$ of $r$ such that $H\subseteq K$.
\end{definition}
Note that if a transition rule $r$ can be replaced by a transition
rule $s$, the TSSs $(\Sigma,R\cup\{r\})$ and $(\Sigma,R\cup\{s\})$
specify the same transition relation. 

The following proposition requires an abundance of variables. Whereas
for Theorem~\ref{thm:ruloid_ready_simulation} and
Propositions~\ref{prop:IC96} and~\ref{prop:pure_tyft} we merely needed
infinitely many variables and $|V|\geq|A|+|\Sigma|$, here we
need uncountably many variables and $|V|>|\Sigma|$, so that we have
$|V|>|\cterms|$.

\begin{proposition}\label{prop:replacement}
Suppose $V$ is uncountable and $|\Sigma|<|V|$.
Any pure xytt rule $r$ can be replaced by a pure xytt rule $s$ with bounded lookahead with the same conclusion.
\end{proposition}

\begin{proof}
Let $r = \frac{H}{\alpha}$. 
Let $\kappa$ be an infinite cardinal, such that $|\cterms|<\kappa \leq |V|$, and let $\mathcal{O}_\kappa$ denote the set of sequences of strictly decreasing ordinals that have a cardinality smaller than $\kappa$. 
Let $V(r)$ denote the finite set of variables $y_0$ such that $r$ has premises $y_0 \trans{a_1} y_1 \trans{a_2} \cdots \trans{a_n} y_n$ for $n\geq 0$ with $y_n$ occurring in $\alpha$, and let $U(r)$ be the set of all other variables occurring in $r$. 
For every variable $x\in U(r)$ and $\eta\in\mathcal{O}_\kappa$, pick a distinct variable $x_\eta\in V$ not occurring in $r$. 
This is possible because $|{\cal O}_\kappa| = \kappa$.
Let $s=\frac{K}{\alpha}$ with
$$\begin{array}{ll}
K =& \{x\trans{a}y \mid (x\trans{a}y)\in H,\ y \in V(r)\}\;\cup \\
& \{x\trans{a}y_\lambda \mid (x\trans{a}y)\in H,\ x\in V(r),\ y\in U(r),\ \lambda < \kappa\}\;\cup\\
& \{x_\eta\trans{a}y_{\eta\lambda} \mid (x\trans{a}y)\in H,\ x\in U(r),\ \eta,\eta\lambda\in\mathcal{O}_\kappa\}.\\
\end{array}$$
By definition $s$ is an xytt rule, and if $r$ is pure then so is $s$. As there are only finitely many variables occurring in $\alpha$, and there is no infinite chain of strictly decreasing ordinals, the rule $s$ has bounded lookahead. It remains to be shown that $r$ can be replaced by $s$.

First of all the substitution $\xi$ given by $\xi(x_\eta)=x$ for all $x\in U(r)$ and $\eta\in\mathcal{O}_\kappa$ shows that $r$ is a substitution instance of $s$.

Now consider a closed substitution $\sigma$. We need to define a closed substitution $\rho$, such that $\rho(H) \subseteq \sigma(K)$ and $\rho(\alpha)=\sigma(\alpha)$. For $x \in V(r)$ let $\rho(x)=\sigma(x)$. Since $x\in V(r)$ for $x\in\var(\alpha)$, $\rho(\alpha)=\sigma(\alpha)$. 
Define the {\em relative depth} ${\it rd}(x)$ of variables $x\in\var(r)$ by
$$\begin{array}{l@{~~}l}
{\it rd}(x) = 0              & \textnormal{for }x \in V(r)\\
{\it rd}(y) = rd(x)+1        & \textnormal{for }y \in U(r)\textnormal{ and }(x\trans a y)\in H.
\end{array}$$
As in Definition~\ref{def:depth} this is well-defined because $r$ is well-founded. With induction on the relative depth of $x \in U(r)$ we are going to define $\rho(x)$ and $S_x\subseteq\linebreak[4]\{\eta\in\mathcal{O}_\kappa \mid \sigma(x_\eta) = \rho(x)\}$ such that $|\{\lambda<\kappa \mid \exists\eta\in\mathcal{O}_\kappa: \eta\lambda\in S_x\}| = \kappa$.

\noindent \emph{Base case}: Let $x \in V(r)$, $y \in U(r)$ and $(x \trans{a} y) \in H$. As $|\cterms|<\kappa$, there must be a set $S \subseteq \{\lambda \mid \lambda<\kappa\}$ with $|S|=\kappa$ and $\sigma(y_\lambda) = \sigma(y_{\lambda'})$ for $\lambda,\lambda' \in S$. Let $\rho(y) = \sigma(y_\lambda)$ for some $\lambda \in S$. We define $S_y=S$. Then we have $\rho(x \trans{a} y) = \sigma(x \trans{a} y_\lambda) \in \sigma(K)$ for $\lambda\in S_y$ and $|\{\lambda<\kappa \mid \exists\eta\in{\cal O}_\kappa: \eta\lambda\in S_y\}| = |S_y| = \kappa$.

\noindent \emph{Induction step}: Let $x \in U(r)$, $\rho(x)$ is already defined, and $(x \trans{a} y) \in H$. As $|\{\lambda<\kappa \mid \exists\eta\in{\cal O}_\kappa: \eta\lambda\in S_x\}| = \kappa$ and hence $|\{\nu \mid \exists\eta\lambda\in S_x: \nu < \lambda\}| = \kappa$, whereas $|T(\Sigma)| < \kappa$, there must be a set $S' \subseteq \{\eta\nu \in {\cal O}_\kappa \mid \eta\in S_x\}$ with $|\{\nu<\kappa \mid \exists\eta\in{\cal O}_\kappa: \eta\nu\in S'\}| = \kappa$ and $\sigma(y_\eta) = \sigma(y_{\eta'})$ for $\eta,\eta'\in S'$. Let $\rho(y) = \sigma(y_{\eta\nu})$ for some $\eta\nu\in S'$. We define $S_y = S'$. Then we have $\rho(x\trans{a}y)=\sigma(x_{\eta}\trans{a}y_{\eta\nu})\in\sigma(K)$ for $\eta\nu\in S_y$. Hence, $\rho(H)\subseteq\sigma(K)$. So $r$ can be replaced by $s$.
\end{proof}
In the following definition of a ruloid and the forthcoming
Theorems~\ref{thm:ruloid-tyft/tyxt} and~\ref{thm:decomposition} we
assume the existence of sufficiently many variables (satisfying the
conditions of Propositions~\ref{prop:pure_tyft} and~\ref{prop:replacement}).
However, this assumption will be discharged in
Section~\ref{sec:discharge}, showing that our mail result
(Theorem~\ref{thm:decomposition}) will hold regardless.

\begin{definition}[ruloid]\label{def:ruloid}
Let $P$ be a TSS in tyft/tyxt format. According to Proposition~\ref{prop:IC96} there is a TSS $Q$ in pure xyft format, such that $P\vdash\alpha\Leftrightarrow Q\vdash\alpha$ for all closed positive literals $\alpha$. The set of \emph{$P$-ruloids} is obtained by first taking the set of pure xytt rules, irredundantly provable from $Q$, and next replacing each of these pure xytt rules by one with bounded lookahead, using Proposition~\ref{prop:replacement}. 
\end{definition}

\begin{theorem}\label{thm:ruloid-tyft/tyxt}

Suppose $V$ is uncountable and $|A|\leq|V|$.
Let $P=(\Sigma,R)$ be a TSS in tyft/tyxt format with $|\Sigma|<|V|$. Then $P\vdash\sigma(t)\trans a p$ for $t\in\terms$, $p\in\cterms$ and $\sigma$ a closed substitution, if and only if there are a $P$-ruloid $\frac{H}{t\trans a u}$ and a closed substitution $\sigma'$ with $P\vdash\sigma'(\alpha)$ for $\alpha \in H$, $\sigma'(t)=\sigma(t)$ and $\sigma'(u)=p$.
\end{theorem}

\begin{proof}
According to Proposition~\ref{prop:IC96} there is a TSS $Q$ in pure xyft format, such that $P\vdash\alpha\Leftrightarrow Q\vdash\alpha$ for all closed positive literals $\alpha$.

\fbox{$\Rightarrow$} Suppose $P\vdash\sigma(t)\trans a p$. Then $Q\vdash\sigma(t)\trans a p$. According to Proposition~\ref{prop:pure_tyft} ($\Rightarrow$), there are a pure xytt rule $\frac{G}{t\trans a u}$ and a closed substitution $\sigma'$ with $Q\vdash_{\rm irr}\frac{G}{t\trans a u}$, $Q\vdash\sigma'(\alpha)$ for $\alpha\in G$, $\sigma'(t)=\sigma(t)$ and $\sigma'(u)=p$. Replace $\frac{G}{t\trans a u}$ by the $P$-ruloid $\frac{H}{t\trans a u}$, using Proposition~\ref{prop:replacement}. According to Definition~\ref{def:replacement}, there is a substitution $\sigma''$ such that $\sigma''(\frac{H}{t\trans a u})=\frac{G}{t\trans a u}$. Hence $Q\vdash\sigma'\sigma''(\alpha)$ for $\alpha\in H$, $\sigma''(t)=t$ and $\sigma''(u)=u$. Thus for the $P$-ruloid $\frac{H}{t\trans a u}$ and the closed substitution $\sigma'\sigma''$ we have $P\vdash\sigma'\sigma''(\alpha)$ for $\alpha\in H$, $\sigma'\sigma''(t)=\sigma'(t)=\sigma(t)$ and $\sigma'\sigma''(u)=\sigma'(u)=p$.

\fbox{$\Leftarrow$} Suppose there are a $P$-ruloid $\frac{H}{t\trans a u}$ and a closed substitution $\sigma'$ with $P\vdash\sigma'(\alpha)$ for $\alpha\in H$, $\sigma'(t)=\sigma(t)$ and $\sigma'(u)=p$. Then $Q\vdash\sigma'(\alpha)$ for $\alpha\in H$. $\frac{H}{t\trans a u}$ is a replacement of a pure xytt rule $\frac{G}{t\trans a u}$ irredundantly provable from $Q$. According to Definition~\ref{def:replacement}, for $\sigma'(\frac{H}{t\trans a u})$ there is a closed substitution $\sigma''$ such that $\sigma''(G)\subseteq\sigma'(H)$, $\sigma''(t)=\sigma'(t)$ and $\sigma''(u)=\sigma'(u)$. Since $Q\vdash\sigma'(\alpha)$ for $\alpha\in H$, we have $Q\vdash\sigma''(\alpha)$ for $\alpha\in G$. Thus according to Proposition~\ref{prop:pure_tyft} ($\Leftarrow$) we have $Q\vdash\sigma(t)\trans a p$, so $P\vdash\sigma(t)\trans a p$.
\end{proof}


\subsection{Decomposition of HML Formulas}\label{sec:decomposition_hml_formulas}

Given a TSS $P=(\Sigma,R)$ in tyft/tyxt format or in ready simulation format, the following definition assigns to each term $t\in\terms$ and each observation $\phi\in\mathds{O}$ a collection $t^{-1}_P(\phi)$ of decomposition mappings $\psi:V\rightarrow\mathds{O}$. Each of these mappings $\psi\in t^{-1}_P(\phi)$ guarantees, given a closed substitution $\sigma$, that $\sigma(t)$ satisfies $\phi$ if $\sigma(x)$ satisfies the formula $\psi(x)$ for all $x\in\var(t)$. Moreover, whenever for some closed substitution $\sigma$ the term $\sigma(t)$ satisfies $\phi$, there must be a $\psi \in t^{-1}_P(\phi)$ with $\sigma(x)$ satisfying $\psi(x)$ for all $x \in \var(t)$. This is formalised in Theorem~\ref{thm:decomposition}.

\begin{definition}\label{def:inverse}
Let $P=(\Sigma,R)$ be a TSS in tyft/tyxt format (resp.\ ready
simulation format) and assume that the set $V$ of variables is
infinite, with $|V|\geq|A|$ and $|V|>|\Sigma|$.
Then $\cdot_P^{-1}:\terms\rightarrow(\mathds{O}\rightarrow\pow(V\rightarrow\mathds{O}))$ is defined by:
\begin{itemize}
\item $\psi\in t_P^{-1}(\diam{a}\phi)$ iff there is a $P$-ruloid $\frac{H}{t\trans{a}u}$ and a $\chi\in u^{-1}_P(\phi)$ and $\psi:V\rightarrow\mathds{O}$ is given by
\[\psi(x)=\left\{
  \begin{array}{@{}l@{~~~~}l}
  \displaystyle{\bigwedge_{(x\trans{b}y)\in H}\!\!\!\!\!\diam{b}\psi(y) 
                ~\land~ \bigwedge_{(x\ntrans{c})\in H}\!\!\!\!\!\neg\diam{c}\top} ~\land~ \chi(x) & \mbox{if $x\in\var(u)$}\\[5ex]
  \displaystyle{\bigwedge_{(x\trans{b}y)\in H}\!\!\!\!\!\diam{b}\psi(y)
                ~\land~ \bigwedge_{(x\ntrans{c})\in H}\!\!\!\!\!\neg\diam{c}\top} & \mbox{if $x\not\in\var(u)$}
  \end{array}
\right.\]

\item $\psi\in t_P^{-1}(\bigwedge_{i\in I}\phi_i)$ iff 
\[\psi(x)= \displaystyle{\bigwedge_{i\in I}\psi_i(x)}\]
where $\psi_i\in t_P^{-1}(\phi_i)$ for $i\in I$.
\item $\psi\in t_P^{-1}(\neg\phi)$ iff there is a function $h:t_P^{-1}(\phi)\rightarrow\var(t)$ and $\psi:V\rightarrow\mathds{O}$ is given by
\[\psi(x)= \displaystyle{\bigwedge_{\chi\in h^{-1}(x)}\!\!\!\neg\chi(x)} \]
\end{itemize}
\end{definition}
To explain the idea behind Definition~\ref{def:inverse}, we expand on
two of its cases. Consider $t_P^{-1}(\diam{a}\phi)$, and let $\sigma$
be any closed substitution. The question is under which conditions
$\psi(x)\in\mathds{O}$ on $\sigma(x)$, for $x\in\var(t)$, there is a
transition $\sigma(t)\trans{a}q$ with $q\models\phi$. According to
Theorems~\ref{thm:ruloid_ready_simulation}
and~\ref{thm:ruloid-tyft/tyxt}, there is such a transition if and only
if there is a closed substitution $\sigma'$ with $\sigma'(t)=\sigma(t)$ and
a $P$-ruloid $\frac{H}{t\trans{a}u}$ such that (1) the premises in
$\sigma'(H)$ are satisfied and (2) $\sigma'(u)\models\phi$. The first
condition is covered if for $x\in\var(t)$, $\psi(x)$ contains
conjuncts $\diam{b}\psi(y)$ for $x\trans{b}y\in H$ and conjuncts
$\neg\diam{c}\top$ for $x\ntrans{c}\;\in H$. By adding, for some
$\chi\in u^{-1}(\phi)$, a conjunct $\chi(x)$ if $x\in\var(u)$, the
second condition is covered as well.

Consider $t_P^{-1}(\neg\phi)$, and let $\sigma$ be any closed substitution. We have $\sigma(t)\not\models\phi$ if and only if there is no $\chi\in t^{-1}(\phi)$ such that $\sigma(x)\models\chi(x)$ for all $x\in\var(t)$. In other words, for each $\chi\in t^{-1}(\phi)$, $\psi(x)$ must contain a conjunct $\neg\chi(x)$, for some $x\in\var(t)$.

Each $\psi(x)$ in Definition~\ref{def:inverse} is a HML formula, owing to the fact that the rule $\frac{H}{t\trans{a} u}$ in the definition of $t^{-1}_P(\diam{a}\phi)$ has bounded lookahead. When clear from the context, subscripts $P$ will be omitted.

\begin{theorem}\label{thm:decomposition}
\hspace{-1pt}
Let $P=(\Sigma,R)$ be a complete TSS in tyft/tyxt format (resp.\ ready simulation format). For any $t\in\terms$, $\sigma:V\rightarrow\cterms$ and $\phi\in\mathds{O}$:
\[
\sigma(t)\models_P\phi~~\Leftrightarrow~~
\exists\psi\in t^{-1}_P(\phi)\,\forall x\in\var(t):\sigma(x)\models_P\psi(x)
\]
\end{theorem}

\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]
With induction on the structure of $\phi$. Here we assume that $V$ is
infinite, $|V|\geq|A|$ and $|V|>|\Sigma|$. This assumption will be
discharged in Section~\ref{sec:discharge}.
\begin{itemize}
\item $\phi=\diam{a}\phi'$

\fbox{$\Rightarrow$} Suppose $\sigma(t)\models\diam{a}\phi'$. Then by Definition~\ref{def:sat} there is a $p\in\cterms$ with $P\vdash_{\it ws}\sigma(t)\trans{a}p$ and $p\models\phi'$. Thus, by Theorem~\ref{thm:ruloid-tyft/tyxt} (resp.\ Theorem~\ref{thm:ruloid_ready_simulation}) there must be a $P$-ruloid $\frac{H}{t\trans{a}u}$ and a closed substitution $\sigma'$ with $P\vdash_{\it ws}\sigma'(\alpha)$ for $\alpha \in H$, $\sigma'(t)=\sigma(t)$, i.e.\ $\sigma'(x)=\sigma(x)$ for $x\in\var(t)$, and $\sigma'(u)=p$. Since $\sigma'(u)\models\phi'$, the induction hypothesis can be applied, and there must be a $\chi\in u^{-1}(\phi')$ such that $\sigma'(z)\models\chi(z)$ for all $z\in\var(u)$. Now define $\psi\in t^{-1}(\diam{a}\phi')$ as indicated in Definition~\ref{def:inverse}, using $\frac{H}{t\trans{a}u}$ and $\chi$. For $\mbox{$(x\trans{b}y)$}\in H$ one has $P\vdash_{\it ws}\sigma'(x)\trans{b}\sigma'(y)$. Moreover, for $(x\ntrans{c})\in H$ one has $P\vdash_{\it ws}\sigma'(x)\ntrans{c}$, so the consistency of $\vdash_{\it ws}$ yields $P\not\vdash_{\it ws}\sigma'(x)\trans{c}q$ for all $q\in\cterms$, and thus $\sigma'(x)\models\neg\diam{c}\top$. We proceed to prove that $\sigma'(x)\models\psi(x)$ for $x\in V$. We apply ordinal induction on the {\em lookahead of $x$ in $H$}, which is defined by
\[
\sup\{1+\mbox{lookahead of $y$ in $H$}\mid x\trans{b}y\in H\mbox{ for some }b\in A\}
\]
Since $\frac{H}{t\trans{a}u}$ has bounded lookahead, the lookahead of $x$ in $H$ is a well-defined ordinal number. We distinguish two cases.
\begin{description}
\item
$x\in\var(u)$. Then $\psi(x)=\bigwedge_{(x\trans{b}y)\in H}\diam{b}\psi(y)\land \bigwedge_{(x\ntrans{c})\in H}\neg\diam{c}\top\land\chi(x)$. By induction on lookahead $\sigma'(y)\models\psi(y)$, so $\sigma'(x)\models\diam{b}\psi(y)$ for $(x\trans{b}y)\in H$. Since moreover $\sigma'(x)\models\neg\diam{c}\top$ for $(x\ntrans{c})\in H$ and $\sigma'(x)\models\chi(x)$, it follows that $\sigma'(x)\models\psi(x)$.

\item
$x\not\in\var(u)$. Then $\psi(x)=\bigwedge_{(x\trans{b}y)\in H}\diam{b}\psi(y)\land \bigwedge_{(x\ntrans{c})\in H}\neg\diam{c}\top$. By induction on lookahead $\sigma'(y)\models\psi(y)$, so $\sigma'(x)\models\diam{b}\psi(y)$ for $(x\trans{b}y)\in H$. Since moreover $\sigma'(x)\models\neg\diam{c}\top$ for $(x\ntrans{c})\in H$, it follows that $\sigma'(x)\models\psi(x)$.
\end{description}
Finally, $\sigma(x)=\sigma'(x)\models\psi(x)$ for $x\in\var(t)$.

\fbox{$\Leftarrow$} Suppose that there is a $\psi\in t^{-1}(\diam{a}\phi')$ such that $\sigma(x)\models\psi(x)$ for all $x\in\var(t)$.
Let $\psi$ be defined in terms of the $P$-ruloid $\frac{H}{t\trans{a}u}$ and $\chi\in u^{-1}(\varphi')$. We define a closed substitution $\sigma'$ with as domain the variables in this $P$-ruloid such that:
\begin{equation}\label{eq:source}
\sigma'(t)=\sigma(t),
\end{equation}
\begin{equation}\label{eq:pos_prem}
P \vdash_{\it ws} \sigma'(x) \trans{b} \sigma'(y)\textnormal{ for }(x \trans{b}y) \in H,
\end{equation}
\begin{equation}\label{eq:neg_prem}
P \vdash_{\it ws} \sigma'(x) \ntrans{c}\textnormal{ for }(x \ntrans{c}) \in H;\textnormal{ and}
\end{equation}
\begin{equation}\label{eq:sat}
\sigma'(y)\models\psi(y)\textnormal{ for }y\in\dom(\sigma').
\end{equation}
$\sigma'(y)$ is defined by induction on the depth of $y$ in the $P$-ruloid.
\begin{itemize}
\item
$\depth(y)=0$. Then $y\in\var(t)$. We define $\sigma'(y)=\sigma(y)$. This yields property (\ref{eq:source}). Moreover, property (\ref{eq:sat}) for $y$ holds. The formula $\psi(y)$ contains the conjunct $\neg\diam{c}\top$ for $(y\ntrans{c})\in H$, so by the completeness of $P$, property (\ref{eq:sat}) for $y$ implies property (\ref{eq:neg_prem}) for $y$.
\item
$\depth(y)>0$. Let $x \trans{b} y$ be the positive premise in the $P$-ruloid with right-hand side $y$. By induction, $\sigma'(x)$ is already defined. By property (\ref{eq:sat}), $\sigma'(x) \models \psi(x)$, so $\sigma'(x) \models \diam{b}\psi(y)$. Hence, $P \vdash_{\it ws} \sigma'(x) \trans{b} p$ for some $p \in \cterms$ with $p \models \psi(y)$. We define $\sigma'(y)=p$. Then property (\ref{eq:pos_prem}) for the premise $x \trans{b} y$ and property (\ref{eq:sat}) for $y$ hold. By the completeness of $P$, property (\ref{eq:sat}) for $y$ implies that property (\ref{eq:neg_prem}) for $y$ holds as well.
\end{itemize}
Since $\psi(z)$ implies $\chi(z)$ for $z\in\var(u)$, property (\ref{eq:sat}) yields $\sigma'(y) \models \chi(y)$ for $y\in \var(u)$. Thus the induction hypothesis can be applied, so $\sigma'(u) \models \phi'$. By properties (\ref{eq:source})--(\ref{eq:neg_prem}) together with Theorem~\ref{thm:ruloid-tyft/tyxt} (resp.\ Theorem~\ref{thm:ruloid_ready_simulation}), $P \vdash_{\it ws} \sigma(t) \trans{a} \sigma'(u)$. Hence, $\sigma(t)\models\diam{a}\phi'$.

\item $\phi=\bigwedge_{i\in I}\phi_i$

$\sigma(t) \models \bigwedge_{i\in I}\phi_i~\Leftrightarrow~ \forall i\!\in\! I: \sigma(t) \models \phi_i ~\\\Leftrightarrow~ \forall i\!\in\! I ~\exists \psi_i \!\in\! t^{-1}(\phi_i) ~\forall x\!\in\!\var(t): \sigma(x) \models \psi_i(x) ~\\\Leftrightarrow~ \exists \psi \!\in\! t^{-1}(\bigwedge_{i\in I}\phi_i)~\forall x\!\in\! \var(t): \sigma(x) \models \psi(x)$.

\item $\phi=\neg\phi'$

$\sigma(t)\models\neg\phi'~\Leftrightarrow~\sigma(t)\not\models\phi'~\\
  \Leftrightarrow~\exists h:t^{-1}(\phi')\rightarrow \var(t)\ \forall\chi\in
  t^{-1}(\phi'):\sigma(h(\chi))\not\models\chi(h(\chi))~\\\Leftrightarrow~
  \exists h:t^{-1}(\phi')\rightarrow \var(t)\ \forall
  x\in\var(t):\sigma(x)\models\bigwedge_{\chi\in h^{-1}(x)}\neg\chi(x)~\\
  \Leftrightarrow~\exists\psi\in t^{-1}(\neg\phi')\ \forall
  x\in\var(t):\sigma(x)\models\psi(x)$.
\hfill $\square$\end{itemize}
\end{trivlist}

\subsection{Counting variables}\label{sec:discharge}

So far we have developed a modal decomposition method that applies to
arbitrary languages with a structural operational semantics in
tyft/tyxt format or in ready simulation format, provided that we have
an uncountable set of variables whose cardinality exceeds the
cardinality of the collection of operators in the language, and at
least equals the cardinality of the set of actions. In computer
science applications, however, it is customary to work with countable
sets of variables. Here we show that our decomposition result applies
regardless of the cardinality of the set of variables.

Assume a given set of \emph{true variables} $V_{\it true}$. These are
the only ones that are used in a given application. Now, given a set
of actions $A$ and a TSS $P=(\Sigma,R)$, we \emph{define} an
uncountable set $V\supseteq V_{\it true}$ satisfying $|V|\geq |A|$
and $|V|>|\Sigma|$.  The elements of $V$ are called \emph{variables}
and variables in $V-V_{\it true}$ are \emph{virtual variables}.
As long as only the true variables appear in TSSs and specifications
of processes, nothing stops us from defining any amount of virtual
variables to be used in our constructions. Terms, TSSs, ruloids and
other syntactic constructions are called \emph{true} if they only
contain true variables, and \emph{virtual} otherwise.

Theorems~\ref{thm:ruloid_ready_simulation}
and~\ref{thm:ruloid-tyft/tyxt} (our intermediate results) apply merely
to virtual ruloids; they may fail to hold for true ruloids.
Definition~\ref{def:inverse} on the other hand provides a modal
decomposition $t^{-1}(\phi)$ for any virtual term $t$ (and any HML
formula $\phi$), and thus surely for every true term $t$. Such a modal
decomposition consists of a set of decomposition mappings $\psi$, each
of which allocates an HML formula $\psi(x)$ to every variable $x$.  As
only the $\psi(x)$ for $x\in \var(t)$ play a r\^ole in
Theorem~\ref{thm:decomposition}, nothing is lost by restricting the
domain of $\psi(x)$ to $\var(t)$. (This is an \emph{a posteriori}
restriction; virtual variables may have been used in the definition of
$\psi(x)$.) Using this restriction of the decomposition mappings,
Theorem~\ref{thm:decomposition} restricts to a valid statement
involving true variables only.

\subsection{Examples}\label{sec:examples}

We give two examples of the application of Theorem~\ref{thm:decomposition}.
\begin{example}\label{ex:negation}
Let $A=\{a,b\}$ and $P=(\Sigma,R)$, where $\Sigma$ consists of the constant $c$ and the binary function symbol $f$, and $R$ is:
$$
c\trans a c
\qquad
\frac{x_1\trans{a} y}{f(x_1,x_2)\trans{b} y}
\qquad
\frac{x_2\trans{a} y \quad x_1 \ntrans{b}}{f(x_1,x_2)\trans{b} y}
$$
This TSS is complete and in ready simulation format. We proceed to compute $f(x_1,x_2)^{-1}(\diam{b}\top)$. The only two $P$-ruloids (modulo $\alpha$-conversion) with a conclusion $f(x_1,x_2)\trans{b}\_$ are
$$
\frac{x_1\trans{a} y}{f(x_1,x_2)\trans{b} y}
\qquad
\frac{x_2\trans{a} y \quad x_1 \ntrans{b}}{f(x_1,x_2)\trans{b} y}
$$
According to Definition~\ref{def:inverse}, $f(x_1,x_2)^{-1}(\diam{b}\top)=\{\psi_1,\psi_2\}$ where $\psi_1$ and $\psi_2$ are defined as follows, using some $\chi\in y^{-1}(\top)$ (so $\chi(x)=\top$ for all $x\in V$):
$$
\begin{array}{l@{~~~~~}l}
\psi_1(y)=\chi(y)=\top                                        & \psi_2(y)=\chi(y)=\top \\
\psi_1(x_1)=\diam{a}\psi_1(y)=\diam{a}\top                    & \psi_2(x_1)=\neg\diam{b}\top \\
\psi_1(z)=\top \mbox{ if } z\not\in\{y,x_1\}                  & \psi_2(x_2)=\diam{a}\psi_2(y)=\diam{a}\top \\
                                                              & \psi_2(z)=\top \mbox{ if } z\not\in\{y,x_1,x_2\}
\end{array}
$$
So by Theorem~\ref{thm:decomposition} a closed term $f(p_1,p_2)$ can execute a $b$ if and only if $p_1$ can execute an $a$, or $p_1$ cannot execute a $b$ and $p_2$ can execute an $a$.

We proceed to compute $f(x_1,x_2)^{-1}(\neg\diam{b}\top)$. There are four possible functions $h:f(x_1,x_2)^{-1}(\diam b\top)\rightarrow\var(f(x_1,x_2))$, yielding four possible definitions of $\psi\in f(x_1,x_2)^{-1}(\neg\diam{b}\top)$. In all four cases, $\psi(z)=\top$ for $z\not\in\{x_1,x_2\}$.
\begin{enumerate}
\item If $h(\psi_1)=h(\psi_2)=x_1$ then
    \[\begin{array}{@{}l}
    \psi(x_1)=\neg\psi_1(x_1)\land\neg\psi_2(x_1)=\neg\diam a\top\land\neg\neg\diam b\top=\neg\diam a\top\land\diam b\top\\
    \psi(x_2)=\top
    \end{array}\]
\item If $h(\psi_1)=h(\psi_2)=x_2$ then
    \[\begin{array}{@{}l}
    \psi(x_1)=\top\\
    \psi(x_2)=\neg\psi_1(x_2)\land\neg\psi_2(x_2)=\neg\top\land\neg\diam a\top
    \end{array}\]
\item If $h(\psi_1)=x_1$ and $h(\psi_2)=x_2$ then
    \[\begin{array}{@{}l}
    \psi(x_1)=\neg\psi_1(x_1)=\neg\diam a\top\\
    \psi(x_2)=\neg\psi_2(x_2)=\neg\diam a\top
    \end{array}\]
\item If $h(\psi_1)=x_2$ and $h(\psi_2)=x_1$ then
    \[\begin{array}{@{}l}
    \psi(x_1)=\neg\psi_2(x_1)=\neg\neg\diam b\top=\diam b\top\\
    \psi(x_2)=\neg\psi_1(x_2)=\neg\top
    \end{array}\]
\end{enumerate}
By Theorem~\ref{thm:decomposition} a closed term $f(p_1,p_2)$ can\emph{not} execute a $b$ if and only if either (1) $p_1$ can execute a $b$ but not an $a$, or (3) neither $p_1$ nor $p_2$ can execute an $a$. The other two possibilities (2) and (4) do not qualify, since no term can ever satisfy $\neg\top$.
\end{example}

\begin{example}\label{ex:lookahead}
Let $A=\{a,b\}$ and $P=(\Sigma,R)$, where $\Sigma$ consists of the constant $c$ and the unary function symbol $f$, and $R$ is:
$$
c\trans a c
\qquad
\frac{x\trans{a} y}{f(x)\trans{b}y}
\qquad
\frac{x\trans{b} y \quad y\trans{a} z}{f(x)\trans{a}f(y)}
$$
This TSS is complete and in tyft/tyxt format. We compute $f(f(x))^{-1}(\diam b \diam a\top)$. The only $P$-ruloid (modulo $\alpha$-conversion) with a conclusion $f(f(x))\trans{b}\_$ is
$$
\frac{x\trans{b}y \quad y\trans{a} z}{f(f(x))\trans{b}f(y)}
$$
So for each $\psi\in f(f(x))^{-1}(\diam b \diam a\top)$ we have $\psi(x)=\diam b\psi(y)=\diam b(\diam a\psi(z)\land\chi(y))=\diam b(\diam a\top\land\chi(y))$ with $\chi\in f(y)^{-1}(\diam a\top)$. The only $P$-ruloid (modulo $\alpha$-conversion) with a conclusion $f(y)\trans{a}\_$ is
$$
\frac{y\trans{b}z \quad z\trans{a}w}{f(y)\trans{a}f(z)}
$$
So $\chi(y)=\diam b\chi(z)=\diam b(\diam a\chi(w)\land\chi'(z))=\diam b(\diam a\top\land\chi'(z))$ for some $\chi'\in f(z)^{-1}(\top)$. Since $\chi'(z)=\top$, $\psi(x)=\diam b(\diam a\top\land\diam b\diam a\top)$.

By Theorem~\ref{thm:decomposition} a closed term $f(f(p))$ can execute a $b$ followed by an $a$ if and only if $p\trans{b}p'$ where $p'$ can execute an $a$ and also a $b$ followed by an $a$.
\end{example}


\subsection{Counterexamples}\label{sec:counter-examples}

The following example shows that in Theorem~\ref{thm:decomposition} it is essential that the TSS is complete. That is, the result would fail if we took the transition relation induced by a TSS to consist of those transitions for which a well-supported proof exists.

\begin{example}
Let $A=\{a,b\}$ and $P=(\Sigma,R)$, where $\Sigma$ consists of the constant $c$ and the unary function symbol $f$, and $R$ is:
$$
\frac{x\ntrans{a}}{f(x)\trans{b}c}
\qquad
\frac{c\ntrans{a}}{c\trans{a}c}
$$
As shown in Example~\ref{exa:well-supported}, this TSS, which is in
ready simulation format, is incomplete. In particular, neither $P\vdash_{\it ws} c\trans{a}p$ for a closed term $p$ nor $P\vdash_{\it ws} c\ntrans{a}$.

Let us assume that the transition relation induced by this TSS consists of those transitions for which a well-supported proof exists. Then there is no $a$-transition for $c$ and no $b$-transition for $f(c)$, so $c\models_P\neg\diam a \top$ and $f(c)\models_P\neg\diam b \top$.

The only $P$-ruloid with a conclusion $f(x)\trans{b}\_$ is $\frac{x\ntrans{a}}{f(x)\trans{b}c}$. Hence Theorem~\ref{thm:decomposition} would yield $f(c)\models_P \diam b \top \Leftrightarrow c\models_P\neg\diam a \top$. Since this is false, Theorem~\ref{thm:decomposition} would fail with respect to $P$.
\end{example}

Finally, we argue that Theorem~\ref{thm:ruloid_ready_simulation} and Theorem~\ref{thm:ruloid-tyft/tyxt} cannot be combined in a straightforward fashion to apply to TSSs that contain both bounded lookahead and negative premises.

\begin{example}
Let $A=\{a,b\}$ and $P=(\Sigma,R)$, where $\Sigma$ consists of the constant $0$, the unary function symbols $a\_$, $b\_$ and $f$ and the binary function symbol $\_+\_$, and $R$ is as follows for all $m\in A$:
$$
\frac{x\trans m x'}{x+y\trans m x'}
\qquad
\frac{y\trans m y'}{x+y\trans m y'}
\qquad
m x\trans m x
$$

$$
\frac{x\trans{a}y}{f(x)\trans{a}f(y)}
\qquad
\frac{x\trans a y \quad y\ntrans b}{f(x)\trans b 0}
$$
This TSS is complete and in nxyft format. Note that for closed substitutions $\sigma$,
$$\begin{array}{clcl}
&\sigma(f(f(x)))&\models&\diam{b}\top \\
\Leftrightarrow~~ & \sigma(f(x))&\models&\diam{a}(\neg\diam{b}\top) \\
\Leftrightarrow~~ & \sigma(x)&\models&\diam{a}\neg(\diam{a}\neg\diam{b}\top)
\end{array}$$
Suppose that there would exist a notion of $P$-ruloids, being nxytt rules, such that $P\vdash_{\it ws}\sigma(f(f(x)))\trans a 0$ for $\sigma$ a closed substitution if and only if there are a $P$-ruloid $\frac{H}{f(f(x))\trans a u}$ and a closed substitution $\sigma'$ with $P\vdash_{\it ws}\sigma'(\alpha)$ for $\alpha \in H$, $\sigma'(x)=\sigma(x)$ and $\sigma'(u)=0$. In that case we would have, as in Theorem~\ref{thm:decomposition}, that for all closed substitutions $\sigma$,
\[
\sigma(f(f(x)))\models\diam{b}\top ~~\Leftrightarrow~~ \exists \psi\in f(f(x))^{-1}(\diam{b}\top):\sigma(x)\models\psi(x)
\]
However, according to Definition~\ref{def:inverse}, for each $\psi\in f(f(x))^{-1}(\diam{b}\top)$ and $y\in V$, $\psi(y)$ does not contain nested negations, whereas the formula $\diam{a}\neg(\diam{a}\neg\diam{b}\top)$ above cannot be written as a (possibly infinite) disjunction of HML formulas (as defined in Definition~\ref{def:HML}) without nested negations.
The latter follows because the formula $\diam{a}\neg(\diam{a}\neg\diam{b}\top)$
distinguishes the two process of Figure~\ref{fig:2-nested}---yet these
processes are \emph{2-nested simulation equivalent} \cite{GV92} and 2-nested
equivalent processes cannot be distinguished by HML formulas without
nested negations \cite{GV92}.
\begin{figure}
\unitlength 1mm
\begin{center}
\begin{picture}(40,40)(-20,-13)
\put(0,33.5){\vector(0,-1){3}}
\put(0,30){\circle{1}}
\put(-.35,29.65){\vector(-1,-1){9.3}}
\put(-8,25){$a$}
\put(-10,20){\circle{1}}
\put(-10.35,19.65){\vector(-1,-1){9.3}}
\put(-18,15){$a$}
\put(-20,10){\circle{1}}
\put(-9.65,19.65){\vector(1,-1){9.3}}
\put(-4,15){$a$}
\put(0,10){\circle{1}}
\put(0,9.5){\vector(0,-1){9}}
\put(1,5){$b$}
\put(0,0){\circle{1}}
\put(0.35,29.65){\vector(1,-1){9.3}}
\put(6,25){$a$}
\put(10,20){\circle{1}}
\put(10,19.5){\vector(0,-1){9}}
\put(11,15){$a$}
\put(10,10){\circle{1}}
\put(10,9.5){\vector(0,-1){9}}
\put(11,5){$b$}
\put(10,0){\circle{1}}
\put(0,-8){\makebox(0,0){$a(a0+ab0)+aab0$}}
\put(0,-13){\makebox(0,0){$\models\diam{a}\neg(\diam{a}\neg\diam{b}\top)$}}
\end{picture}
~~~~~~~~~~~~~~~~~~~~
\begin{picture}(20,40)(-10,-13)
\put(0,33.5){\vector(0,-1){3}}
\put(0,30){\circle{1}}
\put(-.35,29.65){\vector(-1,-1){9.3}}
\put(-8,25){$a$}
\put(-10,20){\circle{1}}
\put(-10.35,19.65){\vector(-1,-1){9.3}}
\put(-18,15){$a$}
\put(-20,10){\circle{1}}
\put(-9.65,19.65){\vector(1,-1){9.3}}
\put(-4,15){$a$}
\put(0,10){\circle{1}}
\put(0,9.5){\vector(0,-1){9}}
\put(1,5){$b$}
\put(0,0){\circle{1}}
\put(-10,-8){\makebox(0,0){$a(a0+ab0)$}}
\put(-10,-13){\makebox(0,0){$\not\models\diam{a}\neg(\diam{a}\neg\diam{b}\top)$}}
\end{picture}
\end{center}
\caption{Two 2-nested simulation equivalent processes that can be
  distinguished by the HML formula with nested negations
  $\diam{a}\neg(\diam{a}\neg\diam{b}\top)$}
\label{fig:2-nested}
\vspace{-2em}
\end{figure}
\end{example}


\section{Bisimulation as a Congruence}
\label{sec:bisimulation}

In \cite{GV92}, {\sc Groote \& Vaandrager} introduced the tyft/tyxt format, and proved that on any LTS specified by a well-founded TSS in tyft/tyxt format, bisimulation equivalence is a congruence, i.e.\ is preserved by all functions in the signature. {\sc Fokkink \& van Glabbeek} showed in \cite{FvG96} that the well-foundedness condition can be dropped, by constructing for each TSS in tyft/tyxt format an equivalent TSS that consists of pure xyft rules only. In this section we show that the congruence result for TSSs in tyft/tyxt format is a corollary of Theorem~\ref{thm:decomposition}.

\begin{corollary}
Let $P=(\Sigma,R)$ be a TSS in tyft/tyxt format, $t \in \mathds{T}(\Sigma)$ and $\sigma, \sigma'$ closed substitutions. If $\sigma(x) \bis \sigma'(x)$ for $x \in \var(t)$, then $\sigma(t) \bis \sigma'(t)$.
\end{corollary}

\begin{proof}
In light of Proposition~\ref{prop:O_characterizes_bis}, it suffices to show that $\sigma(t)$ and $\sigma(t')$ satisfy the same formulas from $\mathds{O}$. Let $\sigma(t)\models\phi\in\mathds{O}$. By Theorem~\ref{thm:decomposition} there is a $\psi \in t^{-1}(\phi)$ such that $\sigma(x) \models \psi(x)$ for $x\in\var(t)$. Since $\psi(x)\in\mathds{O}$ and $\sigma(x)\bis\sigma'(x)$ for $x\in\var(t)$, it follows by Proposition~\ref{prop:O_characterizes_bis} that $\sigma'(x)\models\psi(x)$ for $x \in \var(t)$. So by Theorem~\ref{thm:decomposition}, $\sigma'(t)\models\phi$. By symmetry, $\sigma'(t)\models\phi\in\mathds{O}$ implies $\sigma(t)\models\phi$.
\end{proof}
Likewise, it follows from Theorem~\ref{thm:decomposition} that on any LTS specified by a complete TSS in ready simulation format, bisimulation equivalence is a congruence. This is a special case of the congruence result from \cite{BG96,FvG96} for complete TSSs in ntyft/ntyxt format.\pagebreak[2]

{\sc Bloom, Fokkink \& van Glabbeek} \cite{BFvG04} showed how the decomposition method of modal formulas can be used to obtain general congruence formats for a wide range of behavioural semantics. The idea is to take as a starting point the modal characterization of the semantics under scrutiny, this being a set $\mathcal{O}$ of HML formulas such that two processes are semantically equivalent if and only if they make true the same formulas in $\mathcal{O}$. The congruence format for this semantics should guarantee that the decomposition of a formula in $\mathcal{O}$ always produces formulas in $\mathcal{O}$. With the decomposition method in the current paper, we could use this same approach to produce congruence formats that include lookahead. We leave this as future work.

%\bibliography{sos}
\begin{thebibliography}{10}

\bibitem{And95}
{\sc H.~R. Andersen} (1995):
\newblock {\em Partial model checking.}
\newblock In {\sl Proceedings Tenth Annual {IEEE} Symposium on Logic in Computer Science}, IEEE Computer Society Press, San Diego, California, pp. 398--407.

\bibitem{ASW94}
{\sc H.R. Andersen, C.~Stirling \& G.~Winskel} (1994):
\newblock {\em A compositional proof system for the modal $\mu$-calculus.}
\newblock In {\sl Proceedings Ninth Annual {IEEE} Symposium on Logic in Computer Science}, IEEE Computer Society Press, pp. 144--153.

\bibitem{AW92}
{\sc H.R. Andersen \& G.~Winskel} (1992):
\newblock {\em Compositional checking of satisfaction.}
\newblock {\sl Formal Methods in System Design} 1(4), pp. 323--354.

\bibitem{BKP84}
{\sc H.~Barringer, R.~Kuiper \& A.~Pnueli} (1984):
\newblock {\em Now you may compose temporal logic specifications.}
\newblock In {\sl {ACM} Symposium on Theory of Computing (STOC~'84)}, ACM Press, pp. 51--63.

\bibitem{BFvG04}
{\sc B.~Bloom, W.J. Fokkink \& R.J.~van Glabbeek} (2004):
\newblock {\em Precongruence formats for decorated trace semantics.}
\newblock {\sl Transactions on Computational Logic} 5(1), pp. 26--78.

\bibitem{BIM95}
{\sc B.~Bloom, S.~Istrail \& A.R. Meyer} (1995):
\newblock {\em Bisimulation can't be traced.}
\newblock {\sl Journal of the ACM} 42(1), pp. 232--268.

\bibitem{BG96}
{\sc R.~Bol \& J.F. Groote} (1996):
\newblock {\em The meaning of negative premises in transition system specifications.}
\newblock {\sl Journal of the ACM} 43(5), pp. 863--914.

\bibitem{BHR84}
{\sc S.D. Brookes, C.A.R. Hoare \& A.W. Roscoe} (1984):
\newblock {\em A theory of communicating sequential processes.}
\newblock {\sl Journal of the ACM} 31(3), pp. 560--599.

\bibitem{FvG96}
{\sc W.J. Fokkink \& R.J.~van Glabbeek} (1996):
\newblock {\em Ntyft/ntyxt rules reduce to ntree rules.}
\newblock {\sl Information and Computation} 126(1), pp. 1--10.

\bibitem{FvGdW03}
{\sc W.J. Fokkink, R.J.~van Glabbeek \& P.~de Wind} (2003):
\newblock {\em Compositionality of {H}ennessy-{M}ilner logic through structural operational semantics.}
\newblock In A.~Lingas \& B.J. Nilsson, editors: {\sl $14^{th}$ International Symposium on Fundamentals of Computation Theory (FCT~'03)}, LNCS 2751, Springer, pp. 412--422.

\bibitem{vGl01}
{\sc R.J.~van Glabbeek} (2001):
\newblock {\em The linear time -- branching time spectrum {I}: {T}he semantics of concrete, sequential processes.}
\newblock In J.A. Bergstra, A.~Ponse \& S.A. Smolka, editors: {\sl Handbook of Process Algebra}, chapter~1, Elsevier, pp. 3--99.

\bibitem{vGl04}
{\sc R.J.~van Glabbeek} (2004):
\newblock {\em The meaning of negative premises in transition system specifications {II}.}
\newblock {\sl Journal of Logic and Algebraic Programming} 60/61, pp. 229--258.

\bibitem{Gro93}
{\sc J.F. Groote} (1993):
\newblock {\em Transition system specifications with negative premises.}
\newblock {\sl Theoretical Computer Science} 118(2), pp. 263--299.

\bibitem{GV92}
{\sc J.F. Groote \& F.~Vaandrager} (1992):
\newblock {\em Structured operational semantics and bisimulation as a congruence.}
\newblock {\sl Information and Computation} 100(2), pp. 202--260.

\bibitem{HKP82}
{\sc D.~Harel, D.~Kozen \& R.~Parikh} (1982):
\newblock {\em Process logic: Expressiveness, decidability, completeness.}
\newblock {\sl Journal of Computer and System Sciences} 25(2), pp. 144--170.

\bibitem{HM85}
{\sc M.C.B. Hennessy \& R.~Milner} (1985):
\newblock {\em Algebraic laws for non-determinism and concurrency.}
\newblock {\sl Journal of the ACM} 32(1), pp. 137--161.

\bibitem{HS85}
{\sc M.C.B. Hennessy \& C.~Stirling} (1985):
\newblock {\em The power of the future perfect in program logics.}
\newblock {\sl Information and Control} 67, pp. 23--52.

\bibitem{Koz83}
{\sc D.~Kozen} (1983):
\newblock {\em Results on the propositional $\mu$-calculus.}
\newblock {\sl Theoretical Computer Science} 27(3), pp. 333--354.

\bibitem{LaLa95}
{\sc F.~Laroussinie \& K.~G. Larsen} (1995):
\newblock {\em Compositional model checking of real time systems.}
\newblock In I.~Lee \& S.~A. Smolka, editors: {\sl CONCUR~'95: Concurrency Theory, 6th Conference}, LNCS 962, Springer-Verlag, pp. 27--41.

\bibitem{Lar86}
{\sc K.G. Larsen} (1986):
\newblock {\em Context-Dependent Bisimulation between Processes}.
\newblock PhD thesis, University of Edinburgh, Edinburgh.

\bibitem{LX91}
{\sc K.G. Larsen \& L.~Xinxin} (1991):
\newblock {\em Compositionality through an operational semantics of contexts.}
\newblock {\sl Journal of Logic and Computation} 1(6), pp. 761--795.

\bibitem{Mil80}
{\sc R.~Milner} (1980):
\newblock {\em A Calculus of Communicating Systems}.
\newblock Springer.
\newblock LNCS 92.

\bibitem{Mil81}
{\sc R.~Milner} (1981):
\newblock {\em A modal characterization of observable machine-behaviour.}
\newblock In E.~Astesiano \& C.~B{\"o}hm, editors: {\sl CAAP~'81: Trees in Algebra and Programming, $6^{th}$ Colloquium}, LNCS 112, Springer, pp. 25--34.

\bibitem{Mil83}
{\sc R.~Milner} (1983):
\newblock {\em Calculi for synchrony and asynchrony.}
\newblock {\sl Theoretical Computer Science} 25(3), pp. 267--310.

\bibitem{Plo04}
{\sc G.~D. Plotkin} (2004):
\newblock {\em A structural approach to operational semantics.}
\newblock {\sl Journal of Logic and Algebraic Programming} 60/61, pp. 17--139.
\newblock Originally appeared in 1981.

\bibitem{Pnu81}
{\sc A.~Pnueli} (1981):
\newblock {\em The temporal logic of concurrent programs.}
\newblock {\sl Theoretical Computer Science} 13, pp. 45--60.

\bibitem{Sim85}
{\sc R.~de Simone} (1985):
\newblock {\em Higher-level synchronising devices in \textsc{Meije}--{SCCS}.}
\newblock {\sl Theoretical Computer Science} 37(3), pp. 245--267.

\bibitem{Sim04}
{\sc A.~Simpson} (2004):
\newblock {\em Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS.}
\newblock {\sl Journal of Logic and Algebraic Programming} 60/61, pp. 287--322.

\bibitem{Sti85-obs-eq}
{\sc C.~Stirling} (1985):
\newblock {\em A proof-theoretic characterization of observational equivalence.}
\newblock {\sl Theoretical Computer Science} 39(1), pp. 27--45.

\bibitem{Sti85-SCCS}
{\sc C.~Stirling} (1985):
\newblock {\em A complete modal proof system for a subset of {SCCS}.}
\newblock In H.~Ehrig, C.~Floyd, M.~Nivat \& J.W. Thatcher, editors: {\sl Mathematical Foundations of Software Development: Proceedings of the Joint Conference on Theory and Practice of Software Development (TAPSOFT), Volume~1: Colloquium on Trees in Algebra and Programming (CAAP~'85)}, LNCS 185, Springer, pp. 253--266.

\bibitem{Sti85-CCS}
{\sc C.~Stirling} (1985):
\newblock {\em A complete compositional modal proof system for a subset of {CCS}.}
\newblock In W.~Brauer, editor: {\sl Automata, Languages and Programming, 12th Colloquium (ICALP~'85)}, LNCS 194, Springer, pp. 475--486.

\bibitem{Sti87}
{\sc C.~Stirling} (1987):
\newblock {\em Modal logics for communicating systems.}
\newblock {\sl Theoretical Computer Science} 49(2-3), pp. 311--347.

\bibitem{Win86}
{\sc G.~Winskel} (1986):
\newblock {\em A complete proof system for {SCCS} with modal assertions.}
\newblock {\sl Fundamenta Informaticae} IX, pp. 401--420.

\bibitem{Win90}
{\sc G.~Winskel} (1990):
\newblock {\em On the compositional checking of validity (extended abstract).}
\newblock In J.C.M. Baeten \& J.W. Klop, editors: {\sl CONCUR~'90: Theories of Concurrency: Unification and Extension}, LNCS 458, Springer, pp. 481--501.

\end{thebibliography}
\end{document}
