The $\mbox{MSR($\ {\mathscr C} $)}$ language

In the following we will use the notion of multisets. We use $\oplus$ and $\ominus$ to denote multiset union and multiset difference, respectively.

Let ${\mathscr P}$ be a finite set of predicate symbols, and ${\mathscr V}$ a denumerable set of variables. An atomic formula over ${\mathscr P}$ and ${\mathscr V}$ has the form $p(x_1,\ldots,x_n)$ (with $n\geq 0$), where $p\in {\mathscr P}$, and $x_1,\ldots,x_n$ are distinct variables in ${\mathscr V}$.

Now, let ${\mathscr P}$ be a finite set of predicate symbols, and ${\mathscr V}$ a denumerable set of variables. A multiset of atomic formulas $A_1$, ..., $A_k$ (with $k\geq 1$) over ${\mathscr P}$ and ${\mathscr V}$, is indicated as $A_1\ \vert\ \ldots\ \vert\ A_k$, where $A_i$ and $A_j$ must have distinct variables for $i\not=j$, and $\vert$ is an associative and commutative constructor. The empty multiset is denoted by $\epsilon$.

In the rest of the paper will use ${\mathcal M}$, ${\mathcal N}$, $\ldots$ to denote multisets of atomic formulas.

Let ${\mathscr P}$ be a finite set of predicate symbols, and ${\mathscr C} =\langle { {\mathscr V} , {\mathscr L} , {\mathscr D} ,\mathscr{S},\sqsubseteq^c} \rangle$ a constraint system. An $\mbox{MSR($\ {\mathscr C} $)}$ rule over ${\mathscr P}$ and ${\mathscr C}$ has the form ${ {\mathcal M} }\,\longrightarrow\,{ {\mathcal M} '}\,:\,{\varphi}$, where ${\mathcal M}$ and ${\mathcal M} '$ are two multisets of atomic formulas over ${\mathscr P}$ and ${\mathscr V}$, with distinct variables, and $\varphi\in {\mathscr L}$.

Note that ${ {\mathcal M} }\,\longrightarrow\,{\epsilon }\,:\,{\varphi}$ and ${\epsilon }\,\longrightarrow\,{ {\mathcal M} }\,:\,{\varphi}$ are possible $\mbox{MSR($\ {\mathscr C} $)}$ rules.

In order to make the intuitive semantics of the previous specification precise, we introduce the ingredients for the operational reading of MSR rules. We first define the notion of ground formulas. Let ${\mathscr P}$ be a finite set of predicate symbols, and ${\mathscr C} =\langle { {\mathscr V} , {\mathscr L} , {\mathscr D} ,\mathscr{S},\sqsubseteq^c} \rangle$ a constraint system. A ground atomic formulas over ${\mathscr P}$ and ${\mathscr C}$ has the form $p(d_1,\ldots,d_n)$ (with $n\geq 0$), where $p\in {\mathscr P}$ and $d_1,\ldots,d_n\in {\mathscr D}$.

In the following, we will denote by $\sigma( {\mathcal M} )$ the application of a solution ${\sigma}:{ {\mathscr V} }\rightarrow{ {\mathscr D} }$ to a multiset of atomic formulas ${\mathcal M}$. Formally, $\sigma(A_1~\vert~\ldots~\vert~A_k)=\sigma(A_1)~\vert~\ldots~\vert~\sigma(A_k)$, and $\sigma(p(x_1,\ldots,x_m))=p(d_1,\ldots,d_m)$ if $\sigma(x_i)=d_i$ for $x_i\in {\mathscr V}$ and $v_i\in {\mathscr D}$, $i:1,\ldots,m$.

Given an $\mbox{MSR($\ {\mathscr C} $)}$ rule $R={ {\mathcal M} }\,\longrightarrow\,{ {\mathcal M} '}\,:\,{\varphi}$, over ${\mathscr P}$ and ${\mathscr C}$, the set of ground instances of $R$, denoted $\mathit {Inst}({R})$, is the set of ground multiset rewrite rules defined as follows:

$$\mathit {Inst}({R})=\{{\sigma( {\mathcal M} )}\,\longright... ...a( {\mathcal M} ')}\ \vert\ \sigma\in\mathscr{S}({\varphi})\}$$

A central notion for our semantics is that of current configuration given below.

Let ${\mathscr P}$ be a finite set of predicate symbols, and ${\mathscr C}$ a constraint system. An $\mbox{MSR($\ {\mathscr C} $)}$ configuration is a multiset of ground atomic formulas over ${\mathscr P}$ and ${\mathscr C}$.

Configurations can be ordered with respect multiset inclusion as follows. Given two multisets of atomic formulas ${\mathcal M} \preccurlyeq {\mathcal N}$ if and only if $Occ_{A}( {\mathcal M} )\leq Occ_{A}( {\mathcal N} )$ for every atomic formula $A$, where $Occ_{A}( {\mathcal M} )$ denotes the number of occurrences of $A$ in ${\mathcal M}$.

An $\mbox{MSR($\ {\mathscr C} $)}$ specification is defined as follows.

The operational semantics of an $\mbox{MSR($\ {\mathscr C} $)}$ specification $\langle { {\mathscr P} , {\mathscr C} , {\mathscr I} , {\mathscr R} } \rangle$ can be defined as follows. Let ${\mathcal M}$ be a configuration. A rule ${\mathcal H} ~{\longrightarrow}~ {\mathcal B} ~:~\varphi$ from ${\mathscr R}$ is enabled at ${\mathcal M}$ via the solution $\sigma\in \mathscr{S}(\varphi)$ of the constraint $\varphi$ if and only if $\sigma( {\mathcal H} )\preccurlyeq {\mathcal M}$.

Now, sup.pngpose $R~\equiv~ {\mathcal H} ~{\longrightarrow}~ {\mathcal B} ~:\varphi$ is enabled at ${\mathcal M}$ via $\sigma\in \mathscr{S}(\varphi)$. Firing this rule at ${\mathcal M}$ yields the new configuration ${\mathcal M} '$, written ${\mathcal M} \Rightarrow_R {\mathcal M} '$, if and only if ${\mathcal M} ~=~\sigma( {\mathcal H} ) \oplus {\mathcal Q}$, and ${\mathcal M} '~=~\sigma( {\mathcal B} ) \oplus {\mathcal Q}$.

A run is a sequence of configurations ${\mathcal M} _0 {\mathcal M} _1 {\mathcal M} _2\ldots {\mathcal M} _i\ldots$ with ${\mathcal M} _0\in {\mathscr I}$ and for which there exist $R_0R_1\ldots \in {\mathscr R}$ such that ${\mathcal M} _{i}\Rightarrow_{R_{i}} {\mathcal M} _{i+1}$ for $i\geq 0$.

Let $S$ a set of configurations. The successor operator $Post$ is defined as

$$Post(S)=\{ {\mathcal M} '~\vert~ {\mathcal M} \Rightarrow_R {\mathcal M} ',~ {\mathcal M} \in S,~R\in {\mathscr R} \},$$

whereas, the predecessor operator $Pre$ is defined as

$$Pre(S)=\{ {\mathcal M} ~\vert~ {\mathcal M} \Rightarrow_R {\mathcal M} ',~ {\mathcal M} '\in S,~R\in {\mathscr R} \}.$$

The reflexive and transitive closures of the predecessor and successor operators are denoted $Pre^*$ and $Post^*$, respectively.

The reachability set is defined as $Post^*( {\mathscr I} )$, ${\mathscr I}$ being the initial states of the $\mbox{MSR($\ {\mathscr C} $)}$ specification under consideration.