1: \documentclass[12pt]{article}
2:
3: \usepackage{amsmath}
4: \usepackage{amssymb}
5: \usepackage{a4wide}
6: \usepackage{amsmath,amsthm,amssymb,xspace}
7: \newtheorem{Theorem}{Theorem}[section]
8: \newtheorem{Lemma}{Lemma}[section]
9: \newtheorem{Remark}{Remark}[section]
10: \newtheorem{Proposition}{Proposition}[section]
11: \newtheorem{Definition}{Definition}[section]
12:
13: % MACROS FOR VARIOUS DERIVATION SYMBOLS
14: \newcommand{\oneder}[2]{\ensuremath{{\mathop{{%
15: \Rightarrow}}\limits^{{#1}}}_{\!\!_{#2}}\!}}
16: \newcommand{\multider}[1]{\ensuremath{{\mathop{{ %
17: \Rightarrow}}\limits^{{#1}}}_{\!_\Re} %
18: \raisebox{2pt}{\!\!\!\scriptsize *}}}
19: \newcommand{\multidernorm}[2]{\ensuremath{{\mathop{{%
20: \Rightarrow}}\limits^{{#1}}}%
21: \raisebox{2pt}{\!\scriptsize *}}\!_{\!_{#2}}\,}
22: \newcommand{\prsoneder}[1]{\ensuremath{\oneder{#1}{\Re}}}
23: \newcommand{\onederparK}[1]{\ensuremath{\oneder{#1}{\Re^{K}_{PAR}}}}
24: \newcommand{\onederparKomega}[1]{\ensuremath{\oneder{#1}{\Re^{K,K^{\omega}}_{PAR}}}}
25: \newcommand{\onederseqK}[1]{\ensuremath{\oneder{#1}{\Re^{K}_{SEQ}}}}
26:
27:
28: \newcommand{\multiderparK}[1]{\ensuremath{\multidernorm{#1}{\Re^{K}_{PAR}}}}
29: \newcommand{\multiderparKomega}[1]{\ensuremath{\multidernorm{#1}{\Re^{K,K^{\omega}}_{PAR}}}}
30: \newcommand{\multiderseqK}[1]{\ensuremath{\multidernorm{#1}{\Re^{K}_{SEQ}}}}
31: \newcommand{\Rule}[1]{\ensuremath{{\mathop{{%
32: \rightarrow}}\limits^{{#1}}}}}
33:
34: \def\prsder#1#2#3{{#1\,\multidernorm{#2}{\Re}#3}}
35: \def\prsderpar#1#2#3{{#1\,\multidernorm{#2}{\Re_{PAR}^{K}}#3}}
36:
37:
38: % MACROS FOR PRS RULES
39: \def\prsrule#1#2#3{{#1\mathop{{\rightarrow}}\limits^{{#2}}#3}}
40: %\def\prslongrule#1#2#3{{#1\mathop{{\longrightarrow}}\limits^{{#2}}#3}}
41: \def\prslongrule#1#2#3{{#1\mathop{{\rightarrow}}\limits^{{#2}}#3}}
42:
43:
44: % MACROS FOR PRS TERM DERIVATIONS
45: \def\prsdernorm#1#2#3#4{{\,#1\,\multidernorm{#2}{#3}#4}}
46:
47:
48: % MACROS FOR MAXIMAL
49: \newcommand{\maximal}[1]{$\Upsilon^{f}_{M}({#1})$}
50: \newcommand{\maximalG}[2]{$\Upsilon^{f}_{#1}({#2})$}
51: \newcommand{\maximalGInf}[2]{$\Upsilon^{\infty}_{#1}({#2})$}
52: \newcommand{\maximalseq}[1]{$\Upsilon^{f}_{M_{SEQ,K}}({#1})$}
53: \newcommand{\maximalseqInf}[1]{$\Upsilon^{\infty}_{M_{SEQ}^{K}}({#1})$}
54: \newcommand{\maximalpar}[1]{$\Upsilon^{f}_{M_{PAR,K}}({#1})$}
55: \newcommand{\maximalparK}[1]{$\Upsilon^{f}_{M^{K}_{PAR}}({#1})$}
56: \newcommand{\maximalparKomega}[1]{$\Upsilon^{f}_{M^{K,K^{\omega}}_{PAR}}({#1})$}
57: \newcommand{\maximalparKomegaPlus}[1]{$\Upsilon^{f}_{M^{K,K^{\omega}}_{PAR,\infty}}({#1})$}
58: \newcommand{\maximalparKomegaInf}[1]{$\Upsilon^{\infty}_{M^{K,K^{\omega}}_{PAR}}({#1})$}
59: \newcommand{\maximalseqK}[1]{$\Upsilon^{f}_{M^{K}_{SEQ}}({#1})$}
60: \newcommand{\maximalseqInfK}[1]{$\Upsilon^{\infty}_{M_{SEQ}^{K}}({#1})$}
61: \newcommand{\maximalInf}[1]{$\Upsilon^{\infty}_{M}({#1})$}
62: \newcommand{\maximalparInf}[1]{$\Upsilon^{\infty}_{M_{PAR,K}}({#1})$}
63:
64:
65:
66: % MACROS FOR COMPOSITION OPERATORS
67: \def\parcomp#1#2{{#1\!\parallel\!#2}}
68: \def\seqcomp#1#2{{#1.(#2)}}
69:
70:
71: % OTHER MACROS
72: \def\PRS{\text{{\em PRS}}\xspace}
73: \def\PRSs{\text{{\em PRS\/}s}\xspace}
74: \def\BRS{\text{{\em BRS}}\xspace}
75: \def\BRSs{\text{{\em BRS\/}s}\xspace}
76: \def\ALTL{\text{{\em ALTL}}\xspace}
77: \def\LTL{\text{{\em LTL}}\xspace}
78: \def\MBRS{\text{{\em MBRS}}\xspace}
79: \def\MBRSs{\text{{\em MBRS\/}s}\xspace}
80:
81: \def\npla#1{{\langle #1\rangle}}
82:
83:
84: \def\ldsrule#1#2#3{\ensuremath{
85: \cfrac[c]{#1}
86: {\ #2\ }\text{\footnotesize \ \ensuremath{#3}}}}
87:
88: \def\suffix#1{\ensuremath{\text{\emph{suffix}}}(#1)}
89: \def\firstact#1{\ensuremath{\text{\emph{firstact}}}(#1)}
90:
91: \title{Verification of Process Rewrite Systems in normal form}
92: \author{
93: L.~Bozzelli$^1$ \\[10pt]
94: {\small\begin{tabular}{c@{\hspace{0cm}}c}
95: $\!\!^1$Dept. of Mathematics and Applications \\
96: Universit\`a di Napoli ``Federico II'' \\
97: Napoli, Italy \\
98: {\tt laura.bozzelli@dma.unina.it}
99: \end{tabular}
100: }}
101:
102: \date{}
103:
104: \begin{document}
105: \maketitle
106: \begin{abstract}
107: We consider the problem of model--checking
108: for Process Rewrite Systems (\PRSs) in normal form. In a \PRS in normal form
109: every rewrite rule either only deals with procedure calls and procedure
110: termination, possibly with value return, (this kind of rules
111: allows to capture Pushdown Processes), or only deals with dynamic
112: activation of processes and synchronization (this kind of rules
113: allows to capture Petri Nets). The model-checking problem for
114: \PRSs and action-based linear temporal logic (\ALTL) is
115: undecidable. However, decidability of model--checking for \PRSs and
116: some interesting fragment of \ALTL remains an open question.
117: In this paper we state decidability results concerning
118: generalized acceptance properties about infinite derivations (infinite term
119: rewritings) in \PRSs in normal form. As a consequence, we obtain
120: decidability of the model-checking (restricted to infinite runs)
121: for \PRSs in normal form and a meaningful fragment of \ALTL.
122: \end{abstract}
123:
124:
125: \section{Introduction}
126: Automatic verification of systems is nowadays one of the most
127: investigated topics. A major difficulty to face when considering
128: this problem comes to the fact that, reasoning about systems in
129: general may require dealing with infinite state models. For
130: instance, software systems may introduce infinite states both
131: manipulating data ranging over infinite domains, and having
132: unbounded control structures such as recursive procedure calls
133: and/or dynamic creation of concurrent processes (e.g.
134: multi--treading). Many different formalisms have been proposed for
135: the description of infinite state systems. Among the most popular
136: are the well known formalisms of Context Free Processes, Pushdown
137: Processes, Petri Nets, and Process Algebras. The first two are
138: models of sequential computation, whereas Petri Nets and Process
139: Algebra explicitly take into account concurrency. The model
140: checking problem for these infinite state formalisms have been
141: studied in the literature. As far as Context Free Processes and
142: Pushdown Automata are concerned (see
143: \cite{ay98,bouajjani97,BS94,burkart01,hun94,ehrs00,walukiewicz96}),
144: decidability of the modal $\mu$--calculus, the most powerful of
145: the modal and temporal logics used for verification, has been
146: established (e.g. see \cite{BS94,hun94}). In
147: \cite{esp97,esparza94}, model checking for Petri nets has been
148: studied. The branching temporal logic as well as the state-based
149: linear temporal logic are undecidable even for restricted logics.
150: Fortunately, the model checking for action-based linear temporal
151: logic (\ALTL) is decidable.\newline
152:
153:
154: Verification of formalisms which accommodate both parallelism and
155: recursion is a challenging problem. To formally study this kind of
156: systems, recently the formal framework of Process Rewrite Systems
157: (\PRSs) has been introduced \cite{mayr98}. This framework, which
158: is based on term rewriting, subsumes many common infinite states
159: models such us Pushdown Systems, Petri Nets, Process Algebra, etc.
160: The decidability results already
161: known in the literature for the general framework of \PRSs
162: concerns reachability analysis. However, the model checking of
163: action-based temporal logic becomes undecidable. It remains
164: un\-de\-ci\-dable even for restricted models such as those
165: presented in
166: \cite{bouajjani96}.\newline
167:
168: In this paper we extend the known decidability results, for a
169: relevant syntactic fragment of \PRSs, to properties of infinite
170: derivations, thus allowing for automatic verification of some
171: interesting classes of action-based linear time properties. The
172: fragment we consider is that of \PRSs in normal form, where every
173: rewrite rule either only deals with procedure calls and procedure
174: termination, possibly with value return, (this kind of rules
175: allows to capture Pushdown Processes), or only deals with dynamic
176: activation of processes and synchronization (this kind of rules
177: allows to capture Petri Nets).\newline Our result extends our
178: previous result established in \cite{Bozz03}, and regards the
179: decidability of two problems: the first (resp., the second)
180: concerns generalized acceptance properties of finite derivations
181: (resp., infinite derivations) in \PRSs in normal form. As a
182: consequence we obtain decidability of the model-checking
183: (restricted to infinite executions) for \PRSs in normal form and a
184: meaningful \ALTL fragment.\newline
185: The rest
186: of the paper is structured as follows. In Section 2, we recall
187: the framework of Process Rewrite Systems, we summarize some
188: decidability results for reachability problems, and our previous
189: result for \PRSs in normal form. In Section 3, it is shown how our
190: decidability results about generalized acceptance properties of
191: infinite derivations in \PRSs in normal form can be used in
192: model-checking for a meaningful \ALTL fragment. In Section 4, we
193: prove decidability of the two problems about finite and infinite
194: derivations in $\PRSs$ in normal form, mentioned above. Appendix
195: contains detailed proof of our results.
196:
197:
198: \section{Process Rewrite Systems}
199:
200: In this section we recall the framework of \emph{Process Rewrite
201: Systems} (\PRSs). We also recall the notion of \emph{B\"{u}chi
202: Rewrite System} (\BRS) introduced in \cite{Bozz03} to prove
203: decidability of the model--checking problem for some classes of
204: linear time properties
205: and \PRSs \emph{in normal form}. We conclude
206: this section by summarizing some decidability results on \PRSs,
207: known in the literature, that will be exploited in further
208: sections of the paper.
209:
210: \subsection{Process Rewrite Systems and B\"{u}chi Rewrite Systems}
211:
212: In this subsection we recall the notion of Process Rewrite System,
213: as introduced in~\cite{mayr98}. The idea is that a process (and
214: its current state) is described by a term. The behavior of a
215: process is given by rewriting the corresponding term by means of a
216: finite set of rewrite rules.
217:
218: \begin{Definition}[Process Term] Let $Var$ be a finite set of process
219: variables. The set $T$ of {\em process terms} over $Var$ is
220: inductively defined as follows:
221: \begin{itemize}
222: \item $Var\subseteq T$
223: \item $\varepsilon\in{}T$
224: \item
225: $t_{1}$$\parallel$$t_{2}\in{}T$, for all $t_{1},t_{2}\in{}T$
226: \item $X.(t)\in{}T$, for all $X\in{}Var$ and $t\in{}T$
227: \end{itemize}
228: where $\varepsilon$ denotes the empty term, ``\,$\parallel$''
229: denotes parallel composition, and ``$.()$'' denotes sequential
230: composition\footnote{\cite{mayr98} also allows terms of the form
231: $t_{1}.(t_{2})$, where $t_{1}$ is a parallel composition of
232: variables. In the current context this generalization is not
233: relevant.}.
234: \end{Definition}
235:
236: We denote by $T_{SEQ}$ the subset of terms in $T$ devoid of any
237: occurrence of parallel composition operator, and by $T_{PAR}$ the
238: subset of terms in $T$ devoid of any occurrence of the sequential
239: composition operator. Notice that we have $T_{PAR}\cap T_{SEQ} =
240: Var\cup\{\varepsilon\}$.
241:
242: In the rest of the paper we only consider process terms modulo
243: commutativity and associativity of ``$\parallel$'', moreover
244: $\varepsilon$ will act as the identity for both parallel and
245: sequential composition.
246: Therefore, we introduce the relation
247: $\approx_{T}$, which is the smallest equivalence relation on $T$
248: such that for all $t_1,t_2, t_3\in{}T$ and $X\in{}Var$:
249: %
250: \begin{itemize}
251: \item $t_{1}$$\parallel$$t_{2}\approx_{T}t_{2}$$\parallel$$t_{1}$,
252: $t_{1}$$\parallel$$(t_{2}$$\parallel$$t_3)\approx_{T}(t_{1}$$\parallel$$t_{2})$$\parallel$$t_3$,
253: and
254: $t_{1}$$\parallel$$\varepsilon\approx_{T}t_{1}$.
255: \item $X.(\varepsilon)\approx_{T}X$, and if
256: $t_{1}\approx_{T}t_{2}$,
257: then $X.(t_{1})\approx_{T}X.(t_{2})$.
258: \end{itemize}
259:
260:
261: In the paper, we always confuse terms and their equivalence
262: classes (w.r.t. $\approx_{T}$). In particular, $t_1 = t_2$
263: (resp., $t_1 \not= t_2$) will be used to mean that $t_1$ is
264: equivalent (resp., not equivalent) to $t_2$.
265:
266: \begin{Definition}[Process Rewrite System]
267: A {\em Process Rewrite System} $\mathrm{(}$or \PRS, or {\em Rewrite System}$\mathrm{)}$ over the
268: alphabet $\Sigma$ and the set of process variables $Var$ is a finite
269: set of rewrite rules $\Re\subseteq{}T\times\Sigma\times{}T$ of the
270: form $\prsrule{t}{a}{t'}$, where $t$ $\mathrm{(}$$\neq\varepsilon$$\mathrm{)}$ and $t'$
271: are terms in $T$, and $a\in\Sigma$.
272: \end{Definition}
273:
274: The semantics of a \PRS $\Re$ is given by a Labelled Transition
275: System $\npla{T,\Sigma,\prslongrule{}{}{}}$, where the set of
276: states is the set of terms $T$ of $\Re$, the set of actions is the
277: alphabet $\Sigma$ of $\Re$, and the transition relation
278: $\prslongrule{}{}{} \subseteq T \times \Sigma \times T$ is the
279: smallest relation satisfying the following inference rules:
280:
281: \ldsrule{}{\prslongrule{t}{a}{t'}}{(\prsrule{t}{a}{t'})\in\Re}\hspace*{1cm}
282: \ldsrule{\prslongrule{t_1}{a}{t_1'}}
283: {\prslongrule{\parcomp{t_1}{t}}{a}{\parcomp{t_1'}{t}}}{\forall{}t\in{}T}
284: \hspace*{1cm}
285: \ldsrule{\prslongrule{t_1}{a}{t_1'}}
286: {\prslongrule{\seqcomp{X}{t_1}}{a}{\seqcomp{X}{t_1'}}}{\forall{}X\in{}Var}
287: \newline\newline
288:
289:
290: For a \PRS $\Re$ with set of terms $T$ and LTS
291: $\npla{T,\Sigma,\prslongrule{}{}{}}$, a \emph{path in} $\Re$ from
292: $t\in{}T$ is a path in $\npla{T,\Sigma,\prslongrule{}{}{}}$ from
293: $t$, i.e. a (finite or infinite) sequence of LTS edges
294: $\prsrule{t_{0}}{a_{0}}{t_{1}} \prsrule{}{a_{1}}{t_{2}}
295: \prsrule{}{a_{2}}{}$ such that $t_0=t$ and
296: $\prsrule{t_{j}}{a_{j}}{t_{j+1}} \in \prsrule{}{}{}$ for any $j$.
297: A \emph{run in $\Re$} from $t$ is a maximal path from $t$, i.e. a
298: path from $t$ which is either infinite or has the form
299: $\prsrule{t_{0}}{a_{0}}{t_{1}} \prsrule{}{a_{1}}{\ldots}
300: \prsrule{}{a_{n-1}}{t_n}$ and there is no edge
301: $\prsrule{t_n}{a_n}{t'} \in \prsrule{}{}{}$, for any $a_n\in
302: \Sigma$ and $t' \in T$. We write $runs_{\Re}(t)$ (resp.,
303: $runs_{\Re,\infty}(t)$) to refer to the set of runs (resp.,
304: infinite runs) in $\Re$ from $t$, and $runs(\Re)$ to refer to the
305: set of all the runs in $\Re$.
306:
307: \bigskip
308:
309: The LTS semantics induces, for a rule $r\in \Re$, the following
310: notion of \emph{one--step derivation} by $r$. The \emph{one--step
311: derivation} by $r$ relation, \prsoneder{r}, is the least relation
312: such that:
313: \begin{itemize}
314: \item $t$ \prsoneder{r} $t'$, for $r=\prsrule{t}{a}{t'}$ \item
315: $t_{1}$$\parallel$$t$ \prsoneder{r} $t_{2}$$\parallel$$t$, if
316: $t_{1}$ \prsoneder{r} $t_{2}$ and $t\in{}T$ \item $X.(t_{1})$
317: \prsoneder{r} $X.(t_{2})$, if $t_{1}$ \prsoneder{r} $t_{2}$ and
318: $X\in{}Var$
319: \end{itemize}
320:
321: A \emph{finite derivation} in $\Re$ from a term $t$ to a term $t'$
322: (through a finite sequence $\sigma = r_{1}r_{2}\ldots{}r_{n}$ of
323: rules in $\Re$), is a sequence $d$ of one--step derivations $t_0$
324: \prsoneder{r_1} $t_1$ \prsoneder{r_2} $t_2\ldots$
325: \prsoneder{r_{n-1}} $t_{n-1}$ \prsoneder{r_n} $t_n$, with $t_0=t$,
326: $t_n=t'$ and $t_i$ \prsoneder{r_{i+1}} $t_{i+1}$ for all
327: $i=0,\ldots,n-1$. The derivation $d$ is a \emph{$n$--step
328: derivation} (or a \emph{derivation of length $n$}), and for
329: succinctness is denoted by $t$ \multider{\sigma} $t'$. Moreover,
330: we say that $t'$ is \emph{reachable} in $\Re$ from term $t$
331: (through derivation $d$). If $\sigma$ is empty, we say that $d$ is
332: a {\em null derivation\/}.
333: \newline
334: A \emph{infinite derivation} in $\Re$ from a term $t$ (through an
335: infinite sequence $\sigma = r_{1}r_{2}\ldots $ of rules in $\Re$),
336: is an infinite sequence of one step derivations $t_0$
337: \prsoneder{r_1} $t_1$ \prsoneder{r_2} $t_2\ldots$ such that
338: $t_0=t$ and $t_i$ \prsoneder{r_{i+1}} $t_{i+1}$ for all $i \geq
339: 0$. For succinctness such derivation is denoted by $t$
340: \multider{\sigma}.
341: \newline
342: Notice that there is a strict correspondence between the notion of
343: derivation from a term $t$ and that of path from the term $t$. In
344: fact, there exists a path $\prsrule{t_{0}}{a_{0}}{t_{1}}
345: \prsrule{}{a_{1}}{t_{2}\ldots}$ from $t_0$ in $\Re$ iff there
346: exists a derivation $t_0$ \prsoneder{r_1} $t_1$ \prsoneder{r_2}
347: $t_2\ldots$ from $t_0$ in $\Re$, with $a_i = label(r_i)$, for any
348: $i$ (where for a rule $r \in \Re$ with $r = \prsrule {t}{a}{t'}$,
349: $label(r)$ denotes the label $a$ of $r$).
350:
351: \bigskip
352:
353: In the following, we shall consider \PRSs in a syntactical
354: restricted form called \emph{normal form}.
355:
356: \begin{Definition}[Normal Form] A \PRS $\Re$ is said to be in {\em
357: normal form} if every rule $r\in\Re$ has one of the following forms:
358: \begin{description}
359: \item[PAR rules:] Any rule devoid of sequential composition;
360: \item[SEQ rules:] $\prsrule{X}{a}{Y.(Z)}$, $\prsrule{X.(Y)}{a}{Z}$
361: or
362: $\prsrule{X}{a}{Y}$, or $\prsrule{X}{a}{\varepsilon}$.
363: \end{description}
364: \noindent with $X,Y,Z\in{}Var$. A \PRS where all the rules are SEQ
365: rules is called \emph{sequential} \PRS. Similarly, a \PRS where
366: all the rules are PAR rules is called \emph{parallel} \PRS.
367: \end{Definition}
368:
369:
370:
371: The sequential and parallel fragments of $PRS$ are significant: in
372: \cite{mayr98} it is shown that sequential \PRS\/s are semantically
373: equivalent (via \emph{bisimulation equivalence}) to Pushdown
374: Processes, while parallel \PRS\/s are semantically equivalent to
375: Petri Nets. Moreover, from the fact that Pushdown systems and
376: Petri Nets are not comparable (see \cite{M96,BCS96}) it follows
377: that \PRSs in normal form are strictly more expressive than both
378: their sequential and parallel fragment. So, the following result
379: holds:
380:
381: \begin{Proposition}
382: \PRSs in normal form are strictly more expressive than Petri nets
383: and Pushdown Processes.
384: \end{Proposition}
385:
386:
387: Now, let us extend the notion of \PRS to that of B\"{u}chi Process
388: Rewrite System (\BRS). Intuitively, a \BRS is a \PRS where we can
389: distinguish between non--accepting rewrite rules and accepting
390: rewrite rules.
391:
392: \begin{Definition}[B\"{u}chi Rewrite System]
393: A \emph{B\"{u}chi Rewrite System} $\mathrm{(BRS)}$ over
394: a finite set of process variables $Var$ and an alphabet $\Sigma$ is
395: a pair $\npla{\Re,\Re_{F}}$, where $\Re$ is a \PRS over $Var$
396: and $\Sigma$, and
397: $\Re_{F}\subseteq\Re$ is the set of accepting rules.
398: \end{Definition}
399:
400: A B\"{u}chi Rewrite System $\npla{\Re,\Re_{F}}$ is called a \BRS
401: \emph{in normal form} (resp., \emph{sequential} \BRS,
402: \emph{parallel} \BRS), if the underlying process rewrite system
403: $\Re$ is a \PRS in normal form (resp., parallel \PRS, sequential
404: \PRS).
405: \newline
406: \begin{Definition}[Acceptance in B\"{u}chi Rewrite Systems]\label{Def:OldAcceptance}
407: Let us consider a \BRS $M=\npla{\Re,\Re_{F}}$. An \emph{infinite}
408: derivation $t$ \multider{\sigma} in $\Re$ from $t$ is said to
409: be \emph{accepting} $\mathrm{(}$in $M\mathrm{)}$ if
410: $\sigma$ contains infinite occurrences of accepting
411: rules.\newline
412: A \emph{finite}
413: derivation $t$ \multider{\sigma} $t'$ in $\Re$ from $t$ is said to
414: be \emph{accepting} $\mathrm{(}$in $M\mathrm{)}$ if
415: $\sigma$ contains some occurrence of accepting rule.
416: \end{Definition}
417:
418:
419:
420: \subsection{Decidability results for \PRSs}\label{sec:OldResults}
421:
422: In this section we will summarize decidability results on \PRSs
423: which are known in the literature, and which will be exploited in
424: further sections of the paper.
425:
426: \paragraph{Verification of ALTL (Action--based LTL)}\
427:
428: Given a finite set $\Sigma$ of atomic propositions, the set of
429: formulae $\varphi$ of ALTL over $\Sigma$ is defined as follows:
430: %
431: \begin{displaymath}
432: \textrm{$\varphi::= true$ $|$ $\neg\varphi$ $|$
433: $\varphi_{1}\wedge\varphi_{2}$ $|$
434: $\npla{a}\varphi$
435: $|$ $\varphi_{1}U\varphi_{2}$ $|$ $G\varphi$ $|$ $F\varphi$}
436: \end{displaymath}
437:
438: \noindent where $a\in\Sigma$.
439: %
440:
441: In order to give semantics to ALTL formulae on a \PRS $\Re$, we
442: need some additional notation. Given a path $\pi=t_{0}$
443: $\mathop{\rightarrow}\limits^{a_{0}}$ $t_{1}$
444: $\mathop{\rightarrow}\limits^{a_{1}}$ $t_{2}$
445: $\mathop{\rightarrow}\limits^{a_{2}}\ldots$ in $\Re$, $\pi^{i}$
446: denotes the suffix of $\pi$ starting from the $i$--th term in the
447: sequence, i.e. the path $t_{i}$
448: $\mathop{\rightarrow}\limits^{a_{i}}$ $t_{i+1}$
449: $\mathop{\rightarrow}\limits^{a_{i+1}}\ldots$. The set of all the
450: suffixes of $\pi$ is denoted by $\suffix{\pi}$ (notice that if
451: $\pi$ is a run in $\Re$, then $\pi^{i}$ is also a run in $\Re$,
452: for each $i$.) If the path $\pi=t_{0}$
453: $\mathop{\rightarrow}\limits^{a_{0}}$ $t_{1}$
454: $\mathop{\rightarrow}\limits^{a_{1}}\ldots$ is \emph{non--trivial}
455: (i.e., the sequence contains at least two terms) $\firstact{\pi}$
456: denotes $a_{0}$, otherwise we set $\firstact{\pi}$ to an element
457: non in $\Sigma$, say it 0.
458:
459: \ALTL formulae over a \PRS $\Re$ are interpreted in terms of the
460: set of the runs in $\Re$ satisfying the given \ALTL formula. The
461: \emph{denotation of a formula $\varphi$} relative to $\Re$, in
462: symbols $[[\varphi]]_{\Re}$, is defined inductively as follows:
463: %
464: \begin{itemize}
465: \item $[[true]]_{\Re}= runs(\Re)$ \item
466: $[[\neg\varphi]]_{\Re}=runs(\Re)\setminus[[\varphi]]_{\Re}$ \item
467: $[[\varphi_{1}\wedge\varphi_{2}]]_{\Re}=
468: [[\varphi_{1}]]_{\Re}\,\cap\,[[\varphi_{2}]]_{\Re}$
469: \item $[[\npla{a}\varphi]]_{\Re}=\{\pi\in{}runs(\Re)\ \mid\
470: \firstact{\pi}=a \text{ and } \pi^{1}\in{}[[\varphi]]_{\Re}\}$
471: \item $[[\varphi_{1}U\varphi_{2}]]_{\Re} = \{\begin{array}[t]{l}
472: \pi\in{}runs(\Re)\ \mid\ \text{for some } i\geq 0,
473: \pi^{i} \text{ is defined and }
474: \pi^{i}\in{}[[\varphi_{2}]]_{\Re}, \text{ and }\\ %
475: \text{for all } j<i, \pi^{j}\in{}[[\varphi_{1}]]_{\Re}\
476: \}\end{array}$
477: \item $[[G\varphi]]_{\Re}=\{\pi\in{}runs(\Re)\ \mid\ \suffix{\pi}
478: \subseteq [[\varphi]]_{\Re}\}$
479: \item $[[F\varphi]]_{\Re}=\{\pi\in{}runs(\Re)\ \mid\
480: \suffix{\pi}\cap[[\varphi]]_{\Re}\not=\emptyset\}$
481: \end{itemize}
482:
483: For any term $t\in{}T$ and \ALTL formula $\varphi$, we say that
484: $t$ satisfies $\varphi$ (resp., satisfies $\varphi$ restricted to
485: infinite runs) (w.r.t $\Re$), in symbols $t \models_{\Re}\varphi$
486: (resp., $t \models_{\Re,\infty}\varphi$), if
487: $runs_{\Re}(t)\subseteq[[\varphi]]_{\Re}$ (resp.,
488: $runs_{\Re,\infty}(t)\subseteq[[\varphi]]_{\Re}$).
489:
490: The model-checking problem (resp., model--checking problem
491: restricted to infinite runs) for \ALTL and \PRSs is the problem of
492: deciding if, given a \PRS $\Re$, a \ALTL formula $\varphi$ and a
493: term $t$ of $\Re$, $t\models_{\Re}\varphi$ (resp.,
494: $t\models_{\Re,\infty}\varphi$). The following are well--known
495: results:
496:
497: \begin{Proposition}[see~\cite{mayr98,esparza94,esp97}]\label{prop:parallel-altl}
498: The model--checking problem for \ALTL and parallel \PRSs, possibly
499: restricted to infinite runs, is decidable.
500: \end{Proposition}
501:
502:
503: \begin{Proposition}[see~\cite{alur01,bouajjani97,mayr98}]\label{prop:sequential-altl}
504: The model--checking problem for \ALTL and sequential \PRSs,
505: possibly restricted to infinite runs, is decidable.
506: \end{Proposition}
507:
508:
509: The model--checking problem for \ALTL and unrestricted \PRSs is
510: known
511: undecidable (see~\cite{mayr98}).\\
512: In ~\cite{Bozz03} we showed that the model--checking problem for \PRSs in
513: normal form (that are more expressive than parallel and sequential
514: \PRSs) and a small fragment of \ALTL is decidable. In particular,
515: we established the following result.
516:
517:
518: \begin{Theorem}[see~\cite{Bozz03}]\label{Theorem:OldResults}
519: \noindent Given a \BRS $\npla{\Re,\Re_F}$ in normal form and a
520: process variable $X$ it is decidable if
521: \begin{enumerate}
522: \item there exists an infinite accepting derivation in
523: $\Re$ from $X$.
524: \item there exists an infinite derivation in $\Re$ from
525: $X$, not containing occurrences of accepting rules.
526: \item there exists an infinite derivation from $X$,
527: containing a finite non--null number of occurrences of accepting
528: rules.
529: \end{enumerate}
530: \end{Theorem}
531:
532: This result implies the decidability of the model--checking
533: problem (restricted to infinite runs) for \PRSs in normal form and
534: the following fragment of \ALTL
535:
536: \setcounter{equation}{0}
537: \begin{equation}\label{Eq:OldFragmentALTL}
538: \varphi ::= F\,\psi\ |\ GF\,\psi \ |\ \neg \varphi
539: \end{equation}
540: where $\psi$ denotes a \ALTL \emph{propositional}
541: formula\footnote{The set of \ALTL propositional formulae $\psi$
542: over the set
543: $\Sigma$ of atomic propositions is so defined:\\
544: \hspace*{4cm}$\psi ::= <$$a$$>true$$ \ | \psi \wedge \psi \ |\
545: \neg \psi$ (where $a\in{}\Sigma$)}.
546:
547: \noindent{}Thus, the following result holds
548:
549: \begin{Theorem}[see~\cite{Bozz03}]\label{Theorem:OldResultOnALTL}
550: \noindent{}The model--checking problem for \PRSs in normal form
551: and the fragment \ALTL
552: $\mathrm{(}$\ref{Eq:OldFragmentALTL}$\mathrm{)}$, restricted to
553: infinite runs from process variables, is decidable.
554: \end{Theorem}
555:
556:
557: \section{Multi B\"{u}chi Rewrite Systems}
558:
559: In this section we generalize the notion of acceptance in \PRSs,
560: as defined in \ref{Def:OldAcceptance}, in\-tro\-ducing the notion
561: of \emph{Multi B\"{u}chi Rewrite System} (\MBRS). Intuitively, a
562: \MBRS is a \PRS with a finite number of accepting components,
563: where each component is a subset of the \PRS. The goal is to
564: extend the decidability result of theorem
565: \ref{Theorem:OldResults}. As a consequence, we obtain decidability
566: of model--checking for \PRSs in normal form and a meaningful
567: fragment of \ALTL, that includes strictly the fragment
568: (\ref{Eq:OldFragmentALTL}) defined in subsection
569: \ref{sec:OldResults}.\newline
570:
571: \begin{Definition}[Multi B\"{u}chi Rewrite System]
572: A \emph{Multi B\"{u}chi Rewrite System} $\mathrm{(}$\emph{MBRS}$\mathrm{)}$
573: $\mathrm{(}$with $n$ \emph{accepting components}$\mathrm{)}$ over a finite set of
574: process variables $Var$ and an alphabet $\Sigma$ is a tuple
575: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$, where $\Re$ is a \PRS over $Var$
576: and $\Sigma$, and
577: $\forall{}i=1,\ldots,n$ $\Re_{i}^{A}\subseteq\Re$. $\Re$ is called the \emph{support} of $M$.
578: \end{Definition}
579:
580: A \MBRS $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ is a
581: \MBRS \emph{in
582: normal form} (resp., \emph{sequential} \MBRS, \emph{parallel} \MBRS),
583: if the underlying \PRS $\Re$ is in normal form (resp., is
584: sequential, is parallel).
585:
586:
587:
588: \begin{Definition}
589: $\forall{}n\in{}N\setminus\{0\}$ let us denote by $P_{n}$ the set
590: $2^{\{1,\ldots,n\}}$ $\mathrm{(}$i.e., the set of the subsets of
591: $\{1,\ldots,n\}$$\mathrm{)}$.
592: \end{Definition}
593:
594:
595: \begin{Definition}[Finite Maximal]
596: Let
597: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ be
598: a \MBRS, and let $\sigma$ be a rule sequence
599: in $\Re$. The
600: \emph{finite maximal of} $\sigma$ \emph{as to} $M$, denoted by \maximal{\sigma}, is the
601: set $\{i\in\{1,\ldots,n\}|$ $\sigma$ contains some occurrence of rule in $\Re_{i}^{A}\}$.
602: \end{Definition}
603:
604:
605: \begin{Definition}[Infinite Maximal]
606: Let
607: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ be
608: a \MBRS, and let $\sigma$ be a rule sequence
609: in $\Re$.
610: The
611: \emph{infinite maximal of} $\sigma$ \emph{as to} $M$, denoted by \maximalInf{\sigma}, is the
612: set $\{i\in\{1,\ldots,n\}|$ $\sigma$ contains infinite occurrences of some rule in $\Re_{i}^{A}\}$.
613: \end{Definition}
614:
615: Now, we give a generalized notion of accepting derivation in a
616: \PRS.
617:
618: \begin{Definition}[Acceptance]
619: Let
620: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ be
621: a \MBRS, and let $t$ \multider{\sigma} be a derivation
622: in $\Re$. Given $K,K^{\omega}\in{}P_{n}$, we say that $t$ \multider{\sigma}
623: is a $(K,K^{\omega})-$\emph{accepting} derivation in $M$ if \maximal{\sigma} $=K$ and
624: \maximalInf{\sigma} $=K^{\omega}$.
625: \end{Definition}
626:
627: \begin{Definition}
628: Let $\sigma_{1}$ and $\sigma_{2}$ be sequences of rules in a \PRS
629: $\Re$.\\ We denote by $Interleaving(\sigma_{1},\sigma_{2})$ the
630: set of rule sequences in $\Re$ defined inductively in the
631: following way $\mathrm{(}$we denote by $\varepsilon$ the empty
632: sequence$\mathrm{)}$:
633: \begin{itemize}
634: \item $Interleaving(\varepsilon,\sigma)=\{\sigma\}$
635: \item $Interleaving(\sigma,\varepsilon)=\{\sigma\}$
636: \item $Interleaving(r_{1}\sigma_{1},r_{2}\sigma_{2})=\{r_{1}\sigma|\sigma\in{}
637: Interleaving(\sigma_{1},r_{2}\sigma_{2})\}\bigcup$\\
638: $\{r_{2}\sigma|\sigma\in{}
639: Interleaving(r_{1}\sigma_{1},\sigma_{2})\}$ where $r_{1}$ and
640: $r_{2}$ are rules in $\Re$.
641: \end{itemize}
642: \end{Definition}
643:
644: The above definition can be extended in obvious way to an
645: arbitrary number of rule sequences.\newline
646:
647:
648: Now, we establish (through propositions \ref{Prop:Maximal})
649: simple properties of rule sequences in \MBRSs, important in the
650: following. We need the following definition.
651:
652: \begin{Definition}
653: Let $\{K_{h}\}_{h\in{}N}$ be a succession of sets in $P_{n}$. Let us
654: denote by $\bigoplus_{h\in{}N}K_{h}$ the subset of
655: $P_{n}$ given by $\{i|$ $\forall{}j\in{}N$ there exists a $h>j$
656: such that $i\in{}K_{h}\}$.
657: \end{Definition}
658:
659:
660: \begin{Proposition}\label{Prop:Maximal}
661: Given a \MBRS
662: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ and two
663: rule sequences $\sigma$ and $\sigma'$ in $\Re$, the following properties hold:
664: \begin{enumerate}
665: \item If $\sigma$ is finite, then
666: \maximalInf{\sigma} = $\emptyset$.
667: \item If $\sigma'$ is a subsequence of
668: $\sigma$, then
669: \maximal{\sigma'} $\subseteq$ \maximal{\sigma} and
670: \maximalInf{\sigma'} $\subseteq$ \maximalInf{\sigma}.
671: \item If
672: $\lambda\in{}Interleaving(\sigma,\sigma')$, then
673: \maximal{\lambda} = \maximal{\sigma} $\cup$ \maximal{\sigma'} and
674: \maximalInf{\lambda} = \maximalInf{\sigma} $\cup$ \maximalInf{\sigma'}.
675: \item If
676: $\sigma=\sigma_0\sigma_1\sigma_2\ldots$, then
677: \maximal{\sigma} = $\bigcup_{h\in{}N}$\maximal{\sigma_{h}} and
678: \maximalInf{\sigma} = $\bigoplus_{h\in{}N}$\maximal{\sigma_{h}}.
679: \item If $\sigma'$ is a reordering of $\sigma$, then
680: \maximal{\sigma} = \maximal{\sigma'} and \maximalInf{\sigma} = \maximalInf{\sigma'}.
681: \end{enumerate}
682: \end{Proposition}
683:
684:
685:
686: In the following subsection we enunciate the two main results of
687: the paper (proved in section \ref{sec:Result}): the one regarding
688: acceptance properties of finite derivations in \MBRSs in normal
689: form, the second regarding acceptance properties of infinite
690: derivations in \MBRSs in normal form. Moreover, we show that the
691: second result can be exploited for automatic verification of some
692: meaningful (action-based) linear time properties of infinite runs
693: in \PRSs in normal form.
694:
695: \subsection{Model-checking of \PRSs in normal form}\label{sec:Model-checkingPRS}
696:
697: \noindent{}The main result of the paper is the following:
698:
699: \noindent \emph{Given a \MBRS in normal form
700: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ over Var and
701: the alphabet $\Sigma$, given a variable $X\in{}Var$ and two
702: sets
703: $K,K^{\omega}\in{}P_{n}$ it is decidable if}:
704: \begin{description}
705: \item[Problem 1:] \emph{There exists a $(K,\emptyset)$-accepting
706: finite derivation in $M$ from $X$}.
707: \item[Problem 2:] \emph{There exists a $(K,K^{\omega})$-accepting infinite
708: derivation in $M$ from $X$}.
709: \end{description}
710:
711: The decidability of Problem 1 is used mainly, as we'll see, to
712: prove decidability of Pro\-blem 2.\\
713: Before proving these results in Sections \ref{sec:finite} and
714: \ref{sec:infinite}, we show how a solution to these pro\-blems can
715: be effectively employed to perform model checking of some linear
716: time properties of infinite runs (from process variables) in \PRSs
717: in normal form. In particular we consider the following \ALTL
718: fragment, that includes strictly the fragment
719: (\ref{Eq:OldFragmentALTL}) defined in subsection
720: \ref{sec:OldResults}
721:
722: \setcounter{equation}{0}
723: \begin{equation}\label{Eq:NewFragmentALTL}
724: \varphi ::= F\,\psi\ |\ GF\,\psi \ |\ \neg \varphi \ |\ \varphi
725: \wedge \varphi \ |\ \varphi
726: \vee \varphi \
727: \end{equation}
728: where $\psi$ denotes a \ALTL \emph{propositional} formula. For
729: succinctness, we denote a \ALTL propositional formula of the form
730: $<$$a$$>true$ (with $a\in\Sigma$) simply by $a$.
731: \newline
732: The difference with fragment (\ref{Eq:OldFragmentALTL}) defined in
733: subsection \ref{sec:OldResults} is that, now, we allow boolean
734: combinations of formulae of the form $T\psi$, where $T$ denotes a
735: temporal operator in $\{F,G,FG,$ $GF\}$ and $\psi$ is a \ALTL
736: propositional formula.\newline Within the fragment above, property
737: patterns frequent in system verification can be expressed. In
738: particular, we can express \emph{safety properties} (e.g.,
739: $G\,p$), \emph{guarantee properties} (e.g., $F\,p$),
740: \emph{obligation properties} (e.g., $F\,p \rightarrow F\,q$, or
741: $G\,p \rightarrow G\,q$), \emph{response properties} (e.g.,
742: $GF\,p$), \emph{persistence properties} (e.g., $FG\,p$), and
743: finally \emph{reactivity properties} (e.g., $GF\,p \rightarrow
744: GF\,q$). Notice that important classes of properties like
745: invariants, as well as strong and weak fairness constraints, can
746: be expressed.\newline
747: To prove decidability of the
748: model--checking problem restricted to infinite runs for this
749: fragment of \ALTL we need some
750: definitions.\\
751: Given a propositional formula $\psi$ over $\Sigma$, we denote by
752: $[[\psi]]_{\Sigma}$ the subset of $\Sigma$ inductively defined as
753: follows
754: \begin{itemize}
755: \item $\forall{a}\in\Sigma$ $[[a]]_{\Sigma}=\{a\}$
756: \item $[[\neg\psi]]_{\Sigma}=\Sigma\setminus[[\psi]]_{\Sigma}$
757: \item $[[\psi_{1}\wedge\psi_{2}]]_{\Sigma}=
758: [[\psi_{1}]]_{\Sigma}\,\cap\,[[\psi_{2}]]_{\Sigma}$
759: \end{itemize}
760: Evidently, given a \PRS $\Re$ over $\Sigma$, a \ALTL propositional
761: formula $\psi$ and an infinite run $\pi$ of $\Re$ we have that
762: $\pi\in[[\psi]]_{\Re}$ iff $firstact(\pi)\in[[\psi]]_{\Sigma}$.\\
763: Given a rule $r=t$\Rule{a}$t'\in\Re$, we say that $r$
764: \emph{satisfies} the propositional formula $\psi$ if
765: $a\in[[\psi]]_{\Sigma}$. We denote by $AC_{\Re}(\psi)$ the set of
766: rules in $\Re$ that satisfy $\psi$. \newline Now, we introduce a
767: new temporal operator, denoted by $F^{+}$, whose semantic is so
768: defined:
769: \begin{itemize}
770: \item $[[F^{+}\varphi]]_{\Re}=\{\pi\in{}runs(\Re)\ \mid\
771: \suffix{\pi}\cap[[\varphi]]_{\Re}\not=\emptyset$, and either
772: $\pi$ is finite or
773: there exists a $j\geq{}0$ such that $\forall{}h\geq{}j$ $\pi^{h}\notin{}[[\varphi]]_{\Re}\}$
774: \end{itemize}
775:
776:
777: \noindent{}Now, we can prove the following result
778:
779: \begin{Theorem}\label{Theorem:NewResultOnALTL}
780: \noindent{}The model--checking problem for \PRSs in normal form
781: and the fragment \ALTL
782: $\mathrm{(}$\ref{Eq:NewFragmentALTL}$\mathrm{)}$, restricted to
783: infinite runs from process variables, is decidable.
784: \end{Theorem}
785:
786: \begin{proof}
787: Given a \PRS $\Re$ in normal form, a variable $X$ and a formula
788: $\varphi$ belonging to \ALTL fragment (\ref{Eq:NewFragmentALTL}),
789: we have to prove that it's decidable if
790: \begin{equation}\label{Eq:1}
791: X \models_{\Re,\infty} \varphi
792: \end{equation}
793: This problem is reducible to the problem of deciding if the
794: following property is satisfied
795: \begin{description}
796: \item[A.] There exists an infinite run $\pi$, with
797: $\pi\in{}runs_{\Re,\infty}(X)$, satisfying the formula
798: $\neg\varphi$, i.e. with $\pi\in[[\neg\varphi]]_{\Re}$.
799: \end{description}
800: Pushing negation inward, and using the following logic
801: equivalences
802: \begin{itemize}
803: \item $G\varphi_{1}\wedge{}G\varphi_{2}\equiv{}G(\varphi_{1}\wedge\varphi_{2})$
804: \item $\neg{}F\varphi_{1}\equiv{}G\neg\varphi_{1}$
805: \item $\neg{}G\varphi_{1}\equiv{}F\neg\varphi_{1}$
806: \item $F\varphi_{1}\equiv{}F^{+}\varphi_{1}\vee{}GF\varphi_{1}$
807: \item
808: $FG\varphi_{1}\equiv{}F^{+}\neg\varphi_{1}\vee{}G\varphi_{1}$
809: (this equivalence holds for infinite runs)
810: \end{itemize}
811: the formula $\neg\varphi$ can be written in the following
812: disjunctive normal form
813: \begin{equation}\label{Eq:2}
814: \neg\varphi \equiv \bigvee_{i} \Bigr( \bigwedge_{j} F^{+}\psi_{j} \wedge
815: \bigwedge_{k} GF\eta_{k} \wedge G\zeta \Bigr)
816: \end{equation}
817: where $\psi_{j}$, $\eta_{k}$ and $\zeta$ are \ALTL propositional
818: formulae. Evidently, we can restrict ourselves to consider a
819: single disjunct in (\ref{Eq:2}). In other words, problem in
820: equation (\ref{Eq:1}) is reducible to the problem of deciding,
821: given a formula having the following form
822: \begin{equation}\label{Eq:3}
823: F^{+}\psi_{1} \wedge\ldots\wedge F^{+}\psi_{m_{1}}\wedge
824: GF\eta_{1} \wedge\ldots\wedge GF\eta_{m_{2}} \wedge
825: G\zeta\footnote{$\psi_{j}$, $\eta_{k}$ and $\zeta$ are \ALTL propositional
826: formulae}
827: \end{equation}
828: if the following property is satisfied
829: \begin{description}
830: \item[B.] There exists an infinite run $\pi$, with
831: $\pi\in{}runs_{\Re,\infty}(X)$, satisfying formula
832: (\ref{Eq:3}).
833: \end{description}
834: Let us consider the \MBRS in normal form
835: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ where
836: $n=m_{1}+m_{2}+1$ and
837: \begin{eqnarray}
838: \textrm{for all $i=1,\ldots,m_{1}\quad\quad$
839: $\Re_{i}^{A}=AC_{\Re}(\psi_{i})$}\nonumber\\
840: \textrm{for all ${}j=1,\ldots,m_{2}\quad\quad$
841: $\Re_{j+m_{1}}^{A}=AC_{\Re}(\eta_{j})$}\nonumber\\
842: \textrm{ $\Re_{m_{1}+m_{2}+1}^{A}=AC_{\Re}(\neg\zeta)$}\nonumber
843: \end{eqnarray}
844: Let $K=\{1,\ldots,m_{1}+m_{2}\}$ and
845: $K^{\omega}=\{m_{1}+1,\ldots,m_{1}+m_{2}\}$. It is easy to show
846: that property B is satisfied if, and only if, there exists a
847: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
848: variable $X$.
849: From decidability of Problem 2, we obtain the assertion.
850: \end{proof}
851:
852:
853:
854:
855: \section{Decidability results on \MBRSs in normal form}\label{sec:Result}
856: In this section we prove the main results of the paper, namely the
857: decidability of problems about derivations in \MBRSs stated in
858: subsection~\ref{sec:Model-checkingPRS}. Therefore, in
859: subsection~\ref{sec:SimpleResults} we report some preliminary
860: results on the decidability of some properties about derivations
861: of parallel and sequential \MBRSs which are necessary to carry out
862: the proof of the main results, which are given in
863: subsection~\ref{sec:finite} and \ref{sec:infinite}.
864:
865:
866:
867: \subsection{Decidability results on parallel and sequential \MBRSs}\label{sec:SimpleResults}
868:
869: In this section we establish simple decidability results on
870: properties of derivations in parallel and sequential \MBRSs. These
871: results are the basis for the decidability proof of the problems
872: 1-2 stated in subsection~\ref{sec:Model-checkingPRS}.
873:
874: \begin{Proposition}\label{Prop:ParMBRS-F}
875: Given a parallel \MBRS
876: $M_{P}=\npla{\Re_{P},\npla{\Re_{P,1}^{A},\ldots,\Re_{P,n}^{A}}}$ over $Var$ and the alphabet
877: $\Sigma$, given two variables $X,Y\in Var$ and $K\in{}P_{n}$,
878: it is decidable if
879: \begin{enumerate}
880: \item there exists a finite derivation
881: in $\Re_{p}$ of the form
882: $\prsdernorm{X}{\sigma}{\Re_{P}}{\parcomp{t}{Y}}$, for some term
883: $t$, with $|\sigma|>0$ and \maximalG{M_{P}}{\sigma} $=K$.
884: \item there exists a finite derivation
885: in $\Re_{P}$ of the form
886: $\prsdernorm{X}{\sigma}{\Re_{P}}{\varepsilon}$ such that \maximalG{M_{P}}{\sigma} $=K$.
887: \item there exists a finite derivation in $\Re_{P}$ of the form
888: $\prsdernorm{X}{\sigma}{\Re_{P}}{Y}$ such that
889: \maximalG{M_{P}}{\sigma} $=K$. \item there exists a
890: $(K,\emptyset)$-accepting finite derivation in $M_{P}$ from $X$.
891: \end{enumerate}
892: \end{Proposition}
893:
894: \begin{proof}
895: We exploit the decidability of the model-checking problem
896: for \ALTL and parallel \PRSs (see prop. \ref{prop:parallel-altl}).\\
897: For all $r\in\Re_{P}$ let us denote by $label(r)$ the set
898: $\{h\in{}\{1,\ldots,n\}|r\in\Re^{A}_{P,h}\}$. Let us denote by
899: $\zeta$ the set $\{label(r)|r\in\Re_{P}\}$.\\
900: Let us consider the first problem. Starting from $\Re_{P}$, we
901: build a new parallel \PRS $\Re'_{P}$ over the alphabet
902: $\overline{\Sigma}=\{Y\}\cup\zeta$, as follows. At first, we
903: substitute every rule $r$ in $\Re_{P}$ of the form
904: $t$\Rule{a}$t'$ with the rule $t$\Rule{label(r)}$t'$. Finally, we
905: add the rule $Y$\Rule{Y}$Y$. The reason to add this rule is to
906: allow to
907: express reachability of variable $Y$ as a \ALTL formula.\\
908: Now, let us assume that $K\neq\emptyset$. A similar reasoning
909: applies if $K=\emptyset$.
910: Let us indicate by $\varphi_{1}$ the following \ALTL formula,
911: \begin{displaymath}
912: \textrm{$F(<Y>true)$ $\bigwedge$
913: $G\Bigr(\neg(<Y>true)$ $\vee$ $<Y>(G(<Y>true))\Bigr)$}
914: \end{displaymath}
915: This formula is satisfied by infinite runs $\pi$ in $\Re'_{P}$
916: having the form $\pi_{1}\pi_{2}$, where $\pi_{2}$ contains only
917: occurrences of label $Y$, and $\pi_{1}$ doesn't contain
918: occurrences of label $Y$.\\
919: It's easy to deduce that property 1 is satisfied if, and only if,
920: there exists a run $\pi$ in $\Re'_{P}$ with
921: $\pi\in{}runs_{\Re'_{P}}(X)$ satisfying the following \ALTL
922: formula:
923: \begin{equation}
924: \textrm{$\varphi:= \varphi_{1} \wedge$
925: $\bigr(\bigwedge_{i\in{}K}\bigvee_{r\in{}\Re^{A}_{P,i}}F(<label(r)>true)\bigr)\wedge$}
926: \textrm{$\bigr(\bigwedge_{i\notin{}K}\bigwedge_{r\in{}\Re^{A}_{P,i}}G(\neg<label(r)>true)\bigr)$}\nonumber
927: \nonumber\footnote{for all $i\in{}K$ if $\Re^{A}_{P,i}=\emptyset$,
928: then
929: $\bigvee_{r\in{}\Re^{A}_{P,i}}F(<label(r)>true)$ denotes $false$}
930: \end{equation}
931:
932: Therefore, property 1 isn't satisfied if, and only if,
933: $\forall\pi\in{}runs_{\Re'_{P}}(X)$
934: $\pi\notin[[\varphi]]_{\Re'_{P}}$, that
935: is if, and only if, $X\models_{\Re'_{P}}\neg\varphi$.\\
936:
937: Now, let us consider the second problem. Similarly to the problem
938: above, starting from $\Re_{P}$, we build a new parallel \PRS
939: $\Re'_{P}$, this time on the alphabet
940: $\overline{\Sigma}=Var\cup{}\zeta$, as follows. At first, we
941: substitute every rule $r$ in $\Re_{P}$ of the form
942: $t$\Rule{a}$t'$ with the rule $t$\Rule{label(r)}$t'$. Finally,
943: $\forall{}Y\in{}Var$ we add the rule $Y$\Rule{Y}$Y$. Notice that,
944: by construction, a term $t$ has no successor in $\Re'_{P}$ if,
945: and only if, $t=\varepsilon$. Let us indicate by $\varphi_{1}$ the
946: following \ALTL propositional formula,
947: \begin{displaymath}
948: \bigvee_{Y\in{}Var}\Bigr(<Y>true\Bigr)\vee\bigvee_{l\in\zeta}\Bigr(<l>true\Bigr)
949: \end{displaymath}
950: The negation of $\varphi_{1}$ means that no rule can be applied,
951: in other words the system
952: has terminated.\\
953: It's easy to deduce that property 2 is satisfied if, and only if,
954: there exists a run $\pi$ in $\Re'_{P}$ with
955: $\pi\in{}runs_{\Re'_{P}}(X)$ satisfying the following \ALTL
956: formula:
957: \begin{eqnarray}
958: \textrm{$\varphi:= F(\neg\varphi_{1}) \wedge$
959: $\bigr(\bigwedge_{i\in{}K}\bigvee_{r\in{}\Re^{A}_{P,i}}F(<label(r)>true)\bigr)
960: \wedge$}\nonumber\\
961: \textrm{$\bigr(\bigwedge_{i\notin{}K}\bigwedge_{r\in{}\Re^{A}_{P,i}}G(\neg<label(r)>true)\bigr)$}\nonumber
962: \end{eqnarray}
963: Therefore, property 2 isn't satisfied if, and only if,
964: $\forall\pi\in{}runs_{\Re'_{P}}(X)$
965: $\pi\notin[[\varphi]]_{\Re'_{P}}$, that
966: is if, and only if, $X\models_{\Re'_{P}}\neg\varphi$.\\
967:
968:
969: Now, let us consider the third problem. Starting from $\Re_{P}$,
970: we build a new parallel \PRS $\Re'_{P}$ over the alphabet
971: $\overline{\Sigma}=\{\varepsilon\}\cup{}Var\cup{}\zeta$, as
972: follows. At first, we substitute every rule $r$ in $\Re_{P}$ of
973: the form $t$\Rule{a}$t'$ with the rule
974: $t$\Rule{label(r)}$t'$. $\forall{}Z\in{}Var$ we add the rule
975: $Z\mathop{\rightarrow}\limits^{Z}Z$. Finally, we add the rule
976: $Y$\Rule{\varepsilon}$\varepsilon$. Notice that, by construction,
977: a term $t$ has no successor in $\Re'_{P}$ if, and only if,
978: $t=\varepsilon$. Let us indicate by
979: $\varphi_{1}$ the following \ALTL propositional
980: formula,
981: \begin{displaymath}
982: \bigvee_{Y\in{}Var}\Bigr(<Y>true\Bigr)\vee<\varepsilon>true\vee\bigvee_{l\in\zeta}\Bigr(<l>true\Bigr)
983: \end{displaymath}
984: Moreover, let us indicate by $\varphi_{2}$ the following \ALTL
985: formula,
986: \begin{displaymath}
987: \textrm{$\bigvee_{l\in\zeta}\Bigr(<l>true\Bigr)$ $U$ $(<\varepsilon> \neg\varphi_{1})$}
988: \end{displaymath}
989: This formula is satisfied by runs in $\Re'_{P}$ that end in
990: $\varepsilon$ such that the last label is $\varepsilon$, with each
991: other label
992: in $\zeta$, and the last but one term is $Y$.\\
993: It's easy to deduce that property 3 is satisfied if, and only if,
994: there exists a run $\pi$ in $\Re'_{P}$ with
995: $\pi\in{}runs_{\Re'_{P}}(X)$ satisfying the following \ALTL
996: formula:
997: \begin{eqnarray}
998: \textrm{$\varphi:= \varphi_{2} \wedge$
999: $\bigr(\bigwedge_{i\in{}K}\bigvee_{r\in{}\Re^{A}_{P,i}}F(<label(r)>true)\bigr)
1000: \wedge$}\nonumber\\
1001: \textrm{$\bigr(\bigwedge_{i\notin{}K}\bigwedge_{r\in{}\Re^{A}_{P,i}}G(\neg<label(r)>true)\bigr)$}\nonumber
1002: \end{eqnarray}
1003: Therefore, property 3 isn't satisfied if, and only if,
1004: $\forall\pi\in{}runs_{\Re'_{P}}(X)$
1005: $\pi\notin[[\varphi]]_{\Re'_{P}}$,
1006: that is if, and only if, $X\models_{\Re'_{P}}\neg\varphi$.\\
1007:
1008: Finally, it's easy to prove the decidability of the fourth problem
1009: applying a reasoning similar to previous ones.
1010: \end{proof}
1011:
1012:
1013:
1014: \begin{Proposition}\label{Prop:ParMBRS-Inf} Let us consider two parallel
1015: \MBRSs
1016: $M_{P_{1}}=\npla{\Re_{P},\npla{\Re_{P_{1},1}^{A},\ldots,\Re_{P_{1},n}^{A}}}$ and
1017: $M_{P_{2}}=\npla{\Re_{P},\npla{\Re_{P_{2},1}^{A},\ldots,\Re_{P_{2},n}^{A}}}$ over $Var$ and the alphabet
1018: $\Sigma$, and with the same support $\Re_{P}$. Given a variable $X\in Var$,
1019: two sets $K,K^{\omega}\in{}P_{n}$, and a subset $\Re^{*}_{P}$ of $\Re_{P}$
1020: it's decidable if the following condition is satisfied:
1021: \begin{enumerate}
1022: \item There exists a derivation in $\Re_{P}$ of
1023: the form $\prsdernorm{X}{\sigma}{\Re_{P}}{}$ such that \maximalG{M_{P_{1}}}{\sigma} $=K$
1024: and \maximalGInf{M_{P_{1}}}{\sigma} $\cup$ \maximalG{M_{P_{2}}}{\sigma}
1025: $=K^{\omega}$. Moreover, either $\sigma$ is
1026: infinite or $\sigma$ contains some occurrence of rule in
1027: $\Re_{P}\setminus\Re^{*}_{P}$.
1028: \end{enumerate}
1029: \end{Proposition}
1030:
1031: \begin{proof}
1032: The proof relies on the decidability of the model-checking problem
1033: for \ALTL and
1034: parallel \PRSs (see prop. \ref{prop:parallel-altl}).\\
1035: Let us consider the tuple
1036: $\npla{\overline{\Re}_{P,1}^{A},\ldots,\overline{\Re}_{P,2n+1}^{A}}$
1037: where $\forall{}i=1,\ldots,n$
1038: $\overline{\Re}_{P,i}^{A}=\Re_{P_{1},i}^{A}$ and
1039: $\overline{\Re}_{P,i+n}^{A}=\Re_{P_{2},i}^{A}$, and
1040: $\overline{\Re}_{P,2n+1}^{A}=\Re_{P}\setminus\Re^{*}_{P}$.\\
1041: Let us denote by $S$ the set
1042: $\{(K_{1},K_{2})\in{}P_{n}\times{}P_{n}|$
1043: $K_{1}\cup{}K_{2}=K^{\omega}\}$. \\
1044: Evidently, property 1 is equivalent to the following property:
1045: \begin{enumerate}
1046: \item[2.] There exists a derivation in $\Re_{P}$ of
1047: the form $\prsdernorm{X}{\sigma}{\Re_{P}}{}$ such that
1048: \begin{enumerate}
1049: \item[2.1] $\forall{}i\in{}K$ $\sigma$ contains some occurrence
1050: of rule in $\overline{\Re}_{P,i}^{A}$, and
1051: $\forall{}j\in{}\{1,\ldots,n\}\setminus{}K$ $\sigma$
1052: doesn't contain occurrences of rules in
1053: $\overline{\Re}_{P,j}^{A}$.
1054: \item[2.2] There exists a $(K_{1},K_{2})\in{}S$ such that
1055: $\forall{}i\in{}K_{1}$ (resp., $\forall{}i\in{}K_{2}$)
1056: $\sigma$ contains infinite occurrences
1057: of rules in $\overline{\Re}_{P,i}^{A}$ (resp., contains
1058: some occurrence of rule in $\overline{\Re}_{P,i+n}^{A}$),
1059: and
1060: $\forall{}j\in{}\{1,\ldots,n\}\setminus{}K_{1}$ (resp., $\forall{}j\in{}\{1,\ldots,n\}\setminus{}K_{2}$)
1061: $\sigma$
1062: doesn't contain infinite occurrences of rules in
1063: $\overline{\Re}_{P,j}^{A}$ (resp., doesn't contain occurrences of rules in
1064: $\overline{\Re}_{P,j+n}^{A}$).
1065: \item[2.3] Either $\sigma$ is infinite or $\sigma$ contains
1066: some occurrence of rule in $\overline{\Re}_{P,2n+1}^{A}$.
1067: \end{enumerate}
1068: \end{enumerate}
1069: For all $r\in\Re_{P}$ let us denote by $label(r)$ the set
1070: $\{h\in{}\{1,\ldots,2n+1\}|$ $r\in\overline{\Re}^{A}_{P,h}\}$. Moreover, let us denote
1071: by
1072: $\zeta$ the set $\{label(r)|r\in\Re_{P}\}$. Now, we construct
1073: a new parallel \PRS $\overline{\Re}_{P}$ over the alphabet
1074: $\zeta\cup{}Var$, as follows.
1075: At first, we replace every rule $r$ in
1076: $\Re_{P}$ of the form $t$\Rule{a}$t'$ with the rule
1077: $t$\Rule{label(r)}$t'$. Finally, $\forall{}Y\in{}Var$
1078: we add the rule $Y$\Rule{Y}$Y$. Let us consider the following \ALTL propositional
1079: formula,
1080: \begin{displaymath}
1081: \psi=\bigvee_{l\in\zeta}\Bigr(<l>true\Bigr)
1082: \end{displaymath}
1083: Now, let us consider the following \ALTL formula.
1084: \begin{displaymath}
1085: \textrm{$\varphi_{3}:=GF(\bigvee_{label(r)\in\zeta}<label(r)>true)$
1086: $\vee$ $\bigvee_{r\in\overline{\Re}^{A}_{2n+1}}F\bigr(<label(r)>(FG\neg\psi)\bigr)$}
1087: \end{displaymath}
1088: This formula is satisfied either from infinite runs in
1089: $\overline{\Re}_{P}$ containing infinite occurrences of labels
1090: associated to rules in $\Re_{P}$, or runs containing some
1091: occurrence of a label associated to a rule belonging to
1092: $\Re_{P}\setminus\Re^{*}_{P}$, and containing a finite number of
1093: occurrences of labels related to rules in $\Re_{P}$. So, formula
1094: $\varphi_{3}$ expresses property 2.3.\\
1095: Now, let us consider the following two \ALTL formulae
1096: \begin{displaymath}
1097: \textrm{$\varphi_{1}:=(
1098: \bigwedge_{i\in{}K}\bigvee_{r\in{}\overline{\Re}^{A}_{P,i}}F(<label(r)>true))
1099: \wedge(\bigwedge_{i\in{}\{1,\ldots,n\}\setminus{}K}\bigwedge_{r\in{}\overline{\Re}^{A}_{P,i}}G(\neg<label(r)>true))$}
1100: \footnote{for all $i\in{}K$ if
1101: $\overline{\Re}^{A}_{P,i}=\emptyset$, then
1102: $\bigvee_{r\in{}\overline{\Re}^{A}_{P,i}}F(<label(r)>true)$ denotes $false$}
1103: \end{displaymath}
1104: \begin{displaymath}
1105: \textrm{$\varphi_{2}:=\bigvee_{(K_{1},K_{2})\in{}S}\Bigr((
1106: \bigwedge_{i\in{}K_{1}}\bigvee_{r\in{}\overline{\Re}^{A}_{P,i}}GF(<label(r)>true))\wedge$}
1107: \footnote{for all $i\in{}K_1$ if
1108: $\overline{\Re}^{A}_{P,i}=\emptyset$, then
1109: $\bigvee_{r\in{}\overline{\Re}^{A}_{P,i}}GF(<label(r)>true)$ denotes $false$}
1110: \end{displaymath}
1111: \begin{displaymath}
1112: \textrm{$
1113: (\bigwedge_{i\in{}\{1,\ldots,n\}\setminus{}K_{1}}\bigwedge_{r\in{}\overline{\Re}^{A}_{P,i}}FG(\neg<label(r)>true))\wedge$}
1114: \end{displaymath}
1115: \begin{displaymath}
1116: \textrm{$(
1117: \bigwedge_{i\in{}K_{2}}\bigvee_{r\in{}\overline{\Re}^{A}_{P,i+n}}F(<label(r)>true))
1118: \wedge(\bigwedge_{i\in{}\{1,\ldots,n\}\setminus{}K_{2}}\bigwedge_{r\in{}\overline{\Re}^{A}_{P,i+n}}G(\neg<label(r)>true))\Bigr)$}
1119: \nonumber \footnote{for all $i\in{}K_2$ if
1120: $\overline{\Re}^{A}_{P,i+n}=\emptyset$, then
1121: $\bigvee_{r\in{}\overline{\Re}^{A}_{P,i+n}}F(<label(r)>true)$ denotes $false$}
1122: \end{displaymath}
1123:
1124: Evidently, formula $\varphi_{1}$ (resp., $\varphi_{2}$) expresses
1125: property 2.1 (resp., 2.2). So, property 2 is satisfied
1126: if, and only if, there
1127: exists a run $\pi$ in $\overline{\Re}_{P}$ with
1128: $\pi\in{}runs_{\overline{\Re}_{P}}(X)$ satisfying the following
1129: \ALTL formula:
1130: \begin{displaymath}
1131: \textrm{$\varphi:=\varphi_{1}\wedge\varphi_{2}\wedge\varphi_{3}$}
1132: \end{displaymath}
1133: Therefore, property 2 isn't satisfied if, and only if,
1134: $\forall\pi\in{}runs_{\overline{\Re}_{P}}(X)$
1135: $\pi\notin[[\varphi]]_{\overline{\Re}_{P}}$, that is if, and only
1136: if, $X\models_{\overline{\Re}_{P}}\neg\varphi$.
1137: \end{proof}
1138:
1139: Now, let us give an additional notion of reachability in
1140: sequential \emph{PRSs}.
1141: \begin{Definition} Given a sequential \PRS $\Re_{S}$ over $Var$, and given $X,Y\in{}Var$,
1142: we say that $Y$ is \emph{reachable from} $X$ \emph{in} $\Re_{S}$
1143: whether there exists a term
1144: $t\in{}T\setminus\{\varepsilon\}$ of the form
1145: $X_{1}.(X_{2}.(\ldots{}X_{n}.(Y)\ldots))$ $\mathrm{(}$with $n$
1146: possibly equals to zero$\mathrm{)}$ such that
1147: $\prsdernorm{X}{}{\Re_{S}}{t}$.
1148: \end{Definition}
1149:
1150: \begin{Proposition}\label{Prop:SeqMBRS} Let us consider a sequential \MBRS
1151: $M_{S}=\npla{\Re_{S},\npla{\Re_{S,1}^{A},\ldots,\Re_{S,n}^{A}}}$ over $Var$ and the alphabet
1152: $\Sigma$. Given two variables $X,Y\in Var$ and two sets
1153: $K,K^{\omega}\in{}P_{n}$, it is decidable if
1154: \begin{enumerate}
1155: \item $Y$ is reachable from $X$ in $\Re_{S}$ through a derivation
1156: having finite maximal $K$ as to $M_{S}$.
1157: \item there exists a
1158: $(K,K^{\omega})$-accepting infinite derivation in $M_{S}$ from
1159: $X$.
1160: \end{enumerate}
1161: \end{Proposition}
1162:
1163: \begin{proof}
1164: The proof relies on the decidability of the model-checking problem
1165: for \ALTL and
1166: sequential \PRSs (possibly restricted to infinite runs) (see prop. \ref{prop:sequential-altl}).\\
1167: $\forall{}r\in\Re_{S}$ let us denote by $label(r)$ the set
1168: $\{h\in{}\{1,\ldots,n\}|r\in\Re^{A}_{S,h}\}$. Moreover, let us denote by
1169: $\zeta$ the set $\{label(r)|r\in\Re_{S}\}$.\\
1170: Let us consider the first problem. Starting from $\Re_{S}$ we
1171: build a new sequential \PRS $\Re'_{S}$ over the alphabet
1172: $\overline{\Sigma}=\{Y\}\cup\zeta$, as follows. At first, we
1173: substitute every rule $r$ in $\Re_{S}$ of the form
1174: $t$\Rule{a}$t'$ with the rule $t$\Rule{label(r)}$t'$.
1175: Finally, we add the rule $Y$\Rule{Y}$Y$.\\
1176: Let us indicate by $\varphi_{1}$ the following \ALTL formula,
1177: \begin{displaymath}
1178: \textrm{$F(<Y>true)$ $\bigwedge$
1179: $G\Bigr(\neg(<Y>true)$ $\vee$ $<Y>(G(<Y>true))\Bigr)$}
1180: \end{displaymath}
1181: This formula is satisfied by infinite runs $\pi$ in $\Re'_{S}$
1182: having the form $\pi_{1}\pi_{2}$ where $\pi_{2}$ contains only
1183: occurrences of label $Y$, and $\pi_{1}$ doesn't contain
1184: occurrences of label $Y$.\\
1185: It's easy to deduce that property 1 is satisfied if, and only if,
1186: there exists a run $\pi$ in $\Re'_{S}$ with
1187: $\pi\in{}runs_{\Re'_{S}}(X)$ satisfying the following \ALTL
1188: formula:
1189: \begin{displaymath}
1190: \textrm{$\varphi:= \varphi_{1} \wedge$
1191: $\bigr(\bigwedge_{i\in{}K}\bigvee_{r\in{}\Re^{A}_{S,i}}F(<label(r)>true)\bigr)
1192: \wedge$}\textrm{$\bigr(\bigwedge_{i\notin{}K}\bigwedge_{r\in{}\Re^{A}_{S,i}}G(\neg<label(r)>true)\bigr)$}\nonumber
1193: \footnote{for all $i\in{}K$ if $\Re^{A}_{S,i}=\emptyset$, then
1194: $\bigvee_{r\in{}\Re^{A}_{S,i}}F(<label(r)>true)$ denotes $false$}
1195: \end{displaymath}
1196: Therefore, property 1 isn't satisfied if, and only if,
1197: $\forall\pi\in{}runs_{\Re'_{S}}(X)$
1198: $\pi\notin[[\varphi]]_{\Re'_{S}}$, that is if, and only if,
1199: $X\models_{\Re'_{S}}\neg\varphi$.\\
1200:
1201: \noindent{}Now, let us consider the second problem. We construct a
1202: new sequential \PRS
1203: $\Re'_{S}$ over the alphabet $\zeta$ in the following way. We substitute every rule $r$ in
1204: $\Re_{S}$ of the form $t$\Rule{a}$t'$ with the rule
1205: $t$\Rule{label(r)}$t'$. \\
1206: It's easy to deduce that property 2 is satisfied if, and only if,
1207: there exists an infinite run $\pi$ in $\Re'_{S}$ with
1208: $\pi\in{}runs_{\Re'_{S},\infty}(X)$ satisfying the following \ALTL
1209: formula:
1210: \begin{displaymath}
1211: \textrm{$\varphi:=(
1212: \bigwedge_{i\in{}K^{\omega}}\bigvee_{r\in{}\Re^{A}_{S,i}}GF(<label(r)>true))
1213: \wedge(\bigwedge_{i\notin{}K^{\omega}}\bigwedge_{r\in{}\Re^{A}_{S,i}}FG(\neg<label(r)>true))\wedge$}
1214: \footnote{for all $i\in{}K^{\omega}$ if $\Re^{A}_{S,i}=\emptyset$,
1215: then
1216: $\bigvee_{r\in{}\Re^{A}_{S,i}}GF(<label(r)>true)$ denotes $false$}
1217: \end{displaymath}
1218: \begin{displaymath}
1219: \textrm{$(
1220: \bigwedge_{i\in{}K}\bigvee_{r\in{}\Re^{A}_{S,i}}F(<label(r)>true))
1221: \wedge(\bigwedge_{i\notin{}K}\bigwedge_{r\in{}\Re^{A}_{S,i}}G(\neg<label(r)>true))$}\nonumber
1222: \footnote{for all $i\in{}K$ if $\Re^{A}_{S,i}=\emptyset$, then
1223: $\bigvee_{r\in{}\Re^{A}_{S,i}}F(<label(r)>true)$ denotes $false$}
1224: \end{displaymath}
1225:
1226: Therefore, property 1 isn't satisfied if, and only if,
1227: $\forall\pi\in{}runs_{\Re'_{S},\infty}(X)$
1228: $\pi\notin[[\varphi]]_{\Re'_{S}}$, that is if, and only if,
1229: $X\models_{\Re'_{S},\infty}\neg\varphi$.
1230: \end{proof}
1231:
1232:
1233:
1234:
1235:
1236: \begin{Theorem}\label{Theorem:ConditionForProblem2-1} Let us consider two parallel
1237: \MBRSs
1238: $M_{P_{1}}=\npla{\Re_{P},\npla{\Re_{P_{1},1}^{A},\ldots,\Re_{P_{1},n}^{A}}}$ and
1239: $M_{P_{2}}=\npla{\Re_{P},\npla{\Re_{P_{2},1}^{A},\ldots,\Re_{P_{2},n}^{A}}}$
1240: with the same support $\Re_{P}$, and a sequential \MBRS
1241: $M_{S}=\npla{\Re_{S},\npla{\Re_{S,1}^{A},\ldots,\Re_{S,n}^{A}}}$. Given a variable $X\in Var$,
1242: two sets $K,K^{\omega}\in{}P_{n}$, and a subset $\Re^{*}_{P}$ of $\Re_{P}$
1243: it's decidable if the following condition is satisfied:
1244: \begin{enumerate}
1245: \item There exists a variable $Y$ reachable from $X$ in
1246: $\Re_{S}$ through a $(K',\emptyset)$-accepting derivation in $M_{S}$
1247: with $K'\subseteq{}K$, and there exists a derivation
1248: $\prsdernorm{Y}{\rho}{\Re_{P}}{}$
1249: such that \maximalG{M_{P_{1}}}{\rho} = $K$
1250: and
1251: \maximalG{M_{P_{2}}}{\rho} $\cup$ \maximalGInf{M_{P_{1}}}{\rho} =
1252: $K^{\omega}$. Moreover, either $\rho$ is
1253: infinite or $\rho$ contains some occurrence of rule in
1254: $\Re_{P}\setminus\Re_{P}^{*}$.
1255: \end{enumerate}
1256: \end{Theorem}
1257: \begin{proof}
1258: Since the sets $\{K'\in{}P_{n}|K'\subseteq{}K\}$ and $Var$ are
1259: finite, the result follows directly from propositions
1260: \ref{Prop:ParMBRS-Inf} and \ref{Prop:SeqMBRS}.
1261: \end{proof}
1262:
1263:
1264:
1265: \begin{Theorem}\label{Theorem:ConditionForProblem2-2} Let us consider two parallel
1266: \MBRSs
1267: $M_{P_{1}}=\npla{\Re_{P},\npla{\Re_{P_{1},1}^{A},\ldots,\Re_{P_{1},n}^{A}}}$ and
1268: $M_{P_{2}}=\npla{\Re_{P},\npla{\Re_{P_{2},1}^{A},\ldots,\Re_{P_{2},n}^{A}}}$
1269: with the same support $\Re_{P}$, and a sequential \MBRS
1270: $M_{S}=\npla{\Re_{S},\npla{\Re_{S,1}^{A},\ldots,\Re_{S,n}^{A}}}$. Given a variable $X\in Var$,
1271: two sets $K,K^{\omega}\in{}P_{n}$, and a subset $\Re^{*}_{P}$ of $\Re_{P}$
1272: it's decidable if one of the following conditions is satisfied:
1273: \begin{enumerate}
1274: \item There exists a variable $Y$ reachable from $X$ in
1275: $\Re_{S}$ through a $(K',\emptyset)$-accepting derivation in $M_{S}$
1276: with $K'\subseteq{}K$, and there exists a derivation
1277: $\prsdernorm{Y}{\rho}{\Re_{P}}{}$
1278: such that \maximalG{M_{P_{1}}}{\rho} = $K$
1279: and
1280: \maximalG{M_{P_{2}}}{\rho} $\cup$ \maximalGInf{M_{P_{1}}}{\rho} =
1281: $K^{\omega}$. Moreover, either $\rho$ is
1282: infinite or $\rho$ contains some occurrence of rule in
1283: $\Re_{P}\setminus\Re_{P}^{*}$.
1284: \item There exists a
1285: $(K,K^{\omega})$-accepting infinite derivation in $M_{S}$ from
1286: $X$.
1287: \end{enumerate}
1288: \end{Theorem}
1289: \begin{proof}
1290: Since the sets $\{K'\in{}P_{n}|K'\subseteq{}K\}$ and $Var$ are
1291: finite, the result follows directly from propositions
1292: \ref{Prop:ParMBRS-Inf} and \ref{Prop:SeqMBRS}.
1293: \end{proof}
1294:
1295:
1296: \subsection{Decidability results on finite derivations of \MBRSs in normal form}\label{sec:finite}
1297:
1298: In this section we prove the decidability of Problem 1 stated in
1299: subsection~\ref{sec:Model-checkingPRS}, that for clarity we
1300: recall.
1301: \begin{description}
1302: \item[Problem 1]\emph{ Given a \MBRS in normal form
1303: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ over Var and
1304: the alphabet $\Sigma$, given a variable $X\in{}Var$ and a set
1305: $K\in{}P_{n}$, to decide if there exists a $(K,\emptyset)$-accepting finite derivation in $M$
1306: from $X$}.
1307: \end{description}
1308:
1309: We show that problem 1, with input a set $K\in{}P_{n}$, can be
1310: reduced to a similar, but simpler, problem, that is a
1311: decidability problem on finite derivations restricted to parallel
1312: \MBRSs. In particular, we show that it is possible to construct
1313: effectively a parallel \MBRS
1314: $M^{K}_{PAR}=\npla{\Re^{K}_{PAR},\npla{\Re^{K,A}_{PAR,1},\ldots,\Re_{PAR,n}^{K,A}}}$
1315: in such a way that Pro\-blem 1, with input the set $K$ and a
1316: variable $X$, is reducible to the problem of deciding if the
1317: following condition is satisfied:
1318: \begin{itemize}
1319: \item There exists a $(K,\emptyset)$-accepting finite
1320: derivation in $M^{K}_{PAR}$ from
1321: $X$.
1322: \end{itemize}
1323: Since this last problem is decidable (see proposition
1324: \ref{Prop:ParMBRS-F}), decidability of Problem 1 is entailed.
1325:
1326:
1327: Before illustrating the main idea underlying our approach, we need
1328: few additional definitions and notations, which allows us to look
1329: more in detail at the structure of derivations in \MBRSs in normal
1330: form. The following definition introduces the notion of level of
1331: application of a rule in a derivation:
1332:
1333: \begin{Definition}
1334: Let $t$ \prsoneder{r} $t'$ be a single--step derivation in $\Re$.
1335: We say that $r$ is \emph{applicable at level 0} in
1336: $t$ \prsoneder{r} $t'$, if $t = \overline{t}$$\parallel$$s$,
1337: $t' = \overline{t}$$\parallel$$s'$ $\mathrm{(}$for some $\overline{t}, s, s'\in
1338: T$$\mathbb{)}$, and $r = s$\Rule{a}$s'$, for some $a\in\Sigma$.
1339:
1340: We say that $r$ is \emph{applicable at level $k > 0$ in}
1341: $t$ \prsoneder{r} $t'$, if $t = \overline{t}$$\parallel$$X.(s)$,
1342: $t' = \overline{t}$$\parallel$$X.(s')$ $\mathrm{(}$for some
1343: $\overline{t}, s,s'\in T$$\mathbb{)}$, $s$ \prsoneder{r} $s'$, and
1344: $r$ is applicable at level $k-1$ in $s$ \prsoneder{r} $s'$.
1345:
1346: The \emph{level of application} of $r$ in $t$ \prsoneder{r}
1347: $t'$ is the greatest level of applicability of $r$ in $t$ \prsoneder{r}
1348: $t'$.
1349: \end{Definition}
1350:
1351: The definition above extends in the obvious way to $n$--step
1352: derivations and to infinite derivations. The next definition
1353: introduces the notion of subderivation starting from a term.
1354:
1355: \begin{Definition}[Subderivation]
1356: Let $\overline{t}$ \multider{\lambda}
1357: $t$$\parallel$$X.(s)$ \multider{\sigma} be a finite or infinite
1358: derivation in $\Re$ starting from $\overline{t}$. The set of the
1359: \emph{subderivations $d'=s$ \multider{\mu} of
1360: $d=t$$\parallel$$X.(s)$ \multider{\sigma} from $s$} is inductively
1361: defined as follows:
1362:
1363: \begin{enumerate}
1364: \item if $d$ is a null derivation or $s = \varepsilon$, then $d'$
1365: is
1366: the null derivation from $s$;
1367: \item if $\sigma = r\sigma'$, and $d$ is of the form
1368: \begin{displaymath}
1369: \textrm{
1370: $t$$\parallel$$X.(Z)$ \prsoneder{r} $t$$\parallel$$Y$
1371: \multider{\sigma'} $\quad\mathrm{(}$with $r =X.(Z)$\Rule{a}$Y$ and $s=Z\in{}Var$$\mathrm{)}$}
1372: \end{displaymath}
1373: \noindent then $d'$ is the null derivation from $s$; \item if
1374: $\sigma = r\sigma'$, and $d$ is of the form
1375: \begin{displaymath}
1376: \textrm{
1377: $t$$\parallel$$X.(s)$ \prsoneder{r} $t$$\parallel$$X.(s')$
1378: \multider{\sigma'} $\quad\mathrm{(}$with $s$ \prsoneder{r} $s'$$\mathrm{)}$}
1379: \end{displaymath}
1380: \noindent then $d' = s$ \prsoneder{r} $s'$ \multider{\mu'}, where
1381: $s'$ \multider{\mu'} is a subderivation of $t$$\parallel$$X.(s')$
1382: \multider{\sigma'} from $s'$;
1383: \item if
1384: $\sigma = r\sigma'$, and $d$ is of the form
1385: \begin{displaymath}
1386: \textrm{
1387: $t$$\parallel$$X.(s)$ \prsoneder{r} $t'$$\parallel$$X.(s)$
1388: \multider{\sigma'} $\quad\mathrm{(}$with $t$ \prsoneder{r} $t'$$\mathrm{)}$}
1389: \end{displaymath}
1390: \noindent then $d'$ is a subderivation of $t'$$\parallel$$X.(s)$
1391: \multider{\sigma'} from $s$;
1392: \end{enumerate}
1393: Moreover, we say that $d'$ is a subderivation of $\overline{t}$
1394: \multider{\lambda}
1395: $t$$\parallel$$X.(s)$ \multider{\sigma}.
1396: \end{Definition}
1397:
1398:
1399: Clearly, in the definition above $\mu$ is a subsequence of
1400: $\sigma$. Moreover, if $k$ is the level of application of a rule
1401: occurrence of $\mu$ in the derivation $d$ then, $k>0$, and the
1402: level of application of this occurrence in the subderivation
1403: $d'=s$ \multider{\mu} is $k'$ with $k'<k$.
1404:
1405: Given a sequence $\sigma=r_{1}r_{2} \ldots{}r_{n} \ldots{}$ of
1406: rules in $\Re$, and a subsequence $\sigma'=r_{k_{1}}r_{k_{2}}
1407: \ldots{} r_{k_{m}} \ldots{}$ of $\sigma$, $\sigma\setminus
1408: \sigma{}'$ denotes the sequence obtained by removing from $\sigma$
1409: all and only the occurrences of rules in $\sigma'$ (namely, those
1410: $r_{i}$ for which there exists a $j=1,\ldots,|\sigma'|$ such that
1411: $k_{j}=i$).\newline
1412:
1413: In the following,
1414: $M_{P}=\npla{\Re_{P},\npla{\Re_{P,1}^{A},\ldots,\Re_{P,n}^{A}}}$
1415: denotes the restriction of $M$ to PAR rules, that is $\Re_{P}$
1416: (resp., $\Re_{P,i}^{A}$ for $i=1,\ldots,n$) is the set $\Re$
1417: (resp., $\Re_{i}^{A}$ for $i=1,\ldots,n$) restricted to the PAR
1418: rules.\\
1419:
1420: \setcounter{equation}{0} Let us sketch the main ideas at the basis
1421: of our technique. We show how it is possible to mimic a
1422: $(K,\emptyset)$-accepting finite derivation in $M$ from a variable
1423: by using only PAR rules belonging to an extension of the parallel
1424: \MBRS $M_{P}$, denoted by
1425: $M^{K}_{PAR}=\npla{\Re^{K}_{PAR},\npla{\Re^{K,A}_{PAR,1},\ldots,\Re_{PAR,n}^{K,A}}}$.
1426: More precisely, we show that
1427: \begin{description}
1428: \item[i.] if $p$ \multider{\sigma} (with
1429: $p\in{}T_{PAR}$) is a $(\overline{K},\emptyset)$-accepting finite
1430: derivation in $M$ with $\overline{K}\subseteq{}K$ then, there
1431: exists a $(\overline{K},\emptyset)$-accepting finite derivation in
1432: $M^{K}_{PAR}$
1433: from $p$, and vice versa.
1434: \end{description}
1435: So, let $p$ \multider{\sigma} be a
1436: $(\overline{K},\emptyset)$-accepting finite derivation in $M$ with
1437: $p\in{}T_{PAR}$ and $\overline{K}\subseteq{}K$. Then, all its
1438: possible subderivations contain all, and only, the rule
1439: occurrences in $\sigma$ applied at a level $k$ greater than $0$ in
1440: $p$ \multider{\sigma}. If $\sigma$ contains only PAR rule
1441: occurrences the statement \textbf{i} is evident, since
1442: $M^{K}_{PAR}$ is an extension of $M_{P}$. Otherwise, $p$
1443: \multider{\sigma} can be written in the form:
1444: \begin{equation}\label{eq:derivation}
1445: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
1446: $t$$\parallel$$Y.(Z)$ \multider{\omega}}
1447: \end{equation}
1448: where $r = X$\Rule{a}$Y.(Z)$, $\lambda$ contains only occurrences of rules
1449: in $\Re_{P}$, $t\in{}T_{PAR}$ and $X,Y,Z\in{}Var$. Let $Z$ \multider{\rho} be a subderivation of
1450: $t$$\parallel$$Y.(Z)$ \multider{\omega} from $Z$. Evidently, \maximal{\rho} $\subseteq{}K$. Moreover,
1451: only one of the following three cases may occur:
1452: \begin{description}
1453: \item[A] $Z$ \multider{\rho} leads to the term $\varepsilon$, and
1454: $p$ \multider{\sigma} is of the form
1455: \begin{equation}\label{eq:form1}
1456: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
1457: $t$$\parallel$$Y.(Z)$ \multider{\omega_{1}} $\overline{t}$$\parallel$$Y$ \multider{\omega_{2}}}
1458: \end{equation}
1459: where $\rho$ is a subsequence of $\omega_1$ and $t$
1460: \multider{\omega_{1}\setminus\rho} $\overline{t}$. The finite derivation above is
1461: $(\overline{K},\emptyset)$-accepting if, and only if, the following finite derivation,
1462: obtained by anticipating (by interleaving) the application of the
1463: rules in $\rho$ before the application of the rules in $\xi=
1464: \omega_1\setminus\rho$, is $(\overline{K},\emptyset)$-accepting
1465: \begin{equation}\label{eq:form1-2}
1466: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
1467: $t$$\parallel$$Y.(Z)$ \multider{\rho} $t$$\parallel$$Y$ \multider{\xi}
1468: $\overline{t}$$\parallel$$Y$ \multider{\omega_{2}}}
1469: \end{equation}
1470: Let \maximal{r\rho} =
1471: $K'\subseteq{}K$. The idea is to collapse the derivation $X$ \prsoneder{r}
1472: $Y.(Z)$ \multider{\rho} $Y$ into a
1473: single PAR rule of the form $r'=X$\Rule{K'}$Y$,
1474: where \maximalparK{r'} = $K'$ = \maximal{r\rho}.\\
1475: Notice that in the step from (2) to (3),
1476: we exploit the fact that the property on finite derivations we
1477: are interested in is insensitive to permutations
1478: of rule applications within a derivation.
1479: Now, we can apply recursively the same reasoning to the finite
1480: derivation in $\Re$ from $t$$\parallel$$Y\in{}T_{PAR}$
1481: \begin{equation}
1482: \textrm{$t$$\parallel$$Y$ \multider{\xi} $\overline{t}$$\parallel$$Y$
1483: \multider{\omega_{2}}}
1484: \end{equation}
1485: whose finite maximal as to $M$ is
1486: contained in $K$.
1487: \item[B] $Z$ \multider{\rho} leads to a variable $W$, and
1488: $p$ \multider{\sigma} can be written as
1489: \begin{equation}\label{eq:form1}
1490: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
1491: $t$$\parallel$$Y.(Z)$ \multider{\omega_{1}} $\overline{t}$$\parallel$$Y.(W)$
1492: \prsoneder{r'} $\overline{t}$$\parallel$$W'$ \multider{\omega_{2}}}
1493: \end{equation}
1494: where $r'=Y.(W)$\Rule{b}$W'$ (with $W'\in{}Var$),
1495: $\rho$ is a subsequence of $\omega_1$ and $t$
1496: \multider{\omega_{1}\setminus\rho} $\overline{t}$. The finite derivation above is
1497: $(\overline{K},\emptyset)$-accepting if, and only if, the following finite derivation
1498: is $(\overline{K},\emptyset)$-accepting
1499: \begin{equation}\label{eq:form1-2}
1500: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
1501: $t$$\parallel$$Y.(Z)$ \multider{\rho} $t$$\parallel$$Y.(W)$ \prsoneder{r'} $t$$\parallel$$W'$
1502: \multider{\xi}
1503: $\overline{t}$$\parallel$$W'$ \multider{\omega_{2}}}
1504: \end{equation}
1505: where $\xi=\omega_{1}\setminus\rho$.
1506: Let \maximal{rr'\rho} =
1507: $K'\subseteq{}K$. The idea is to collapse the derivation $X$ \prsoneder{r}
1508: $Y.(Z)$ \multider{\rho} $Y.(W)$ \prsoneder{r'} $W'$ into a
1509: single PAR rule of the form $r''=X$\Rule{K'}$W'$,
1510: where \maximalparK{r''} = $K'$ = \maximal{rr'\rho}.\\
1511: Now, we can apply recursively the same reasoning to the finite
1512: derivation in $\Re$ from $t$$\parallel$$W'\in{}T_{PAR}$
1513: \begin{equation}
1514: \textrm{$t$$\parallel$$W'$ \multider{\xi} $\overline{t}$$\parallel$$W'$
1515: \multider{\omega_{2}}}
1516: \end{equation}
1517: whose finite maximal as to $M$ is
1518: contained in $K$.
1519: \item[C] In this case $Z$ \multider{\rho} does not influence the
1520: applicability of rules in $\omega \setminus \rho$ in the derivation
1521: $t$$\parallel$$Y.(Z)$ \multider{\omega}
1522: (i.e. the rule occurrences in $\rho$ can be arbitrarily
1523: interleaved with any rule occurrence in $\omega\setminus\rho$). In other
1524: words, we have $t$ \multider{\omega\setminus\rho}. Moreover,
1525: \maximal{r\rho} $=K'$ with $K'\subseteq{}K$.
1526: Then, we keep track of the sequence $r\rho$
1527: by adding a new variable $\hat{Z}_{F}$ (where $\hat{Z}_{F}\notin{}Var$) and
1528: a PAR rule of the form $r'=X$\Rule{K'}$\hat{Z}_{F}$, where
1529: \maximalparK{r'} = $K'$ = \maximal{r\rho}.
1530: Now, we can apply recursively the same reasoning to the finite
1531: derivation $t$$\parallel$$\hat{Z}_{F}$ \multider{\omega\setminus\rho} in $\Re$ from
1532: the parallel term $t$$\parallel$$\hat{Z}_{F}$,
1533: whose finite maximal as to $M$ is
1534: contained in $K$.
1535: \end{description}
1536:
1537: The parallel \MBRS
1538: $M^{K}_{PAR}=\npla{\Re^{K}_{PAR},\npla{\Re^{K,A}_{PAR,1},\ldots,\Re_{PAR,n}^{K,A}}}$
1539: is defined as follows.
1540:
1541: \begin{Definition}\label{def:MPAR-K}
1542: The \MBRS $M^{K}_{PAR}=\npla{\Re^{K}_{PAR},\npla{\Re^{K,A}_{PAR,1},\ldots,\Re_{PAR,n}^{K,A}}}$
1543: is
1544: the least parallel \MBRS with $n$ accepting components, over $Var\cup\{\hat{Z}_{F}\}$ and the alphabet $\overline{\Sigma} = \Sigma
1545: \cup{}P_{n}$\footnote{let us assume that $\Sigma\cap{}P_{n}=\emptyset$}, satisfying the following properties:
1546: \begin{enumerate}
1547: \item $\Re^{K}_{PAR}\supseteq\{r\in\Re|\textrm{$r$ is a PAR rule}\}$
1548: and $\forall{}i=1,\ldots,n$
1549: $\Re^{K,A}_{PAR,i}\supseteq\{r\in\Re_{i}^{A}|\textrm{ $r$ is }$ a PAR rule\}
1550: \item Let $r=X$\Rule{a}$Y.(Z)\in{}\Re$ and
1551: $Z$ \multiderparK{\sigma} $p$ for some term $p$, with \maximal{r} $=K_{1}\subseteq{}K$
1552: and \maximalparK{\sigma} $=K_{2}\subseteq{}K$. Denoted by $K'$
1553: the set $K_{1}\cup{}K_{2}$, then we have
1554: $r'=X$\Rule{K'}$\hat{Z}_{F}\in{}\Re^{K}_{PAR}$ and
1555: \maximalparK{r'} $=K'$.
1556: \item Let $r=X$\Rule{a}$Y.(Z)\in{}\Re$ and
1557: $Z$ \multiderparK{\sigma} $\varepsilon$ with \maximal{r} $=K_{1}\subseteq{}K$
1558: and \maximalparK{\sigma} $=K_{2}\subseteq{}K$. Denoted by $K'$
1559: the set $K_{1}\cup{}K_{2}$, then we have
1560: $r'=X$\Rule{K'}$Y\in{}\Re^{K}_{PAR}$ and
1561: \maximalparK{r'} $=K'$.
1562: \item Let $r=X$\Rule{a}$Y.(Z)\in{}\Re$, $r'=Y.(W)$\Rule{b}$W'\in{}\Re$
1563: and $Z$ \multiderparK{\sigma} $W$ with \maximal{r} $=K_{1}\subseteq{}K$,
1564: \maximal{r'} $=K_{2}\subseteq{}K$
1565: and \maximalparK{\sigma} $=K_{3}\subseteq{}K$. Denoted by $K'$
1566: the set $K_{1}\cup{}K_{2}\cup{}K_{3}$, then we have
1567: $r''=X$\Rule{K'}$W'\in{}\Re^{K}_{PAR}$ and
1568: \maximalparK{r''} $=K'$.
1569: \item If $r=X$\Rule{K'}$Y\in{}\Re^{K}_{PAR}\setminus\Re$
1570: then, $X$ \multider{\sigma} $t$ for some term $t$, with $|\sigma|>0$ and
1571: \maximal{\sigma} $=K'$. Moreover, if $Y\in{}Var$ then
1572: $t=Y$.
1573: \end{enumerate}
1574: \end{Definition}
1575:
1576: \setcounter{equation}{0}
1577: \begin{Lemma}\label{Lemma:Algo}
1578: The parallel \MBRS
1579: $M^{K}_{PAR}=\npla{\Re^{K}_{PAR},\npla{\Re^{K,A}_{PAR,1},\ldots,\Re_{PAR,n}^{K,A}}}$
1580: can be effectively constructed.
1581: \end{Lemma}
1582: \begin{proof}
1583: Figure \ref{fig:algo} reports the procedure
1584: BUILD-PARALLEL-MBRS($M$,$K$), which, starting from \MBRS $M$ (in
1585: normal form) and a set $K\in{}P_{n}$, builds a parallel \MBRS
1586: $M_{P}=\npla{\Re_{P},\npla{\Re_{P,1}^{A},\ldots,\Re_{P,n}^{A}}}$.
1587: >From proposition \ref{Prop:ParMBRS-F}, the conditions in each of
1588: the \textbf{if} statements in lines 9, 16 and 27 are decidable,
1589: therefore, the procedure is effective.\\
1590: Now, let us show that the algorithm terminates. It suffices to
1591: prove that the number of iterations of the \textbf{repeat} loop is
1592: finite. The termination condition of this loop is \emph{flag} =
1593: \emph{false}. On the other hand, at the beginning of every
1594: iteration the
1595: \emph{flag} is set to \emph{false}, and can be reset to \emph{true}
1596: when a rule of the form
1597: $X$\Rule{K'}$Y$ (with $X\in{}Var$, $Y\in{}Var\cup\{\hat{Z}_{F}\}$
1598: and $K'\in{}P_{n}$) not
1599: belonging to $\Re_{P}$ is added to $\Re_{P}$
1600: (lines 11--15, 18--22 and 29--33). Since the set of rules
1601: of the form $X$\Rule{K'}$Y$ with $X\in{}Var$,
1602: $Y\in{}Var\cup\{\hat{Z}_{F}\}$ and $K'\in{}P_{n}$
1603: is finite, termination immediately follows.\\
1604:
1605: \begin{figure}[htbp]
1606: \ \\\noindent \textbf{Algorithm}
1607: B{\small{}UILD}--{\small{}PARALLEL}--MBRS($M$,$K$)\vspace{4pt}
1608: \\\small
1609: 1 $\Re_{P}:=\{r\in\Re|$ \emph{$r$ is a PAR rule}\};\\
1610: 2 \textbf{for} $i=1,\ldots,n$ \textbf{do}\\
1611: 3 $\quad\quad\Re_{P,i}^{A}:=\{r\in\Re_{i}^{A}|$ \emph{$r$ is a PAR rule}\};\\
1612: 4 \textbf{repeat}\\
1613: 5 $\quad\quad{}$\emph{flag:=false;}\\
1614: 6 $\quad\quad{}$\textbf{for each} $r=X$\Rule{a}$Y.(Z)\in\Re$ \emph{such that} \maximal{r} $\subseteq{}K$ \textbf{do}\\
1615: 7 $\quad\quad\quad\quad{}$\emph{Set} $K_{1}=$ \maximal{r}\\
1616: 8 $\quad\quad\quad\quad{}$\textbf{for each} $K_{2}\subseteq{}K$ \textbf{do}\\
1617: 9 $\quad\quad\quad\quad\quad\quad{}$\textbf{if}
1618: $\prsdernorm{Z}{\sigma}{\Re_{P}}{p}$ for some $p$
1619: \emph{such that} \maximalG{M_{P}}{\sigma} $=K_{2}$ \textbf{then}\\
1620: 10 $\quad\quad\quad\quad\quad\quad\quad\quad{}$\emph{Set}
1621: $K'=K_{1}\cup{}K_{2}=\{i_{1},\ldots,i_{|K'|}\}$;\\
1622: 11 $\quad\quad\quad\quad\quad\quad\quad\quad{}$\textbf{if}
1623: $X$\Rule{K'}$\hat{Z}_{F}\notin{}\Re_{P}$ \textbf{then}\\
1624: 12
1625: $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}\Re_{P}:=\Re_{P}\cup\{X$\Rule{K'}$\hat{Z}_{F}\};$\\
1626: 13 $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}$\textbf{for} $j=1,\ldots,|K'|$ \textbf{do}\\
1627: 14
1628: $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}\Re_{P,i_{j}}^{A}:=\Re_{P,i_{j}}^{A}\cup\{X$\Rule{K'}$\hat{Z}_{F}\};$\\
1629: 15 $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}$\emph{flag:=true;}\\
1630: 16 $\quad\quad\quad\quad\quad\quad{}$\textbf{if}
1631: $\prsdernorm{Z}{\sigma}{\Re_{P}}{\varepsilon}$
1632: \emph{such that} \maximalG{M_{P}}{\sigma} $=K_{2}$ \textbf{then}\\
1633: 17 $\quad\quad\quad\quad\quad\quad\quad\quad{}$\emph{Set}
1634: $K'=K_{1}\cup{}K_{2}=\{i_{1},\ldots,i_{|K'|}\}$;\\
1635: 18 $\quad\quad\quad\quad\quad\quad\quad\quad{}$\textbf{if}
1636: $X$\Rule{K'}$Y\notin{}\Re_{P}$ \textbf{then}\\
1637: 19
1638: $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}\Re_{P}:=\Re_{P}\cup\{X$\Rule{K'}$Y\};$\\
1639: 20 $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}$\textbf{for} $j=1,\ldots,|K'|$ \textbf{do}\\
1640: 21
1641: $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}\Re_{P,i_{j}}^{A}:=\Re_{P,i_{j}}^{A}\cup\{X$\Rule{K'}$Y\};$\\
1642: 22 $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}$\emph{flag:=true;}\\
1643: 23 $\quad\quad\quad\quad{}$\textbf{done} $\rhd$ for\\
1644: 24 $\quad\quad\quad\quad{}$\textbf{for each} $r'=Y.(W)$\Rule{b}$W'\in\Re$ \emph{such that} \maximal{r'} $\subseteq{}K$\textbf{do}\\
1645: 25 $\quad\quad\quad\quad\quad\quad{}$\emph{Set} $K_{2}=$ \maximal{r'}\\
1646: 26 $\quad\quad\quad\quad\quad\quad{}$\textbf{for each} $K_{3}\subseteq{}K$ \textbf{do}\\
1647: 27 $\quad\quad\quad\quad\quad\quad\quad\quad{}$\textbf{if}
1648: $\prsdernorm{Z}{\sigma}{\Re_{P}}{W}$
1649: \emph{such that} \maximalG{M_{P}}{\sigma} $=K_{3}$ \textbf{then}\\
1650: 28
1651: $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}$\emph{Set}
1652: $K'=K_{1}\cup{}K_{2}\cup{}K_{3}=\{i_{1},\ldots,i_{|K'|}\}$;\\
1653: 29
1654: $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}$\textbf{if}
1655: $X$\Rule{K'}$W'\notin{}\Re_{P}$ \textbf{then}\\
1656: 30
1657: $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}\Re_{P}:=\Re_{P}\cup\{X$\Rule{K'}$W'\};$\\
1658: 31 $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}$\textbf{for} $j=1,\ldots,|K'|$ \textbf{do}\\
1659: 32
1660: $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}\Re_{P,i_{j}}^{A}:=\Re_{P,i_{j}}^{A}\cup\{X$\Rule{K'}$W'\};$\\
1661: 33 $\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{}$\emph{flag:=true;}\\
1662: 34 $\quad\quad\quad\quad\quad\quad{}$\textbf{done} $\rhd$ for\\
1663: 35 $\quad\quad\quad\quad{}$\textbf{done} $\rhd$ for\\
1664: 36 $\quad\quad{}$\textbf{done} $\rhd$ for\\
1665: 37 \textbf{until} \emph{flag = false} \\
1666: \caption{Algorithm to turn a \MBRS into a parallel
1667: \MBRS.}\label{fig:algo}
1668: \end{figure}
1669:
1670: Now, let us denote by $\Re^{K}_{PAR}$, (resp., $\Re^{K,A}_{PAR,i}$
1671: for $i=1,\ldots,n$) the set $\Re_{P}$ (resp., $\Re_{P,i}^{A}$ for
1672: $i=1,\ldots,n$) at termination of the algorithm. Let $M^{K}_{PAR}$
1673: the parallel \MBRS
1674: $\npla{\Re^{K}_{PAR},\npla{\Re^{K,A}_{PAR,1},\ldots,\Re_{PAR,n}^{K,A}}}$.
1675: Since a new rule is
1676: added to $\Re_{P}$ only once, it follows that the following
1677: property holds:
1678: \begin{description}
1679: \item[a.] Each rule $r$ in
1680: $\Re^{K}_{PAR}\setminus\{r\in\Re|\textrm{$r$ is a PAR rule}\}$ has
1681: the form $X$\Rule{K'}$Y$, with $X\in{}Var$,
1682: $Y\in{}Var\cup\{\hat{Z}_{F}\}$ and
1683: $K'\in{}P_{n}$. Moreover, \maximalparK{r} $=K'$.
1684: \end{description}
1685: Now, let us show that $M^{K}_{PAR}$ satisfies properties 1-5 of
1686: definition \ref{def:MPAR-K}. Evidently, property 1 is
1687: satisfied.\\
1688: Let us prove property 2. Let $r=X$\Rule{a}$Y.(Z)\in{}\Re$ and $Z$
1689: \multiderparK{\sigma} $p$ for some term $p$, with \maximal{r}
1690: $=K_{1}\subseteq{}K$ and \maximalparK{\sigma}
1691: $=K_{2}\subseteq{}K$. Denoted by $K'$ the set $K_{1}\cup{}K_{2}$,
1692: then we have to prove that
1693: $r'=X$\Rule{K'}$\hat{Z}_{F}\in{}\Re^{K}_{PAR}$, and
1694: \maximalparK{r'} $=K'$. From property \textbf{a} (notice that
1695: $r'\notin\Re$) it suffices to prove that $r'$ is added to
1696: $\Re_{P}$ during the computation. Let us consider the last
1697: iteration of the \textbf{repeat} loop. Since any update of the
1698: sets $\Re_{P}$,$\Re_{P,1}^{A},\ldots,\Re_{P,n}^{A}$ (the
1699: \emph{flag} is set to $true$) involves a new iteration of this
1700: loop, we deduce that in this computation phase
1701: \begin{equation}
1702: \textrm{$\Re_{P}=\Re^{K}_{PAR}$ and
1703: $\forall{}i=1,\ldots,n$ $\Re_{P,i}^{A}=\Re^{K,A}_{PAR,i}$}
1704: \end{equation}
1705: and they will not be updated anymore. Now, the rule
1706: $r=X$\Rule{a}$Y.(Z)$ will be examined during an iteration of the
1707: \textbf{for} loop in lines 6--36. From (1) it follows that during
1708: the inner \textbf{for} loop (lines 8--23) iteration associated to
1709: $K_{2}$, the condition of the \textbf{if} statement in line 9 is
1710: satisfied.
1711: Since $\Re_{P}$ cannot be updated anymore, we deduce that the
1712: condition of the \textbf{if} statement in line 11 cannot be
1713: satisfied. Therefore, $X$\Rule{K'}$\hat{Z}_{F}\in\Re_{P}$,
1714: and the assertion is proved.\\
1715: Following a similar reasoning we can easily prove that also
1716: properties 3 and 4 in definition \ref{def:MPAR-K} are satisfied. \\
1717: \noindent Now, let us prove property 5 of definition
1718: \ref{def:MPAR-K}. Let
1719: $\overline{r}=X$\Rule{K'}$p'\in\Re^{K}_{PAR}\setminus\Re$.
1720: Therefore, $X\in{}Var$, $p'\in{}Var\cup\{\hat{Z}_{F}\}$ and
1721: $K'\in{}P_{n}$. We have to prove that $X$ \multider{\sigma} $t$
1722: for some term $t$, with $|\sigma|>0$, \maximal{\sigma} $=K'$
1723: and $t=p'$ if $p'\in{}Var$.
1724: Let us assume that $\overline{r}$ is
1725: the \emph{n}-th rule added to $\Re_{P}$
1726: during the computation. Then, $\overline{r}$ is added to $\Re_{P}$
1727: during an iteration of the \textbf{for} loop in lines 6-36, in
1728: which a rule $r$ of the form $X$\Rule{a}$Y.(Z)\in\Re$ is examined.
1729: Let $K_{1}=$ \maximal{r}.
1730: The proof is by induction on $n$.\\
1731: \textbf{Base Step}: $n=1$. In this phase
1732: \begin{enumerate}
1733: \item[1.] $\Re_{P}=\{r\in\Re|\textrm{ $r$ is a PAR rule}\}$
1734: and $\forall{}i=1,\ldots,n$
1735: $\Re_{P,i}^{A}=\{r\in\Re_{i}^{A}|\textrm{ $r$ is}$ a PAR
1736: rule\}.
1737: \item[2.] $\forall{}r'\in{}\Re_{P}$ we have \maximal{r'} =
1738: \maximalG{M_{p}}{r'}.
1739: \end{enumerate}
1740: There are three cases:
1741: \begin{itemize}
1742: \item $\overline{r}$ is added to
1743: $\Re_{P}$ in line 12.
1744: Then, $p'=\hat{Z}_{F}\notin{}Var$, and the condition of the
1745: \textbf{if} statement in line 9 is satisfied:
1746: $\prsdernorm{Z}{\sigma}{\Re_{P}}{p}$ for some $p$, with
1747: \maximalG{M_{P}}{\sigma} $=K_{2}$ and
1748: $K'=K_{1}\cup{}K_{2}$. From 1 we deduce that $\sigma$ is a sequence
1749: of PAR rules in $\Re$. From 2 it follows that \maximal{\sigma} =
1750: \maximalG{M_{P}}{\sigma}. Therefore,
1751: $X$ \prsoneder{r} $Y.(Z)$ \multider{\sigma} $Y.(p)$ with
1752: \maximal{r\sigma} $=K_{1}\cup{}K_{2}=K'$, and the assertion is proved.
1753: \item $\overline{r}$ is added to
1754: $\Re_{P}$ in line 19.
1755: Then, $p'=Y\in{}Var$, and the condition of the
1756: \textbf{if} statement in line 16 is satisfied:
1757: $\prsdernorm{Z}{\sigma}{\Re_{P}}{\varepsilon}$ with
1758: \maximalG{M_{P}}{\sigma} $=K_{2}$ and
1759: $K'=K_{1}\cup{}K_{2}$. From 1 we deduce that $\sigma$ is a sequence
1760: of PAR rules in $\Re$. From 2 it follows that \maximal{\sigma} =
1761: \maximalG{M_{P}}{\sigma}. Therefore,
1762: $X$ \prsoneder{r} $Y.(Z)$ \multider{\sigma} $Y$ with
1763: \maximal{r\sigma} $=K_{1}\cup{}K_{2}=K'$, and the assertion is proved.
1764: \item $\overline{r}$ is added to
1765: $\Re_{P}$ by the inner \textbf{for} loop in lines 24-35, when
1766: a rule $r'$ of the form $Y.(W)$\Rule{b}$W'\in\Re$ is examined.
1767: Then, $p'=W'\in{}Var$, and $\overline{r}$ is added to
1768: $\Re_{P}$ in line 30. So,
1769: the condition of the \textbf{if} statement in linea 27 is satisfied:
1770: $\prsdernorm{Z}{\sigma}{\Re_{P}}{W}$ with
1771: \maximalG{M_{P}}{\sigma} $=K_{3}$ and
1772: $K'=K_{1}\cup{}K_{2}\cup{}K_{3}$, where $K_{2}=$ \maximal{r'}.
1773: From 1 we deduce that $\sigma$ is a sequence
1774: of PAR rules in $\Re$. From 2 it follows that \maximal{\sigma} =
1775: \maximalG{M_{P}}{\sigma}. Therefore,
1776: $X$ \prsoneder{r'} $Y.(Z)$ \multider{\sigma} $Y.(W)$ \prsoneder{r''} $W'$
1777: with
1778: \maximal{r\sigma{}r'} $=K_{1}\cup{}K_{2}\cup{}K_{3}=K'$, and the assertion is proved.
1779: \end{itemize}
1780: \textbf{Induction Step}: $n>1$. Let $\overline{\Re}_{P}$
1781: (resp., $\overline{\Re}_{P,i}^{A}$ for $i=1,\ldots,n$) be
1782: the set of the rules in $\Re^{K}_{PAR}\setminus\Re$
1783: (resp., $\Re^{K,A}_{PAR,i}\setminus\Re$ for $i=1,\ldots,n$) after $n-1$ rules have been
1784: added to $\Re_{P}$. Then,
1785: in this phase we have
1786: \begin{itemize}
1787: \item $\Re_{P}$ $=\{r\in\Re|$ $r$ is a PAR
1788: rule$\}\cup\overline{\Re}_{P}$, and $\forall{}i=1,\ldots,n$ $\Re_{P,i}^{A}$
1789: $=\{r\in\Re_{i}^{A}|$ $r$ is a PAR
1790: rule$\}\cup\overline{\Re}_{P,i}^{A}$.
1791: \item $\forall{}\hat{r}=\hat{t}$\Rule{\hat{K}}$\hat{t}'\in\overline{\Re}_{P}$
1792: we have \maximalG{M_{P}}{\hat{r}} $=\hat{K}$.
1793: \item $\forall{}r'\in{}\{r\in\Re|$ $r$ is a PAR
1794: rule$\}$ we have \maximal{r'} =
1795: \maximalG{M_{p}}{r'}.
1796: \end{itemize}
1797: >From the inductive hypothesis, we deduce easily that the following
1798: property is satisfied
1799: \begin{enumerate}
1800: \item[3.] If $\prsdernorm{\hat{t}}{\sigma}{\Re_{P}}{\hat{t}'}$, where
1801: $\hat{t}$ is a parallel term,
1802: then $\hat{t}$ \multider{\rho} $\hat{t}''$ for some term $\hat{t}''$, with \maximal{\rho}
1803: = \maximalG{M_{P}}{\sigma}. Moreover, if $\hat{t}'$ doesn't
1804: contain occurrences of $\hat{Z}_{F}$ then
1805: $\hat{t}''=\hat{t}'$.
1806: \end{enumerate}
1807: As before, there are three cases:
1808: \begin{itemize}
1809: \item $\overline{r}$ is added to
1810: $\Re_{P}$ in line 12. Then, $p'=\hat{Z}_{F}\notin{}Var$,
1811: and the condition of the
1812: \textbf{if} statement in line 9 is satisfied:
1813: $\prsdernorm{Z}{\sigma}{\Re_{P}}{p}$ for some term $p$, with
1814: \maximalG{M_{P}}{\sigma} $=K_{2}$ and
1815: $K'=K_{1}\cup{}K_{2}$. From 3 it follows that
1816: $Z$ \multider{\rho} $t$ for some term $t$, with \maximal{\rho}
1817: = \maximalG{M_{P}}{\sigma}. Therefore,
1818: $X$ \prsoneder{r} $Y.(Z)$ \multider{\rho} $Y.(t)$ with
1819: \maximal{r\rho} $=K_{1}\cup{}K_{2}=K'$, and the assertion is proved.
1820: \item $\overline{r}$ is added to
1821: $\Re_{P}$ in line 19.
1822: Then, $p'=Y\in{}Var$, and the condition of the
1823: \textbf{if} statement in line 16 is satisfied:
1824: $\prsdernorm{Z}{\sigma}{\Re_{P}}{\varepsilon}$ with
1825: \maximalG{M_{P}}{\sigma} $=K_{2}$ and
1826: $K'=K_{1}\cup{}K_{2}$. From 3 it follows that
1827: $Z$ \multider{\rho} $\varepsilon$, with \maximal{\rho}
1828: = \maximalG{M_{P}}{\sigma}. Therefore,
1829: $X$ \prsoneder{r} $Y.(Z)$ \multider{\rho} $Y$ with
1830: \maximal{r\rho} $=K_{1}\cup{}K_{2}=K'$, and the assertion is proved.
1831: \item $\overline{r}$ is added to
1832: $\Re_{P}$ by the inner \textbf{for} loop in lines 24-35, when
1833: a rule $r'$ of the form $Y.(W)$\Rule{b}$W'\in\Re$ is examined.
1834: Then, $p'=W'\in{}Var$, and $\overline{r}$ is added to
1835: $\Re_{P}$ in line 30. So,
1836: the condition of the \textbf{if} statement in line 27 is satisfied:
1837: $\prsdernorm{Z}{\sigma}{\Re_{P}}{W}$ with
1838: \maximalG{M_{P}}{\sigma} $=K_{3}$ and
1839: $K'=K_{1}\cup{}K_{2}\cup{}K_{3}$, where $K_{2}=$ \maximal{r'}.
1840: From 3 it follows that
1841: $Z$ \multider{\rho} $W$ with \maximal{\rho}
1842: = \maximalG{M_{P}}{\sigma}. Therefore,
1843: $X$ \prsoneder{r'} $Y.(Z)$ \multider{\rho} $Y.(W)$ \prsoneder{r''} $W'$
1844: with
1845: \maximal{r\rho{}r'} $=K_{1}\cup{}K_{2}\cup{}K_{3}=K'$, and the assertion is proved.
1846: \end{itemize}
1847:
1848: \noindent{} Finally, it's easy to show that $M^{K}_{PAR}$ is the
1849: least parallel \MBRS over $Var$ and the alphabet
1850: $\overline{\Sigma}$ satisfying properties 1-5 of definition
1851: \ref{def:MPAR-K}.
1852: \end{proof}
1853:
1854: \begin{Remark}\label{Remark:MKPAR}By construction the following
1855: properties hold:
1856: \begin{itemize}
1857: \item $\forall{}r\in\Re\cap\Re^{K}_{PAR}$ we have \maximalparK{r}
1858: = \maximal{r}.
1859: \item $\forall{}r=X$\Rule{K'}$p\in\Re_{PAR}^{K}\setminus\Re$ we have \maximalparK{r}
1860: = $K'$.
1861: \end{itemize}
1862: \end{Remark}
1863:
1864:
1865: Soundness and completeness of the procedure described above is
1866: stated by the following theorem, whose proof is reported in
1867: appendix (section B).
1868:
1869: \begin{Theorem}\label{Theorem:Problem1}
1870: For all $X\in{}Var$ there exists a $(K,\emptyset)$-accepting
1871: finite derivation in $M$ from $X$ if, and only if, there exists a
1872: $(K,\emptyset)$-accepting finite derivation in
1873: $M^{K}_{PAR}$ from $X$.
1874: \end{Theorem}
1875:
1876:
1877: This result, together with proposition \ref{Prop:ParMBRS-F},
1878: allow us to conclude that
1879: Problem 1, stated at the beginning of this section, is decidable.
1880:
1881:
1882:
1883: \subsection{Decidability results on infinite derivations of \MBRSs in normal form}\label{sec:infinite}
1884:
1885: \setcounter{equation}{0}
1886:
1887:
1888: In this section we prove the decidability of Problem 2 stated in
1889: subsection~\ref{sec:Model-checkingPRS}, that for clarity we
1890: recall.
1891: \begin{description}
1892: \item[Problem 2]\emph{ Given a \MBRS in normal form
1893: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ over Var and
1894: the alphabet $\Sigma$, given a variable $X\in{}Var$ and two
1895: sets
1896: $K,K^{\omega}\in{}P_{n}$, to decide if there exists a $(K,K^{\omega})$-accepting infinite derivation in $M$
1897: from $X$}.
1898: \end{description}
1899:
1900: Let us observe that a necessary condition for the existence of a
1901: $(K,K^{\omega})$-accepting infinite derivation
1902: in $M$ is that $K\supseteq{}K^{\omega}$.\\
1903: The proof of decidability is by induction on $|K|+|K^{\omega}|$.\\
1904: \textbf{Base Step}: $|K|=0$ and $|K^{\omega}|=0$. Let $M_{F}=\npla{\Re,\Re_{F}}$
1905: be the \BRS with $\Re_F=\bigcup_{i=1}^{n}\Re_{i}^{A}$. Given an
1906: infinite derivation $X$ \multider{\sigma} in $\Re$ from a variable $X$ then,
1907: this derivation is $(\emptyset,\emptyset)$-accepting in $M$ if,
1908: and only if, it doesn't contain occurrences of accepting rules in
1909: $M_{F}$. So, the decidability result follows from theorem
1910: \ref{Theorem:OldResults}.\\
1911: \textbf{Inductive Step}: $|K|+|K^{\omega}|>0$. From the
1912: inductive hypothesis, for each $K'\subseteq{}K$ and
1913: $K'^{\omega}\subseteq{}K^{\omega}$ with
1914: $|K'|+|K'^{\omega}|<|K|+|K^{\omega}|$ the
1915: result holds. In other words, it is decidable if there exists a
1916: $(K',K'^{\omega})$-accepting infinite derivation in $M$ from a
1917: variable $X$.
1918: Starting from this assumption
1919: we show that problem 2, with input the sets $K$ and $K^{\omega}$,
1920: can be reduced to (a combination of) two similar, but simpler,
1921: problems: the first is a decidability problem on infinite
1922: derivations restricted to parallel \MBRSs; the second is a
1923: decidability problem on infinite derivations restricted to
1924: sequential \MBRSs. More precisely, we show that it is possible to
1925: construct effectively two parallel \MBRSs
1926: $M^{K,K^{\omega}}_{PAR}=\npla{\Re^{K,K^{\omega}}_{PAR},\npla{\Re^{K,K^{\omega},A}_{PAR,1},\ldots,\Re_{PAR,n}^{K,K^{\omega},A}}}$
1927: and
1928: $M^{K,K^{\omega}}_{PAR,\infty}=\npla{\Re^{K,K^{\omega}}_{PAR},\npla{\Re^{K,K^{\omega},A}_{PAR,\infty,1},\ldots,\Re_{PAR,\infty,n}^{K,K^{\omega},A}}}$
1929: with the same support, and a sequential \MBRS
1930: $M_{SEQ}^{K}=\npla{\Re_{SEQ}^{K},\npla{\Re^{K,A}_{SEQ,1},\ldots,\Re_{SEQ,n}^{K,A}}}$,
1931: in such a way that Problem 2, with input the sets $K$ and
1932: $K^{\omega}$ and a variable $X\in{}Var$, is reducible to one of
1933: two following problems depending if $K\supset{}K^{\omega}$ or
1934: $K=K^{\omega}$.\\
1935:
1936:
1937: \noindent\textbf{Problem 3} $(K\supset{}K^{\omega})$. To decide if
1938: the following condition is satisfied:
1939: \begin{itemize}
1940: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
1941: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
1942: with $K'\subseteq{}K$, and there exists a derivation
1943: $Y$ \multiderparKomega{\rho}
1944: such that \maximalparKomega{\rho} = $K$
1945: and
1946: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
1947: $K^{\omega}$. Moreover, either $\rho$ is
1948: infinite or $\rho$ contains some occurrence of rule in
1949: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$ (where $\Re_{PAR}^{K}$ is the
1950: support of the parallel \MBRS $M_{PAR}^{K}$ defined in the previous subsection).
1951: \end{itemize}
1952:
1953:
1954: \noindent\textbf{Problem 4} $(K=K^{\omega})$. To decide if one of
1955: the following conditions is satisfied:
1956: \begin{itemize}
1957: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
1958: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
1959: with $K'\subseteq{}K$, and there exists a derivation
1960: $Y$ \multiderparKomega{\rho}
1961: such that \maximalparKomega{\rho} = $K$
1962: and
1963: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
1964: $K^{\omega}$. Moreover, either $\rho$ is
1965: infinite or $\rho$ contains some occurrence of rule in
1966: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
1967: \item There exists a
1968: $(K,K^{\omega})$-accepting infinite derivation in $M_{SEQ}^{K}$ from
1969: $X$.
1970: \end{itemize}
1971:
1972: Since these last problems are decidable (see theorems
1973: \ref{Theorem:ConditionForProblem2-1} and
1974: \ref{Theorem:ConditionForProblem2-2}), decidability of Problem 2
1975: is entailed.
1976:
1977:
1978: Before illustrating the main idea underlying our approach, we need
1979: the following definition.
1980:
1981:
1982:
1983: \begin{Definition}
1984: Let us denote by $\Pi^{K,K^{\omega}}_{PAR,\infty}$ the set of
1985: derivations $t$ \multider{\sigma} in $\Re$ \emph{\textbf{not}}
1986: satisfying the following property:
1987: \begin{itemize}
1988: \item There exists a subderivation of $t$ \multider{\sigma}
1989: that is a $(K,K^{\omega})$-accepting infinite derivation in
1990: $M$.
1991: \end{itemize}
1992: \end{Definition}
1993:
1994:
1995: In the following we use a new variable $\hat{Z}_{\infty}$, and denote
1996: by $T$ (resp., $T_{PAR}$, $T_{SEQ}$) the set of process terms
1997: (resp., the set of terms in which no sequential composition
1998: occurs, the set of terms in which no parallel composition occurs)
1999: over
2000: $Var\cup\{\hat{Z}_{F},\hat{Z}_{\infty}\}$\footnote{$\hat{Z}_{F}$
2001: is the variable used in the previous subsection for the
2002: construction of the parallel \MBRS $M_{PAR}^{K}$}.\newline
2003:
2004:
2005: \noindent{}Let us sketch the main ideas at the basis of our
2006: technique. At first, let us focus on the class of derivations
2007: $\Pi^{K,K^{\omega}}_{PAR,\infty}$, showing how it is possible to
2008: mimic a $(K,K^{\omega})$-accepting infinite derivation in $M$ from
2009: a variable, belonging to this class, by using only PAR rules
2010: belonging to extensions of the parallel \MBRS $M_{PAR}^{K}$
2011: computed by the algorithm of lemma \ref{Lemma:Algo} (with input
2012: $M$ and $K$). More precisely, we'll show, as anticipated, that it
2013: is possible construct two parallel extensions of $M_{PAR}^{K}$
2014: with the same support, denoted by
2015: $M^{K,K^{\omega}}_{PAR}=\npla{\Re^{K,K^{\omega}}_{PAR},\npla{\Re^{K,K^{\omega},A}_{PAR,1},\ldots,\Re_{PAR,n}^{K,K^{\omega},A}}}$
2016: and
2017: $M^{K,K^{\omega}}_{PAR,\infty}=\npla{\Re^{K,K^{\omega}}_{PAR},\npla{\Re^{K,K^{\omega},A}_{PAR,\infty,1},\ldots,\Re_{PAR,\infty,n}^{K,K^{\omega},A}}}$
2018: (with $\Re^{K,K^{\omega},A}_{PAR,i}\supseteq{}\Re^{K,A}_{PAR,i}$
2019: and
2020: $\Re^{K,K^{\omega},A}_{PAR,\infty,i}\cap\Re^{K,A}_{PAR,i}=\emptyset$
2021: for $i=1,\ldots,n$), in such way that the following condition
2022: holds:
2023: \begin{description}
2024: \item[i.] There exists a $(\overline{K},\overline{K}^{\omega})$-accepting
2025: derivation in $M$ belonging to $\Pi^{K,K^{\omega}}_{PAR,\infty}$
2026: of the form $p$ \multider{\sigma}, with $p\in{}T_{PAR}$,
2027: $\overline{K}\subseteq{}K$ and
2028: $\overline{K}^{\omega}\subseteq{}K^{\omega}$ if, and only if,
2029: there exists a derivation $p$ \multiderparKomega{\rho} in
2030: $\Re^{K,K^{\omega}}_{PAR}$
2031: from $p$ such that \maximalparKomega{\rho} = $\overline{K}$ and
2032: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
2033: $\overline{K}^{\omega}$. Moreover, if $\sigma$ is infinite then, either $\rho$ is
2034: infinite or $\rho$ contains some occurrence of rule in
2035: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$, and vice versa.
2036: \end{description}
2037:
2038: So, let $p$ \multider{\sigma} be a
2039: $(\overline{K},\overline{K}^{\omega})$-accepting derivation in
2040: $M$ belonging to $\Pi^{K,K^{\omega}}_{PAR,\infty}$ with
2041: $p\in{}T_{PAR}$, $\overline{K}\subseteq{}K$ and
2042: $\overline{K}^{\omega}\subseteq{}K^{\omega}$. Then, all its
2043: possible subderivations contain all, and only, the rule
2044: occurrences in $\sigma$ applied at a level $k$ greater than $0$ in
2045: $p$ \multider{\sigma}. If $\sigma$ contains only PAR rule
2046: occurrences the statement \textbf{i} is evident, since by
2047: construction (remember that $\Re_{PAR}^{K}$ contains all PAR rules
2048: of $\Re$) we have $p$ \multiderparKomega{\sigma} with
2049: \maximalparKomega{\sigma} = $\overline{K}$,
2050: \maximalparKomegaInf{\sigma} =
2051: $\overline{K}^{\omega}$ and \maximalparKomegaPlus{\sigma} = $\emptyset$. Otherwise,
2052: $p$ \multider{\sigma} can be written in the form:
2053: \begin{equation}\label{eq:derivation}
2054: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
2055: $t$$\parallel$$Y.(Z)$ \multider{\omega}}
2056: \end{equation}
2057: where $r = X$\Rule{a}$Y.(Z)$, $\lambda$ contains only occurrences of PAR rules
2058: in $\Re$, $t\in{}T_{PAR}$ and $X,Y,Z\in{}Var$. Let $Z$ \multider{\rho} be a subderivation of
2059: $t$$\parallel$$Y.(Z)$ \multider{\omega} from $Z$.
2060: Since $p$ \multider{\sigma} is in
2061: $\Pi^{K,K^{\omega}}_{PAR,\infty}$, $Z$ \multider{\rho} is
2062: \emph{not} a $(K,K^{\omega})$-accepting infinite derivation in
2063: $M$. More precisely, \maximal{\rho} $\subseteq{}K$,
2064: \maximalInf{\rho} $\subseteq{}K^{\omega}$ (since $\rho$ is a
2065: subsequence of $\sigma$) and
2066: $|$\maximal{\rho}$|+|$\maximalInf{\rho}$|<|K|+|K^{\omega}|$. Thus,
2067: only one of the following four cases may occur:
2068: \begin{description}
2069: \item[A] $Z$ \multider{\rho} leads to the term $\varepsilon$, and
2070: $p$ \multider{\sigma} is of the form
2071: \begin{equation}\label{eq:form1}
2072: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
2073: $t$$\parallel$$Y.(Z)$ \multider{\omega_{1}} $\overline{t}$$\parallel$$Y$ \multider{\omega_{2}}}
2074: \end{equation}
2075: where $\rho$ is a subsequence of $\omega_1$ and $t$
2076: \multider{\omega_{1}\setminus\rho} $\overline{t}$. The derivation above is
2077: $(\overline{K},\overline{K}^{\omega})$-accepting in $M$ if, and only if, the following
2078: derivation
2079: is $(\overline{K},\overline{K}^{\omega})$-accepting in $M$
2080: \begin{equation}\label{eq:form1-2}
2081: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
2082: $t$$\parallel$$Y.(Z)$ \multider{\rho} $t$$\parallel$$Y$ \multider{\xi}
2083: $\overline{t}$$\parallel$$Y$ \multider{\omega_{2}}}
2084: \end{equation}
2085: where $\xi=\omega_{1}\setminus\rho$.
2086: Let us consider the derivation $X$ \prsoneder{r} $Y.(Z)$
2087: \multider{\rho} $Y$ where \maximal{r\rho} $\subseteq{}K$. From properties of $M^{K}_{PAR}$ (see lemma \ref{Lemma:From-M-To-MKPAR} in appendix)
2088: there exists a derivation of the form $X$ \multiderparK{\eta} $Y$
2089: such that \maximalparK{\eta} = \maximal{r\rho}.
2090: Now, we can apply recursively the same reasoning to the
2091: derivation in $\Re$ from $t$$\parallel$$Y\in{}T_{PAR}$
2092: \begin{equation}
2093: \textrm{$t$$\parallel$$Y$ \multider{\xi} $\overline{t}$$\parallel$$Y$
2094: \multider{\omega_{2}}}
2095: \end{equation}
2096: which belongs to $\Pi^{K,K^{\omega}}_{PAR,\infty}$ and whose finite (resp., infinite)
2097: maximal as to $M$ is
2098: contained in $K$ (resp., $K^{\omega}$).
2099: \item[B] $Z$ \multider{\rho} leads to a variable $W$, and
2100: $p$ \multider{\sigma} can be written as
2101: \begin{equation}\label{eq:form1}
2102: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
2103: $t$$\parallel$$Y.(Z)$ \multider{\omega_{1}} $\overline{t}$$\parallel$$Y.(W)$
2104: \prsoneder{r'} $\overline{t}$$\parallel$$W'$ \multider{\omega_{2}}}
2105: \end{equation}
2106: where $r'=Y.(W)$\Rule{b}$W'$ (with $W'\in{}Var$),
2107: $\rho$ is a subsequence of $\omega_1$ and $t$
2108: \multider{\omega_{1}\setminus\rho} $\overline{t}$. The derivation above is
2109: $(\overline{K},\overline{K}^{\omega})$-accepting if, and only if, the following derivation
2110: is $(\overline{K},\overline{K}^{\omega})$-accepting
2111: \begin{equation}\label{eq:form1-2}
2112: \textrm{$p$ \multider{\lambda} $t$$\parallel$$X$ \prsoneder{r}
2113: $t$$\parallel$$Y.(Z)$ \multider{\rho} $t$$\parallel$$Y.(W)$ \prsoneder{r'} $t$$\parallel$$W'$
2114: \multider{\xi}
2115: $\overline{t}$$\parallel$$W'$ \multider{\omega_{2}}}
2116: \end{equation}
2117: where $\xi=\omega_{1}\setminus\rho$.
2118: Let us consider the derivation $X$ \prsoneder{r} $Y.(Z)$
2119: \multider{\rho} $Y.(W)$ \prsoneder{r'} $W'$ where \maximal{rr'\rho} $\subseteq{}K$.
2120: From properties of $M^{K}_{PAR}$ (see lemma \ref{Lemma:From-M-To-MKPAR} in appendix)
2121: there exists a derivation of the form $X$ \multiderparK{\eta} $W'$
2122: such that \maximalparK{\eta} = \maximal{rr'\rho}.
2123: Now, we can apply recursively the same reasoning to the
2124: derivation in $\Re$ from $t$$\parallel$$W'\in{}T_{PAR}$
2125: \begin{equation}
2126: \textrm{$t$$\parallel$$W'$ \multider{\xi} $\overline{t}$$\parallel$$W'$
2127: \multider{\omega_{2}}}
2128: \end{equation}
2129: which belongs to $\Pi^{K,K^{\omega}}_{PAR,\infty}$ and whose finite (resp., infinite)
2130: maximal as to $M$ is
2131: contained in $K$ (resp., $K^{\omega}$).
2132: \item[C] $Z$ \multider{\rho} is finite and does not influence
2133: the
2134: applicability of rule occurrences in $\omega \setminus \rho$ in the derivation
2135: $t$$\parallel$$Y.(Z)$ \multider{\omega}. In other
2136: words, we have $t$ \multider{\omega\setminus\rho}. Moreover,
2137: \maximal{r\rho} $\subseteq{}K$.
2138: Let us consider the finite derivation $X$ \prsoneder{r} $Y.(Z)$
2139: \multider{\rho}.
2140: From properties of $M^{K}_{PAR}$ (see lemma \ref{Lemma:From-M-To-MKPAR} in appendix)
2141: there exists a finite derivation of the form $X$
2142: \multiderparK{\eta} $\overline{p}$ with $\overline{p}\in{}T_{PAR}$
2143: and \maximalparK{\eta} = \maximal{r\rho}.
2144: Now, we can apply recursively the same reasoning to the
2145: derivation $t$$\parallel$$\overline{p}$ \multider{\omega\setminus\rho} in $\Re$ from
2146: $t$$\parallel$$\overline{p}$ (where $t$$\parallel$$\overline{p}\in{}T_{PAR}$),
2147: which belongs to $\Pi^{K,K^{\omega}}_{PAR,\infty}$ and whose finite (resp., infinite)
2148: maximal as to $M$ is
2149: contained in $K$ (resp., $K^{\omega}$).
2150: \item[D] $Z$ \multider{\rho} is infinite. From the definition of
2151: subderivation we have $t$ \multider{\omega\setminus\rho}.
2152: Moreover,
2153: \maximal{\rho} $=K_1\subseteq{}K$, \maximalInf{\rho} $=K_{1}^{\omega}\subseteq{}K^{\omega}$,
2154: \maximal{r} $=K_2\subseteq{}K$, \maximalInf{r} $=\emptyset$
2155: and $|K_1|+|K_{1}^{\omega}|<|K|+|K^{\omega}|$.
2156: From our assumptions (inductive hypothesis)
2157: it is decidable if there exists a
2158: $(K_1,K_{1}^{\omega})$-accepting infinite derivation in $M$ from
2159: variable $Z$.
2160: Then, we keep track of the infinite sequence $r\rho$
2161: by adding the new variable $\hat{Z}_{\infty}$ (where $\hat{Z}_{\infty}\notin{}Var$) and
2162: a PAR rule of the form $r'=X$\Rule{K',K_{1}^{\omega}}$\hat{Z}_{F}$ with
2163: $K'=K_1\cup{}K_2$,
2164: \maximalparKomega{r'} = $K'$ and \maximalparKomegaPlus{r'} = $K_{1}^{\omega}$.
2165: Now, we can apply recursively the same reasoning to the
2166: derivation $t$$\parallel$$\hat{Z}_{\infty}$ \multider{\omega\setminus\rho} in $\Re$ from
2167: $t$$\parallel$$\hat{Z}_{\infty}$ (where $t$$\parallel$$\hat{Z}_{\infty}\in{}T_{PAR}$),
2168: which belongs to $\Pi^{K,K^{\omega}}_{PAR,\infty}$ and whose finite (resp., infinite)
2169: maximal as to $M$ is
2170: contained in $K$ (resp., $K^{\omega}$).
2171: \end{description}
2172:
2173: In other words, all subderivations in $p$ \multider{\sigma} are
2174: abstracted away by PAR rules not belonging to $\Re$,
2175: according to the intuitions given above.\newline
2176:
2177: By the parallel \MBRS $M_{PAR}^{K}$ we keep track of subderivations of the forms \textbf{A},
2178: \textbf{B} and \textbf{C}.
2179: In order to simulate subderivations of the form \textbf{D}, we
2180: need to add additional PAR rules in $M_{PAR}^{K}$.
2181: The following definition provides an extension of
2182: $M_{PAR}^{K}$ suitable for our purposes.
2183:
2184:
2185: \begin{Definition}\label{Def:M-PARs-Infinite}
2186: By
2187: $M^{K,K^{\omega}}_{PAR}=
2188: \npla{\Re^{K,K^{\omega}}_{PAR},\npla{\Re^{K,K^{\omega},A}_{PAR,1},\ldots,
2189: \Re^{K,K^{\omega},A}_{PAR,n}}}$
2190: and \newline
2191: $M^{K,K^{\omega}}_{PAR,\infty}=
2192: \npla{\Re^{K,K^{\omega}}_{PAR},\npla{\Re^{K,K^{\omega},A}_{PAR,\infty,1},\ldots,
2193: \Re^{K,K^{\omega},A}_{PAR,\infty,n}}}$ we denote the parallel \MBRSs
2194: over $Var\cup\{\hat{Z}_{F},\hat{Z}_{\infty}\}$ and the alphabet
2195: $\Sigma\cup{}P_n\cup{}P_n\times{}P_n$,
2196: defined by $M$ and $M_{PAR}^{K}$
2197: in the following way:
2198: \begin{itemize}
2199: \item $\Re^{K,K^{\omega}}_{PAR}=\begin{array}[t]{l}%
2200: \Re_{PAR}^{K} \cup \\
2201: %
2202: \{\prsrule{X}{\overline{K},\overline{K}^{\omega}}{\hat{Z}_{\infty}} \mid \begin{array}[t]{l}
2203: \overline{K}\subseteq{}K,
2204: \overline{K}^{\omega}\subseteq{}K^{\omega},
2205: \text{ there exists a
2206: rule } r=\prsrule{X}{a}{Y.(Z)}\in\Re \\[4pt]
2207: \text{and
2208: an infinite derivation } \prsder{Z}{\sigma}{} \text{
2209: such that } \\[4pt] |\text{\maximal{\sigma}}| +
2210: |\text{\maximalInf{\sigma}}|
2211: < |K|+|K^{\omega}| \text{ and} \\[4pt]
2212: \text{ \maximal{\sigma} $\cup$ \maximal{r} } =\overline{K} \text{ and}
2213: \text{ \maximalInf{\sigma} } =\overline{K}^{\omega}
2214: \}\
2215: \end{array}
2216: \end{array}$
2217: \item
2218: $\Re^{K,K^{\omega},A}_{PAR,i}=\Re_{PAR,i}^{K,A}\cup\{
2219: X$\Rule{\overline{K},\overline{K}^{\omega}}$\hat{Z}_{\infty}\in\Re^{K,K^{\omega}}_{PAR}|$
2220: $i\in{}\overline{K}$\} for all $i=1,\ldots,n$
2221: \item
2222: $\Re^{K,K^{\omega},A}_{PAR,i,\infty}=\{
2223: X$\Rule{\overline{K},\overline{K}^{\omega}}$\hat{Z}_{\infty}\in\Re^{K,K^{\omega}}_{PAR}|$
2224: $i\in{}\overline{K}^{\omega}$\} for all $i=1,\ldots,n$
2225: \end{itemize}
2226: \end{Definition}
2227:
2228:
2229: \noindent{}From the inductive hypothesis on the decidability of
2230: problem 2 for sets $\overline{K},\overline{K}^{\omega}\in{}P_{n}$
2231: such that $\overline{K}\subseteq{}K$,
2232: $\overline{K}^{\omega}\subseteq{}K^{\omega}$ and
2233: $|\overline{K}|+|\overline{K}^{\omega}|<|K|+|K^{\omega}|$, it
2234: follows that $M^{K,K^{\omega}}_{PAR}$ and
2235: $M^{K,K^{\omega}}_{PAR,\infty}$ can be built effectively. Thus,
2236: the following result holds.
2237:
2238: \begin{Lemma}
2239: $M^{K,K^{\omega}}_{PAR}$ and $M^{K,K^{\omega}}_{PAR,\infty}$ can
2240: be built effectively.
2241: \end{Lemma}
2242:
2243:
2244: \begin{Remark}\label{Remark:MPAR-Inf}By construction, the
2245: following properties hold:
2246: \begin{itemize}
2247: \item for all $r\in\Re_{PAR}^{K}$ we have \maximalparKomega{r} =
2248: \maximalparK{r} and \maximalparKomegaPlus{r}
2249: $=\emptyset$.
2250: \item for all $r\in\Re^{K,K^{\omega}}_{PAR}\cap\Re$ we have \maximalparKomega{r} =
2251: \maximal{r} and \maximalparKomegaPlus{r}
2252: $=\emptyset$.
2253: \item for all $r=X$\Rule{\overline{K},\overline{K}^{\omega}}$\hat{Z}_{\infty}\in
2254: \Re^{K,K^{\omega}}_{PAR}$
2255: we have \maximalparKomega{r} = $\overline{K}$ and
2256: \maximalparKomegaPlus{r} = $\overline{K}^{\omega}$.
2257: \end{itemize}
2258: \end{Remark}
2259:
2260:
2261: Now, let us go back to Problem 2 and consider a
2262: $(K,K^{\omega})$-accepting infinite derivation in $M$ from a
2263: variable $X$ of the form $X$ \multider{\sigma}, and non belonging
2264: to $\Pi^{K,K^{\omega}}_{PAR,\infty}$. In this case, the
2265: derivation $X$ \multider{\sigma} can be written in the form $X$
2266: \multider{} $t$$\parallel$$Y.(Z)$ \multider{\rho}, with
2267: $Z\in{}Var$, and such that there exists a subderivation of
2268: $t$$\parallel$$Y.(Z)$ \multider{\rho} from $Z$ that is a
2269: $(K,K^{\omega})$-accepting infinite derivation in $M$. To manage
2270: this kind of derivation, we build, starting from the \MBRSs $M$
2271: and $M_{PAR}^{K}$, a sequential \MBRS $M_{SEQ}^{K}$ according to
2272: the following definition:
2273:
2274:
2275: \begin{Definition}\label{Def:M-SEQ}
2276: By $M_{SEQ}^{K}=\npla{\Re_{SEQ}^{K},\npla{\Re_{SEQ,1}^{K,A},\ldots,\Re_{SEQ,n}^{K,A}}}$ we denote
2277: the sequential \MBRS
2278: over $Var$ and the alphabet $\overline{\Sigma}=\Sigma\cup{}P_{n}$ so defined:
2279: \begin{itemize}
2280: \item $\Re_{SEQ}^{K}=\begin{array}[t]{l}%
2281: \{\prsrule{X}{a}{Y.(Z)}\in\Re\}\ \cup \\
2282: %
2283: \{\prsrule{X}{K'}{Y} \mid \begin{array}[t]{l}
2284: X,Y\in{}Var, K'\subseteq{}K \text{ and there exists a
2285: derivation } \prsderpar{X}{\sigma}{\parcomp{p}{Y}} \\[4pt]
2286: \text{ in } \Re_{PAR}^{K} \text{
2287: for some } p\in{}T_{PAR}
2288: \text{, with } |\sigma|>0 \text{ and \maximalparK{\sigma} = $K'$} \}\
2289: \end{array}
2290: \end{array}$
2291: \item
2292: $\Re_{SEQ,i}^{K,A}=\{X$\Rule{a}$Y.(Z)\in\Re_{i}^{A}\}\cup\{X$\Rule{K'}$Y\in\Re_{SEQ}^{K}|
2293: i\in{}K'$\} for all $i=1,\ldots,n$
2294: \end{itemize}
2295: \end{Definition}
2296:
2297:
2298: \begin{Remark}\label{Remark:MKSEQ} By construction the following
2299: properties hold
2300: \begin{itemize}
2301: \item for all $r\in\Re\cap\Re_{SEQ}^{K}$ we have
2302: \maximal{r} = \maximalseqK{r}.
2303: \item for all $r=X$\Rule{K'}$Y\in\Re_{SEQ}^{K}\setminus\Re$ we have \maximalseqK{r}
2304: = $K'$.
2305: \end{itemize}
2306: \end{Remark}
2307:
2308:
2309: \begin{Lemma}
2310: $M_{SEQ}^{K}$ can be built effectively.
2311: \end{Lemma}
2312:
2313: \begin{proof}
2314: The result follows directly from the definition of $M_{SEQ}^{K}$
2315: and proposition \ref{Prop:ParMBRS-F}.
2316: \end{proof}
2317:
2318:
2319:
2320: \setcounter{equation}{0}
2321:
2322:
2323: Soundness and completeness of the procedure described above is
2324: stated by the following two theorems, whose proof is reported in
2325: appendix (section C).
2326:
2327: \begin{Theorem}\label{Theorem:Problem2.1}
2328: Let us assume that $K\neq{}K^{\omega}$. Given $X\in{}Var$, there
2329: exists a
2330: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
2331: $X$ if, and only if, the following property is satisfied:
2332: \begin{itemize}
2333: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
2334: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
2335: with $K'\subseteq{}K$, and there exists a derivation
2336: $Y$ \multiderparKomega{\rho}
2337: such that \maximalparKomega{\rho} = $K$
2338: and
2339: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
2340: $K^{\omega}$. Moreover, either $\rho$ is
2341: infinite or $\rho$ contains some occurrence of rule in
2342: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
2343: \end{itemize}
2344: \end{Theorem}
2345:
2346:
2347:
2348: \begin{Theorem}\label{Theorem:Problem2.2}
2349: Let us assume that $K=K^{\omega}$. Given $X\in{}Var$, there exists
2350: a
2351: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
2352: $X$ if, and only if, one of the following properties is satisfied:
2353: \begin{enumerate}
2354: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
2355: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
2356: with $K'\subseteq{}K$, and there exists a derivation
2357: $Y$ \multiderparKomega{\rho}
2358: such that \maximalparKomega{\rho} = $K$
2359: and
2360: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
2361: $K^{\omega}$. Moreover, either $\rho$ is
2362: infinite or $\rho$ contains some occurrence of rule in
2363: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
2364: \item There exists a
2365: $(K,K^{\omega})$-accepting infinite derivation in $M_{SEQ}^{K}$ from
2366: $X$.
2367: \end{enumerate}
2368: \end{Theorem}
2369:
2370: These two results, together with theorems
2371: \ref{Theorem:ConditionForProblem2-1} and
2372: \ref{Theorem:ConditionForProblem2-2}, allow us to conclude that
2373: Pro\-blem 2, stated at the beginning of this subsection, is decidable.
2374:
2375: \bibliographystyle{plain}
2376:
2377: %\bibliography{./a-l,./m-z,./new}
2378:
2379: \begin{thebibliography}{1}
2380:
2381:
2382: \bibitem{ay98}
2383: R. Alur, S. Kannan, and M. Yannakakis. Model checking of
2384: hierarchical state machines. In Proc. 6th ACM Symp. on Found. of
2385: Software Engineering, 1998, 175--188.
2386: %
2387:
2388: \bibitem{alur01}%
2389: R.~Alur, K.~Etessami, and M.~Yannakakis.%
2390: \newblock Analysis of Recursive State Machine. %
2391: \newblock In \emph{Proceedings of CAV'01}, Springer LNCS n. 2102,
2392: pp. 207-220, 2001.
2393:
2394:
2395: \bibitem{bouajjani96}%
2396: A.~Bouajjani and P.~Habermehl. %
2397: \newblock Constraint properties, semi-linear systems, and Petri nets. %
2398: \newblock In \emph{Proc. of CONCUR'96}, Springer LNCS 1119, 1996.
2399:
2400: \bibitem{bouajjani97}%
2401: A.~Bouajjani, J.~Esparza, and O.~Maler. %
2402: \newblock Reachability Analysis of Pushdown Automata: Application to
2403: Model-Checking. %
2404: \newblock In \emph{Proc. CONCUR'97}, Springer LNCS 1243,
2405: pp. 135-150, 1997.
2406:
2407:
2408: \bibitem{Bozz03}%
2409: L.~Bozzelli, M.~Benerecetti, and A.~Peron. %
2410: \newblock Verification of recursive parallel systems.%
2411: \newblock Technical report number 42, Dept. of Mathematics and Applications
2412: - University of Naples "Federico II", Italy , 2003.
2413: \newblock Submitted to TPLP Special Issue on Specification, Analysis and Verification
2414: of Reactive Systems -- Cambridge University Press, november 2003.
2415:
2416: \bibitem{BS94}
2417: O.~Burkart, B.~Steffen. Parallel Composition and model checking.
2418: In \emph{Proc. of CONCUR'94}, LNCS 836, Springer, 1994, pp.
2419: 98-113.
2420:
2421: \bibitem{BCS96}
2422: O.~Burkart, D.~Caucal, B.~Steffen. The process taxonomy. In
2423: \emph{Proc. of CONCUR'96}, LNCS 1119, Springer, 1996.
2424:
2425: \bibitem{burkart01}%
2426: O.~Burkart, D.~Caucal,~F. Moller, and B.~Steffen. %
2427: \newblock Verification On Infinite Structures. %
2428: \newblock In \emph{Handbook on Process Algebra}, North-Holland,
2429: 2001.
2430:
2431: \bibitem{davis83}%
2432: Martin D.~Davis, Elaine J.~Weyuker. %
2433: \newblock \emph{Computability, Complexity, and Languages}. %
2434: \newblock pag.~47-49, Academic Press, 1983.
2435: 2001.
2436:
2437: \bibitem{esparza94}%
2438: J.~Esparza. %
2439: \newblock On the decidability of model checking for several
2440: $\mu$-calculi and Petri nets. %
2441: \newblock In \emph{Trees in Algebra and Programming}, CAAP'94, vol.
2442: 787 of LNCS. Springer Verlag, 1994.
2443:
2444: \bibitem{esp97}%
2445: J.~Esparza. %
2446: \newblock Decidability of model checking for infinite--state
2447: concurrent systems. %
2448: \newblock In \emph{Acta Informaticae}, 34, 1997, pp. 85--107.
2449:
2450:
2451: \bibitem{ehrs00}
2452: J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient
2453: algorithms for model checking
2454: pushdown systems. In \emph{Proc. Computer Aided Verification}
2455: (CAV'00), Springer LNCS 1855, 2000, 232--247.
2456:
2457:
2458: \bibitem{hun94}
2459: H. Hungar. Model checking of macro processes. In \emph{Proc. of
2460: CAV'94}, LNCS 818, 1994, pp. 169--182.
2461:
2462:
2463:
2464: \bibitem{mayr98}%
2465: R. Mayr.%
2466: \newblock Decidability and Complexity of Model Checking Problems for
2467: Infinite-State Systems.%
2468: \newblock PhD. thesis, TU--M\"unchen, 1998.
2469:
2470: \bibitem{M96}
2471: F. Moller. Infinite results. In \emph{Proc. of CONCUR'96}, LNCS
2472: 1119, Springer, 1996.
2473:
2474:
2475: \bibitem{walukiewicz96}%
2476: I.~Walukiewicz. Pushdown processes: Games and model checking.%
2477: \newblock In \emph{Int. Conf. on Compter Aided Verification}, LNCS 1102,
2478: pages 62-74. Springer Verlag, 1996.
2479:
2480: \end{thebibliography}
2481:
2482:
2483: \newpage
2484:
2485:
2486:
2487:
2488: \appendix
2489: \begin{LARGE}
2490: \textbf{APPENDIX}
2491: \end{LARGE}
2492:
2493: \section{Definitions and simple properties}
2494:
2495: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2496: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2497: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2498: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2499: %%% DEFINIZIONI %%%
2500: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2501: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2502: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2503: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2504:
2505: In this section we give some definitions and deduce simple
2506: properties that will be used in sections B and C for the proof of
2507: theorems 4.1-4.3.
2508:
2509: In the following $\hat{Var}$ denotes the set of variables
2510: $Var\cup\{\hat{Z}_{F},\hat{Z}_{\infty}\}$, $T$ denotes the set of
2511: terms over $\hat{Var}$, and $T_{PAR}$ (resp., $T_{SEQ}$) the set
2512: of terms in $T$ not containing sequential (resp., parallel)
2513: composition.
2514:
2515:
2516: \begin{Definition}
2517: The set of {\em subterms\/} of a term $t\in{}T$, denoted by
2518: $SubTerms(t)$, is defined inductively as follows:
2519: \begin{itemize}
2520: \item $SubTerms(\varepsilon)=\{\varepsilon\}$ \item
2521: $SubTerms(X)=\{X\}$, for all $X\in{}\hat{Var}$ \item
2522: $SubTerms(X.(t))=SubTerms(t)\cup\{X.(t)\}$, for all $X.(t)\in{}T$
2523: with $t\neq\varepsilon$ \item
2524: $SubTerms($$t_{1}$$\parallel$$t_{2})=\bigcup_{(t_{1}',t_{2}')\in{}S}
2525: (SubTerms(t_{1}')\cup{} SubTerms(t_{2}'))$ $\cup$
2526: $\{t_{1}$$\parallel$$t_{2}\}$,
2527: \newline
2528: with $S=\{(t_{1}',t_{2}')\in{}T\times{}T \mid
2529: t_{1}',t_{2}'\neq\varepsilon$
2530: and $t_{1}$$\parallel$$t_{2}={}t_{1}'$$\parallel$$t_{2}'\}$ and
2531: $t_{1},t_{2}\in{}T\setminus \{\varepsilon\}$.
2532: \end{itemize}
2533: \end{Definition}
2534:
2535: \begin{Definition} The set of terms obtained from a term $t\in T$
2536: {\em substituting\/} an occurrence of a subterm $st$ of $t$ with a
2537: term $t'\in T$, denoted by $t[st\rightarrow{}t']$, is defined
2538: inductively as follows:
2539: \begin{itemize}
2540: \item $t[t\rightarrow{}t']=\{t'\}$
2541: \item $X.(t)[st\rightarrow{}t']=
2542: \{X.(s) \mid s\in{}t[st\rightarrow{}t']\}$, for all terms
2543: $X.(t)\in{}T$ with $t\neq\varepsilon$ and
2544: $st\in{}SubTerms(X.(t))\setminus \{X.(t)\}$
2545: \item $t_{1}$$\parallel$$t_{2}[st\rightarrow{}t']=$
2546: $\{\parcomp{t''}{t'_2} \mid (t'_1,t'_2) \in T \times T, t'_1,t'_2
2547: \neq \varepsilon$, $\parcomp{t'_1}{t'_2} = \parcomp{t_1}{t_2}$,
2548: $st \in SubTerms(t'_1)$, $t''\in{}t_{1}'[st\rightarrow{}t']\}$,
2549: for all $t_1,t_2\in T\setminus\{\varepsilon\}$ and $st \in
2550: SubTerms(\parcomp{t_1}{t_2})\setminus \{\parcomp{t_1}{t_2}\}$.
2551: \end{itemize}
2552: \end{Definition}
2553:
2554: \begin{Definition}
2555: For a term $t\in{}T$, the set of terms $SEQ(t)$ is the subset of
2556: $T_{SEQ}\setminus\{\varepsilon\}$ defined inductively as follows:
2557: \begin{itemize}
2558: \item $SEQ(\varepsilon)=\emptyset$
2559: \item $SEQ(X)=\{X\}$, for all $X\in{}\hat{Var}$
2560: \item $SEQ(X.(t))=\{X.(t') \mid t'\in{}SEQ(t)\}$, for all
2561: $X\in{}\hat{Var}$ and $t\in{}T\setminus \{\varepsilon\}$
2562: \item $SEQ(t_{1}$$\parallel$$t_{2})=SEQ(t_{1})\cup{}SEQ(t_{2})$.
2563: \end{itemize}
2564: \end{Definition}
2565:
2566:
2567:
2568: For a term $t\in{}T_{SEQ}\setminus \{\varepsilon\}$ having the
2569: form $t=X_{1}.(X_{2}.(\ldots{}X_{n}.(Y)\ldots))$, with $n\geq0$,
2570: we denote the variable $Y$ by $last(t)$. Given two terms
2571: $t,t'\in{}T_{SEQ}\setminus\{\varepsilon\}$, with
2572: $t=X_{1}.(X_{2}.(\ldots{}X_{n}.(Y)\ldots))$ and
2573: $t'=X_{1}'.(X_{2}'.(\ldots{}X_{k}'.(Y')\ldots))$, we denote by
2574: $t\circ{}t'$ the term
2575: $X_{1}.(X_{2}.(\ldots{}X_{n}.(X_{1}'.(X_{2}'$
2576: $.(\ldots{}X_{k}'.(Y')\ldots)))\ldots))$. Notice that $t\circ{}t'$ is
2577: the only term in $t[Y\rightarrow{}t']$, and that the operation
2578: $\circ$ on terms in $T_{SEQ} \setminus \{\varepsilon\}$ is
2579: associative.
2580:
2581: %***************************************
2582: % Proposizione A.1
2583: %****************************************
2584:
2585: \begin{Proposition}[see~\cite{Bozz03}]
2586: \label{Prop:Subterms1} The following properties hold:
2587: \begin{enumerate}
2588: \item If $t$ \multider{\sigma} $t'$ and $t\in{}SubTerms(s)$,
2589: for some $s\in{}T$, then it holds $s$ \multider{\sigma} $s'$ for
2590: all $s'\in{}s[t\rightarrow{}t']$; \item If $t$ \multider{\sigma}
2591: is an infinite derivation in $\Re$ and $t\in{}SubTerms(s)$, for
2592: some $s\in{}T$, then it holds $s$ \multider{\sigma}.
2593: \end{enumerate}
2594: \end{Proposition}
2595:
2596: %***************************************
2597: % Fine Proposizione A.1
2598: %****************************************
2599:
2600: %***************************************
2601: % Proposizione A.2
2602: %****************************************
2603: \begin{Proposition}[see~\cite{Bozz03}]\label{Prop:Subterms2}
2604: If
2605: $t,t'\in{}T_{SEQ}\setminus \{\varepsilon\}$ such that
2606: $last(t)$ \multider{\rho}
2607: $t'$, then it holds that
2608: \begin{enumerate}
2609: \item $t$ \multider{\rho} $t\circ{}t'$;
2610: \item $t''\circ{}t$ \multider{\rho} $t''\circ{}t\circ{}t'$
2611: for all $t''\in{}T_{SEQ}\setminus\{\varepsilon\}$.
2612: \end{enumerate}
2613: \end{Proposition}
2614:
2615: %***************************************
2616: % Fine proposizione A.2
2617: %****************************************
2618:
2619:
2620:
2621: %***************************************
2622: % Lemma A.1
2623: %****************************************
2624: \begin{Lemma}\label{Lemma:Subderivations1}
2625: Let $t$$\parallel$$X.(s)$ \multider{\sigma} be a
2626: derivation in $\Re$, and let $s$ \multider{\sigma{}'} be a
2627: subderivation of $t$$\parallel$$X.(s)$ \multider{\sigma} from
2628: $s$. Then, the following properties are satisfied:
2629: \begin{enumerate}
2630: \item If $s$ \multider{\sigma{}'} is infinite, then it holds
2631: that
2632: $t$ \multider{\sigma\setminus\sigma{}'}.
2633: Moreover, if $t$$\parallel$$X.(s)$ \multider{\sigma}
2634: is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$, then also $t$ \multider{\sigma\setminus\sigma{}'} is in
2635: $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
2636: \item If $s$ \multider{\sigma{}'} leads
2637: to $\varepsilon$, then the derivation
2638: $t$$\parallel$$X.(s)$ \multider{\sigma} can be written in the form
2639: \begin{displaymath}
2640: \textrm{$t$$\parallel$$X.(s)$ \multider{\sigma_{1}} $t'$$\parallel$$X$ \multider{\sigma_{2}}}
2641: \end{displaymath}
2642: where $t$ \multider{\lambda} $t'$ with $\sigma_{1}\in{}Interleaving(\lambda,\sigma{}')$.
2643: Moreover, if $t$$\parallel$$X.(s)$ \multider{\sigma}
2644: is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$, there is a derivation
2645: of the form $t$$\parallel$$X$ \multider{\lambda} $t'$$\parallel$$X$ \multider{\sigma_{2}}
2646: belonging to $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
2647: \item If $s$ \multider{\sigma{}'} leads
2648: to a term $s'\neq\varepsilon$ one of the following conditions is satisfied:
2649: \begin{itemize}
2650: \item $t$ \multider{\sigma\setminus\sigma{}'}.
2651: If $t$$\parallel$$X.(s)$ \multider{\sigma}
2652: is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$, then also $t$ \multider{\sigma\setminus\sigma{}'}
2653: is in
2654: $\Pi^{K,K^{\omega}}_{PAR,\infty}$. Moreover, if
2655: $t$$\parallel$$X.(s)$ \multider{\sigma} is finite
2656: and leads to $\overline{t}$, then
2657: $\overline{t}=X.(s')$$\parallel$$t'$ where $t$
2658: \multider{\sigma\setminus\sigma{}'} $t'$.
2659: \item $s'=W\in{}Var$ and the derivation
2660: $t$$\parallel$$X.(s)$ \multider{\sigma} can be written in the
2661: form
2662: \begin{displaymath}
2663: \textrm{$t$$\parallel$$X.(s)$ \multider{\sigma_{1}}
2664: $t'$$\parallel$$X.(W)$ \prsoneder{r}
2665: $t'$$\parallel$$W'$ \multider{\sigma_{2}}}
2666: \end{displaymath}
2667: where $r=X.(W)$\Rule{a}$W'\in{}\Re$, and
2668: $t$ \multider{\lambda} $t'$
2669: with $\sigma_{1}\in{}Interleaving(\lambda,\sigma{}')$.
2670: Moreover, if $t$$\parallel$$X.(s)$ \multider{\sigma}
2671: is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$, there is a derivation
2672: of the form $t$$\parallel$$W'$ \multider{\lambda} $t'$$\parallel$$W'$ \multider{\sigma_{2}}
2673: belonging to $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
2674: \end{itemize}
2675: \end{enumerate}
2676: \end{Lemma}
2677:
2678: \begin{proof}
2679: The assertion follows easily from the definition of subderivation.
2680: \end{proof}
2681:
2682: %***************************************
2683: % Fine Lemma A.1
2684: %****************************************
2685:
2686:
2687:
2688:
2689: %***************************************
2690: % Lemma A.3
2691: %****************************************
2692: \begin{Lemma}\label{Lemma:Base}
2693: \setcounter{equation}{0}
2694: Let $p$ \multider{\sigma}
2695: $t$$\parallel$$Y.(s)$ \multider{\omega} with $s\neq\varepsilon$
2696: and $p\in{}T_{PAR}$. Then, $p$ \multider{\sigma}
2697: $t$$\parallel$$Y.(s)$ can be written in the form
2698: \begin{equation}
2699: \textrm{$p$ \multider{\sigma_{1}} $t'$$\parallel$$Z$ \prsoneder{r}
2700: $t'$$\parallel$$Y.(Z')$ \multider{\sigma_{2}}
2701: $t$$\parallel$$Y.(s)$}
2702: \end{equation}
2703: with $r=Z$\Rule{a}$Y.(Z')$, and
2704: \begin{equation}
2705: \textrm{$Z'$ \multider{\sigma_{2}'} $s\quad$ and $t'$
2706: \multider{\sigma_{2}''} $t$}
2707: \end{equation}
2708: with $\sigma_{2}\in{}Interleaving(\sigma_{2}',\sigma_{2}'')$.
2709: Moreover, the following property is satisfied:
2710: \begin{description}
2711: \item[A] Let $s$ \multider{\omega'} be a subderivation of $t$$\parallel$$Y.(s)$
2712: \multider{\omega} from $s$. Then, the derivation
2713: \begin{displaymath}
2714: \textrm{$Z'$ \multider{\sigma_{2}'} $s$
2715: \multider{\omega'}}
2716: \end{displaymath}
2717: is a subderivation of $t'$$\parallel$$Y.(Z')$ \multider{\sigma_{2}}
2718: $t$$\parallel$$Y.(s)$ \multider{\omega} from $Z'$.
2719: \end{description}
2720: \end{Lemma}
2721:
2722: \begin{proof}
2723: The assertion follows easily by induction on the length of $\sigma$.
2724: \end{proof}
2725:
2726: %***************************************
2727: % Fine Lemma A.3
2728: %****************************************
2729:
2730: \section{Proof of Theorem \ref{Theorem:Problem1}}
2731:
2732: In order to prove theorem \ref{Theorem:Problem1} we need the
2733: following two lemmata
2734: \ref{Lemma:From-MKPAR-To-M}--\ref{Lemma:From-M-To-MKPAR}
2735:
2736:
2737:
2738:
2739: \begin{Lemma}\label{Lemma:From-MKPAR-To-M} Let $p$
2740: \multiderparK{\sigma} $p'$$\parallel$$p''$ with
2741: $p,p',p''\in{}T_{PAR}$, $p'$ not containing occurrences of
2742: $\hat{Z}_{F}$ and $\hat{Z}_{\infty}$, and $p''$ not containing
2743: occurrences of variables in $Var$. Then, there exists a $t\in{}T$
2744: such that $p$ \multider{\rho} $p'$$\parallel$$t$ with
2745: \maximal{\rho} = \maximalparK{\sigma}, and $|\rho|>0$ if
2746: $|\sigma|>0$.
2747: \end{Lemma}
2748: \begin{proof}
2749: The proof is by induction on $|\sigma|$.\\
2750: \textbf{Base Step}: $|\sigma|=0$. In this case the assertion is
2751: obvious.\\
2752: \textbf{Induction Step}: $|\sigma|>0$. In this case the derivation
2753: $p$ \multiderparK{\sigma} $p'$$\parallel$$p''$ can be written in
2754: the form
2755: \begin{displaymath}
2756: \textrm{$p$ \multiderparK{\sigma'}
2757: $\overline{p}'$$\parallel$$\overline{p}''$ \onederparK{r}
2758: $p'$$\parallel$$p''\quad$ with $|\sigma'|<|\sigma|$,
2759: $r\in\Re^{K}_{PAR}$ and
2760: $\overline{p}',\overline{p}''\in{}T_{PAR}$}
2761: \end{displaymath}
2762: Moreover, $\overline{p}'$ doesn't contain occurrences of
2763: $\hat{Z}_{F}$ and $\hat{Z}_{\infty}$, and $\overline{p}''$ doesn't
2764: contain occurrences of variables in $Var$. From the inductive
2765: hypothesis, there exists a $\overline{t}\in{}T$ such that $p$
2766: \multider{\rho'} $\overline{p}'$$\parallel$$\overline{t}$ with
2767: \maximal{\rho'} = \maximalparK{\sigma'}.\\
2768: There are two cases:
2769: \begin{enumerate}
2770: \item $r$ is a PAR rule of $\Re$. From remark \ref{Remark:MKPAR}
2771: \maximal{r} = \maximalparK{r}. Moreover, $\overline{p}''=p''$
2772: and $\overline{p}'$ \onederparK{r} $p'$. Then, we deduce that
2773: $p$ \multider{\rho'}
2774: $\overline{p}'$$\parallel$$\overline{t}$ \prsoneder{r}
2775: $p'$$\parallel$$\overline{t}$ with
2776: \maximal{\rho'r} = \maximalparK{\sigma'r}, and the assertion is
2777: proved.
2778: \item $r\in\Re^{K}_{PAR}\setminus\Re$. There are two subcases:
2779: \begin{itemize}
2780: \item $r=X$\Rule{K'}$Y$
2781: with $X,Y\in{}Var$ and $K'\in{}P_{n}$.
2782: From remark \ref{Remark:MKPAR} \maximalparK{r} = $K'$.
2783: From property 5 in the definition of $M_{PAR}^{K}$
2784: we have $X$ \multider{\rho''} $Y$ with
2785: \maximal{\rho''} $=K'$ and $|\rho''|>0$. Moreover,
2786: $\overline{p}''=p''$ and $\overline{p}'$ \onederparK{r} $p'$. Then,
2787: we deduce that
2788: $p$ \multider{\rho'}
2789: $\overline{p}'$$\parallel$$\overline{t}$ \multider{\rho''}
2790: $p'$$\parallel$$\overline{t}$ with
2791: \maximal{\rho'\rho''} = \maximalparK{\sigma'r}, and the assertion is
2792: proved.
2793: \item $r=X$\Rule{K'}$\hat{Z}_{F}$ with $X\in{}Var$, and
2794: \maximalparK{r} = $K'$. From property 5 in the definition of $M_{PAR}^{K}$, we
2795: deduce that $X$ \multider{\rho''} $t$, for some term $t$,
2796: with
2797: \maximal{\rho''} = \maximalparK{r} and $|\rho''|>0$. Evidently,
2798: $p''=\overline{p}''$$\parallel$$\hat{Z}_{F}$ and
2799: $\overline{p}'=p'$$\parallel$$X$. Then,
2800: we deduce that
2801: $p$ \multider{\rho'}
2802: $\overline{p}'$$\parallel$$\overline{t}=p'$$\parallel$$X$$\parallel$$\overline{t}$
2803: \multider{\rho''} $p'$$\parallel$$t$$\parallel$$\overline{t}$
2804: with
2805: \maximal{\rho'\rho''} = \maximalparK{\sigma'r}, and the assertion is
2806: proved.
2807: \end{itemize}
2808: \end{enumerate}
2809: \end{proof}
2810:
2811:
2812:
2813:
2814: \setcounter{equation}{0}
2815: $\newline$\begin{Lemma}\label{Lemma:From-M-To-MKPAR}
2816: Let $p$ \multider{\sigma} $t$$\parallel$$p'$
2817: with $p,p'\in{}T_{PAR}$ and \maximal{\sigma} $\subseteq{}K$. Then,
2818: there exists a $s\in{}T_{PAR}$ such that $p$ \multiderparK{\rho} $s$$\parallel$$p'$
2819: with
2820: \maximal{\sigma} = \maximalparK{\rho}, and $s=\varepsilon$ if
2821: $t=\varepsilon$.
2822: \end{Lemma}
2823: \begin{proof}
2824: The proof is by induction on the length of finite derivations $p$
2825: \multider{\sigma} in $\Re$ from terms in $T_{PAR}$ with
2826: \maximal{\sigma} $\subseteq{}K$.\\
2827: \\
2828: \textbf{Base Step}: $|\sigma|=0$. In this case the assertion is
2829: obvious.\\
2830: \\
2831: \textbf{Induction Step}: $|\sigma|>0$. The derivation $p$
2832: \multider{\sigma} can be written in the form
2833: \begin{equation}
2834: \textrm{$p$ \prsoneder{r} $\overline{t}$ \multider{\sigma'}
2835: $t$$\parallel$$p'$ $\quad$ }
2836: \end{equation}
2837: with $r\in\Re$, $|\sigma'|<|\sigma|$ and \maximal{\sigma'}
2838: $\subseteq{}K$. There are two cases:
2839: \begin{enumerate}
2840: \item r is a PAR rule. Then, we have $\overline{t}\in{}T_{PAR}$. >From the
2841: inductive hypothesis, there exists a $s\in{}T_{PAR}$ such that
2842: $\overline{t}$ \multiderparK{\rho'} $s$$\parallel$$p'$
2843: with \maximal{\sigma'} = \maximalparK{\rho'}, and
2844: $s=\varepsilon$ if $t=\varepsilon$.
2845: By construction, $r\in\Re^{K}_{PAR}$. From remark \ref{Remark:MKPAR}, it follows that
2846: \maximal{r} = \maximalparK{r}. By proposition
2847: \ref{Prop:Maximal} we obtain
2848: $p$ \onederparK{r} $\overline{t}$ \multiderparK{\rho'} $s$$\parallel$$p'$ with
2849: \maximal{r\sigma'} = \maximalparK{r\rho'}, and
2850: $s=\varepsilon$ if $t=\varepsilon$. Hence, the assertion is proved.
2851: \item $r=Z$\Rule{a}$Y.(Z')$ with \maximal{r} $\subseteq{}K$. Then, we have
2852: $p=p''$$\parallel$$Z$ and $\overline{t}=p''$$\parallel$$Y.(Z')$, with $p''\in{}T_{PAR}$.
2853: From (1), let $Z'$ \multider{\lambda} $t_{1}$ a subderivation of $\overline{t}=p''$$\parallel$$Y.(Z')$
2854: \multider{\sigma'} from $Z'$. Evidently,
2855: \maximal{\lambda} $\subseteq{}K$. From lemma \ref{Lemma:Subderivations1} we can
2856: distinguish three subcases:
2857: \begin{itemize}
2858: \item $t_{1}\neq\varepsilon$ and $p''$ \multider{\sigma'\setminus\lambda} $t'$. Moreover,
2859: $t$$\parallel$$p'=t'$$\parallel$$Y.(t_{1})$, $t'=p'$$\parallel$$t''$ for some
2860: term $t''$, and
2861: $t=t''$$\parallel$$Y.(t_{1})$. In particular,
2862: $t\neq\varepsilon$. Since
2863: \maximal{\sigma'\setminus\lambda} $\subseteq{}K$, from the
2864: inductive hypothesis there exists an $s\in{}T_{PAR}$
2865: such that $p''$ \multiderparK{\rho'}
2866: $s$$\parallel$$p'$ with
2867: \maximal{\sigma'\setminus\lambda} = \maximalparK{\rho'}.
2868: Moreover, since \maximal{\lambda} $\subseteq{}K$,
2869: from the inductive hypothesis we have that
2870: $Z'$ \multiderparK{\rho''} $\overline{p}$ for some
2871: $\overline{p}\in{}T_{PAR}$, with
2872: \maximalparK{\rho''} = \maximal{\lambda}.
2873: Since \maximalparK{\rho''} = \maximal{\lambda} $\subseteq{}K$ and
2874: \maximal{r} $\subseteq{}K$, from property 2 in the
2875: definition of $M^{K}_{PAR}$ we deduce that
2876: $r'=Z$\Rule{K'}$\hat{Z}_{F}\in\Re^{K}_{PAR}$ with
2877: $K'=$ \maximal{\lambda} $\cup{}$ \maximal{r} and
2878: \maximalparK{r} = $K'$. Then, by proposition \ref{Prop:Maximal}
2879: we have $p=p''$$\parallel$$Z$ \onederparK{r'}
2880: $p''$$\parallel$$\hat{Z}_{F}$ \multiderparK{\rho'}
2881: $s$$\parallel$$p'$$\parallel$$\hat{Z}_{F}$ with
2882: \maximalparK{r'\rho'} = \maximal{r\lambda(\sigma'\setminus\lambda)} =
2883: \maximal{\sigma}, and the assertion is proved.
2884: \item $t_{1}=\varepsilon$ and the derivation $p''$$\parallel$$Y.(Z')$
2885: \multider{\sigma'} $t$$\parallel$$p'$ can be written in the
2886: form
2887: \begin{equation}
2888: \textrm{$p''$$\parallel$$Y.(Z')$
2889: \multider{\sigma_{1}} $t'$$\parallel$$Y$ \multider{\sigma_{2}} $t$$\parallel$$p'\quad$
2890: with $p''$ \multider{\sigma'_{1}} $t'$, and
2891: $\sigma_{1}\in{}Interleaving(\lambda,\sigma'_{1})$}
2892: \end{equation}
2893: Now, $Z'$ \multider{\lambda} $\varepsilon$ with
2894: $|\lambda|<|\sigma|$ and
2895: \maximal{\lambda} $\subseteq{}K$. From the inductive
2896: hypothesis, we have $Z'$ \multiderparK{\rho}
2897: $\varepsilon$
2898: such that
2899: \maximal{\lambda} = \maximalparK{\rho}.
2900: From property 3 in the definition of $M^{K}_{PAR}$
2901: it follows that $r'=Z$\Rule{K'}$Y\in\Re^{K}_{PAR}$
2902: where
2903: $K'=$ \maximal{r} $\cup{}$ \maximalparK{\rho} and
2904: \maximalparK{r'} = $K'$.
2905: Now, we have $p''$$\parallel$$Y$
2906: \multider{\sigma'_{1}} $t'$$\parallel$$Y$ \multider{\sigma_{2}}
2907: $t$$\parallel$$p'$ with
2908: \maximal{\sigma'_{1}\sigma_{2}} $\subseteq{}K$ and
2909: $|\sigma'_{1}\sigma_{2}|<|\sigma|$. From the
2910: inductive hypothesis, there exists a $s\in{}T_{PAR}$
2911: such that $p''$$\parallel$$Y$
2912: \multiderparK{\rho'}
2913: $s$$\parallel$$p'$, with
2914: \maximalparK{\rho'} = \maximal{\sigma'_{1}\sigma_{2}},
2915: and $s=\varepsilon$ if $t=\varepsilon$. After all,
2916: considering proposition \ref{Prop:Maximal},
2917: we have $p=p''$$\parallel$$Z$ \onederparK{r'}
2918: $p''$$\parallel$$Y$ \multiderparK{\rho'}
2919: $s$$\parallel$$p'$ with
2920: \maximal{r'\rho'} = \maximal{r\lambda\sigma'_{1}\sigma_{2}} =
2921: \maximal{\sigma}, and $s=\varepsilon$ if $t=\varepsilon$. So, the assertion is proved.
2922: \item
2923: $t_{1}=W\in{}Var$ and the derivation $p''$$\parallel$$Y.(Z')$
2924: \multider{\sigma'} $t$$\parallel$$p'$ can be written in the
2925: form
2926: \begin{eqnarray}
2927: \textrm{$p''$$\parallel$$Y.(Z')$
2928: \multider{\sigma_{1}} $t'$$\parallel$$Y.(W)$
2929: \prsoneder{r'} $t'$$\parallel$$W'$ \multider{\sigma_{2}}
2930: $t$$\parallel$$p'$}\\
2931: \textrm{with $p''$ \multider{\sigma'_{1}} $t'$,
2932: $r'=Y.(W)$\Rule{b}$W'$ and
2933: $\sigma_{1}\in{}Interleaving(\lambda,\sigma'_{1})$}
2934: \end{eqnarray}
2935: Now, $Z'$ \multider{\lambda} $W$ with
2936: $|\lambda|<|\sigma|$ and
2937: \maximal{\lambda} $\subseteq{}K$. From the inductive
2938: hypothesis, we have $Z'$ \multiderparK{\rho}
2939: $W$
2940: such that
2941: \maximal{\lambda} = \maximalparK{\rho}.
2942: From property 4 in the definition of $M^{K}_{PAR}$,
2943: considering that $r=Z$\Rule{a}$Y.(Z')\in\Re$ and
2944: $r'=Y.(W)$\Rule{b}$W'\in\Re$ with \maximal{r} $\subseteq{}K$
2945: and \maximal{r'} $\subseteq{}K$, it follows that $r''=Z$\Rule{K'}$W'\in\Re^{K}_{PAR}$
2946: where
2947: $K'=$ \maximal{rr'} $\cup{}$ \maximalparK{\rho}
2948: and \maximalparK{r''} = $K'$.
2949: Now, we have $p''$$\parallel$$W'$
2950: \multider{\sigma'_{1}} $t'$$\parallel$$W'$ \multider{\sigma_{2}}
2951: $t$$\parallel$$p'$ with
2952: \maximal{\sigma'_{1}\sigma_{2}} $\subseteq{}K$ and $|\sigma'_{1}\sigma_{2}|<|\sigma|$.
2953: From the
2954: inductive hypothesis there exists a $s\in{}T_{PAR}$
2955: such that $p''$$\parallel$$W'$
2956: \multiderparK{\rho'}
2957: $s$$\parallel$$p'$, with
2958: \maximalparK{\rho'} = \maximal{\sigma'_{1}\sigma_{2}},
2959: and $s=\varepsilon$ if $t=\varepsilon$. After all,
2960: considering proposition \ref{Prop:Maximal},
2961: we obtain $p=p''$$\parallel$$Z$ \onederparK{r''}
2962: $p''$$\parallel$$W'$ \multiderparK{\rho'}
2963: $s$$\parallel$$p'$ with
2964: \maximalparK{r''\rho'} = \maximal{rr'\lambda\sigma'_{1}\sigma_{2}} =
2965: \maximal{\sigma}, and $s=\varepsilon$ if $t=\varepsilon$. So, the assertion is proved.
2966: \end{itemize}
2967: \end{enumerate}
2968: \end{proof}
2969:
2970: At this point, theorem \ref{Theorem:Problem1} follows directly
2971: from lemmata
2972: \ref{Lemma:From-MKPAR-To-M}--\ref{Lemma:From-M-To-MKPAR}.
2973:
2974:
2975:
2976: \section{Proof of Theorems \ref{Theorem:Problem2.1} and \ref{Theorem:Problem2.2}}
2977:
2978: \setcounter{equation}{0}
2979:
2980: In order to prove theorems \ref{Theorem:Problem2.1} and
2981: \ref{Theorem:Problem2.2} we need the following lemmata
2982: \ref{Lemma:next}--\ref{Lemma:From-M-To-MSEQ3}\newline
2983:
2984: To prove lemma \ref{Lemma:From-MPAR-To-M-Inf} we use a mapping
2985: for coding pairs of integers by single integers. In particular,
2986: we consider the following bijective mapping from $N\times{}N$ to
2987: $N$, that is a primitive recursive function \cite{davis83}
2988: \begin{displaymath}
2989: \textrm{$<$ $>$$: (x,y)\in{}N\times{}N\rightarrow{}2^{x}(2y+1)-1$}
2990: \end{displaymath}
2991: Let $\ell$ (resp. $\wp$) be the first component (resp. the second
2992: component) of $<$ $>^{-1}$. The following properties are
2993: satisfied:
2994: \begin{enumerate}
2995: \item $\forall{}x,y\in{}N$ $\ell(<$$x,y$$>)=x$ and $\wp(<$$x,y$$>)=y$.
2996: \item $\forall{}z\in{}N$ $<$$\ell(z),\wp(z)$$>$ $=z$.
2997: \item $\forall{}z\in{}N$ $\ell(z),\wp(z)\leq{}z$.
2998: \item $\forall{}z,z'\in{}N$ if $z>z'$ and $\ell(z)=\ell(z')$ then $\wp(z)>\wp(z')$.
2999: \end{enumerate}
3000: Now, we introduce a new function
3001: $next:N\times{}N\rightarrow{}N\times{}N$ defined by primitive
3002: recursion in the following way
3003: \begin{displaymath}
3004: next(x,0)=(x,0)
3005: \end{displaymath}
3006: \begin{displaymath}
3007: next(x,y+1)= \left\{ \begin{array}{ll}
3008: (\ell(y),\wp(y)+1) & \textrm{if $next(x,y)=(\ell(y),\wp(y))$}\\
3009: next(x,y) & \textrm{otherwise}
3010: \end{array}
3011: \right.
3012: \end{displaymath}
3013:
3014: For all $x,y\in{}N$ let us denote by $next_{x}(y)$ the second
3015: component of $next(x,y)$. The following lemma establishes some
3016: properties of $next$.
3017:
3018:
3019: \begin{Lemma}\label{Lemma:next}
3020: The function $next$ satisfies the following properties:
3021: \begin{enumerate}
3022: \item $\forall{}x,y\in{}N$ if $y\leq{}x$ then
3023: $next(x,y)=(x,0)$.
3024: \item $\forall{}x,y\in{}N$ $next(x,y)=(x,z_{x,y})$ for some $z_{x,y}\in{}N$.
3025: \item $\forall{}x,y\in{}N$
3026: $next_{x}(y)\leq{}next_{x}(y+1)$.
3027: \item Let $x,y_{1},y_{2}\in{}N$ with
3028: $next_{x}(y_{1})<next_{x}(y_{2})$. Then, there exists a
3029: $k\in{}N$ such that $next(x,k)=(\ell(k),\wp(k))$, $\wp(k)=next_{x}(y_{2})-1$
3030: and $y_{1}\leq{}k<y_{2}$
3031: \item $\forall{}x,n\in{}N$ there exists a $y\in{}N$
3032: such that $next(x,y)=(x,n)$.
3033: \item $\forall{}x\in{}N$ $next(\ell(x),x)=(\ell(x),\wp(x))$.
3034: \item $\forall{}x,i\in{}N$ if $i\neq\ell(x)$ then $next(i,x+1)=next(i,x)$.
3035: \end{enumerate}
3036: \end{Lemma}
3037:
3038: \begin{proof}
3039: At first, let us consider property 1. We prove it by induction
3040: on $y$. By construction, for $y=0$ we have $next(x,0)=(x,0)$.\\
3041: Now, let $0<y\leq{}x$. From the inductive hypothesis
3042: $next(x,y-1)=(x,0)$. So, it suffices to prove that
3043: $next(x,y)=next(x,y-1)$. By absurd, let us assume that
3044: $next(x,y)\neq{}next(x,y-1)$. Then, by construction we have
3045: $next(x,y-1)=(\ell(y-1),\wp(y-1))$ and
3046: $next(x,y)=(\ell(y-1),\wp(y-1)+1)$. Therefore, $x=\ell(y-1)$. But,
3047: $x>y-1\geq{}\ell(y-1)$. So, we obtain an
3048: absurd.\\
3049: Now, let us consider property 2. We prove it by induction
3050: on $y$. By construction, for $y=0$ we have $next(x,0)=(x,0)$.\\
3051: Now, let $y>0$. From the inductive hypothesis $next(x,y-1)=(x,m)$
3052: for some $m\in{}N$. Now, by construction either
3053: $next(x,y)=next(x,y-1)=(x,m)$ or $next(x,y)=(x,m+1)$. In both
3054: cases the assertion is satisfied.\\
3055: Now, let us consider property 3. By construction,
3056: $\forall{}x,y\in{}N$ either $next_{x}(y+1)=next_{x}(y)$ or
3057: $next_{x}(y+1)=next_{x}(y)+1$. So, the assertion is satisfied.\\
3058: \\
3059: Now, let us consider property 4. From property 3 $y_{1}<y_{2}$.
3060: The proof is by induction on
3061: $y_{2}-y_{1}$.\\
3062: \textbf{Base Step}: $y_{2}-y_{1}=1$. So, $y_{2}=y_{1}+1$. From
3063: hypothesis $next(x,y_{1})\neq{}next(x,y_{2})$. Therefore, by
3064: construction we deduce that
3065: $next(x,y_{1})=(\ell(y_{1}),\wp(y_{1}))$ and
3066: $next(x,y_{2})=(\ell(y_{1}),\wp(y_{1})+1)$. So, setting $k=y_{1}$
3067: we have $next(x,k)=(\ell(k),\wp(k))$, $\wp(k)=next_{x}(y_{2})-1$
3068: and $y_{1}\leq{}k<y_{2}$. The
3069: assertion is proved.\\
3070: \textbf{Induction Step}: $y_{2}-y_{1}>1$. From property 3 there
3071: are two cases:
3072: \begin{itemize}
3073: \item $next_{x}(y_{2}-1)=next_{x}(y_{2})$. So,
3074: $next_{x}(y_{1})<next_{x}(y_{2}-1)$. Since
3075: $(y_{2}-1)-y_{1}<y_{2}-y_{1}$, from the inductive hypothesis
3076: there exists a
3077: $k\in{}N$ such that $next(x,k)=(\ell(k),\wp(k))$,
3078: $\wp(k)=next_{x}(y_{2}-1)-1$ and $y_{1}\leq{}k<y_{2}-1$. Since
3079: $next_{x}(y_{2}-1)=next_{x}(y_{2})$ we obtain the assertion.
3080: \item $next_{x}(y_{2}-1)<next_{x}(y_{2})$. We reason as in the
3081: base step.
3082: \end{itemize}
3083:
3084: Now, let us consider property 5. The proof is by induction on
3085: $n$. By construction, for $n=0$ we have $next(x,0)=(x,0)$. So, in
3086: this case the assertion is satisfied. Now, let $n>0$. From the
3087: inductive hypothesis there exists a $y\in{}N$ such that
3088: $next(x,y)=(x,n-1)$. From property 4, we deduce that it suffices
3089: to prove that there exists a $m>n-1$ such that $next(x,z)=(x,m)$
3090: for some $z\in{}N$. By absurd we assume that this property isn't
3091: satisfied. From property 2 and 3, we deduce that
3092: \begin{equation}
3093: \forall{}z\geq{}y{} \textrm{ $next(x,z)=(x,n-1)$}
3094: \end{equation}
3095: Let $k=$ $<$$x,n-1$$>$. Then, $x=\ell(k)$ and $n-1=\wp(k)$. There
3096: are two cases:
3097: \begin{itemize}
3098: \item $k\geq{}y$. From (1) we have $next(x,k)=(\ell(k),\wp(k))$. By
3099: construction, we obtain $next(x,k+1)=(\ell(k),\wp(k)+1)=(x,n)$ in
3100: contrast with (1).
3101: \item $k<y$. Now, $next(x,k)=(\ell(k),\overline{n})$. From
3102: property 3, it follows that $\overline{n}\leq{}\wp(k)$. There
3103: are two subcases:
3104: \begin{itemize}
3105: \item[-] $\overline{n}=\wp(k)$. So,
3106: $next(x,k)=(\ell(k),\wp(k))$. By construction, we obtain
3107: $next(x,k+1)=(\ell(k),\wp(k)+1)=(x,n)$. So, we have
3108: $k+1\leq{}y$ and $next_{x}(k+1)>next_{x}(y)$ in contrast with
3109: property 3.
3110: \item[-] $\overline{n}<\wp(k)$. In other words,
3111: we have $k<y$ and
3112: $next_{x}(k)<next_{x}(y)=\wp(k)$. From property 4, there exists
3113: a $k'\geq{}k$ such that
3114: $next(x,k')=(\ell(k'),\wp(k'))$ and
3115: $\wp(k')=next_{x}(y)-1=\wp(k)-1$. From property 2,
3116: $\ell(k')=x$. So, we have $\ell(k)=\ell(k')$, $k'\geq{}k$ and
3117: $\wp(k')<\wp(k)$. This is in contradiction with properties
3118: of $\wp$ and $\ell$.
3119: \end{itemize}
3120: \end{itemize}
3121:
3122: Now, let us consider property 6. Let $x\in{}N$. So, $x=$
3123: $<$$\ell(x),\wp(x)$$>$. From property 5 there exist two integers
3124: $y,z\in{}N$ such that $next(\ell(x),y)=(\ell(x),\wp(x)+1)$ and
3125: $next(\ell(x),z)=(\ell(x),\wp(x))$ where $y>z$. Since
3126: $next_{\ell(x)}$ is crescent there exists the greatest
3127: $\overline{z}$ such that
3128: $next(\ell(x),\overline{z})=(\ell(x),\wp(x))$. In particular,
3129: $next(\ell(x),\overline{z}+1)\neq{}next(\ell(x),\overline{z})$.
3130: >From definition of $next$ it follows that
3131: $next(\ell(x),\overline{z})=(\ell(\overline{z}),\wp(\overline{z}))$.
3132: Therefore,
3133: $(\ell(x),\wp(x))=(\ell(\overline{z}),\wp(\overline{z}))$. From
3134: this we deduce that $\overline{z}=x$, and the assertion is proved.
3135:
3136:
3137: Finally, let us consider property 7. Let $x,i\in{}N$ with
3138: $i\neq\ell(x)$. By absurd let us assume that
3139: $next(i,x+1)\neq{}next(i,x)$. Then, by construction
3140: $next(i,x)=(\ell(x),\wp(x))$. From property 2 we obtain
3141: $i=\ell(x)$, an absurd.
3142: \end{proof}
3143:
3144:
3145: Now, we give the notion of \emph{Interleaving} of a succession of
3146: rule sequences in a \PRS $\Re$. To formalize this concept and
3147: facilitate the proof of some connected results, we redefine the
3148: notion of sequence rule. Precisely, a sequence rule in $\Re$ can
3149: be seen as a mapping $\sigma:N'\rightarrow{}\Re$ where $N'$ can be
3150: a generic subset of $N$. In particular, this facilitates the
3151: formalization of the notion of subsequence. A rule sequence
3152: $\sigma':N''\rightarrow{}\Re$ is a subsequence of
3153: $\sigma:N'\rightarrow{}\Re$ iff $N''\subseteq{}N'$ and
3154: $\sigma'=\sigma|_{N''}$, that is $\sigma'$
3155: is the restriction of $\sigma$ to set $N''$.\\
3156: Given a rule sequence $\sigma:N'\rightarrow{}\Re$, we denote by
3157: $pr(\sigma)$ the set $N'$.\\
3158: Given a set $N'$, subset of $N$, we denote by $min(N')$ the
3159: smallest element of $N'$.\\
3160: Finally, given two rule sequences $\sigma$ and $\sigma'$, we say
3161: that they are disjoint if $pr(\sigma)\cap{}pr(\sigma')=\emptyset$.
3162:
3163: \begin{Definition}\label{Def:Interleaving}
3164: Let $\{\rho_{h}\}_{h\in{}N}$ be a succession of rule sequences in
3165: a \PRS $\Re$. The \emph{Interleaving} of $\{\rho_{h}\}_{h\in{}N}$,
3166: denoted by $Interleaving(\{\rho_{h}\})$, is the set of rule
3167: sequences $\sigma$ in $\Re$ such that there exists an
3168: \emph{injective} mapping
3169: $M_{\sigma}:\bigcup_{h\in{}N}(\{h\}\times{}pr(\rho_{h}))\rightarrow{}N$
3170: $\mathrm{(}$depending on $\sigma$$\mathrm{)}$ satisfying the
3171: following properties $\mathrm{(}$where $\Delta$ is the set
3172: $\bigcup_{h\in{}N}(\{h\}\times{}pr(\rho_{h})$$\mathrm{))}$
3173: \begin{itemize}
3174: \item $\forall{}h\in{}N$ $\forall{}n,n'\in{}pr(\rho_{h})$ with
3175: $n<n'$ then $M_{\sigma}(h,n)<M_{\sigma}(h,n')$.
3176: \item $pr(\sigma)=M_{\sigma}(\Delta)$.
3177: \item $\forall{}(h,n)\in{}\Delta$ we have
3178: $\sigma(M_{\sigma}(h,n))=\rho_{h}(n)$.
3179: \end{itemize}
3180: \end{Definition}
3181:
3182: \begin{Proposition}\label{Prop:MaximalInterleaving}
3183: Let
3184: $M=\npla{\Re,\npla{\Re_{1}^{A},\ldots,\Re_{n}^{A}}}$ be
3185: a \MBRS and let $\{\sigma_{h}\}_{h\in{}N}$ be a succession of rule
3186: sequences in $\Re$. Then,
3187: $\forall{}\pi\in{}Interleaving(\{\sigma_{h}\})$ we have
3188: \begin{enumerate}
3189: \item \maximal{\pi} = $\bigcup_{h\in{}N}$\maximal{\sigma_{h}}.
3190: \item \maximalInf{\pi} =
3191: $\bigcup_{h\in{}N}$\maximalInf{\sigma_{h}} $\cup$
3192: $\bigoplus_{h\in{}N}$\maximal{\sigma_{h}}.
3193: \end{enumerate}
3194: \end{Proposition}
3195: \begin{proof}
3196: We prove property 2. In similar way it's possible to prove
3197: property 1. Let
3198: $\Delta=\bigcup_{h\in{}N}(\{h\}\times{}pr(\sigma_{h})$$\mathrm{)}$.
3199: >From hypothesis
3200: there exists an \emph{injective} mapping
3201: $M_{\pi}:\Delta\rightarrow{}N$ such that
3202: $pr(\pi)=M_{\pi}(\Delta)$, and
3203: for all $(h,k)\in{}\Delta$
3204: $\pi(M_{\pi}(h,k))=\sigma_{h}(k)$.\\
3205: Let $i\in{}\{1,\ldots,n\}$. We have to prove that
3206: \begin{displaymath}
3207: \textrm{$i\in$\maximalInf{\pi} $\Leftrightarrow$ $i\in$
3208: $\bigcup_{h\in{}N}$\maximalInf{\sigma_{h}} $\cup$
3209: $\bigoplus_{h\in{}N}$\maximal{\sigma_{h}}.}
3210: \end{displaymath}
3211: $(\Rightarrow)$. Let $i\in$\maximalInf{\pi}. So, $\pi$ contains
3212: infinite occurrences of a rule $r\in\Re^{A}_{i}$. Therefore, the
3213: set $\{k\in{}M_{\pi}(\Delta)|$ $\pi(k)=r\}$ is infinite. Then, the
3214: set $\{(h,k)\in{}\Delta|$ $\sigma_{h}(k)=r\}$ is infinite. There
3215: are two cases:
3216: \begin{itemize}
3217: \item $\exists{}h\in{}N$ such that the set $\{j\in{}pr(\sigma_{h})|$ $\sigma_{h}(j)=r\}$
3218: is infinite. Therefore, $i\in$ \maximalInf{\sigma_{h}}
3219: \item The set $\{h\in{}N|$ $\sigma_{h}$ contains some occurrence of $r\}$ is infinite.
3220: Therefore, $i\in$ $\bigoplus_{h\in{}N}$\maximal{\sigma_{h}}.
3221: \end{itemize}
3222: In both cases the result holds.\\
3223: $(\Leftarrow)$. Let
3224: $i\in$ $\bigcup_{h\in{}N}$\maximalInf{\sigma_{h}} $\cup$
3225: $\bigoplus_{h\in{}N}$\maximal{\sigma_{h}}.
3226: There are two cases:
3227: \begin{itemize}
3228: \item $\exists{}h\in{}N$ such that $i\in$
3229: \maximalInf{\sigma_{h}}. Since $M_{\pi}$ is injective, the set
3230: $\{k\in{}M_{\pi}(\Delta)|$ $\pi(k)\in\Re^{A}_{i}\}$ is infinite. So,
3231: $i\in$\maximalInf{\pi}.
3232: \item The set $\{h\in{}N|$ $\sigma_{h}$ contains some occurrence of a rule in
3233: $\Re_{i}^{A}\}$ is infinite. Since $M_{\pi}$ is injective, it follows
3234: that
3235: $i\in$\maximalInf{\pi}.
3236: \end{itemize}
3237: \end{proof}
3238:
3239: \setcounter{equation}{0}
3240: \begin{Lemma}\label{Lemma:From-MPAR-To-M-Inf}
3241: Let $p$ \multiderparKomega{\sigma} with $p\in{}T_{PAR}$. Then,
3242: there exists in $\Re$ a derivation from $p$ of the form $p$
3243: \multider{\delta} such that \maximal{\delta} =
3244: \maximalparKomega{\sigma} and \maximalInf{\delta} =
3245: \maximalparKomegaInf{\sigma} $\cup$ \maximalparKomegaPlus{\sigma}.
3246: Moreover, if $\sigma$ is infinite or contains some occurrence of
3247: rule in $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$ then,
3248: $\delta$ is infinite.
3249: \end{Lemma}
3250:
3251: \begin{proof}
3252: For the proof we use the following property
3253: \begin{description}
3254: \item[A.] Let $p'$$\parallel$$p''$\multiderparKomega{\sigma} with $p',p''\in{}T_{PAR}$ and $p''$
3255: not
3256: containing variables in $Var$. Then
3257: $p'$ \multiderparKomega{\sigma}.
3258: \end{description}
3259: Property \textbf{A} follows easily from the observation that the
3260: left-hand side of each rule in $\Re^{K,K^{\omega}}_{PAR}$ doesn't
3261: contain occurrences of $\hat{Z}_{F}$ and
3262: $\hat{Z}_{\infty}$.\newline Let $\lambda$ be the subsequence of
3263: $\sigma$ containing all, and only, the occurrences of rules in
3264: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$. Let us assume
3265: that $\lambda$ is infinite. In similar way we reason if $\lambda$
3266: is finite. Now, $\lambda=r_{0}r_{1}r_{2}\ldots$, where
3267: $\forall{}h\in{}N$
3268: $r_{h}\in\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
3269: Moreover, $\sigma$ can be written in the form
3270: $\rho_{0}r_{0}\rho_{1}r_{1}\rho_{2}r_{2}\ldots$, where
3271: $\sigma\setminus\lambda=\rho_{0}\rho_{1}\rho_{2}\ldots$ and
3272: $\forall{}h\in{}N$ $\rho_{h}$ is a rule sequence (possibly empty)
3273: in $\Re_{PAR}^{K}$. For all $h\in{}N$ we denote by $\sigma^{h}$
3274: the suffix of
3275: $\sigma$ $\rho_{h}r_{h}\rho_{h+1}r_{h+1}\ldots$.\\
3276: Now,
3277: we prove that there exists a succession of terms in $T_{PAR}$,
3278: $(p_{h})_{h\in{N}}$, a succession of variables
3279: $(X_{h})_{h\in{}N}$ and a succession of terms $(t_{h})_{h\in{}N}$
3280: such that:
3281: \begin{description}
3282: \item[i.] $p_{0}=p$.
3283: \item[ii.] $\forall{}h\in{}N$ $p_{h}$ \multiderparKomega{\sigma^{h}}.
3284: \item[iii.] $\forall{}h\in{}N$ $p_{h}$ \multider{\eta_{h}}
3285: $p_{h+1}$$\parallel$$t_{h}$$\parallel$$X_{h}$ with \maximal{\eta_{h}} =
3286: \maximalparKomega{\rho_{h}}.
3287: \item[iv.] $\forall{}h\in{}N$ $X_{h}$ \multider{\pi_{h}}
3288: with $\pi_{h}$ infinite, \maximal{\pi_{h}} =
3289: \maximalparKomega{r_{h}} and \maximalInf{\pi_{h}} =
3290: \maximalparKomegaPlus{r_{h}}.
3291: \end{description}
3292:
3293: Setting $p_{0}=p$, property ii is satisfied for $h=0$. So, let us
3294: assume that the statement is true $\forall{}h=0,\ldots,k$. Then,
3295: it suffices to prove that
3296: \begin{description}
3297: \item[B.] there exists a $p_{k+1}\in{}T_{PAR}$, a term $t_{k}$ and a variable
3298: $X_{k}$ such that $p_{k}$ \multider{\eta_{k}}
3299: $p_{k+1}$$\parallel$$t_{k}$$\parallel$$X_{k}$, $p_{k+1}$ \multiderparKomega{\sigma^{k+1}},
3300: and $X_{k}$ \multider{\pi_{k}}
3301: with $\pi_{k}$ infinite. Moreover, \maximal{\eta_{k}} =
3302: \maximalparKomega{\rho_{k}}, \maximal{\pi_{k}} =
3303: \maximalparKomega{r_{k}} and \maximalInf{\pi_{k}} =
3304: \maximalparKomegaPlus{r_{k}}.
3305: \end{description}
3306: >From the inductive hypothesis we have $p_{k}$
3307: \multiderparKomega{\sigma^{k}}. The derivation $p_{k}$
3308: \multiderparKomega{\sigma^{k}} can be written in the form
3309: \begin{displaymath}
3310: \textrm{$p_{k}$ \multiderparKomega{\rho_{k}}
3311: $p'$$\parallel$$p''$$\parallel$$X$
3312: \onederparKomega{r_{k}} $p'$$\parallel$$p''$$\parallel$$\hat{Z}_{\infty}$
3313: \multiderparKomega{\sigma^{k+1}}}
3314: \end{displaymath}
3315: where $r_{k}=X$\Rule{K',K'^{\omega}}$\hat{Z}_{\infty}$ with
3316: $X\in{}Var$ and $K',K'^{\omega}\in{}P_{n}$. Moreover, $p'$ doesn't
3317: contain occurrences of $\hat{Z}_{F}$ and $\hat{Z}_{\infty}$, and
3318: $p''$ doesn't contain occurrences of variables in $Var$. From the
3319: definition of $\Re^{K,K^{\omega}}_{PAR}$ we have $X$
3320: \multider{\pi_{k}}
3321: with $\pi_{k}$ infinite, \maximal{\pi_{k}} $=K'$ and \maximalInf{\pi_{k}}
3322: $=K'^{\omega}$. From remark \ref{Remark:MPAR-Inf} we have
3323: \maximalparKomega{r_{k}} $=K'$ and
3324: \maximalparKomegaPlus{r_{k}} $=K'^{\omega}$.
3325: From property \textbf{A} it follows that $p'$
3326: \multiderparK{\sigma^{k+1}}. Since $\rho_{k}$ is a rule sequence
3327: in $\Re_{PAR}^{K}$, from lemma \ref{Lemma:From-MKPAR-To-M} it
3328: follows that $p_{k}$ \multider{\eta_{k}}
3329: $p'$$\parallel$$t$$\parallel$$X$ for some term $t$ and
3330: \maximal{\eta_{k}} = \maximalparK{\rho_{k}}. From remark \ref{Remark:MPAR-Inf}
3331: we deduce that \maximal{\eta_{k}} =
3332: \maximalparKomega{\rho_{k}}.
3333: Setting $p_{k+1}=p'$, $t_{k}=t$ and
3334: $X_{k}=t$ we obtain that property \textbf{B} is satisfied.\\
3335: Thus, properties i-iv are satisfied. Now, let us consider
3336: $\forall{}h\in{}N$ the infinite derivation $X_{h}$
3337: \multider{\pi_{h}}. It can be written in the form
3338: \begin{equation}
3339: \textrm{$s_{(h,0)}$ \prsoneder{r_{(h,0)}} $s_{(h,1)}$
3340: \prsoneder{r_{(h,1)}} $s_{(h,2)}\ldots$}
3341: \end{equation}
3342: where $s_{(h,0)}=X_{h}$ and $\forall{}k\in{}N$ $r_{(h,k)}\in\Re$.
3343: For all $k\in{}N$ we denote by $\overline{r}_{k}$ the rule
3344: $r_{(\ell(k),\wp(k))}$. For all $h,k\in{}N$ we denote by
3345: $s_{h}(k)$ the term $s_{next(h,k)}$. Now, we show that
3346: $\forall{}k\in{}N$ the following result holds
3347: \begin{eqnarray}
3348: \textrm{$p_{k+1}$$\parallel$$t_{0}$$\parallel$$\ldots$$\parallel$$t_{k}$$\parallel$$s_{0}(k)$$\parallel$$s_{1}(k)$$\parallel$$\ldots$$\parallel$$s_{k}(k)$
3349: \multider{\eta_{k+1}\overline{r}_{k}}}\nonumber\\
3350: \textrm{
3351: $p_{k+2}$$\parallel$$t_{0}$$\parallel$$\ldots$$\parallel$$t_{k}$$\parallel$$t_{k+1}$$\parallel$$s_{0}(k+1)$$\parallel$$s_{1}(k+1)$$\parallel$$\ldots$$\parallel$$s_{k+1}(k+1)$
3352: }
3353: \end{eqnarray}
3354: Since $\forall{}k\in{}N$ $s_{k}(k)=s_{next(k,k)}$, from property 1
3355: of lemma \ref{Lemma:next} it follows that
3356: $s_{k}(k)=s_{(k,0)}=X_{k}$. From iii we deduce that
3357: \begin{eqnarray}
3358: \textrm{$p_{k+1}$$\parallel$$t_{0}$$\parallel$$\ldots$$\parallel$$t_{k}$$\parallel$$s_{0}(k)$$\parallel$$s_{1}(k)$$\parallel$$\ldots$$\parallel$$s_{k}(k)$
3359: \multider{\eta_{k+1}}}\nonumber\\
3360: \textrm{
3361: $p_{k+2}$$\parallel$$t_{0}$$\parallel$$\ldots$$\parallel$$t_{k}$$\parallel$$t_{k+1}$$\parallel$$s_{0}(k)$$\parallel$$s_{1}(k)$$\parallel$$\ldots$$\parallel$$s_{k}(k)$$\parallel$$s_{k+1}(k+1)$
3362: }
3363: \end{eqnarray}
3364: So, to obtain (2) it suffices to prove that
3365: \begin{equation}
3366: \textrm{$s_{0}(k)$$\parallel$$s_{1}(k)$$\parallel$$\ldots$$\parallel$$s_{k}(k)$
3367: \prsoneder{\overline{r}_{k}}
3368: $s_{0}(k+1)$$\parallel$$s_{1}(k+1)$$\parallel$$\ldots$$\parallel$$s_{k}(k+1)$
3369: }
3370: \end{equation}
3371: >From property 6 of lemma \ref{Lemma:next} $\forall{}k\in{}N$
3372: $next(\ell(k),k)=(\ell(k),\wp(k))$. Moreover,
3373: $next(\ell(k),k+1)=(\ell(k),\wp(k)+1)$. Therefore, we have
3374: $s_{\ell(k)}(k)=s_{(\ell(k),\wp(k))}$ \prsoneder{\overline{r}_{k}}
3375: $s_{(\ell(k),\wp(k)+1)}=s_{\ell(k)}(k+1)$. From property 7 of
3376: lemma \ref{Lemma:next} $\forall{}i\neq{}\ell(k)$
3377: $next(i,k+1)=next(i,k)$. So, $\forall{}i\neq{}\ell(k)$
3378: $s_{i}(k+1)=s_{i}(k)$. Since $\ell(k)\leq{}k$, we obtain
3379: evidently (4). So, (2) is satisfied $\forall{}k\in{}N$. Moreover,
3380: since $s_{0}(0)=X_{0}$, we have
3381: \begin{equation}
3382: \textrm{$p=p_{0}$ \multider{\eta_{0}}
3383: $p_{1}$$\parallel$$t_{0}$$\parallel$$s_{0}(0)$
3384: }
3385: \end{equation}
3386: Setting
3387: $\delta=\eta_{0}\eta_{1}\overline{r}_{0}\eta_{2}\overline{r}_{1}\eta_{3}\overline{r}_{2}\ldots$,
3388: from (2) and (5) we obtain that $p$ \multider{\delta} with
3389: $\delta$ infinite. So, to obtain the assertion it remains to prove
3390: that \maximal{\delta} = \maximalparKomega{\sigma} and
3391: \maximalInf{\delta} = \maximalparKomegaInf{\sigma} $\cup$
3392: \maximalparKomegaPlus{\sigma}. Let
3393: $\mu=\overline{r}_{0}\overline{r}_{1}\overline{r}_{2}\ldots$. Let
3394: us observe that $\mu\in{}Interleaving(\{\pi_{h}\})$.
3395: From iii-iv, propositions \ref{Prop:Maximal} and \ref{Prop:MaximalInterleaving},
3396: and remembering that
3397: $\sigma=\rho_{0}r_{0}\rho_{1}r_{1}\ldots$, we obtain
3398: \begin{displaymath}
3399: \textrm{\maximal{\delta} = $\bigcup_{h\in{}N}$\maximal{\eta_{h}}
3400: $\cup$ \maximal{\mu} =
3401: $\bigcup_{h\in{}N}$\maximalparKomega{\rho_{h}} $\cup$
3402: $\bigcup_{h\in{}N}$\maximal{\pi_{h}}
3403: =}
3404: \end{displaymath}
3405: \begin{displaymath}
3406: \textrm{$\bigcup_{h\in{}N}$\maximalparKomega{\rho_{h}} $\cup$
3407: $\bigcup_{h\in{}N}$\maximalparKomega{r_{h}} =
3408: \maximalparKomega{\sigma}.}
3409: \end{displaymath}
3410: >From remark \ref{Remark:MPAR-Inf}, $\forall{}r\in\Re_{PAR}^{K}$
3411: \maximalparKomegaPlus{r} = $\emptyset$. Remembering that
3412: $\lambda=r_{0}r_{1}r_{2}\ldots$, from iii-iv and propositions
3413: \ref{Prop:Maximal}, \ref{Prop:MaximalInterleaving} we obtain
3414: \begin{displaymath}
3415: \textrm{\maximalInf{\delta} =
3416: $\bigoplus_{h\in{}N}$\maximal{\eta_{h}} $\cup$ \maximalInf{\mu} =
3417: $\bigoplus_{h\in{}N}$\maximalparKomega{\rho_{h}} $\cup$
3418: $\bigcup_{h\in{}N}$\maximalInf{\pi_{h}} $\cup$
3419: $\bigoplus_{h\in{}N}$\maximal{\pi_{h}}
3420: =}
3421: \end{displaymath}
3422: \begin{displaymath}
3423: \textrm{\maximalparKomegaInf{\sigma\setminus\lambda} $\cup$
3424: $\bigcup_{h\in{}N}$\maximalparKomegaPlus{r_{h}} $\cup$
3425: $\bigoplus_{h\in{}N}$\maximalparKomega{r_{h}} = }
3426: \end{displaymath}
3427: \begin{displaymath}
3428: \textrm{\maximalparKomegaInf{\sigma\setminus\lambda} $\cup$
3429: \maximalparKomegaPlus{\sigma} $\cup$ \maximalparKomegaInf{\lambda}
3430: = \maximalparKomegaInf{\sigma} $\cup$
3431: \maximalparKomegaPlus{\sigma}.}
3432: \end{displaymath}
3433: This concludes the proof.
3434: \end{proof}
3435:
3436:
3437: \setcounter{equation}{0}
3438: \begin{Lemma}\label{Lemma:From-MKSEQ-To-M}
3439: Let $t,t'\in{}T_{SEQ}$ and $s$ be any term in $T$ such that
3440: $t\in{}SEQ(s)$. The following results hold
3441: \begin{enumerate}
3442: \item If $t$ \onederseqK{r} $t'$, then
3443: there exists a $s'\in{}T$ with $t'\in{}SEQ(s')$ such that $s$ \multider{\sigma} $s'$,
3444: with \maximal{\sigma} = \maximalseqK{r} and $|\sigma|>0$.
3445: \item If $t$ \multiderseqK{\sigma} $t'$ with $t\neq\varepsilon$,
3446: then there exists a $s'\in{}T$ with $t'\in{}SEQ(s')$ such that $s$
3447: \multider{\rho} $s'$, with \maximal{\rho} =
3448: \maximalseqK{\sigma}, and $|\rho|>0$ if $|\sigma|>0$.
3449: \item If $t$ \multiderseqK{\sigma} is a $(K,K^{\omega})$-accepting infinite derivation in
3450: $M_{SEQ}^{K}$ from $t\in{}T_{SEQ}$, then there exists a $(K,K^{\omega})$-accepting infinite derivation
3451: in $M$ from s.
3452: \end{enumerate}
3453: \end{Lemma}
3454: \begin{proof}
3455: At first, we prove property 1. We use the following properties,
3456: whose proof is immediate. Let $t\in{}SEQ(s)$,
3457: $s\in{}T$ and $t=X_{1}.(X_{2}.(\ldots{}X_{n}.(Y)\ldots))$, with
3458: $n\geq0$. Then
3459: \begin{description}
3460: \item[A.] if
3461: $st\in{}T_{SEQ}\setminus\{\varepsilon\}$ and
3462: $t'=X_{1}.(X_{2}.(\ldots{}X_{n}.(st)\ldots))$, then there
3463: exists a
3464: $s'\in{}s[Y\rightarrow{}st]$
3465: (notice that $Y$ is a subterm of $s$) such that $t'\in{}SEQ(s')$.
3466: \item[B.] if $Z\in{}Var$, $st'\in{}T$ and
3467: $st=st'$$\parallel$$Z$, then
3468: there exists a $s'\in{}s[Y\rightarrow{}st]$
3469: such that
3470: $X_{1}.(X_{2}.(\ldots{}X_{n}.(Z)\ldots))$ $\in{}SEQ(s')$.
3471: \end{description}
3472: We can, now, distinguish the following two cases:
3473: \begin{itemize}
3474: \item $r=Y$\Rule{a}$Z_{1}.(Z_{2})\in{}\Re$. From remark \ref{Remark:MKSEQ}
3475: \maximal{r} = \maximalseqK{r}. Moreover,
3476: $t=X_{1}.(X_{2}.(\ldots{}X_{n}.(Y)\ldots))$ and $t'=X_{1}.(X_{2}.(\ldots{}X_{n}$
3477: $.(Z_{1}.(Z_{2}))\ldots))$.
3478: Let $s\in{}T$ be such that $t\in{}SEQ(s)$. From \textbf{A} above,
3479: there exists a $s'\in{}s[Y\rightarrow{}Z_{1}.(Z_{2})]$
3480: such that $t'\in{}SEQ(s')$. Since $Y$ \prsoneder{r}
3481: $Z_{1}.(Z_{2})$,
3482: by proposition \ref{Prop:Subterms1} it follows that $s$ \prsoneder{r} $s'$, and the
3483: thesis is proved.
3484: \item $r=Y$\Rule{K'}$Z$ with $Y,Z\in{}Var$ and
3485: \maximalseqK{r} = $K'$. Moreover, $t=X_{1}.(X_{2}.(\ldots{}$
3486: $X_{n}.(Y)\ldots))$
3487: and $t'=X_{1}.(X_{2}.(\ldots{}X_{n}.(Z)\ldots))$.
3488: From the definition of $\Re^{K}_{SEQ}$ there exists a derivation
3489: in
3490: $\Re^{K}_{PAR}$ of the form $Y$ \multiderparK{\sigma} $p$$\parallel$$Z$
3491: for some
3492: $p\in{}T_{PAR}$, with \maximalparK{\sigma} = \maximalseqK{r} and
3493: $|\sigma|>0$.
3494: From lemma \ref{Lemma:From-MKPAR-To-M} there exists a term
3495: $st$ such that $Y$ \multider{\rho} $st$$\parallel$$Z$ with
3496: \maximal{\rho} = \maximalparK{\sigma} and $|\rho|>0$. So, \maximal{\rho} = \maximalseqK{r}.
3497: Let $s\in{}T$ be
3498: such that
3499: $t\in{}SEQ(s)$. From property \textbf{B} above, there exists a
3500: $s'\in{}s[Y\rightarrow{}st$$\parallel$$Z]$
3501: such that
3502: $t'\in{}SEQ(s')$.
3503: Since $Y$ \multider{\rho} $st$$\parallel$$Z$,
3504: by proposition \ref{Prop:Subterms1} we conclude that $s$ \multider{\rho} $s'$
3505: with $|\rho|>0$. Hence, the thesis.
3506: \end{itemize}
3507: Property 2 can be easily proved by induction on the length of
3508: $\sigma$, and using property 1. It remains to prove property 3.
3509: The infinite derivation $t$
3510: \multiderseqK{\sigma} can be written in the form
3511: \begin{displaymath}
3512: \textrm{$t_{0}$ \onederseqK{r_{0}} $t_{1}$ \onederseqK{r_{1}}
3513: $t_{2}$ \onederseqK{r_{2}} $\ldots$}
3514: \end{displaymath}
3515: where $t_{0}=t$ and $\forall{}i\in{}N$ $r_{i}\in{}\Re_{SEQ}^{K}$.
3516: Let $s\in{}T$ such that $t\in{}SEQ(s)$. From property 1 there
3517: exists a $s_{1}\in{}T$ with $t_{1}\in{}SEQ(s_{1})$ such that $s$
3518: \multider{\lambda_{0}} $s_{1}$ with \maximal{\lambda_{0}} =
3519: \maximalseq{r_{0}} and $|\lambda_{0}|>0$. Iterating such reasoning
3520: we deduce that there exists a succession of terms,
3521: $(s_{h})_{h\in{}N}$, such that for all $h\in{}N$
3522: \begin{displaymath}
3523: \textrm{ $s_{h}$ \multider{\lambda_{h}} $s_{h+1}$ with
3524: \maximal{\lambda_{h}} = \maximalseqK{r_{h}}, $|\lambda_{h}|>0$ and
3525: $s_{0}=s$.}
3526: \end{displaymath}
3527: Therefore,
3528: \begin{displaymath}
3529: \textrm{$s=s_{0}$ \multider{\lambda_{0}} $s_{1}$
3530: \multider{\lambda_{1}}$\ldots$ $s_{h}$ \multider{\lambda_{h}}
3531: $s_{h+1}\ldots$}
3532: \end{displaymath}
3533: Let $\rho=\lambda_{0}\lambda_{1}\lambda_{2}\ldots$. So, $s$
3534: \multider{\rho}
3535: is an infinite derivation in $\Re$ from $s$ with $t\in{}SEQ(s)$. Moreover, by
3536: proposition \ref{Prop:Maximal} we
3537: obtain
3538: \begin{displaymath}
3539: \textrm{\maximal{\rho} = $\bigcup_{h\in{}N}$ \maximal{\lambda_{h}}
3540: = $\bigcup_{h\in{}N}$ \maximalseqK{r_{h}} = \maximalseqK{\sigma} =
3541: $K$. }
3542: \end{displaymath}
3543: \begin{displaymath}
3544: \textrm{\maximalInf{\rho} = $\bigoplus_{h\in{}N}$
3545: \maximal{\lambda_{h}} = $\bigoplus_{h\in{}N}$ \maximalseqK{r_{h}}
3546: = \maximalseqInfK{\sigma} = $K^{\omega}$. }
3547: \end{displaymath}
3548: This proves the thesis.
3549: \end{proof}
3550:
3551:
3552:
3553:
3554: \setcounter{equation}{0}
3555:
3556: \begin{Proposition}\label{Prop:Interleaving}
3557: Let $\sigma$ be a rule sequence in $\Re$ and
3558: $\{\rho_{h}\}_{h\in{}N}$ be a succession of subsequences of
3559: $\sigma$ two by two disjoints and such that
3560: $\bigcup_{h\in{}N}pr(\rho_{h})=pr(\sigma)$. Then,
3561: $\sigma\in{}Interleaving(\{\rho_{h}\})$.
3562: \end{Proposition}
3563: \begin{proof}
3564: Setting $\Delta=\bigcup_{h\in{}N}(\{h\}\times{}pr(\rho_{h}))$, let
3565: us consider the following mapping
3566: \begin{displaymath}
3567: M_{\sigma}: (h,n)\in{}\Delta\rightarrow{}n
3568: \end{displaymath}
3569: Since for all $h,h'\in{}N$ with $h\neq{}h'$ we have
3570: $pr(\rho_{h})\cap{}pr(\rho_{h'})=\emptyset$, it follows that
3571: $M_{\sigma}$ is an injective mapping. Let us observe that
3572: $M_{\sigma}(h,n_{1})<M_{\sigma}(h,n_{2})$ if $n_{1}<n_{2}$.
3573: Moreover, $pr(\sigma)=M_{\sigma}(\Delta)$, and
3574: $\forall{}(h,n)\in\Delta$ we have
3575: $\sigma(M_{\sigma}(h,n))=\sigma(n)=\rho_{h}(n)$. From definition
3576: \ref{Def:Interleaving} we obtain the assertion.
3577: \end{proof}
3578:
3579: \begin{Lemma}\label{Lemma:From-M-To-MPAROMEGA}
3580: Let $p$ \multider{\sigma}$ $ be a $(\overline{K},\overline{K}^{\omega})$-accepting
3581: non--null derivation in $M$ belonging to
3582: $\Pi^{K,K^{\omega}}_{PAR,\infty}$,
3583: with $p\in{}T_{PAR}$, $\overline{K}\subseteq{}K$ and
3584: $\overline{K}^{\omega}\subseteq{}K^{\omega}$. Then,
3585: there exists a derivation $p$ \multiderparKomega{\rho} in $\Re^{K,K^{\omega}}_{PAR}$
3586: from $p$ such that
3587: \begin{description}
3588: \item[a] \maximalparKomega{\rho} = $\overline{K}$
3589: \item[b]
3590: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} = $\overline{K}^{\omega}$
3591: \item[c] If $\sigma$ is infinite then, either $\rho$ is
3592: infinite or $\rho$ contains some occurrence of rule in
3593: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
3594: \end{description}
3595: \end{Lemma}
3596: \begin{proof}
3597:
3598: \noindent{}At first, let us prove the following property
3599: \begin{description}
3600: \item[d] There exists a $p'\in{}T_{PAR}$, a non empty finite rule
3601: sequence $\lambda$ in $\Re^{K,K^{\omega}}_{PAR}$, and a non
3602: empty subsequence $\eta$ (possibly infinite) of $\sigma$ such that:
3603: \begin{enumerate}
3604: \item $min(pr(\eta))=min(pr(\sigma))$ (i.e. the first rule
3605: occurrence in $\eta$ is the first rule occurrence in
3606: $\sigma$).
3607: \item $p$ \multiderparKomega{\lambda} $p'$
3608: \item \maximalparKomega{\lambda} = \maximal{\eta}
3609: \item \maximalparKomegaPlus{\lambda} = \maximalInf{\eta}
3610: \item $p'$ \multider{\sigma\setminus\eta}, and this derivation
3611: is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
3612: \item If $\sigma$ is infinite then, either $\sigma\setminus\eta$
3613: is infinite or $\lambda$ is a rule in $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
3614: \end{enumerate}
3615: \end{description}
3616:
3617: Now, let us show that from property \textbf{d} the thesis follows.
3618: So, let us assume that property \textbf{d} is satisfied. Since
3619: $\sigma\setminus\eta$ is a subsequence of $\sigma$, we have
3620: \maximal{\sigma\setminus\eta} $\subseteq{}K$ and
3621: \maximalInf{\sigma\setminus\eta} $\subseteq{}K^{\omega}$. Thus, if
3622: $\sigma\neq\eta$ we can apply property \textbf{d} to the
3623: derivation $p'$ \multider{\sigma\setminus\eta}. Iterating this
3624: reasoning it follows that there exists a $m\in{}N\cup\{\infty\}$,
3625: a succession $\{p_{h}\}_{h=0}^{m+1}$ of terms in $T_{PAR}$, a
3626: succession $\{\lambda_{h}\}_{h=0}^{m}$ of non empty finite rule
3627: sequences in $\Re^{K,K^{\omega}}_{PAR}$, two successions
3628: $\{\sigma_{h}\}_{h=0}^{m}$ and $\{\eta_{h}\}_{h=0}^{m}$ of non
3629: empty rule sequences in $\Re$ such that
3630: \begin{enumerate}
3631: \item[7.] $p=p_{0}$ and $\sigma=\sigma_{0}$.
3632: \item[8.] for all $h=0,\ldots,m\quad$ $\eta_{h}$ is a subsequence of
3633: $\sigma_{h}$ and $min(pr(\eta_{h}))=min(pr(\sigma_{h}))$.
3634: \item[9.] for all $h=0,\ldots,m-1\quad$
3635: $\sigma_{h+1}=\sigma_{h}\setminus\eta_{h}$.
3636: \item[10.] for all $h=0,\ldots,m\quad$
3637: $p_{h}$ \multiderparKomega{\lambda_{h}} $p_{h+1}$.
3638: \item[11.] for all $h=0,\ldots,m\quad$
3639: \maximalparKomega{\lambda_{h}} = \maximal{\eta_{h}} and
3640: \maximalparKomegaPlus{\lambda_{h}} = \maximalInf{\eta_{h}}
3641: \item[12.] for all $h=1,\ldots,m\quad$ $p_{h}$
3642: \multider{\sigma_{h}}.
3643: \item[13.] If $m$ is finite then, $\sigma_{m}=\eta_{m}$.
3644: \item[14.] If $\sigma$ is infinite then, either $m$ is infinite or
3645: there exists an $h$ such that $\lambda_{h}$ is a rule in
3646: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
3647: \end{enumerate}
3648: \noindent{}By setting $\rho=\lambda_{0}\lambda_{1}\ldots$ we have
3649: that $p$ \multiderparKomega{\rho}. From property 14 it follows
3650: that if $\sigma$ is infinite then, either $\rho$ is infinite or
3651: $\rho$ contains some occurrence of rule in
3652: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$. So, property
3653: \textbf{c} is satisfied. It remains to prove properties
3654: \textbf{a} and \textbf{b}. Let us assume that $m=\infty$. The
3655: proof in the case where $m$ is finite is simpler. From properties
3656: 7-9 $\eta_{0},\eta_{1},\ldots$ are non empty subsequences of
3657: $\sigma$ two by two disjoints. Since $\sigma$ is infinite, we can
3658: assume that $pr(\sigma)=N$. Now, let us show that
3659: \begin{enumerate}
3660: \item[15.] $\sigma\in{}Interleaving(\{\eta_{h}\})$
3661: \end{enumerate}
3662: >From proposition \ref{Prop:Interleaving} it suffices to prove that
3663: $\forall{}h\in{}N$ there exists a $i\in{}N$ such that
3664: $h\in{}pr(\eta_{i})$. From properties 8-9 it follows that
3665: $\forall{}h\in{}N$ $min(pr(\sigma_{h}))< min(pr(\sigma_{h+1}))$.
3666: Let $h\in{}N$, then there exists the smallest $i\in{}N$ such that
3667: $h\notin{}pr(\sigma_{i})$. Since $\sigma_0=\sigma$, $i>0$ and
3668: $h\in{}pr(\sigma_{i-1})$. Since
3669: $\sigma_{i}=\sigma_{i-1}\setminus\eta_{i-1}$,
3670: $h\notin{}pr(\sigma_{i})$ and $h\in{}pr(\sigma_{i-1})$, it follow
3671: that
3672: $h\in{}pr(\eta_{i-1})$. Thus, property 15 holds.\\
3673: >From properties 11, 15, and propositions \ref{Prop:Maximal} and
3674: \ref{Prop:MaximalInterleaving} it follows that
3675: \begin{displaymath}
3676: \textrm{\maximalparKomega{\rho} $=$
3677: $\bigcup_{h\in{}N}$\maximalparKomega{\lambda_{h}} $=$
3678: $\bigcup_{h\in{}N}$\maximal{\eta_{h}} $=$ \maximal{\sigma} $=$
3679: $\overline{K}$.}
3680: \end{displaymath}
3681: Therefore, property \textbf{a} holds. Moreover,
3682: \begin{displaymath}
3683: \textrm{\maximalparKomegaInf{\rho} $\cup$
3684: \maximalparKomegaPlus{\rho} $=$
3685: $\bigoplus_{h\in{}N}$\maximalparKomega{\lambda_{h}} $\cup$
3686: $\bigcup_{h\in{}N}$\maximalparKomegaPlus{\lambda_{h}} =}
3687: \end{displaymath}
3688: \begin{displaymath}
3689: \textrm{$\bigoplus_{h\in{}N}$\maximal{\eta_{h}} $\cup$
3690: $\bigcup_{h\in{}N}$\maximalInf{\eta_{h}} $=$ \maximalInf{\sigma}
3691: $=$ $\overline{K}^{\omega}$.}
3692: \end{displaymath}
3693: Therefore,
3694: property \textbf{b} is satisfied.\\
3695: \noindent{}At this point, it remains to prove property \textbf{d}. The derivation
3696: $p$ \multider{\sigma} can be written in the form
3697: \begin{equation}
3698: \textrm{$p$ \prsoneder{r} $t$ \multider{\sigma'}}
3699: \end{equation}
3700: Since each subderivation of $t$ \multider{\sigma'} is also a
3701: subderivation of $p$ \multider{\sigma}, it follows that $t$
3702: \multider{\sigma'} is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
3703: There are two cases:
3704: \begin{enumerate}
3705: \item r is a PAR rule. Then, we have that $t\in{}T_{PAR}$ and
3706: $r\in\Re^{K,K^{\omega}}_{PAR}$. From remark \ref{Remark:MPAR-Inf}
3707: \maximalparKomega{r} = \maximal{r}, and
3708: \maximalparKomegaPlus{r} = $\emptyset$ = \maximalInf{r}.
3709: Moreover,
3710: $t$ \multider{\sigma'}
3711: is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$ with
3712: $\sigma'=\sigma\setminus{}r$.
3713: Thus, since $\sigma'$ is infinite if $\sigma$ is infinite,
3714: property \textbf{d} follows, setting $p'=t$, $\lambda=r$ and
3715: $\eta=r$.
3716: \item $r=Z$\Rule{a}$Y.(Z')$. So, $p=p''$$\parallel$$Z$ and
3717: $t=p''$$\parallel$$Y.(Z')$ with $p''\in{}T_{PAR}$.
3718: From (1), let $Z'$ \multider{\nu} a subderivation of $t=p''$$\parallel$$Y.(Z')$
3719: \multider{\sigma'} from $Z'$. From lemma \ref{Lemma:Subderivations1} we can
3720: distinguish four subcases:
3721: \begin{itemize}
3722: \item $Z'$ \multider{\nu} is infinite,
3723: and $p''$ \multider{\sigma'\setminus\nu}.
3724: Moreover, $p''$ \multider{\sigma'\setminus\nu}
3725: is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
3726: Clearly, for every $\overline{p}\in{}T_{PAR}$
3727: we have that $p''$$\parallel$$\overline{p}$
3728: \multider{\sigma'\setminus\nu}, and this derivation
3729: belongs to $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
3730: From hypothesis, we have that
3731: $($\maximal{\nu},\maximalInf{\nu}$)\neq(K,K^{\omega})$,
3732: \maximal{\nu} $\subseteq{}K$ and
3733: \maximalInf{\nu} $\subseteq{}K^{\omega}$.
3734: Hence, $|$\maximal{\nu}$|+|$\maximalInf{\nu}$|<|K|+|K^{\omega}|$.
3735: Moreover, $r=Z$\Rule{a}$Y.(Z')$ with \maximal{r} $\subseteq{}K$.
3736: From the definition of $\Re^{K,K^{\omega}}_{PAR}$, it follows that
3737: $r'=Z$\Rule{K_{1},K^{\omega}_{1}}$\hat{Z}_{\infty}\in\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$
3738: where $K_{1}$ = \maximal{\nu} $\cup$ \maximal{r} and
3739: $K^{\omega}_{1}$ = \maximalInf{\nu}.
3740: From remark \ref{Remark:MPAR-Inf}, we have that
3741: \maximalparKomega{r'} = $K_{1}$ and \maximalparKomegaPlus{r'} = $K^{\omega}_{1}$.
3742: Therefore, we deduce that $p=p''$$\parallel$$Z$
3743: \onederparKomega{r'}
3744: $p''$$\parallel$$\hat{Z}_{\infty}$.
3745: Moreover, $p''$$\parallel$$\hat{Z}_{\infty}$
3746: \multider{\sigma'\setminus\nu} and this derivation is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
3747: Since
3748: $\sigma'\setminus\nu=\sigma\setminus{}r\nu$ and
3749: \maximalparKomegaPlus{r'} = \maximalInf{\nu} = \maximalInf{r\nu},
3750: property \textbf{d} follows, setting
3751: $p'=p''$$\parallel$$\hat{Z}_{\infty}$, $\lambda=r'$ and
3752: $\eta=r\nu$.
3753: \item $Z'$ \multider{\nu} leads to a term $t_{1}\neq\varepsilon$,
3754: and $p''$ \multider{\sigma'\setminus\nu}. Moreover, $p''$ \multider{\sigma'\setminus\nu}
3755: is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
3756: Since \maximal{\nu} $\subseteq$ $K$, from lemma
3757: \ref{Lemma:From-M-To-MKPAR} there exists a
3758: $\overline{p}\in{}T_{PAR}$ such that
3759: $Z'$ \multiderparK{\gamma} $\overline{p}$, where
3760: \maximalparK{\gamma} = \maximal{\nu}.
3761: Since \maximal{r} $\subseteq$ $K$, from the
3762: definition of $\Re_{PAR}^{K}$ it follows that
3763: $r'=Z$\Rule{K'}$\hat{Z}_{F}\in\Re_{PAR}^{K}$
3764: with \maximalparK{r'} = $K'$, where
3765: $K'=$ \maximal{r\nu}. By construction
3766: $r'\in\Re^{K,K^{\omega}}_{PAR}$, and
3767: from remark \ref{Remark:MPAR-Inf} \maximalparKomega{r'} = $K'$ and
3768: \maximalparKomegaPlus{r'} = $\emptyset$. Since
3769: $\sigma'\setminus\nu=\sigma\setminus{}r\nu$,
3770: \maximalparKomegaPlus{r'} =
3771: $\emptyset$ = \maximalInf{r\nu}, and $\sigma'\setminus\nu$ is infinite if
3772: $\sigma$ is infinite,
3773: property \textbf{d} follows, setting
3774: $p'=p''$$\parallel$$\hat{Z}_{F}$, $\lambda=r'$ and
3775: $\eta=r\nu$.
3776: \item $Z'$ \multider{\nu} leads to $\varepsilon$ and the derivation $p''$$\parallel$$Y.(Z')$
3777: \multider{\sigma'} can be written in the
3778: following form
3779: \begin{equation}
3780: \textrm{$p''$$\parallel$$Y.(Z')$
3781: \multider{\sigma_{1}} $t'$$\parallel$$Y$
3782: \multider{\sigma_{2}} $\quad$
3783: with $p''$ \multider{\sigma'_{1}} $t'$ and
3784: $\sigma_{1}\in{}Interleaving(\nu,\sigma'_{1})$ }
3785: \end{equation}
3786: Moreover, $p''$$\parallel$$Y$
3787: \multider{\sigma'_{1}} $t'$$\parallel$$Y$
3788: \multider{\sigma_{2}} and this derivation is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
3789: Since $Z'$ \multider{\nu} $\varepsilon$ and
3790: \maximal{\nu} $\subseteq$ $K$, from lemma
3791: \ref{Lemma:From-M-To-MKPAR}
3792: $Z'$ \multiderparK{\chi}
3793: $\varepsilon$ with
3794: \maximalparK{\chi} = \maximal{\nu}.
3795: Since $r=Z$\Rule{a}$Y.(Z')$ with \maximal{r} $\subseteq$
3796: $K$, from the definition of $\Re_{PAR}^{K}$ it
3797: follows that $r'=Z$\Rule{K'}$Y\in\Re_{PAR}^{K}$
3798: where
3799: $K'=$ \maximal{r\nu} and
3800: \maximalparK{r'} = $K'$.
3801: By construction
3802: $r'\in\Re^{K,K^{\omega}}_{PAR}$, and
3803: from remark \ref{Remark:MPAR-Inf} \maximalparKomega{r'} = $K'$ and
3804: \maximalparKomegaPlus{r'} = $\emptyset$.
3805: Since
3806: $\sigma\setminus{}r\nu=\sigma'_{1}\sigma_{2}$,
3807: \maximalparKomegaPlus{r'} =
3808: $\emptyset$ = \maximalInf{r\nu} , and $\sigma'_{1}\sigma_{2}$ is
3809: infinite if $\sigma$ is infinite,
3810: property \textbf{d} follows, setting
3811: $p'=p''$$\parallel$$Y$, $\lambda=r'$ and
3812: $\eta=r\nu$.
3813: \item
3814: $Z'$ \multider{\nu} leads to a variable $W\in{}Var$ and the derivation
3815: $p''$$\parallel$$Y.(Z')$
3816: \multider{\sigma'} can be written in the
3817: following form
3818: \begin{eqnarray}
3819: \textrm{$p''$$\parallel$$Y.(Z')$
3820: \multider{\sigma_{1}} $t'$$\parallel$$Y.(W)$
3821: \prsoneder{r'} $t'$$\parallel$$W'$ \multider{\sigma_{2}}}\\
3822: \textrm{with $p''$ \multider{\sigma'_{1}} $t'$,
3823: $r'=Y.(W)$\Rule{b}$W'$ and
3824: $\sigma_{1}\in{}Interleaving(\lambda,\sigma'_{1})$}
3825: \end{eqnarray}
3826: Moreover, $p''$$\parallel$$W'$
3827: \multider{\sigma'_{1}} $t'$$\parallel$$W'$
3828: \multider{\sigma_{2}} and this derivation is in $\Pi^{K,K^{\omega}}_{PAR,\infty}$.
3829: Since $Z'$ \multider{\nu} $W$
3830: and
3831: \maximal{\nu} $\subseteq$ $K$, from lemma
3832: \ref{Lemma:From-M-To-MKPAR} we have that $Z'$ \multiderparK{\chi}
3833: $W$ with
3834: \maximalparK{\chi} = \maximal{\nu}.
3835: Since $r=Z$\Rule{a}$Y.(Z')\in\Re$ and
3836: $r'=Y.(W)$\Rule{a}$W'\in\Re$, where \maximal{r} $\subseteq$
3837: $K$ and
3838: \maximal{r'} $\subseteq$ $K$, from the definition of
3839: $\Re_{PAR}^{K}$ it follows that
3840: $r''=Z$\Rule{K'}$W'\in\Re_{PAR}^{K}$
3841: where
3842: $K'=$ \maximal{rr'} $\cup{}$ \maximalpar{\chi} = \maximal{r\nu{}r'} and
3843: \maximalparK{r''} = $K'$. By construction,
3844: $r''\in\Re^{K,K^{\omega}}_{PAR}$, and
3845: from remark \ref{Remark:MPAR-Inf} \maximalparKomega{r''} = $K'$ and
3846: \maximalparKomegaPlus{r''} = $\emptyset$.
3847: Since
3848: $\sigma\setminus{}r\nu{}r'=\sigma'_{1}\sigma_{2}$,
3849: \maximalparKomegaPlus{r''} = $\emptyset$ = \maximalInf{r\nu{}r'},
3850: and $\sigma'_{1}\sigma_{2}$ is
3851: infinite if $\sigma$ is infinite,
3852: property \textbf{d} follows setting
3853: $p'=p''$$\parallel$$W'$, $\lambda=r''$ and
3854: $\eta=r\nu{}r'$.
3855: \end{itemize}
3856: \end{enumerate}
3857: \end{proof}
3858:
3859:
3860: \noindent{}Now, let us assume that $K\neq{}K^{\omega}$. Then, the
3861: following result holds.
3862:
3863: \begin{Lemma}\label{Lemma:From-M-To-MSEQ1}
3864: Let us assume that $K\neq{}K^{\omega}$. Given a variable
3865: $X\in{}Var$ and a
3866: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
3867: $X$, the following property is satisfied:
3868: \begin{enumerate}
3869: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
3870: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
3871: with $K'\subseteq{}K$, and there exists a derivation
3872: $Y$ \multiderparKomega{\rho}
3873: such that \maximalparKomega{\rho} = $K$
3874: and
3875: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
3876: $K^{\omega}$. Moreover, either $\rho$ is
3877: infinite or $\rho$ contains some occurrence of rule in
3878: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
3879: \end{enumerate}
3880: \end{Lemma}
3881: \begin{proof}
3882: Since $K\neq{}K^{\omega}$ and $K\supseteq{}K^{\omega}$, it follows
3883: that $K\supset{}K^{\omega}$.
3884: Let $d=X$ \multider{\sigma} be
3885: a $(K,K^{\omega})$-accepting infinite derivation in $M$ from
3886: $X$. Evidently,
3887: $K\setminus{}K^{\omega}=\{i\in\{1,\ldots,n\}|$ $\sigma$ contains a
3888: finite non--null number of occurrences of rules in
3889: $\Re_{i}^{A}\}$. Then, for all $i\in{}K\setminus{}K^{\omega}$ it's
3890: defined the greatest application level, denoted by $h_{i}(d)$, of
3891: occurrences of rules of $\Re_{i}^{A}$ in the derivation $d$. The
3892: proof is by induction on
3893: $max_{i\in{}K\setminus{}K^{\omega}}\{h_{i}(d)\}$.\\
3894: \textbf{Base Step}:
3895: $max_{i\in{}K\setminus{}K^{\omega}}\{h_{i}(d)\}=0$. In this case
3896: it follows that each subderivation of $d=X$ \multider{\sigma}
3897: does not contain occurrences of rules in
3898: $\bigcup_{i\in{}K\setminus{}K^{\omega}}\Re_{i}^{A}$. So, $d$ is
3899: belonging to
3900: $\Pi^{K,K^{\omega}}_{PAR,\infty}$. Then, from lemma
3901: \ref{Lemma:From-M-To-MPAROMEGA} we obtain the assertion
3902: setting $Y=X$.\\
3903: \textbf{Induction Step}: $max_{i\in{}K\setminus{}K^{\omega}}\{h_{i}(d)\}>0$. If
3904: $d=X$ \multider{\sigma} is in
3905: $\Pi^{K,K^{\omega}}_{PAR,\infty}$, from lemma
3906: \ref{Lemma:From-M-To-MPAROMEGA} we obtain the assertion setting
3907: $Y=X$. Otherwise, from lemma \ref{Lemma:Base} it follows that the
3908: derivation $X$ \multider{\sigma} can be written in the form
3909: \begin{displaymath}
3910: \textrm{$X$ \multider{\sigma_{1}} $t$$\parallel$$Z$ \prsoneder{r}
3911: $t$$\parallel$$Y.(Z')$ \multider{\sigma_{2}}}
3912: \end{displaymath}
3913: where $r=Z$\Rule{a}$Y.(Z')$, and there exists a subderivation of
3914: $t$$\parallel$$Y.(Z')$ \multider{\sigma_{2}} from $Z'$, namely
3915: $d'=Z'$ \multider{\sigma_{2}'}, that is a
3916: $(K,K^{\omega})$-accepting infinite derivation in $M$. Evidently,
3917: $max_{i\in{}K\setminus{}K^{\omega}}\{h_{i}(d')\}<max_{i\in{}K\setminus{}K^{\omega}}\{h_{i}(d)\}$.
3918: By inductive hypothesis, the thesis holds for the derivation $d'$.
3919: Therefore, it suffices to prove that $Z'$ is reachable from $X$ in
3920: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
3921: with $K'\subseteq{}K$. From lemma \ref{Lemma:From-M-To-MKPAR}, applied to
3922: the derivation $X$ \multider{\sigma_{1}} $t$$\parallel$$Z$
3923: where \maximal{\sigma_{1}} $\subseteq{}K$, there exists a $p\in{}T_{PAR}$
3924: such that $X$ \multiderparK{\rho_{1}} $p$$\parallel$$Z$
3925: with \maximalparK{\rho_{1}} = \maximal{\sigma_{1}}. From the
3926: definition of $\Re_{SEQ}^{K}$ we obtain that $X$
3927: \multiderseqK{\gamma} $Z$ \onederseqK{r} $Y.(Z')$,
3928: with \maximalseqK{\gamma} = \maximalparK{\rho_{1}} and
3929: \maximalseqK{r} = \maximal{r} $\subseteq{}K$. So,
3930: \maximalseqK{\gamma{}r} $\subseteq{}K$. This concludes the proof.
3931: \end{proof}
3932:
3933:
3934: \noindent{}Now, let us assume that $K=K^{\omega}$. The next two
3935: lemmata manage this case.
3936:
3937: \begin{Lemma}\label{Lemma:From-M-To-MSEQ2}
3938: Let $i\in{}K$, $X\in{}Var$ and
3939: $X$ \multider{\sigma} be a
3940: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
3941: $X$.
3942: Then, one of the following conditions is satisfied:
3943: \begin{enumerate}
3944: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
3945: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
3946: with $K'\subseteq{}K$, and there exists a derivation
3947: $Y$ \multiderparKomega{\rho} such that \maximalparKomega{\rho} = $K$
3948: and
3949: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
3950: $K^{\omega}$. Moreover, either $\rho$ is
3951: infinite or $\rho$ contains some occurrence of rule in
3952: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
3953: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
3954: $\Re_{SEQ}^{K}$ through a $(K_{i},\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
3955: with $\{i\}\subseteq{}K_{i}\subseteq{}K$, and
3956: there exists a $(K,K^{\omega})$-accepting infinite derivation in $M$ from
3957: $Y$.
3958: \end{enumerate}
3959: \end{Lemma}
3960: \begin{proof}
3961: The proof is by induction on the level $k$ of application of the
3962: first occurrence of a rule $r$ of $\Re_{i}^{A}$ in a
3963: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
3964: a variable.\\
3965: \textbf{Base Step}: $k=0$. If $X$ \multider{\sigma} is in
3966: $\Pi^{K,K^{\omega}}_{PAR,\infty}$, from lemma
3967: \ref{Lemma:From-M-To-MPAROMEGA} property 1 follows, setting $Y=X$.
3968: Otherwise, from lemma \ref{Lemma:Base} it follows that the
3969: derivation $X$ \multider{\sigma} can be written in the form
3970: \begin{displaymath}
3971: \textrm{$X$ \multider{\sigma_{1}} $t$$\parallel$$Z$ \prsoneder{r'}
3972: $t$$\parallel$$Y.(Z')$ \multider{\sigma_{2}}}
3973: \end{displaymath}
3974: where $r'=Z$\Rule{a}$Y.(Z')$, and there exists a subderivation of
3975: $t$$\parallel$$Y.(Z')$ \multider{\sigma_{2}} from $Z'$, namely
3976: $Z'$ \multider{\sigma_{2}'}, that is a $(K,K^{\omega})$-accepting
3977: infinite derivation in $M$. By noticing that every rule occurrence
3978: in $\sigma_{2}'$ is applied to a level greater than zero in $X$
3979: \multider{\sigma}, and that we are considering the case where
3980: $k=0$, it follows that $r$ must occur in the rule sequence
3981: $\sigma_{1}r'(\sigma_{2}\setminus\sigma_{2}')$.
3982: From lemma \ref{Lemma:Subderivations1}, we have $t$
3983: \multider{\sigma_{2}\setminus\sigma_{2}'}. Therefore, there
3984: exists a derivation of the form $X$ \multider{\lambda}
3985: $t'$$\parallel$$Z$ \prsoneder{r'} $t'$$\parallel$$Y.(Z')$ with
3986: $\{i\}\subseteq$ \maximal{\lambda{}r'} $\subseteq{}K$. From lemma
3987: \ref{Lemma:From-M-To-MKPAR}, applied to the derivation $X$ \multider{\lambda}
3988: $t'$$\parallel$$Z$, there exists a $p\in{}T_{PAR}$ such that $X$
3989: \multiderparK{\rho} $p$$\parallel$$Z$, with \maximalparK{\rho} =
3990: \maximal{\lambda}. From the definition of $\Re_{SEQ}^{K}$ we have
3991: that $X$ \multiderseqK{\mu} $Z$ \onederseqK{r'}
3992: $Y.(Z')$, with \maximalseqK{\mu} = \maximalparK{\rho} and
3993: \maximalseqK{r'} = \maximal{r'}. Therefore, \maximalseqK{\mu{}r'}
3994: = \maximal{\lambda{}r'}.
3995: Thus, variable $Z'$ is reachable from $X$ in
3996: $\Re_{SEQ}^{K}$ through a $(K_{i},\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
3997: with $\{i\}\subseteq{}K_{i}\subseteq{}K$, and
3998: there exists a $(K,K^{\omega})$-accepting infinite derivation in $M$ from
3999: $Z'$. This is exactly what property 2 states.\\
4000: \textbf{Induction Step}: $k>0$. If $X$ \multider{\sigma} is in
4001: $\Pi^{K,K^{\omega}}_{PAR,\infty}$, from lemma
4002: \ref{Lemma:From-M-To-MPAROMEGA} property 1 follows, setting $Y=X$.
4003: Otherwise, from lemma \ref{Lemma:Base} it follows that the
4004: derivation $X$ \multider{\sigma} can be written in the form
4005: \begin{displaymath}
4006: \textrm{$X$ \multider{\sigma_{1}} $t$$\parallel$$Z$ \prsoneder{r'}
4007: $t$$\parallel$$Y.(Z')$ \multider{\sigma_{2}}}
4008: \end{displaymath}
4009: where $r'=Z$\Rule{a}$Y.(Z')$, and there exists a subderivation of
4010: $t$$\parallel$$Y.(Z')$ \multider{\sigma_{2}} from $Z'$, namely
4011: $Z'$ \multider{\sigma_{2}'}, that is a $(K,K^{\omega})$-accepting
4012: infinite derivation in $M$.
4013: There can be two
4014: cases:
4015: \begin{itemize}
4016: \item The rule sequence
4017: $\sigma_{1}r'( \sigma_{2}\setminus\sigma_{2}')$ contains the first occurrence of $r$
4018: in $\sigma$. In this case, the thesis follows by reasoning as
4019: in the base step.
4020: \item $\sigma_{2}'$ contains the first occurrence of $r$ in $\sigma$.
4021: Clearly, this occurrence is the first occurrence of a rule of $\Re_{i}^{A}$
4022: in the $(K,K^{\omega})$-accepting
4023: infinite derivation
4024: $Z'$ \multider{\sigma_{2}'}, and it is applied to level $k'$ in
4025: $Z'$ \multider{\sigma_{2}'} with $k'<k$. By inductive hypothesis, the thesis holds for
4026: the derivation $Z'$ \multider{\sigma_{2}'}.
4027: Therefore, it suffices to prove that $Z'$
4028: is reachable from $X$ in $\Re_{SEQ}^{K}$
4029: through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
4030: with $K'\subseteq{}K$. From lemma \ref{Lemma:From-M-To-MKPAR}, applied
4031: to the
4032: derivation $X$ \multider{\sigma_{1}} $t$$\parallel$$Z$, there exists a $p\in{}T_{PAR}$
4033: such that $X$ \multiderparK{\rho} $p$$\parallel$$Z$
4034: with \maximalparK{\rho} = \maximal{\sigma_{1}} $\subseteq{}K$. >From the
4035: definition of $\Re_{SEQ}^{K}$ we obtain that $X$
4036: \multiderseqK{\mu} $Z$ \onederseqK{r'} $Y.(Z')$
4037: with \maximalseqK{\mu} = \maximalparK{\rho} and
4038: \maximalseqK{r'} = \maximal{r'} $\subseteq{}K$.
4039: So, \maximalseqK{\mu{}r'} $\subseteq{}K$. This concludes the proof.
4040: \end{itemize}
4041: \end{proof}
4042:
4043:
4044:
4045: \begin{Lemma}\label{Lemma:From-M-To-MSEQ3}
4046: Let $X\in{}Var$ and
4047: $X$ \multider{\sigma} be a
4048: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
4049: $X$.
4050: Then, one of the following conditions is satisfied:
4051: \begin{enumerate}
4052: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
4053: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
4054: with $K'\subseteq{}K$, and there exists a derivation
4055: $Y$ \multiderparKomega{\rho} such that \maximalparKomega{\rho} = $K$
4056: and
4057: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
4058: $K^{\omega}$.
4059: Moreover, either $\rho$ is
4060: infinite or $\rho$ contains some occurrence of rule in
4061: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
4062: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
4063: $\Re_{SEQ}^{K}$ through a $(K,\emptyset)$-accepting derivation in $M_{SEQ}^{K}$, and
4064: there exists a $(K,K^{\omega})$-accepting infinite derivation in $M$ from
4065: $Y$.
4066: \end{enumerate}
4067: \end{Lemma}
4068: \begin{proof}
4069: It suffices to prove that, assuming that property 1 is not
4070: satisfied, property 2 must hold. If $|K|=0$, property 2 is
4071: obviously satisfied. So, let us assume that $|K|>0$. Let
4072: $K=\{j_{1},\ldots,j_{|K|}\}$, and for all $p=1,\ldots,|K|$ let
4073: $K_{p}=\{j_{1},\ldots,j_{p}\}$. Let us prove by induction on $p$
4074: that for all $p=1,\ldots,|K|$ the following property is satisfied
4075: (assuming that property 1 isn't satisfied):
4076: \begin{description}
4077: \item[a] There exists a variable $Y$ reachable from $X$ in
4078: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
4079: with $K_{p}\subseteq{}K'\subseteq{}K$, and
4080: there exists a $(K,K^{\omega})$-accepting infinite derivation in $M$ from
4081: $Y$.
4082: \end{description}
4083: \textbf{Base Step}: $p=1$. Considering that property 1 isn't satisfied,
4084: the result follows from lemma \ref{Lemma:From-M-To-MSEQ2},
4085: setting $i=j_{1}$.\\
4086: \textbf{Induction Step}: $1<p\leq{}|K|$.
4087: >From the inductive hypothesis there exists a
4088: $t\in{}T_{SEQ}\setminus\{\varepsilon\}$ such that $X$
4089: \multiderseqK{\rho} $t$ with $K_{p-1}\subseteq{}$
4090: \maximalseqK{\rho} $\subseteq{}K$, and there exists a
4091: $(K,K^{\omega})$-accepting infinite derivation in $M$ of the form
4092: $last(t)$ \multider{\eta}. From lemma \ref{Lemma:From-M-To-MSEQ2},
4093: applied to the derivation $last(t)$ \multider{\eta}, and
4094: considering that property 1 isn't satisfied, it follows that
4095: there exists a $\overline{t}\in{}T_{SEQ}\setminus\{\varepsilon\}$
4096: such that $last(t)$ \multiderseqK{\overline{\rho}} $\overline{t}$
4097: with $\{j_{p}\}\subseteq{}$\maximalseqK{\overline{\rho}}
4098: $\subseteq{}K$, and there exists a $(K,K^{\omega})$-accepting
4099: infinite derivation in $M$ from $last(\overline{t})$. So, we have
4100: $X$ \multiderseqK{\rho\overline{\rho}} $t\circ{}\overline{t}$ with
4101: $K_{p}\subseteq{}$\maximalseqK{\rho\overline{\rho}}
4102: $\subseteq{}K$.
4103: Therefore, setting $Y=last(\overline{t})$, we obtain the assertion.\\
4104: >From property \textbf{a}, since $K_{|K|}=K$, the thesis follows.
4105: \end{proof}
4106:
4107: \subsection{Proof of Theorem \ref{Theorem:Problem2.1}}
4108:
4109: Let us assume that $K\neq{}K^{\omega}$. Given $X\in{}Var$, we have
4110: to prove that there exists a
4111: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
4112: $X$ if, and only if, the following property is satisfied:
4113: \begin{itemize}
4114: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
4115: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
4116: with $K'\subseteq{}K$, and there exists a derivation
4117: $Y$ \multiderparKomega{\rho}
4118: such that \maximalparKomega{\rho} = $K$
4119: and
4120: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
4121: $K^{\omega}$. Moreover, either $\rho$ is
4122: infinite or $\rho$ contains some occurrence of rule in
4123: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
4124: \end{itemize}
4125:
4126: ($\Rightarrow$) The result follows directly from Lemma
4127: \ref{Lemma:From-M-To-MSEQ1}.\\
4128:
4129: ($\Leftarrow$) From hypothesis we have
4130: \begin{enumerate}
4131: \item $X$ \multiderseqK{\lambda} $t$ with
4132: $t\in{}T_{SEQ}\setminus\{\varepsilon\}$, $last(t)=Y$ and
4133: \maximalseqK{\lambda} $\subseteq{}K$.
4134: \item $Y$ \multiderparKomega{\rho} with \maximalparKomega{\rho} = $K$
4135: and
4136: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
4137: $K^{\omega}$. Moreover, either $\rho$ is
4138: infinite or $\rho$ contains some occurrence of rule in
4139: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
4140: \end{enumerate}
4141: Since $X\in{}SEQ(X)$, from condition 1 and lemma
4142: \ref{Lemma:From-MKSEQ-To-M}, it follows that there exists a
4143: $s\in{}T$ such that $t\in{}SEQ(s)$ and $X$ \multider{\eta} $s$
4144: with \maximal{\eta} $\subseteq{}K$. From condition 2 and lemma
4145: \ref{Lemma:From-MPAR-To-M-Inf} it follows that there exists a
4146: $(K,K^{\omega})$-accepting infinite derivation in $M$
4147: of the form $Y$ \multider{\sigma}. Since $Y\in{}SubTerms(s)$, from
4148: proposition \ref{Prop:Subterms1} we have that $s$
4149: \multider{\sigma}. After all, we obtain $X$ \multider{\eta} $s$
4150: \multider{\sigma}, that is a
4151: $(K,K^{\omega})$-accepting infinite derivation in $M$ from $X$.
4152: This concludes the proof.
4153:
4154:
4155:
4156: \subsection{Proof of Theorem \ref{Theorem:Problem2.2}}
4157:
4158: Let us assume that $K=K^{\omega}$. Given $X\in{}Var$, we have to
4159: prove that there exists a
4160: $(K,K^{\omega})$-accepting infinite derivation in $M$ from
4161: $X$ if, and only if, one of the following properties is satisfied:
4162: \begin{enumerate}
4163: \item There exists a variable $Y\in{}Var$ reachable from $X$ in
4164: $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting derivation in $M_{SEQ}^{K}$
4165: with $K'\subseteq{}K$, and there exists a derivation
4166: $Y$ \multiderparKomega{\rho}
4167: such that \maximalparKomega{\rho} = $K$
4168: and
4169: \maximalparKomegaInf{\rho} $\cup$ \maximalparKomegaPlus{\rho} =
4170: $K^{\omega}$. Moreover, either $\rho$ is
4171: infinite or $\rho$ contains some occurrence of rule in
4172: $\Re^{K,K^{\omega}}_{PAR}\setminus\Re_{PAR}^{K}$.
4173: \item There exists a
4174: $(K,K^{\omega})$-accepting infinite derivation in $M_{SEQ}^{K}$ from
4175: $X$.
4176: \end{enumerate}
4177:
4178: ($\Rightarrow$) It suffices to prove that, assuming that condition
4179: 1 does not hold, condition 2 must hold. Under this hypothesis, we
4180: show that there exists a succession of terms
4181: $(t_{h})_{h\in{}N}$ in
4182: $T_{SEQ}\setminus\{\varepsilon\}$ satisfying the following
4183: properties:
4184: \begin{description}
4185: \item[i.] $t_{0}=X$
4186: \item[ii.] for all $h\in{}N\quad{}last(t_{h})$
4187: \multiderseqK{\rho_{h}} $t_{h+1}$ with \maximalseqK{\rho_{h}} $=K$.
4188: \item[iii.] for all $h\in{}N$ there exists a
4189: $(K,K^{\omega})$-accepting infinite derivation in $M$ from $last(t_{h})$.
4190: \item[iv.] for all $h\in{}N$ $last(t_{h})$ is
4191: reachable from $X$ in $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting
4192: derivation in $M_{SEQ}^{K}$ with $K'\subseteq{}K$.
4193: \end{description}
4194: For $h=0$ properties iii and iv are satisfied, by setting
4195: $t_{0}=X$. So, assume the existence of a finite sequence of terms
4196: $t_{0},t_{1},\ldots,t_{h}$ in $T_{SEQ}\setminus\{\varepsilon\}$
4197: sa\-ti\-sfying properties i-iv. It suffices to prove that there
4198: exists a term $t_{h+1}$ in $T_{SEQ}\setminus\{\varepsilon\}$
4199: satisfying iii and iv, and such that $last(t_{h})$
4200: \multiderseqK{\rho_{h}} $t_{h+1}$ with \maximalseqK{\rho_{h}} $=K$.
4201: >From the inductive hypothesis, $last(t_{h})$ is reachable from
4202: $X$ in $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting
4203: derivation in $M_{SEQ}^{K}$ with $K'\subseteq{}K$, and there exists a $(K,K^{\omega})$-accepting
4204: infinite derivation in $M$ from $last(t_{h})$.
4205: From lemma \ref{Lemma:From-M-To-MSEQ3} applied to variable $last(t_{h})$,
4206: and the fact that
4207: condition 1 does not hold, it follows that there exists a term
4208: $t\in{}T_{SEQ}\setminus\{\varepsilon\}$ such that
4209: $last(t_{h})$
4210: \multiderseqK{\rho_{h}} $t$ with \maximalseqK{\rho_{h}} $=K$, and
4211: there exists a $(K,K^{\omega})$-accepting infinite derivation in $M$ from
4212: $last(t)$. Since $last(t_{h})$ is reachable from
4213: $X$ in $\Re_{SEQ}^{K}$ through a $(K',\emptyset)$-accepting
4214: derivation in $M_{SEQ}^{K}$ with $K'\subseteq{}K$, it follows that $last(t)$ is reachable
4215: from
4216: $X$ in $\Re_{SEQ}^{K}$ through a $(K,\emptyset)$-accepting
4217: derivation in $M_{SEQ}^{K}$. Thus, setting
4218: $t_{h+1}=t$, we obtain the result.\\
4219: Let $(t_{h})_{h\in{}N}$ be the succession of terms in $T_{SEQ}\setminus\{\varepsilon\}$
4220: satisfying properties i-iv. Since in this case $|K|>0$ (remember that $|K|+|K^{\omega}|>0$),
4221: we have $|\rho_{h}|>0$ for all $h\in{}N$. Then, by property 1 of proposition
4222: \ref{Prop:Subterms2} we obtain that for every
4223: $h\in{}N$
4224: \begin{displaymath}
4225: \textrm{$t_{h}$
4226: \multiderseqK{\rho_{h}} $t_{h}\circ{}t_{h+1}$ with
4227: \maximalseqK{\rho_{h}} = $K$}
4228: \end{displaymath}
4229: >From property 2 of proposition \ref{Prop:Subterms2} we have that
4230: for all $h\in{}N$
4231: \begin{displaymath}
4232: \textrm{
4233: $t_{0}$$\circ$$t_{1}$$\circ$$\ldots$$\circ$$t_{h}$
4234: \multiderseqK{\rho_{h}} $t_{0}$$\circ$$t_{1}$$\circ$$\ldots$$\circ$$t_{h}$$\circ$$t_{h+1}$
4235: }
4236: \end{displaymath}
4237: Therefore,
4238: \begin{eqnarray}
4239: \textrm{$X=t_{0}$ \multiderseqK{\rho_{0}} $t_{0}$$\circ$$t_{1}$
4240: \multiderseqK{\rho_{1}} $t_{0}$$\circ$$t_{1}$$\circ$$t_{2}$
4241: \multiderseqK{\rho_{2}} $\ldots$ \multiderseqK{\rho_{h-1}}
4242: $t_{0}$$\circ$$t_{1}$$\circ$$\ldots$$\circ$$t_{h}$}\nonumber\\
4243: \textrm{\multiderseqK{\rho_{h}}
4244: $t_{0}$$\circ$$t_{1}$$\circ$$\ldots$$\circ$$t_{h}$$\circ$$t_{h+1}$
4245: \multiderseqK{\rho_{h+1}}$\ldots$}\nonumber
4246: \end{eqnarray}
4247: is an infinite derivation in
4248: $\Re_{SEQ}^{K}$ from $X$. Setting $\delta=\rho_{0}\rho_{1}\ldots$,
4249: from ii and proposition \ref{Prop:Maximal} we obtain that
4250: \begin{displaymath}
4251: \textrm{\maximalseqK{\delta} =
4252: $\bigcup_{h\in{}N}$\maximalseqK{\rho_{h}} = $K$.}
4253: \end{displaymath}
4254: \begin{displaymath}
4255: \textrm{\maximalseqInfK{\delta} =
4256: $\bigoplus_{h\in{}N}$\maximalseqK{\rho_{h}} = $K$ = $K^{\omega}$.}
4257: \end{displaymath}
4258: Hence, condition 2 holds.\\
4259:
4260: ($\Leftarrow$) At first, let us assume the condition 2 holds.
4261: Then, since $X\in{}SEQ(X)$, the result follows directly from lemma
4262: \ref{Lemma:From-MKSEQ-To-M}. Assume that condition 1 holds
4263: instead. Then, we reason as in the proof of theorem
4264: \ref{Theorem:Problem2.1}.
4265:
4266:
4267:
4268: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4269:
4270:
4271: \end{document}
4272:
4273: