Symbolic Representation via Constrained Configurations

In order to finitely represent the generators of an upward closed set of configurations, we use a rich assertional language based on the notion of constrained configurations, i.e. multisets of (non ground) atomic formulas annotated with constraints.

Let $\langle { {\mathscr P} , {\mathscr C} , {\mathscr I} , {\mathscr R} } \rangle$ be an $\mbox{MSR($\ {\mathscr C} $)}$ specification, with ${\mathscr C} =\langle { {\mathscr V} , {\mathscr L} , {\mathscr D} ,\mathscr{S},\sqsubseteq^c} \rangle$. A constrained configuration is a multiset of atomic formulas over ${\mathscr P}$ and ${\mathscr C}$, annotated with a constraint, having the form

$${p_1(x_{11},\ldots,x_{1k_1})\ \vert\ \ldots\ \vert\ p_n(x_{n1}\ldots,x_{nk_n})}\,:\,{\varphi}$$

where $p_1,\ldots,p_n\in {\mathscr P}$, $\varphi\in {\mathscr L}$ is a satisfiable constraint, and $x_{11},\ldots,x_{nk_n}$ are distinct variables in ${\mathscr V}$.

The set of ground instances of a constrained configuration can be defined as follows.

Let $\langle {\mathscr P} ,$ ${\mathscr C} ,$ ${\mathscr I} ,$ ${\mathscr R} \rangle$ be an $\mbox{MSR($\ {\mathscr C} $)}$ specification, and ${ {\mathcal M} }\,:\,{\varphi}$ a constrained configuration. The set of ground instances of ${ {\mathcal M} }\,:\,{\varphi}$ is defined as

$$\mathit {Inst}({{ {\mathcal M} }\,:\,{\varphi}})=\{\sigma( {\mathcal M} )\ \vert\ \sigma\in\mathscr{S}({\varphi})\}.$$

As an example, let $C$ be the constrained configuration $use(x)~\vert~user(y)~:~true$. Then, if LC-constraints are interpreted over non-negative integers $\mathit {Inst}({C})$ contains configurations like $use(1)~\vert~use(2)$, $use(4)~\vert~use(6)$, etc.

The previous definition can be extended to sets of constrained configurations (denoted ${\bf S},{\bf S}',\ldots$) in the natural way:

$$\mathit {Inst}({{\bf S}})=\bigcup.png_{C~\in~{\bf S}} \mathit {Inst}({C})$$

Following the intuition we explained in the previous section, instead of taking the set of instances as flat denotation of a set of constrained configurations ${\bf S}$, we choose the following rich denotation.

Let $\langle {\mathscr P} ,$ ${\mathscr C} ,$ ${\mathscr I} ,$ ${\mathscr R} \rangle$ be an $\mbox{MSR($\ {\mathscr C} $)}$ specification, and ${\bf S}$ a set of constrained configurations (with distinct variables from each other). The rich denotation of ${\bf S}$, denoted $[\![{{\bf S}}]\!]$, is given by the upward closure of the set of its ground instances, i.e.

$$[\![{{\bf S}}]\!]=\mathit {Up}({\mathit {Inst}({{\bf S}})})$$