\documentclass[fleqn,runningheads]{llncs}
\usepackage{dsfont}
\bibliographystyle{plain}
\newcommand{\T}{\mathds{T}}
\newcommand{\var}{{\it var}}
\newcommand{\diam}[1]{\langle#1\rangle}
\newcommand{\trans}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\ntrans}[1]{\hspace{4pt}\not\hspace{-4pt}\stackrel{#1\ }{\longrightarrow}}
\renewcommand{\phi}{\varphi}
\title{Compositionality of Hennessy-Milner Logic through Structural Operational Semantics\thanks{To appear in: Proc.\ 14th International Symposium on {\sl Fundamentals of Computation Theory}, Malm\"o, Sweden, LNCS, Springer, August 2003. \hfill \copyright\ Springer-Verlag}}
\titlerunning{Compositionality of Hennessy-Milner Logic}
\author{Wan Fokkink \inst{1,2} \and Rob van Glabbeek \inst{1} \and Paulien de Wind \inst{2}}
\institute{
CWI, Department of Software Engineering
\\PO Box 94079, 1090 GB Amsterdam, The Netherlands
\and
Vrije Universiteit Amsterdam, Department of Theoretical Computer Science\\
De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands\\[3ex]
\email{wan@cwi.nl}, \email{rvg@cs.stanford.edu}, \email{pdwind@cs.vu.nl}\\
\texttt{http://www.cwi.nl/\homedir wan/} \\
\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 formulae. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulae, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is that an earlier decomposition method from {\sc Larsen} \cite{Lar86} for the De Simone format is extended to the more general ntyft/ntyxt format without lookahead.
\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 the components of the composition. Most research papers in this area focus on a particular process algebra.
{\sc Barringer, Kuiper \& Pnueli} \cite{BKP84} present (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 define a language including assignment, conditional and while statements. Interaction between parallel components is done via shared variables.
In {\sc Stirling} \cite{Sti85-obs-eq} modal proof systems are developed for subsets of CCS \cite{Mil80} (with and without silent actions) including only sequential and alternative composition, to decide the validity of formulae from Hennessy-Milner Logic (HML) \cite{HM85}.
In {\sc Stirling} \cite{Sti85-CCS,Sti85-SCCS} the results from \cite{Sti85-obs-eq} are extended\pagebreak[1], 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 {\sc Stirling} \cite{Sti87} the proposals in \cite{Sti85-CCS,Sti85-SCCS} are generalised to be able to cope with the restriction operator.
In {\sc Winskel} \cite{Win86} a method is given to decompose formulae 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} \cite{Lar86} developed 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{Plo81}, 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 formulae 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. {\sc Larsen and Xinxin} \cite{LX91} 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}).
In {\sc Bloom, Fokkink \& van Glabbeek} \cite{BFvG03} a method is given for decomposing formulae from a fragment of HML with infinite conjunctions, with respect to terms from any process algebra that has a structural operational semantics in ntyft/ntyxt format \cite{Gro93} without lookahead. 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 this paper the decomposition method from \cite{BFvG03} is extended to full HML with infinite conjunction, again with respect to terms from any process algebra that has a structural operational semantics in ntyft/ntyxt format without lookahead.
\section{Preliminaries}
In this section we give the basic notions of structural operational semantics and Hennessy-Milner Logic (HML) that are needed to define our decomposition method.
\subsection{Structural Operational Semantics}
Structural operational semantics \cite{Plo81} 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 an infinite set of variables. A syntactic object is called \emph{closed} if it does not contain any variables from $V$.
\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 $\T(\Sigma)$ of \emph{terms} over a signature $\Sigma$ is defined recursively by:
\begin{itemize}
\item $V\subseteq\T(\Sigma)$,
\item if $f\in\Sigma$ and $t_1,\ldots,t_{ar(f)}\in\T(\Sigma)$, then $f(t_1,\ldots,t_{ar(f)})\in\T(\Sigma)$.
\end{itemize}
A term $c()$ is abbreviated as $c$. For $t\in\T(\Sigma)$, $var(t)$ denotes the set of variables that occur in $t$. $T(\Sigma)$ is the set of closed terms over $\Sigma$, i.e. the terms $t\in\T(\Sigma)$ with $var(t)=\emptyset$.
A $\Sigma$-\emph{substitution} $\sigma$ is a partial function from $V$ to $\T(\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 is {\em closed} if it is a total function from $V$ to $T(\Sigma)$.
\end{definition}
In the remainder, let $\Sigma$ denote a signature and $A$ a set of actions, satisfying $|\Sigma| \leq |V|$ and $|A| \leq |V|$.
\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 \T(\Sigma)$ and $a \in A$. For $t,t' \in \T(\Sigma)$ 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}). 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}
\begin{definition}[proof]
Let $P=(\Sigma,R)$ be a TSS. A {\em proof} of a transition rule $\frac{H}{\alpha}$ from $P$ is a well-founded, upwardly branching tree of which the 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$ contains the labels of the hypotheses, and
\item if $\beta$ is the label of a node $q$ which is not an 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}
If a proof of $\frac{K}{\alpha}$ from $P$ exists, then $\frac{K}{\alpha}$ is {\em provable} from $P$, notation $P\vdash\frac{K}{\alpha}$.
\end{definition}
\begin{definition}[transition relation]\label{def:transition relation}
A \emph{transition relation} over $\Sigma$ is a relation $\rightarrow~\subseteq T(\Sigma)\times A\times T(\Sigma)$. We write $p\trans{a}q$ for $(p,a,q)\in~\rightarrow$ and $p\ntrans{a}$ for $\neg\exists q\in T(\Sigma):p\trans{a}q$.
\end{definition}
Thus a transition relation over $\Sigma$ can be regarded as a set of closed positive $\Sigma$-literals (\emph{transitions}).
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 in {\sc Groote} \cite{Gro93}, {\sc Bol \& Groote} \cite{BG96} and {\sc van Glabbeek} \cite{vGl96}. From the latter 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} of a closed literal ${\alpha}$ from $P$ is a well-founded, upwardly branching tree of which the 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 negative closed 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 of $\alpha$ from $P$ exists.
\end{definition}
In \cite{vGl96} it was noted that $\vdash_{\it ws}$ is {\em consistent}, in
the sense that no standard 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.
\subsection{Hennessy-Milner Logic}
A variety of modal logics have been developed to express properties of transition relations. Modal logic aims to formulate properties of process terms, and to identify terms that satisfy the same properties.
{\sc Hennessy \& Milner} \cite{HM85} have defined a modal language, often called Hen\-nessy-Mil\-ner Logic (HML), which characterises the bisimulation equivalence relation on process terms, assuming that each term has only finitely many outgoing transitions. This assumption can be discarded if infinite conjunctions are allowed \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 formulae} is recursively defined by
\[\phi ::= \bigwedge_{i\in I}\phi_i ~|~ \diam{a}\phi ~|~ \neg\phi\]
with $a\in A$ and $I$ some index set.
\end{definition}
\begin{definition}[satisfaction relation]\label{def:sat}
Let $P=(\Sigma,R)$ be a TSS. The \emph{satisfaction relation} $\models_P\,\subseteq T(\Sigma)\times \mathds{O}$ is defined as follows, with $p\in T(\Sigma)$:
\[\begin{array}{@{}ll}
\displaystyle{p\models_P\bigwedge_{i\in I}\phi_i} & \mbox{iff }p\models_P\phi_i\mbox{ for all }i\in I\\
p\models_P\diam{a}\phi
& \mbox{iff there is a }q\in T(\Sigma)\mbox{ such that } P\vdash_{\it ws}p\trans{a}q\mbox{ and }q\models_P\phi\\
p\models_P\neg\phi & \mbox{iff }p\not\models_P\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 formulae 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_P \phi \Leftrightarrow p \models_P \psi$.
\section{Decomposing HML Formulae}
In this section we will see how one can decompose HML formulae with respect to process terms. The TSS defining the transition relation on these terms should be in \emph{ready simulation format} \cite{BFvG03}, allowing only ntyft/ntyxt rules \cite{Gro93} without lookahead.
\begin{definition}[ntyxt,ntyft,nxytt]
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.
\end{definition}
\begin{definition}[lookahead]\label{def:lookahead}
A transition rule has \emph{no lookahead} if the variables occurring in the right-hand sides of its positive premises do not occur in the left-hand sides of its premises.
\end{definition}
\begin{definition}[ready simulation format]\label{def:formats}
A TSS is in \emph{ready simulation format} if its transition rules are ntyft or ntyxt rules that have no lookahead.
\end{definition}
\begin{definition}[free]\label{def:free variable}
A variable occurring in a transition rule is \emph{free} if it does not occur in the source nor in the right-hand sides of the positive premises of this rule.
\end{definition}
\begin{definition}[decent]\label{def:decent}
A transition rule is \emph{decent} if it has no lookahead and does not contain free variables.
\end{definition}
In {\sc Bloom, Fokkink \& van Glabbeek} \cite{BFvG03} for any TSS $P$ in ready simulation format the collection of \emph{$P$-ruloids} is defined. These are decent nxytt rules for which the following holds:
\begin{theorem}\label{the:ruloid} \cite{BFvG03}
Let $P$ be a TSS in ready simulation format. Then $P\vdash_{\it ws}\sigma(t)\trans a p$ for $t$ a term, $p$ a closed term and $\sigma$ a closed substitution, iff 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}
Given a TSS $P=(\Sigma,R)$ in ready simulation format, the following definition assigns to each term $t\in\T(\Sigma)$ and each observation $\phi\in\mathds{O}$ a collection $t^{-1}_P(\phi)$ of {\em 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 decomposition mapping $\psi \in t^{-1}_P(\phi)$ with $\sigma(x)$ satisfying $\psi(x)$ for all $x \in \var(t)$. This is formalised in Theorem \ref{the:crux} and proven thereafter.
\begin{definition}\label{def:inverse}
Let $P=(\Sigma,R)$ be a TSS in ready simulation format. Then $\cdot_P^{-1}:\T(\Sigma)\rightarrow(\mathds{O}\rightarrow\mathcal{P}(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@{~~~~\textrm{if }}l}
\displaystyle{\chi(x) \land \bigwedge_{(x\trans{b}y)\in H}\!\!\!\!\!\diam{b}\chi(y)
\land \bigwedge_{(x\ntrans{c})\in H}\!\!\!\!\!\neg\diam{c}\top} & x\in\var(t)\\
\top & x\not\in\var(t)
\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}
When clear from the context, the subscript $P$ will be omitted.
\end{definition}
It is not hard to see that if $\psi\in t_P^{-1}(\phi)$ then $\psi(x)=\top$
for all $x\not\in\var(t)$.
\begin{theorem}\label{the:crux}
Let $P=(\Sigma,R)$ be a complete TSS in ready simulation format. Let $\phi\in\mathds{O}$. For any term $t\in\T(\Sigma)$ and closed substitution $\sigma:V\rightarrow T(\Sigma)$ one has
\[\sigma(t)\models\phi~~\Leftrightarrow~~\exists\psi\in t^{-1}(\phi)\forall x\in\var(t)\big(\sigma(x)\models\psi(x)\big)\]
\end{theorem}
\begin{proof}
With induction on the structure of $\phi$.
\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 T(\Sigma)$ with $P\vdash_{\it ws}\sigma(t)\trans{a}p$ and $p\models\phi'$. Thus, by Theorem \ref{the:ruloid} 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)$. Furthermore $\sigma'(z)\models\chi(z)=\top$ for all $z\not\in\var(u)$. Now define $\psi$ as indicated in Definition \ref{def:inverse}. By definition, $\psi\in t^{-1} (\diam{a}\phi')$. Let $x \in \var(t)$.
For $(x\trans{b}y)\in H$ one has $P\vdash_{\it ws}\sigma'(x)\trans{b}\sigma'(y)$ and $\sigma'(y)\models\chi(y)$, so $\sigma'(x)\models\diam{b}\chi(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 T(\Sigma)$, and thus $\sigma'(x)\models\neg\diam{c}\top$. It follows that $\sigma(x)=\sigma'(x)\models\psi(x)$.
\fbox{$\Leftarrow$} Now 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)$. This means that there is a $P$-ruloid
\[\frac{\{x\trans{a_i}y_i\mid i\in I_x,~x\in\var(t)\}\cup\{x\ntrans{b_j}\mid j\in J_x,~x\in\var(t)\}}{t\trans{a} u}\]
and a decomposition mapping $\chi\in u^{-1}(\phi')$ such that, for all $x\in\var(t)$, $$\sigma(x)\models\chi(x)\wedge\bigwedge_{i\in I_x}\diam{a_i}\chi(y_i)\wedge\bigwedge_{j\in J_x}\neg\diam{b_j}\top$$ By Definition \ref{def:sat} it follows that, for $x\in\var(t)$ and $i\in I_x$, $P\vdash_{\it ws}\sigma(x)\trans{a_i}p_i$ for some $p_i\in T(\Sigma)$ with $p_i\models\chi(y_i)$. Moreover, for $x \in \var(t)$ and $j \in J_x$, $P \not\vdash_{\it ws} \sigma(x) \trans{b_j} q$ for all $q\in T(\Sigma)$, so by the completeness of $P$, $P \vdash_{\it ws} \sigma(x) \ntrans{b_j}$. Let $\sigma'$ be a closed substitution with $\sigma'(x) = \sigma(x)$ for $x \in \var(t)$ and $\sigma'(y_i) = p_i$ for $i \!\in\! I_x$ and $x\in \var(t)$.
Here we use that the variables $x$ and $y_i$ are all different. Now $\sigma'(z) \models \chi(z)$ for $z\in \var(u)$, using that $u$ contains only variables that occur in $t$ or in the premises of the ruloid. Thus the induction hypothesis can be applied, and $\sigma'(u) \models \phi'$. Moreover, $P \vdash_{\it ws} \sigma'(x) \trans{a_i} \sigma'(y_i)$ for $x\in \var(t)$ and $i\in I_x$, and $P \vdash_{\it ws} \sigma'(x) \ntrans{b_j}$ for $x\in \var(t)$ and $j\in J_x$. So, by Theorem~\ref{the:ruloid}, $P \vdash_{\it ws} \sigma'(t) \trans{a} \sigma'(u)$, which implies $\sigma(t)=\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'$
\fbox{$\Rightarrow$} Suppose $\sigma(t)\models\neg\phi'$. Then by Definition \ref{def:sat} we have $\sigma(t)\not\models\phi'$. Using the induction hypothesis, there is no $\chi\in t^{-1}(\phi')$ such that $\sigma(x)\models\chi(x)$ for all $x\in\var(t)$. So for all $\chi\in t^{-1}(\phi')$ there is an $x\in\var(t)$ such that $\sigma(x)\models\neg\chi(x)$. Let us denote this $x$ as $h(\chi)$, so that we obtain a function $h:t^{-1}(\phi')\rightarrow\var(t)$ such that $\sigma(h(\chi))\models\neg\chi(h(\chi))$ for all $\chi\in t^{-1}(\phi')$. Define $\psi\in t^{-1}(\neg\phi')$ as indicated in Definition \ref{def:inverse}, using $h$. Let $x\in\var(t)$. If $x=h(\chi)$ for some $\chi\in t^{-1}(\phi')$ then $\sigma(x)\models\neg\chi(x)$. Hence, $\sigma(x)\models\bigwedge_{\chi\in h^{-1}(x)}\neg\chi(x)=\psi(x)$.
\fbox{$\Leftarrow$} Suppose that there is a $\psi\in t^{-1}(\neg\phi')$ such that $\sigma(x)\models\psi(x)$ for all $x\in\var(t)$. By Definition \ref{def:inverse} there is a function $h:t^{-1}(\phi')\rightarrow\var(t)$ such that $\psi(x)=\bigwedge_{\chi\in h^{-1}(x)}\neg\chi(x)$ for all $x\in\var(t)$. So for all $x\in\var(t)$ and for all $\chi\in h^{-1}(x)$ we have that $\sigma(x)\models\neg\chi(x)$. In other words, for all $\chi\in t^{-1}(\phi')$,we have $\sigma(h(\chi))\models\neg\chi(h(\chi))$. So $\neg\exists\chi\in t^{-1}(\phi')\forall x\in\var(t)\big(\sigma(x)\models\chi(x)\big)$. Then using the induction hypothesis, we have $\sigma(t)\not\models\phi'$, so $\sigma(t)\models\neg\phi'$.
\end{itemize}
\end{proof}
We give a few examples of the application of Definition \ref{def:inverse}.
\begin{example}\label{ex:bT}
Let $A=\{a,b\}$ and let $P=(\Sigma,R)$ with $\Sigma$ consisting 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)$. There are two $P$-ruloids with a conclusion of the form $f(x_1,x_2)\trans{b}\_$, namely $\frac{x_1\trans{a} y}{f(x_1,x_2)\trans{b} y}$ and $\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}, we have $f(x_1,x_2)^{-1}(\diam{b}\top)=\{\psi_1,\psi_2\}$ with $\psi_1$ and $\psi_2$ as defined below, using $\chi\in y^{-1}(\top)$ (so $\chi(x)=\top$ for all variables $x\in V$):
\[\begin{array}{@{}l}
\psi_1(x_1)=\chi(x_1)\land\diam{a}\chi(y)=\top\land\diam a\top=\diam{a}\top \\
\psi_1(x_2)=\chi(x_2)=\top\\
\psi_1(x)=\top\mbox{ for }x\not\in\var(f(x_1,x_2)) \\
\end{array}\]
\[\begin{array}{@{}l}
\psi_2(x_1)=\chi(x_1)\land\neg\diam{b}\top=\top\land\neg\diam b\top=\neg\diam{b}\top \\
\psi_2(x_2)=\chi(x_2)\land\diam{a}\chi(y)=\top\land\diam a\top=\diam{a}\top\\
\psi_2(x)=\top\mbox{ for }x\not\in\var(f(x_1,x_2))
\end{array}\]
By Theorem \ref{the:crux} a closed term $f(u_1,u_2)$ can execute a $b$ if and only if the closed term $u_1$ can execute an $a$, or the closed term $u_1$ can not execute a $b$ and the closed term $u_2$ can execute an $a$. Looking at the premises, this is what we would expect.
\end{example}
\begin{example}
Using the TSS and the mappings $\psi_1,\psi_2\in f(x_1,x_2)^{-1}(\diam{b}\top)$ from Example \ref{ex:bT}, we can 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)$.
\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{the:crux} a closed term $f(u_1,u_2)$ can \emph{not} execute a $b$ if and only if (1) the closed term $u_1$ can execute a $b$ but not an $a$, or (3) the closed term $u_1$ can not execute an $a$ and the closed term $u_2$ can not execute an $a$. Looking at the premises, this is again what we would expect. The other two possibilities (2) and (4) do not qualify, since no term can ever satisfy $\neg\top$.
\end{example}
A little less obvious example is the following:
\begin{example}
Let $A=\{a,b\}$ and let $P=(\Sigma,R)$ with $\Sigma$ consisting 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}{f(x)\trans{a}f(y)}
$$
This TSS is complete and in ready simulation format. We proceed to compute $f(f(x))^{-1}(\diam b \diam a\top)$. The only $P$-ruloid that has a conclusion $f(f(x))\trans{b}\_$ is $\frac{x\trans{b}y}{f(f(x))\trans{b}f(y)}$. So for each $\psi\in f(f(x))^{-1}(\diam b \diam a\top)$, $\psi(x)=\chi(x)\wedge\diam b\chi(y)$ with $\chi\in f(y)^{-1}(\diam a\top)$. The only $P$-ruloid that has a conclusion $f(y)\trans{a}\_$ is $\frac{y\trans{b}z}{f(y)\trans{a}f(z)}$. So $\chi(y)=\chi'(y)\wedge\diam b\chi'(z)$ with $\chi'\in f(z)^{-1}(\top)$. Since $\chi'(y)=\chi'(z)=\top$ we have $\chi(y)=\diam b\top$. Moreover $x\not\in\var(f(y))$ implies $\chi(x)=\top$. Hence $\psi(x)=\diam b\diam b\top$.
By Theorem \ref{the:crux} a closed term $f(f(u))$ can execute a $b$ followed by an $a$ if and only if the closed term $u$ can execute two consecutive $b$'s.
\end{example}
The following example shows that in Theorem \ref{the:crux} it is essential that the TSS is complete. That is, the theorem would fail if we would take 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 let $P=(\Sigma,R)$ with $\Sigma$ consisting 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}
$$
This TSS, which is in ready simulation format, is incomplete. For example, neither $P\vdash_{\it ws} c\trans{a}t$ for a closed term $t$ 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\not\models\diam a \top$ and $f(c)\not\models\diam b \top$.
The only $P$-ruloid is $\frac{x\ntrans{a}}{f(x)\trans{b}c}$. Hence Theorem \ref{the:crux} would yield $f(c)\models \diam b \top \Leftrightarrow c\models\neg\diam a \top \Leftrightarrow c\not\models\diam a \top$. Since this is false, Theorem \ref{the:crux} would fail with respect to $P$.
\end{example}
\begin{thebibliography}{10}
\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, Paris, France, 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, Baltimore, USA, pp. 51--63.
\bibitem{BFvG03}
{\sc B.~Bloom, W.~J. Fokkink \& R.~J. van Glabbeek} (2003):
\newblock {\em Precongruence formats for decorated trace semantics.}
\newblock {\sl ACM Transactions on Computational Logic}.
\newblock To appear.
\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{vGl96}
{\sc R.~J.~van Glabbeek} (1996):
\newblock {\em The meaning of negative premises in transition system specifications {II}.}
\newblock In F.~Meyer auf~der Heide \& B.~Monien, editors: {\sl Automata, Languages and Programming, 23rd Colloquium (ICALP~'96)}, {\sl Lecture Notes in Computer Science} 1099, Springer-Verlag, Paderborn, Germany, pp. 502--513.
\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{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{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(1--3), 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{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-Verlag.
\newblock Volume 92 of \emph{Lecture Notes in Computer Science}.
\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}, {\sl Lecture Notes in Computer Science} 112, Springer-Verlag, Genoa, 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{Plo81}
{\sc G.~D. Plotkin} (1981):
\newblock {\em A structural approach to operational semantics.}
\newblock Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark.
\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{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-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)}, {\sl Lecture Notes in Computer Science} 194, Springer-Verlag, pp. 475--486.
\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)}, {\sl Lecture Notes in Computer Science} 185, Springer-Verlag, pp. 253--266.
\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}, {\sl Lecture Notes in Computer Science} 458, Springer-Verlag, Amsterdam, The Netherlands, pp. 481--501.
\end{thebibliography}
\end{document}