1: \documentclass[final,10pt,a4paper]{article}

2: \usepackage{times}

3: \usepackage{a4wide} % option: a4paper

4: \usepackage{amsmath}

5: \usepackage{amssymb}

6: \usepackage{amsfonts}

7: \usepackage{stmaryrd}

8: \usepackage{amsthm}

9: %\usepackage[mathscr]{eucal}

10: \usepackage{mathrsfs}

11: %\usepackage[mathcal]{euscript}

12: %\usepackage{mathabx}

13: \usepackage[english]{babel}

14: \usepackage{color,graphicx}

15: \usepackage[all]{xy}

16: 

17: 

18: 

19: %\pdfpagewidth=\paperwidth

20: %\pdfpageheight=\paperheight

21: 

22: % %%%%%%%%%%%%%%%%   THEOREMS-like %%%%%%%%%%

23: 

24: %\spnewtheorem{hypothesis}[theorem]{Hypothesis}{\bfseries}{\itshape}

25: %\spnewtheorem{observation}[theorem]{Observation}{\bfseries}{\rmfamily}

26: %\spnewtheorem{example2}[theorem]{Example}{\bfseries}{\rmfamily}

27: %\spnewtheorem{definition2}[theorem]{Definition}{\bfseries}{\rmfamily}

28: %\spnewtheorem{remark2}[theorem]{Remark}{\bfseries}{\itshape}

29: 

30:  \theoremstyle{plain}

31:  \newtheorem{theorem}{Theorem}[section]

32:  \newtheorem{lemma}[theorem]{Lemma}

33:  \newtheorem{corollary}[theorem]{Corollary}

34:  \newtheorem{proposition}[theorem]{Proposition}

35:  \theoremstyle{definition}

36:  \newtheorem{definition}[theorem]{Definition}

37:  \newtheorem{definition2}[theorem]{Definition}

38:  \newtheorem{example}[theorem]{Example}

39:  \newtheorem{example2}[theorem]{Example}

40:  \newtheorem{hypothesis}[theorem]{Hypothesis}

41:  \theoremstyle{remark}

42:  %\theoremstyle{fact}

43:  \newtheorem{remark2}[theorem]{Remark}

44:  \newtheorem{fact}[theorem]{Fact}

45:  \numberwithin{equation}{section}

46:  \newtheorem{observation}[theorem]{Observation}

47: \theoremstyle{remark}

48:  \newtheorem{problem}{Problem}

49: 

50: 

51: %%%%%%%%%%%%%%%%   MACROS  %%%%%%%%%%%

52: 

53: %comments

54: \newcommand{\comment} [1]{}

55: 

56: %\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}

57: %\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil

58: %\penalty50\hskip1em\null\nobreak\hfil\squareforqed

59: %\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

60: 

61: 

62: \def\smallromani{\renewcommand{\theenumi}{\roman{enumi}}

63:         \renewcommand{\labelenumi}{(\theenumi)}}

64: \def\ok#1{\mbox{\raisebox{0ex}[1ex][1ex]{$#1$}}}

65: \def \tuple#1{\langle #1 \rangle}

66: 

67: \newcommand{\sra}{{\shortrightarrow}}

68: \newcommand{\aR}{\ok{\xrightarrow{\mbox{}_{R}}}}

69: \newcommand{\Sa}{\ok{S^\sharp}}

70: \newcommand{\ddef}{\hfill$\Box$}

71: \newcommand{\sun}{\subseteq_\varnothing}

72: \newcommand{\ulr}{\mbox{\raisebox{0ex}[1ex][1ex]{$\:\stackrel{{\scriptscriptstyle

73: \mathrm{def}}}{\Leftrightarrow}\:$}}}

74: \newcommand{\ulrl}{\mbox{\raisebox{0ex}[1ex][1ex]{$\:\stackrel{{\scriptscriptstyle

75: \mathrm{def}}}{\iff}\:$}}}

76: \newcommand{\ud}{\mbox{\raisebox{0ex}[1ex][1ex]{$\:\stackrel{{\scriptscriptstyle

77: \mathrm{def}}}{=}\:$}}}

78: \newcommand{\us}{\uparrow\!\!}

79: \newcommand{\nat}{\mathbb{N}}

80: \newcommand{\ra}{\rightarrow}

81: \newcommand{\Lra}{\Leftrightarrow}

82: \newcommand{\Ra}{\Rightarrow}

83: \newcommand{\ram}{\ok{\xrightarrow{m}}}

84: \newcommand{\AP}{{\mathit{AP}}}

85: \newcommand{\APb}{{\boldsymbol{AP}}}

86: \newcommand{\BG}{{\mathrm{BG}}}

87: \newcommand{\lb}{{\mathrm{lb}}}

88: \newcommand{\Op}{{\mathit{Op}}}

89: \newcommand{\Opb}{{\boldsymbol{Op}}}

90: \newcommand{\States}{{\mathit{States}}}

91: \newcommand{\Statess}{\ok{{\mathit{States}^\sharp}}}

92: \newcommand{\AStates}{{\mathit{A}\hspace{-1pt}\mathit{States}}}

93: \newcommand{\AbsDom}{{\mathrm{AbsDom}}}

94: \newcommand{\cs}{{\mathcal{S}}}

95: \newcommand{\ci}{{\mathcal{I}}}

96: \newcommand{\ca}{{\mathcal{A}}}

97: \newcommand{\ct}{{\mathcal{T}}}

98: \newcommand{\cL}{{\mathcal{L}}}

99: \newcommand{\cM}{{\mathcal{M}}}

100: \newcommand{\cS}{{\mathcal{S}}}

101: \newcommand{\cX}{{\mathcal{X}}}

102: \newcommand{\sS}{{\mathscr{S}}}

103: \newcommand{\cR}{{\mathcal{R}}}

104: \newcommand{\cP}{{\mathcal{P}}}

105: \newcommand{\cK}{{\mathcal{K}}}

106: \newcommand{\cA}{{\mathcal{A}}}

107: \newcommand{\cT}{{\mathcal{T}}}

108: \newcommand{\bT}{{\mathbb{T}}}

109: \newcommand{\bP}{{\mathbb{P}}}

110: \newcommand{\bN}{{\mathbb{N}}}

111: \newcommand{\bZ}{{\mathbb{Z}}}

112: \newcommand{\bisim}{{\,\simeq}}

113: \newcommand{\compl}{{\,\preccurlyeq}}

114: \newcommand{\fb}{\ensuremath{\mathbb{F}}}

115: \newcommand{\cb}{\ensuremath{\mathbb{C}}}

116: \newcommand{\fc}{\ensuremath{\mathfrak{C}}}

117: \newcommand{\fr}{\ensuremath{\mathscr{F}}}

118: \newcommand{\fL}{\ensuremath{\mathscr{L}}}

119: \newcommand{\crr}{\ensuremath{\mathscr{C}}}

120: \newcommand{\leqp}{{\preccurlyeq}}

121: \newcommand{\beu}{{{\rm\bf EU}_\sra}}

122: \newcommand{\SP}{\ensuremath{\mathrm{SP}}}

123: \newcommand{\ACTL}{\ensuremath{\mathrm{ACTL}}}

124: \newcommand{\CTL}{\ensuremath{\mathrm{CTL}}}

125: \newcommand{\LTL}{\ensuremath{\mathrm{LTL}}}

126: \newcommand{\CTLS}{\ensuremath{\mathrm{CTL}^*}}

127: \newcommand{\ACTLS}{\ensuremath{\mathrm{ACTL}^*}}

128: \newcommand{\CTLX}{\ensuremath{\mathrm{CTL}\mbox{-}\mathrm{X}}}

129: \newcommand{\CTLSX}{\ensuremath{\mathrm{CTL}^*\mbox{-}\mathrm{X}}}

130: \newcommand{\EX}{\mathrm{EX}}

131: \newcommand{\Sign}{\mathit{Sign}}

132: 

133: \newcommand{\pret}{\ensuremath{\widetilde{\pre}}}

134: \newcommand{\postt}{\ensuremath{\widetilde{\post}}}

135: \newcommand{\fbar}{\overline{f}}

136: \newcommand{\semA}[1]{|#1|_{Q_A,\alpha\circ I}}

137: \newcommand{\semX}[1]{|#1|_{Q,\beta\circ\alpha\circ I}}

138: \newcommand{\semXI}[1]{|#1|_{Q,I}}

139: %\def\grasse#1{[\![#1]\!]}

140: \newcommand{\grasse}[1]{\llbracket {#1} \rrbracket}

141: \newcommand{\st}{\mathrm{\;.\;}}

142: \newcommand{\bA}{{\mathbb{A}}}

143: \def\card#1{|#1|}

144: \newcommand{\stp}{\textit{st}}

145: 

146: \newcommand*{\gdca}{(\alpha ,C,A,\gamma)}

147: \newcommand*{\gdcas}{(\alpha ,\wp(\Sigma),A,\gamma)}

148: %\newcommand*{\gdca} {\ok{C \: {\scriptscriptstyle \overset{\gamma}{\underset{^\alpha}{\leftrightarrows}}}\: A}}

149: %%{{C \; \overset{\alpha}{\underset{\gamma}{\rightleftarrows}}\; A}}

150: 

151: \newcommand*{\rarr}[1]{\mbox{\raisebox{0ex}[1ex][1ex]{$

152:   \mathrel{\mathop{

153: \hspace*{1pt}\longrightarrow\hspace*{1pt}}\limits^{\,_{\mbox{\tiny 

154: \hspace*{-2.2pt}#1}}}}$}}}

155: 

156: 

157: \DeclareMathOperator{\Algbis}{{Alg}_{\mathrm{bis}}}

158: \DeclareMathOperator{\Algsimeq}{{Alg}_{\mathrm{simeq}}}

159: \DeclareMathOperator{\AD}{{AD}}

160: \DeclareMathOperator{\sq}{{sq}}

161: \DeclareMathOperator{\id}{id}

162: \DeclareMathOperator{\pre}{pre}

163: \DeclareMathOperator{\post}{{post}}

164: \DeclareMathOperator{\uco}{uco}

165: \DeclareMathOperator{\ucop}{uco^{\mathrm{par}}}

166: \DeclareMathOperator{\Absp}{Abs^{\mathrm{par}}}

167: \DeclareMathOperator{\Absd}{Abs^{\mathrm{disj}}}

168: \DeclareMathOperator{\lco}{lco}

169: \DeclareMathOperator{\dom}{dom}

170: \DeclareMathOperator{\im}{Im}

171: \DeclareMathOperator{\lfp}{lfp}

172: \DeclareMathOperator{\gfp}{gfp}

173: \DeclareMathOperator{\succop}{succ}

174: \DeclareMathOperator{\fix}{fix}

175: \DeclareMathOperator{\img}{img}

176: \DeclareMathOperator{\Part}{Part}

177: \DeclareMathOperator{\PreOrd}{PreOrd}

178: \DeclareMathOperator{\preOrd}{preOrd}

179: \DeclareMathOperator{\preord}{preord}

180: \DeclareMathOperator{\PAbs}{PAbs}

181: \DeclareMathOperator{\Compl}{compl}

182: \DeclareMathOperator{\Rel}{Rel}

183: \DeclareMathOperator{\Par}{Par}

184: \DeclareMathOperator{\maxx}{max}

185: \DeclareMathOperator{\Fun}{Fun}

186: \DeclareMathOperator{\pr}{par}

187: \DeclareMathOperator{\pcl}{pcl}

188: \DeclareMathOperator{\pad}{pad}

189: \DeclareMathOperator{\ad}{ad}

190: \DeclareMathOperator{\adp}{ad^p}

191: \DeclareMathOperator{\add}{ad^d}

192: \DeclareMathOperator{\ap}{{\mathit{AP}}}

193: \DeclareMathOperator{\ex}{\mathrm{EX}}

194: \DeclareMathOperator{\ax}{\mathrm{AX}}

195: \DeclareMathOperator{\ef}{\mathrm{EF}}

196: \DeclareMathOperator{\af}{\mathrm{AF}}

197: \DeclareMathOperator{\PT}{\mathrm{PT}}

198: \DeclareMathOperator{\SimEq}{\mathrm{SimEq}}

199: \DeclareMathOperator{\GV}{\mathrm{GV}}

200: \DeclareMathOperator{\PR}{\mathrm{PR}}

201: \DeclareMathOperator{\Ord}{\mathrm{Ord}}

202: \DeclareMathOperator{\Abs}{\mathrm{Abs}}

203: 

204: 

205: 

206: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

207: %\usepackage[pdftex]{hyperref}

208: 

209: \begin{document}

210: 

211: \title{\Large \bf Generalized Strong Preservation\\ by Abstract Interpretation}

212: 

213: \author{\normalsize {\sc Francesco Ranzato} ~~~ {\sc Francesco Tapparo}\\

214: \normalsize Dipartimento di Matematica Pura ed Applicata, Universit\`a

215: di Padova\\

216: \normalsize Via Belzoni 7, 35131 Padova, Italy\\

217: \normalsize \texttt{franz$@$math.unipd.it} ~~~~ \texttt{tapparo$@$math.unipd.it}

218: }

219: 

220: 

221: \date{}

222: \pagestyle{plain}

223: 

224: 

225: \maketitle

226: 

227: \begin{abstract}

228: Standard abstract model checking relies on abstract Kripke structures

229: which approximate concrete models by gluing together indistinguishable

230: states, namely by a partition of the concrete state space.  Strong

231: preservation for a specification language $\fL$ encodes the

232: equivalence of concrete and abstract model checking of formulas in

233: $\fL$. We show how abstract interpretation can be used to design

234: abstract models that are more general than abstract Kripke

235: structures. Accordingly, strong preservation is generalized to

236: abstract interpretation-based models and precisely related to the

237: concept of completeness in abstract interpretation.  The problem of

238: minimally refining an abstract model in order to make it strongly

239: preserving for some language $\fL$ can be formulated as a minimal

240: domain refinement in abstract interpretation in order to get

241: completeness w.r.t.\ the logical/temporal operators of $\fL$. It turns

242: out that this refined strongly preserving abstract model always exists

243: and can be characterized as a greatest fixed point.  As a consequence,

244: some well-known behavioural equivalences, like bisimulation,

245: simulation and stuttering, and their corresponding partition

246: refinement algorithms can be elegantly characterized in abstract

247: interpretation as completeness properties and refinements.\\[10pt]

248: %

249: \emph{Keywords:} Abstract interpretation, abstract model checking, strong preservation,

250: completeness,   refinement, behavioural

251: equivalence. 

252: \end{abstract}

253: 

254: 

255: \section{Introduction}\label{intro}

256: The design of an abstract model checking framework always includes 

257: a preservation result, roughly stating that for any

258: formula $\varphi$ specified in some temporal language $\fL$, if

259: $\varphi$ holds on an abstract model then $\varphi$ also 

260: holds on the concrete model. On the other hand, \emph{strong

261: preservation} means that a formula of $\fL$ holds on an abstract

262: model if and only if it holds on the concrete model.  Strong

263: preservation is highly desirable since it allows to draw consequences

264: from negative answers on the abstract side~\cite{cgp99}.

265: %

266: %\indent

267: 

268: \medskip

269: \noindent

270: \textbf{Generalized Strong Preservation.}

271: The relationship between abstract interpretation and abstract model

272: checking has been the subject of a number of works (see e.g.\ 

273: \cite{cgl94,cpy95,CC99,CC00,dams96,dgg97,GQ01,loi95,mas02,mas04,RT02,sch04}). 

274: This paper follows the standard abstract interpretation approach

275: \cite{CC77,CC79} where

276: abstract domains are specified by Galois connections, namely pairs of

277: abstraction and concretization maps $\alpha$/$\gamma$. We deal with generic (temporal)

278: languages $\fL$ of state formulae 

279: that are inductively generated by some given sets of atomic

280: propositions and operators.  

281: The interpretation $\boldsymbol{p}$

282: of atomic propositions $p\in \AP$ as subsets of $\States$ and of 

283: operators $f\in \Op$ as mappings $\boldsymbol{f}$ on $\wp(\States)$ is determined by   

284: a suitable semantic structure $\cS$, e.g.\ a Kripke structure, so that

285: the concrete semantics 

286: $\grasse{\varphi}_\cS \in \wp(\States)$ of a formula

287: $\varphi\in \fL$ is the

288: set of states making $\varphi$ true w.r.t.\ $\cS$. 

289: \emph{Abstract semantics} 

290: can be systematically defined by standard abstract interpretation.

291: The powerset $\wp(\States)$ plays the role of concrete semantic

292: domain so that abstract domains range in $\AbsDom(\wp(\States))$. 

293: Any abstract domain $A\in \AbsDom(\wp(States))$ 

294: induces an abstract semantic structure $\cS^A$ where atoms $p$ are

295: abstracted to $\alpha(\boldsymbol{p})$ and operators $f$ are interpreted

296: as best correct approximations on $A$, that is $\alpha \circ

297: \boldsymbol{f} \circ \gamma$. Thus, $A$ 

298: determines an abstract semantics 

299: $\grasse{\varphi}_\cS^A \in A$ that evaluates formulae

300: $\varphi\in \fL$ in the abstract domain $A$. \\

301: %

302: \indent

303: It turns out that this approach generalizes standard abstract model

304: checking \cite{cgl94,cgp99}. Given a Kripke structure $\cK

305: = (\States, \ra)$ (for simplicity we omit here a labeling function

306: for atomic propositions), a standard abstract model is specified as an

307: abstract Kripke structure $\cA = (\AStates,

308: \ok{\ra^\sharp})$ where the set $\AStates$ of abstract states is defined by a

309: surjective map $h:\States \ra \AStates$. Thus, $\AStates$ determines a partition of

310: $\States$ and vice versa. It turns out 

311: that state partitions are particular

312: abstract domains. In fact, the lattice of

313: partitions of $\States$ is an abstract interpretation of the lattice

314: of abstract domains $\AbsDom(\wp(\States))$ so that the abstract state space

315: $\AStates$ corresponds to a particular abstract domain $\ad(\AStates) \in

316: \AbsDom(\wp(\States))$. Abstract domains 

317: that can be derived from a state

318: partition are called \emph{partitioning}. 

319: The interpretation of the language

320: $\fL$ w.r.t.\ the abstract Kripke structure $\cA$ determines an abstract semantic

321: function $\grasse{\varphi}_\cA \in \AStates$.  

322: The abstract Kripke structure $\cA$ strongly preserves $\fL$ when for any

323: $\varphi \in \fL$ and $s\in \States$,

324: it turns out that $h(s)\in \grasse{\varphi}_\cA \: \Lra \: s\in \grasse{\varphi}_\cK$. \\

325: %

326: \indent

327: Strong preservation can then be generalized from standard abstract

328: models to abstract interpretation-based models.  Given a generalized abstract

329: model $A\in \AbsDom(\wp(\States))$, the induced abstract semantics 

330: $\grasse{\cdot}_\cS^A$ is strongly

331: preserving for $\fL$ when for any $\varphi\in \fL$ and

332: $S\in \wp(\States)$, $\alpha(S)\leq_A \grasse{\varphi}_\cS^A\:\Lra S\subseteq

333: \grasse{\varphi}_\cS$. It turns out that this is an abstract domain

334: property, because any abstract semantics $\grasse{\cdot}^\sharp:\fL

335: \ra A$ that evaluates formulae in the abstract domain $A$ is strongly

336: preserving for $\fL$ if and only if $\grasse{\cdot}_\cS^A$ is.

337: Standard strong preservation becomes a particular instance, namely 

338: an abstract Kripke structure

339: strongly preserves $\fL$ if and only if the corresponding

340: partitioning abstract model 

341: strongly preserves $\fL$.  On the other hand, generalized strong

342: preservation may work where standard strong preservation may fail,

343: namely it may happen that

344: although 

345: a strongly preserving abstract semantics on a partitioning abstract

346: model $\ad(\AStates)$ exists this cannot be derived from a strongly preserving

347: abstract Kripke structure on $\AStates$. 

348: 

349:  

350: \medskip

351: \noindent

352: \textbf{Generalized Strong Preservation and Complete Abstract Interpretations.} 

353: Given a language $\fL$ and a Kripke structure $\cK=(\States,\ra)$, a

354: well-known key problem is to compute the smallest abstract state space

355: $\AStates_\fL$, when this exists, such that one can define an abstract

356: Kripke structure $\cA_{\fL}=(\AStates_\fL,\ok{\ra^\sharp})$

357: that strongly preserves $\fL$.  This problem admits solution for a

358: number of well-known temporal languages like $\CTL$ (or, equivalently,

359: the $\mu$-calculus), $\ACTL$ and $\CTLX$ (i.e.\ $\CTL$ without the

360: next-time operator $\mathrm{X}$). A number of algorithms for solving

361: this problem exist, like those by Paige and Tarjan \cite{pt87} for

362: $\CTL$, by Henzinger et al.~\cite{hhk95}, Bustan and

363: Grumberg~\cite{bg03} and Tan and Cleaveland \cite{TC01} for $\ACTL$,

364: and Groote and Vaandrager~\cite{gv90} for $\CTLX$. These are coarsest

365: partition refinement algorithms: given a language $\fL$ and a

366: partition $P$ of $\States$, which is determined by a state labeling,

367: these algorithms can be viewed as computing the coarsest partition

368: $P_\fL$ that refines $P$ and strongly preserves $\fL$.  It is worth

369: remarking that most of these algorithms have been designed for

370: computing well-known behavioural equivalences used in process algebra

371: like bisimulation (for $\CTL$), simulation (for $\ACTL$) and

372: divergence-blind stuttering (for $\CTLX$) equivalence.

373: %As far as the

374: %smallest abstract transition relation is concerned, this is easy to

375: %characterize for the case of $\CTL$ while for $\ACTL$ Bustan and

376: %Grumberg \cite{bg03} show that this exists and provide an algorithm

377: %for computing it.\\

378: %

379: Our abstract

380: interpretation-based framework allows to give a generalized view of the

381: above partition refinement algorithms.  

382: We show that the most abstract

383: domain $\AD_\fL \in \AbsDom(\wp(\States))$ that strongly preserves a

384: given language $\fL$ always exists. 

385: It turns out that $\AD_\fL$ is a

386: partitioning abstract domain if and only if

387: $\fL$ includes full propositional logic, that is when $\fL$ is closed under

388: logical conjunction and negation. Otherwise, a proper loss of

389: information occurs when abstracting $\AD_\fL$ to the corresponding

390: partition $P_\fL$.

391: Moreover, for some languages $\fL$, 

392: it may happen that one cannot define an

393: abstract Kripke structure on the abstract state space $P_{\fL}$

394: %(i.e., to define an abstract transition relation on $P_{\fL}$) 

395: that strongly

396: preserves $\fL$ 

397: whereas the most abstract strongly preserving

398: semantics in $\AbsDom(\wp(\States))$ instead exists.   

399: \\

400: %

401: \indent

402: The concept of 

403: \emph{complete} abstract interpretation is well known \cite{CC79,jacm}. 

404: This encodes an ideal situation where the abstract semantics

405: coincides with the abstraction of the concrete semantics.  We

406: establish a precise correspondence between generalized strong

407: preservation of abstract models and completeness in abstract

408: interpretation. Our results are based on the notion of

409: \emph{forward complete} abstract domain. An abstract domain $A$ 

410: is forward complete for a concrete semantic

411: function $\boldsymbol{f}$ when

412: for any $a\in A$,

413: $\boldsymbol{f}(\gamma(a)) =

414: \gamma(\alpha(\boldsymbol{f}(\gamma(a))))$, namely when no loss of

415: precision occurs by approximating in $A$ a computation

416: $\boldsymbol{f}(\gamma(a))$. This notion of forward completeness is

417: dual and orthogonal to the standard definition of

418: completeness in abstract interpretation.    

419: Giacobazzi et al.~\cite{jacm} showed how complete abstract domains can

420: be systematically and

421: constructively derived from noncomplete abstract domains 

422: by minimal refinements. This can be done for forward

423: completeness as well. Given any domain

424: $A$, the most abstract domain that refines $A$ and is forward

425: complete for $\boldsymbol{f}$ does exist and can be characterized

426: as a greatest fixpoint. Such a domain is called the \emph{forward}

427: \emph{complete shell} of $A$ for $\boldsymbol{f}$. 

428: It turns out that strong preservation is related to forward

429: completeness as follows. As

430: described above, the most abstract domain $\AD_\fL$ that strongly

431: preserves $\fL$ always exists. It turns out that $\AD_\fL$ coincides

432: with the forward complete shell for the operators of $\fL$ 

433: of a basic abstract domain determined by the state labeling.

434: This characterization provides an elegant

435: generalization of  partition refinement algorithms used in standard

436: abstract model checking.  As a consequence of these results, we derive 

437: a novel characterization of the corresponding behavioural equivalences

438: in terms of forward completeness of abstract domains. For example, it

439: turns out that a partition $P$ is a bisimulation on some Kripke

440: structure $\cK$

441: if and only if the corresponding partitioning

442: abstract domain $\ad(P)$ is forward complete

443: for the standard predecessor transformer $\pre_{\ra}$ in $\cK$. 

444: %As a further consequence of our abstract

445: %interpretation-based approach, we show how our generalized notion of

446: %most abstract strongly preserving domain allows to derive a

447: %characterization of the smallest abstract transition relation both for

448: %$\CTL$ and $\ACTL$.

449: 

450: 

451:   

452: \section{Basic Notions}

453: 

454: \subsection{Notation and Preliminaries} \label{not}

455: Let $X$ be any set.

456: $\Fun(X)$ denotes the set of 

457: functions $f:X^n\ra X$, for some $n\geq 0$, called arity of $f$.  

458: Following a standard

459: convention, when $n=0$, $f$ is meant to be a specific object of $X$.

460: The arity of $f$ is also

461: denoted by $\sharp (f)\geq 0$.  $\id$ denotes the identity map.  

462: If $F\subseteq \Fun(X)$ and $Y\subseteq X$ then $F(Y)\ud \{

463: f(\vec{y})~|~ f\in F,\, \vec{y}\in \ok{Y^{\sharp(f)}}\}$, namely $F(Y)$

464: is the set of images of $Y$ for each function in $F$. If $f:X\ra Y$

465: then the image of $f$ is also denoted by $\img(f)=\{f(x)\in Y~|~ x\in X\}$. 

466: If $f:X \ra Y$ and $g: Y \ra Z$ then $g \circ f : X\ra Z$ denotes the

467: composition of $f$ and $g$, i.e.\ $g \circ f = \lambda x. g(f(x))$.  

468: The complement operator for the universe set $X$ is 

469: $\complement :\wp(X)\ra \wp(X)$, where $\complement

470: (S)=X\smallsetminus S$.

471: When writing a set $S$ of subsets of a given set, like a partition,

472: we often write $S$ in a compact form like 

473: $\{1, 12, 13\}$ or $\{[1], [12], [13]\}$ that stand for $\{\{1\},

474: \{1,2\}, \{1,3\}\}$. $\Ord$ denotes the proper

475: class

476: of ordinals and $\omega\in\Ord$ denotes the first infinite ordinal. 

477: 

478: Let $\tuple{P,\leq}$ be a poset. Posets are often denoted also by $P_\leq$.

479: %If $S\subseteq P$ then $\max(S) \ud \{x\in S~|~\forall y\in

480: %S.\, x\leq y \: \Ra \: x=y\}$ denotes the set of maximal elements of

481: %$S$ in $P$.  

482: %A poset $P$ is ACC (i.e., it 

483: %satisfies the ascending chain condition) when $P$ contains no infinite

484: %ascending chain in $P$. It is well known that $P$ is ACC iff for any

485: %$\varnothing \neq S\subseteq P$, $\max(S)\neq \varnothing$. 

486: %A poset $P$ is ACC (i.e., $P$ satisfies the 

487: %ascending chain condition) when $P$ contains no infinite

488: %ascending chain, i.e.\ if $\{x_i\}_{i\in\mathbb{N}}\subseteq P$ is such that,

489: %for any $i\in \mathbb{N}$, 

490: %$x_i \leq x_{i+1}$ then there exists some $k\in \mathbb{N}$ such that

491: %for any $j\geq 0$, $x_{k+j}=x_k$. 

492: %The descending chain condition (DCC) is dually defined. 

493: We use the symbol $\sqsubseteq$ to denote pointwise ordering between

494: functions: If $X$ is any set and $f,g:X \ra P$ then

495: $f\sqsubseteq g$ if for all $x\in X$, $f(x)\leq g(x)$.  

496: A mapping $f: P\ra Q$ on posets is continuous when $f$

497: preserves least upper bounds (lub's) 

498: of countable chains in $P$, while, dually, it is co-continuous when $f$ 

499: preserves greatest lower bounds (glb's) 

500: of countable chains in $P$. A complete lattice $C_\leq$ 

501: is also denoted by $\tuple{C,\leq,\vee,\wedge,\top,\bot}$ where $\vee$,

502: $\wedge$, $\top$ and $\bot$ denote, respectively, lub, glb, greatest

503: element and least element in $C$.  

504: A mapping $f:C\ra D$ between complete lattices

505: is additive (co-additive) when for any $Y\subseteq C$, $f(\vee_C

506: Y)=\vee_D f(Y)$ ($f(\wedge_C

507: Y)=\wedge_D f(Y)$). 

508: We denote by $\lfp(f)$ and $\gfp (f)$,

509: respectively, the least and greatest fixpoint, when they exist, of an

510: operator $f$ on a poset. 

511: The well-known Knaster-Tarski's theorem

512: states that any monotone operator $f:C\ra C$ on a complete

513: lattice $C$ admits a least fixpoint and the

514: following characterization holds:

515: %

516: $$\lfp(f) = \wedge \{x\in C~|~ f(x) \leq

517: x\}=\vee_{\alpha\in \Ord} f^{\alpha,\uparrow} (\bot)$$

518: %

519: where the upper iteration sequence $\{f^{\alpha,\uparrow} (x)\}_{\alpha \in

520: \Ord}$ of $f$ in $x\in C$ is defined by transfinite induction on $\alpha$ as

521: usual: 

522: \begin{itemize}

523: \item[--] $\alpha=0$:~ $\ok{f^{0,\uparrow} (x)= x}$; 

524: \item[--] successor ordinal $\alpha=\beta+1$:~ $\ok{f^{\beta+1,\uparrow}

525: (x)=f(f^{\beta,\uparrow} (x))}$;

526: \item[--] limit ordinal $\alpha$:~ $\ok{f^{\alpha,\uparrow} (x)}

527: =\vee_{\beta<\alpha} 

528: f^{\beta,\uparrow} (x)$. 

529: \end{itemize}

530: It is well known that if $f$ is continuous then $\lfp(f)=\vee_{\alpha\in \omega} 

531: f^{\alpha,\uparrow}(\bot)$. 

532: Dually, $f$ also admits a greatest fixpoint and the

533: following characterization holds:

534: $$\gfp(f) = \vee \{x\in C~|~ x\leq f(x)\} = 

535: \wedge_{\alpha\in \Ord} f^{\alpha,\downarrow} (\top),$$ 

536: where the lower iteration sequence $\{f^{\alpha,\downarrow} (x)\}_{\alpha \in

537: \Ord}$ of $f$ in $x\in C$ is defined as the upper iteration sequence

538: but for the case of limit ordinals: $\ok{f^{\alpha,\downarrow} (x)}

539: =\wedge_{\beta<\alpha} 

540: f^{\beta,\downarrow} (x)$.

541: 

542: 

543: Let $\Sigma$ be any set. $\PreOrd(\Sigma)$ denotes the set of preorder

544: relations on $\Sigma$, that is $R\subseteq \Sigma\times \Sigma$ is a

545: preorder on $\Sigma$ if $R$ is reflexive and transitive.  

546: $\Part(\Sigma)$ denotes the

547: set of partitions of $\Sigma$. Sets in a partition $P$

548: are called blocks of $P$. 

549: If $\equiv\;\subseteq \Sigma \times \Sigma $ is an equivalence relation

550: then we denote by $P_\equiv\in \Part(\Sigma)$ the corresponding partition of

551: $\Sigma$. Vice versa, if $P\in \Part(\Sigma)$ then 

552: $\equiv_P\,\subseteq \Sigma \times \Sigma $ denotes 

553: the corresponding equivalence relation on

554: $\Sigma$. $\Part(\Sigma)$ is endowed with the

555: following standard partial order $\preccurlyeq$: 

556: $P_1

557: \preccurlyeq P_2$, i.e.\ $P_2$ is coarser than $P_1$ (or $P_1$ refines

558: $P_2$) iff $\forall B\in P_1. \exists B' \in P_2 .\: B \subseteq

559: B'$. It is well known that 

560: $\tuple{\Part(\Sigma), \preccurlyeq}$ is a complete lattice. 

561: 

562: 

563: 

564: A transition system $\cT=(\Sigma ,\sra)$ consists of a (possibly

565: infinite) set $\Sigma$ of

566: states  and a transition relation $\sra \subseteq \Sigma \times

567: \Sigma$. 

568: As usual \cite{cgp99}, we assume

569: that

570: the relation $\sra$ is total, i.e., for any $s\in \Sigma $ there

571: exists some $t\in \Sigma $ such that $s\sra t$, so that any maximal path in

572: $\cT$ is necessarily

573: infinite.  

574: $\cT$ is  finitely branching when  

575: for any $s\in \Sigma $, $\{t\in \Sigma ~|~ s \sra t \}$ is a finite

576: set. 

577: The

578: pre/post transformers on $\wp(\Sigma)$ are defined as usual:

579: \begin{itemize}

580: \item[--] $\pre_\sra \ud \lambda Y. \{ a\in \Sigma ~|~\exists b\in Y.\; a \sra

581: b\}$;

582: \item[--] $\pret_\sra \ud \complement \circ \pre_\sra \circ \complement = 

583: \lambda Y. \{ a\in \Sigma  ~|~\forall b\in \Sigma . (a \sra

584: b \Rightarrow  b\in Y)\}$; 

585: \item[--] $\post_\sra \ud \lambda Y. \{ b\in \Sigma ~|~\exists a\in Y.\; a \sra

586: b\}$;

587: \item[--] $\postt_\sra \ud \complement \circ \post_\sra \circ \complement = 

588: \lambda Y. \{ b\in \Sigma ~|~\forall a\in \Sigma . (a \sra

589: b \Rightarrow a\in Y)\}$.

590: \end{itemize}

591: %

592: Let us observe that $\pre_\sra$ and $\post_\sra$ are additive operators on

593: $\wp(\Sigma)_\subseteq$ while $\pret_\sra$ and

594: $\postt_\sra$ are co-additive.

595: 

596: If $R\subseteq \Sigma_1 \times \Sigma_2$ is any relation then the

597: relations $\ok{R^{\exists\exists}},\ok{R^{\forall\exists}}\subseteq

598: \wp(\Sigma_1)\times \wp(\Sigma_2)$ are defined as follows:

599: \begin{itemize}

600: \item[--] $(S_1,S_2)\in \ok{R^{\exists\exists}}~$ iff $~\exists s_1 \in

601: S_1.\exists s_2 \in S_2.\, (s_1,s_2)\in R$;

602: 

603: \item[--] $(S_1,S_2)\in \ok{R^{\forall\exists}}~$ iff $~\forall s_1 \in

604: S_1.\exists s_2 \in S_2.\, (s_1,s_2)\in R$.

605: \end{itemize}

606: 

607: 

608: \subsection{Abstract Interpretation and Completeness}\label{aic}

609: 

610: \subsubsection{Abstract Domains}\label{absdom}

611: 

612: In standard Cousot and Cousot's abstract interpretation,

613: abstract domains can be equivalently specified either by Galois

614: connections, i.e.\ adjunctions, or by upper closure operators

615: (uco's)~\cite{CC77,CC79}.  

616: Let us recall these standard notions.

617: 

618: \paragraph{Galois Connections and Insertions.}

619: If $A$ and $C$ are posets and $\alpha :C\ra A$ and $\gamma :A\ra C$

620: are monotone functions such that $\forall c\in C.\: c \leq_C \gamma

621: (\alpha (c))$ and $\alpha(\gamma (a)) \leq_A a$ then the quadruple

622: $\gdca$ is called a Galois connection (GC for short) between $C$ and

623: $A$.  If in addition $\alpha\circ \gamma =\lambda x.x$ then $\gdca$ is

624: a Galois insertion (GI for short) of $A$ in $C$.  In a GI, $\gamma$ is

625: 1-1 and $\alpha$ is onto.  Let us also recall that the notion of GC is

626: equivalent to that of adjunction: if $\alpha :C\ra A$ and $\gamma

627: :A\ra C$ then $\gdca$ is a GC iff $\forall c\in C.\forall a\in A.\;

628: \alpha (c)\leq_{A} a \Lra c\leq_C \gamma (a)$.  The map $\alpha$

629: ($\gamma$) is called the left- (right-) adjoint to $\gamma$

630: ($\alpha$).  It turns out that one adjoint map $\alpha$/$\gamma$

631: uniquely determines the other adjoint map $\gamma$/$\alpha$ as

632: follows. On the one hand, a map $\alpha:C\ra A$ admits a necessarily

633: unique right-adjoint map $\gamma:A\ra C$ iff $\alpha$ preserves

634: arbitrary lub's; in this case, we have that $\gamma \ud \lambda a.

635: \vee_C \{ c\in C~|~ \alpha(c) \leq_A a\}$. 

636: On the other hand, a map $\gamma:A\ra C$ admits a

637: necessarily unique left-adjoint map $\alpha:C\ra A$ iff $\gamma$

638: preserves arbitrary glb's; in this case, 

639: $\alpha \ud \lambda c. \wedge_A \{ a\in A~|~ c \leq_C \gamma(a)\}$. 

640:   In particular, we have that in any GC

641: $\gdca$ between complete lattices it turns out that $\alpha$ is

642: additive and $\gamma$ is co-additive.  Also, if $\gdca$ is a GI and

643: $C$ is a complete lattice then $A$ is a complete lattice as well and

644: $\tuple{A,\leq_A}$ is order-isomorphic to

645: $\tuple{\img(\gamma),\leq_C}$.

646: 

647: We  assume the standard abstract interpretation framework, where concrete and

648: abstract domains, $C$ and $A$, are complete lattices 

649: related by abstraction and concretization maps $\alpha$ and $\gamma$ forming a GC

650: $\gdca$. $A$ is called an abstraction of $C$

651: and $C$ a concretization of $A$.  The ordering relations on concrete and

652: abstract domains describe the relative precision of domain values:

653: $x\leq y$ means that $y$ is an approximation of $x$ or, equivalently,

654: $x$ is more precise than $y$.

655: Galois connections allow to relate the concrete and

656: abstract notions of relative precision: an abstract value $a\in A$ approximates a

657: concrete value $c\in C$ when $\alpha(c) \leq_A a$, or, equivalently

658: (by adjunction), $c\leq_C \gamma(a)$. As a key consequence of

659: requiring a Galois connection, it turns out that $\alpha(c)$ is the

660: best possible approximation in $A$ of $c$, that is $\alpha(c) = \wedge

661: \{a\in A~|~ c  \leq_C \gamma(a)\}$ holds. 

662: If $\gdca$ is a GI then each value

663: of the abstract domain $A$ is useful in representing $C$, because all

664: the values in $A$ represent distinct members of $C$, being $\gamma$

665: 1-1.  Any GC can be lifted to a GI by identifying in an equivalence class

666: those values of the abstract domain with the same concretization.

667: $\Abs(C)$ denotes the set of abstract domains of $C$ 

668: and  we write $A\in \Abs(C)$ to mean that the abstract

669: domain $A$ is related to $C$

670: through a GI $(\alpha,C,A,\gamma)$. An abstract domain $A$ is

671: disjunctive when the corresponding concretization map $\gamma$ is additive. 

672: 

673: 

674: %

675: 

676: \paragraph{Closure Operators.}

677: An (upper) closure operator, or simply a

678: closure, on a poset $P_\leq$ is an operator $\mu: P\rightarrow P$ that

679: is

680: monotone, idempotent and extensive, i.e., $\forall x\in P.\; x\leq

681: \mu (x)$.  Dually, lower closure operators 

682: are monotone, idempotent, and restrictive, i.e., $\forall x\in P.\; 

683: \mu (x) \leq x$.  

684: $\uco(P)$ denotes the set of closure operators on $P$.

685: %

686: Let $\tuple{C, \leq ,\vee ,\wedge ,\top ,\bot}$ be a complete lattice.

687: A closure $\mu

688: \in\uco(C)$ is uniquely determined by its image $\img(\mu)$, which 

689: coincides with its set of fixpoints, as follows: $\mu=

690: \lambda y.\wedge \{ x\in \img(\mu)~|~ y\leq x\}$. Also, 

691: $X\subseteq C$ is the image of some closure operator $\mu_X$ on $C$

692: iff $X$ is a Moore-family of $C$, i.e., $X=\cM (X)\ud \{\wedge S~|~

693: S\subseteq X\}$~---~where $\wedge \varnothing=\top \in \cM (X)$. In

694: other terms, $X$ is a Moore-family of $C$ when $X$ is meet-closed.  In

695: this case, $\mu_X=\lambda y.\wedge \{ x\in X~|~ y\leq x\}$ is the

696: corresponding closure operator on $C$.  For any $X\subseteq C$, $\cM

697: (X)$ is called the Moore-closure of $X$ in $C$, i.e., $\cM (X)$ is the

698: least (w.r.t.\ set inclusion) subset of $C$ which contains $X$ and is

699: a Moore-family of $C$. Moreover, it turns out that for any $\mu \in

700: \uco(C)$ and any Moore-family $X\subseteq C$, $\mu_{\img(\mu)} = \mu$

701: and $\img(\mu_X)=X$. Thus, closure operators on $C$ are in bijection

702: with Moore-families of $C$. This allows us to consider a closure

703: operator $\mu\in \uco(C)$ both as a function $\mu:C\ra C$ and as a

704: Moore-family $\img(\mu)\subseteq C$.  This is particularly useful and

705: does not give rise to ambiguity since one can distinguish the use of a

706: closure $\mu$ as function or set according to the context.

707: 

708: It turns out that $\tuple{\mu,\leq}$ is a complete meet

709: subsemilattice of $C$, i.e.\ $\wedge$ is its glb, 

710: but, in general, it is not a complete sublattice of $C$, since

711: the lub in $\mu$~---~defined by $\lambda Y\subseteq \mu.\, \mu

712: (\vee Y)$~---~might be different from that in $C$.  In fact, it turns

713: out that $\mu$ is a complete sublattice of $C$ (namely, $\img(\mu)$

714: is also join-closed) iff $\mu$ is additive.  

715: 

716: %

717: If $C$ is a complete lattice then $\uco(C)$ endowed with the pointwise ordering

718: $\sqsubseteq$ is a

719: complete lattice denoted by

720: $\tuple{\uco(C),\sqsubseteq,\sqcup,\sqcap,\lambda x.\top,\lambda x.x}$,

721: where for every $\mu,\eta \in\uco(C)$, $\{

722: \mu_i \}_{i\in I} \subseteq\uco(C)$ and $x\in C$:

723: \begin{itemize}

724: \item[--] $\mu \sqsubseteq \eta$ iff $\forall y\in C.\; \mu (y) \leq

725:  \eta(y)$ iff  $\img(\eta)

726: \subseteq \img(\mu)$;

727: \item[--] $(\sqcap_{i\in I} \mu_i)(x) = \wedge_{i\in I} \mu_i (x)$;

728: \item[--] $x \in \sqcup_{i\in I} \mu_i \:\Lra\:

729: \forall i\in I.\; x\in \mu_i$;

730: \item[--] $\lambda x.\top$ is the greatest element, whereas $\lambda x.x$ is

731: the least element.

732: \end{itemize}

733: Thus, the glb in $\uco(C)$ is defined pointwise, while the

734: lub of a set of closures $\{

735: \mu_i \}_{i\in I} \subseteq\uco(C)$ is the closure whose image 

736: is given by the set-intersection $\cap_{i \in I}

737: \mu_i$.

738: %Let us also recall the following properties of

739: %uco's that we will use without mention in our proofs.

740: %For $\mu,\rho \in\uco(C)$ and $Y\subseteq C$,

741: %\begin{itemize}

742: %\item[{\rm (1)}] $\mu\sqsubseteq \rho$ $\Ra$ $\mu \circ

743: %\rho = \rho \circ \mu = \rho$; 

744: %\item[{\rm (2)}] $\mu (\vee Y) =

745: %\mu (\vee_{y\in Y} \mu(y))$;

746: %\item[{\rm (3)}] if

747: %$\mu,\rho\in \uco(\wp(\Sigma)_\subseteq)$, for some set $\Sigma$, and $\mu$

748: %and $\rho$ are both additive then $\mu=\rho$ iff $\forall s\in

749: %\Sigma.\:\mu(\{s\})=\rho(\{s\})$.

750: %\end{itemize} 

751: 

752: \paragraph{The Lattice of Abstract Domains.}

753: It is well known since \cite{CC79} that abstract domains can be

754: equivalently specified either as Galois insertions or as 

755: closures.  These two

756: approaches are completely equivalent. On the one hand, if $\mu\in\uco(C)$ and

757: $A$ is a complete lattice which is isomorphic to $\img(\mu)$, where 

758: $\iota : \img(\mu)\ra A$ and $\iota^{-1}:

759: A\ra\img(\mu)$ provide the isomorphism, then

760: $(\iota\circ\mu,C,A,\iota^{-1} )$ is a GI. On the other hand, if $\gdca$ is a GI then

761: $\mu_A \ud \gamma \circ \alpha\in\uco(C)$ is the closure associated with $A$

762: such that $\tuple{\img(\mu_A),\leq_C}$ is a complete lattice which is isomorphic to

763: $\tuple{A,\leq_A}$. Furthermore, these two constructions

764: are inverse of each other.  Let us also remark that an abstract domain

765: $A$ is disjunctive iff $\mu_A$ is additive. Given an abstract domain $A$ specified

766: by a GI $\gdca$, its associated closure $\gamma\circ\alpha$ on $C$ can

767: be thought of as the ``logical meaning'' of $A$ in $C$, since this is

768: shared by any other abstract representation for the objects of $A$.

769: Thus, the closure operator approach is particularly convenient when

770: reasoning about properties of abstract domains independently from the

771: representation of their objects.  

772: 

773: 

774: Abstract domains specified by GIs can be pre-ordered w.r.t.\ precision

775: as follows: if $A_1,A_2 \in \Abs(C)$ then $A_1$ is more precise (or

776: concrete) than

777: $A_2$ (or $A_2$ is an abstraction of $A_1$), denoted by $A_1 \preceq

778: A_2$, when $\mu_{A_1} \sqsubseteq \mu_{A_2}$.  The pointwise

779: ordering $\sqsubseteq$ between uco's corresponds therefore to the standard ordering used to

780: compare abstract domains with respect to their precision. Also, $A_1$

781: and $A_2$ are equivalent, denoted by $A_1 \simeq A_2$, when their

782: associated closures coincide, i.e.\ $\mu_{A_1}=\mu_{A_2}$.  Hence, the

783: quotient $\Abs(C)_{/\simeq}$ gives rise to a poset that, by a slight

784: abuse of notation,  is simply denoted by 

785: $\tuple{\Abs(C),\sqsubseteq}$. Thus, when we write $A\in\Abs(C)$ we

786: mean that $A$ is any representative of an equivalence class in 

787: $\Abs(C)_{/\simeq}$

788: and is 

789: specified by a Galois insertition $\gdca$.  

790: It turns out that 

791: $\tuple{\Abs(C),\sqsubseteq}$ is a complete lattice, called the

792: lattice of abstract interpretations of $C$

793: \cite{CC77,CC79},  because it is

794: isomorphic to the complete lattice $\tuple{\uco(C),\sqsubseteq}$.

795: Lub's and glb's in $\Abs(C)$ have therefore the following reading as

796: operators on domains.  Let $\{ A_i\}_{i\in I}\subseteq\Abs(C)$:

797: (i)~$\sqcup_{i\in I}A_i $ is the most concrete among the domains which

798: are abstractions of all the $A_i$'s; (ii)~$\sqcap_{i\in I} A_i $ is

799: the most abstract among the domains which are more concrete than every

800: $A_i$~---~this latter domain is also known as reduced product of all

801: the $A_i$'s.

802: 

803: 

804: \subsubsection{Completeness}\label{secco}

805: Let $C$ be a concrete domain, $f:C\ra C$ be a concrete semantic function\footnote{For

806: simplicity of notation we consider here unary functions since the extension

807: to generic $n$-ary functions is straightforward.}  

808: and let $f^\sharp:A \ra A$ be a corresponding abstract

809: function on an abstract domain $A\in \Abs(C)$ specified by a GI 

810: $(\alpha,C,A,\gamma)$.   Then,

811: $\tuple{A,f^\sharp}$ is a sound abstract interpretation when $\ok{\alpha

812: \circ f \sqsubseteq f^\sharp\circ \alpha}$ holds. The abstract

813: function $\ok{f^\sharp}$ is called a correct approximation on $A$ of

814: $f$. 

815: This means that a concrete

816: computation  $f(c)$

817: can be correctly approximated in $A$ by $\ok{f^\sharp (\alpha (c))}$, namely $\alpha(f(c))

818: \leq_A \ok{f^\sharp (\alpha (c))}$. An abstract function 

819: $\ok{f_1^\sharp}:A \ra A$ is more precise than 

820: $\ok{f_2^\sharp}:A \ra A$ when 

821: $\ok{f_1^\sharp} \sqsubseteq \ok{f_2^\sharp}$. 

822: Since  $\ok{\alpha

823: \circ f \sqsubseteq f^\sharp\circ \alpha}$ holds iff  $\ok{\alpha

824: \circ f \circ \gamma \sqsubseteq f^\sharp}$ holds, 

825: the abstract function

826: $\ok{f^A \ud \alpha \circ f \circ \gamma: A\rightarrow A}$ is called the best correct

827: approximation of $f$ in $A$.  

828: 

829: Completeness in abstract interpretation

830: corresponds to requiring that, in addition to soundness, no loss of

831: precision occurs when $f(c)$ is approximated in $A$  

832: by $\ok{f^\sharp(\alpha(c))}$. Thus, completeness of $\ok{f^\sharp}$

833: for $f$ is encoded by the equation $\ok{\alpha \circ f = f^\sharp \circ

834: \alpha}$. This is also called backward completeness because a dual

835: form of forward completeness may be considered. 

836: As a very simple example, let us consider the abstract domain

837: $\mathit{Sign}$ representing the sign of an integer variable, namely

838: $\mathit{Sign} = \{\bot, \ok{\bZ_{< 0}}, 0, \ok{\bZ_{>0}}, \top\}\in

839: \Abs(\wp(\bZ)_\subseteq )$. Let us consider the binary concrete operation of

840: integer addition on sets

841: of integers, that is 

842: $X+Y \ok{\ud} \{x+y~|~ x\in X,\, y\in Y\}$, and the square operator on sets

843: of integers, that is $\ok{X^2} \ok{\ud} \ok{\{x^2 ~|~ x\in X\}}$.  It turns out that the

844: best correct approximation

845: $\ok{+^\mathit{Sign}}$ of integer addition in

846: $\mathit{Sign}$ is sound but not complete~---~because $\alpha(\{-1\} +

847: \{1\}) = \ok{0 <_{\mathit{Sign}}}  \top = \alpha(\{-1\})

848: \ok{+^{\mathit{Sign}}} \alpha(\{1\})$~---~ while it is easy to check

849: that the best correct approximation of

850: the square operation in $\mathit{Sign}$ is instead complete. 

851: 

852: A dual form of completeness may be considered.  The

853: soundness condition $\ok{\alpha \circ f \sqsubseteq f^\sharp\circ

854: \alpha}$ can be equivalently formulated as $\ok{f\circ \gamma

855: \sqsubseteq \gamma \circ f^\sharp}$. Forward completeness for $\ok{f^\sharp}$

856: corresponds to requiring that the equation $\ok{f\circ \gamma = \gamma

857: \circ f^\sharp}$ holds,

858: and therefore means that no loss of precision occurs when a concrete computation

859: $f(\gamma(a))$, for some abstract value $a\in A$, is approximated in

860: $A$ by $\ok{f^\sharp (a)}$. Let us

861: notice that backward and forward completeness are orthogonal

862: concepts. In fact: (1) as observed above, we have that $\ok{+^\mathit{Sign}}$ is

863: not backward complete while it is forward complete because for any $a_1,a_2 \in

864: \mathit{Sign}$, $\gamma(a_1) + \gamma(a_2) = 

865: \gamma( a_1 \ok{+^\mathit{Sign}} a_2)$; (2)

866: the best correct approximation $\ok{(\cdot)^{2_{\mathit{Sign}}}}$ of

867: the square operator on $\mathit{Sign}$ is

868: not forward complete because $\ok{\gamma( \bZ_{>0} )^2} \subsetneq

869: \gamma(\mathbb{Z}_{>0})=\gamma( \ok{(\bZ_{>0})^{2_{\mathit{Sign}}}})$

870: while, as observed above, it is instead backward complete. 

871: 

872: 

873: Giacobazzi et al.~\cite{jacm} observed that completeness uniquely

874: depends upon the abstraction map, i.e.\ upon the abstract domain: this

875: means that if $\ok{f^\sharp}$ is backward complete for $f$ then the best correct

876: approximation $\ok{f^A}$ of $f$ in $A$ is

877: backward complete as well, and, in this case, $\ok{f^\sharp}$ indeed coincides

878: with $\ok{f^A}$.  Hence, for any abstract domain $A$, one can define

879: a backward complete abstract operation $\ok{f^\sharp}$  on $A$ if and only if $\ok{f^A}$ is

880: backward complete. Thus, an abstract domain $A \in \Abs(C)$ is defined to be

881: backward complete for $f$ iff the equation $\alpha\circ f = \ok{f^A}\circ \alpha$ holds. This

882: simple observation makes backward completeness an abstract domain property,

883: namely an intrinsic characteristic of the abstract domain.  Let us

884: observe that $\alpha\circ f = \ok{f^A} \circ \alpha$ holds iff $\gamma \circ

885: \alpha \circ f = \gamma \circ \ok{f^A} \circ \alpha = \gamma \circ \alpha

886: \circ f \circ \gamma \circ \alpha$ holds, so that $A$ is

887: backward complete for $f$ when $\mu_A \circ f = \mu_A \circ f \circ

888: \mu_A$. Thus, a closure $\mu\in \uco(C)$, that defines some abstract

889: domain, is backward complete for $f$ when $\mu \circ f = \mu \circ f \circ

890: \mu$ holds.

891: Analogous observations apply to 

892: forward completeness, which is also an abstract domain property:

893: $A\in \Abs(C)$ is forward complete for $f$ (or forward $f$-complete) 

894: when $f \circ \mu_A = \mu_A \circ f \circ

895: \mu_A$, while a closure $\mu\in \uco(C)$

896: is forward complete for $f$ when $f \circ \mu = \mu \circ f \circ

897: \mu$ holds.

898: 

899: 

900: Let us also recall that, by a well-known result (see, e.g.,

901: \cite[Theorem~7.1.0.4]{CC79}, \cite[Fact~2.3]{ap86} and

902: \cite[Lemma~4.3]{db83}),  backward 

903: complete abstract domains are ``fixpoint complete'' as well. This

904: means that if $A\in \Abs(C)$ is backward complete for a concrete monotone

905: function $f:C\ra C$ then 

906: $\alpha(\lfp(f)) = \ok{\lfp(f^A)}$. Moreover, if $\alpha$ and $f$ are

907: both co-continuous then this

908: also holds for greatest fixpoints, namely $\alpha(\gfp(f)) =

909: \ok{\gfp(f^A)}$. 

910: As far as forward completeness is concerned, the following result

911: holds.  

912: \begin{lemma}\label{fixrem2}

913: If $A\in \Abs(C)$ is forward complete

914: for a monotone $f$ then $\alpha(\gfp(f))= \gfp(f^A)$. 

915: Moreover, if $\gamma$ and $f$ are

916: both continuous and $\gamma(\bot_A)=\bot_C$

917: then $\alpha(\lfp(f))= \lfp(f^A)$.

918: \end{lemma}

919: \begin{proof}

920: Let us show that $\alpha(\gfp(f)) = \gfp(f^A)$.

921: On the one hand, since $\gfp(f) \leq \gamma(\alpha (\gfp(f)))$, we have that

922: $\gfp(f)=f(\gfp(f)) \leq f(\gamma(\alpha (\gfp(f))))$, therefore, by using

923: forward completeness, $\gfp(f) \leq \gamma(f^A (\alpha (\gfp(f))))$. Thus,

924: $\alpha(\gfp(f)) \leq f^A (\alpha(\gfp(f)))$, from which follows that

925: $\alpha(\gfp(f)) \leq \gfp (f^A)$. On the other hand, by using forward

926: completeness, $f(\gamma(\gfp(f^A))) = \gamma (f^A(\gfp(f^A))) =

927: \gamma(\gfp(f^A))$, so that $\gamma(\gfp(f^A)) \leq \gfp(f)$, and

928: therefore, by applying $\alpha$, we obtain that $\gfp(f^A) =

929: \alpha(\gamma(\gfp(f^A))) \leq \alpha(\gfp(f))$. \\

930: %

931: Assume now that $\gamma$ and $f$ are

932: both continuous and $\gamma(\bot_A)=\bot_C$.

933: Let us show

934: by induction on $k$ that for any $k\in \mathbb{N}$, 

935: $\gamma ((f^A)^{k,\uparrow} (\bot_A)) =

936: f^{k,\uparrow} (\bot_C)$. 

937: \\

938: ($k=0$): By hypothesis, $\gamma ((f^A)^{0,\uparrow} (\bot_A)) = \gamma (\bot_A) =\bot_C = 

939: f^{0,\uparrow} (\bot_C)$.\\ 

940: ($k+1$): 

941: \begin{align*}

942: \gamma ((f^A)^{k+1,\uparrow} (\bot_A)) &=   \\

943: \gamma (f^A ((f^A)^{k,\uparrow} (\bot_A))) &= \text{~~~[by forward

944: completeness]}\\ 

945: f(\gamma ((f^A)^{k,\uparrow}

946: (\bot_A))) &= \text{~~~[by inductive

947: hypothesis]}\\ 

948: f(f^{k,\uparrow} (\bot_C)) &=  \\

949: f^{k+1,\uparrow} (\bot_C)). &

950: \end{align*}

951: Thus, by applying $\alpha$, we obtain that for any $k\in \mathbb{N}$, 

952: $$(f^A)^{k,\uparrow} (\bot_A) =

953: \alpha (f^{k,\uparrow} (\bot_C)).\eqno(\dagger)$$

954: Since $\gamma$ and $f$ are continuous and $\alpha$ is always additive,

955: we have that $f^A = \alpha \circ f \circ \gamma$ is continuous because

956: it is a composition of continuous functions. Hence:

957: \begin{align*}

958: \lfp(f^A) &=  \text{~~~[by Knaster-Tarski's theorem]} \\

959: \vee_{k\in \bN} (f^A)^{k,\uparrow}(\bot_A) & = \text{~~~[by

960: $(\dagger)$]} \\

961: \vee_{k\in \bN} \alpha (f^{k,\uparrow}(\bot_C)) & = \text{~~~[as

962: $\alpha$ is additive]} \\

963: \alpha(\vee_{k\in \bN} f^{k,\uparrow}(\bot_C)) & = \text{~~~[by

964: Knaster-Tarski's theorem]} \\

965: \alpha(\lfp(f)) &

966: \end{align*}

967: and this concludes the proof. 

968: \end{proof}

969: 

970: It is worth noting that concretization maps of abstract domains which

971: satisfies the ascending chain conditions (i.e., every ascending chain

972: is eventually stationary) are always trivially continuous. 

973: 

974: \subsubsection{Shells}

975: Refinements of abstract domains have been studied from the

976: beginning of abstract interpretation \cite{CC77,CC79} and led to the

977: notion of shell of an abstract domain \cite{fgr96,GR97,jacm}.   

978: Given a generic poset $P_\leq$ of semantic objects~---~where $x\leq y$

979: intuitively means  that $x$ is a ``refinement'' of $y$~---~and a property $\cP

980: \subseteq P$ of these objects, 

981: the generic 

982: notion of \emph{shell} goes as follows:

983: the $\cP$-shell of an object $x \in P$ is defined to be 

984: an object $s_x \in P$  such that:

985: \begin{itemize}

986: \item[{\rm (i)}] $s_x$ satisties the property $\cP$, 

987: \item[{\rm (ii)}] $s_x$ is a refinement  of $x$, and

988: \item[{\rm (iii)}] $s_x$ is the greatest among the objects satisfying (i)

989: and (ii). 

990: \end{itemize}

991: Note that if a $\cP$-shell exists then it is unique. Moreover, if the

992: $\cP$-shell exists for any object in $P$ then it turns out that the operator mapping

993: $x\in P$ to its $\cP$-shell is a lower closure operator on $\cP$,

994: being monotone, idempotent and reductive: this operator will be called

995: the \emph{$\cP$-shell refinement}. 

996: We will be particularly interested in shells of abstract domains and

997: partitions, namely shells in the complete lattices of abstract domains and

998: partitions. 

999: Given a state space $\Sigma$ and a partition property

1000: $\cP\subseteq \Part(\Sigma)$, the $\cP$-shell of $P\in \Part(\Sigma)$

1001: is the coarsest refinement of $P$ satisfying $\cP$, when this exists. 

1002: Also, given a concrete domain $C$ and a domain property

1003: $\cP\subseteq \Abs(C)$, the $\cP$-shell of $A\in \Abs(C)$, when this

1004: exists, is the

1005: most abstract domain that satisfies $\cP$ and refines $A$.  

1006: Giacobazzi et al.~\cite{jacm} gave a constructive characterization of

1007: backward complete abstract domains, under the assumption of dealing

1008: with continuous concrete functions.  As a consequence, they showed 

1009: that backward complete shells always exist when the concrete

1010: functions are continuous. 

1011: In Section~\ref{csp} we will follow

1012: this same idea for forward completeness and this will provide the

1013: link between strongly preserving abstract models and complete

1014: abstract interpretations.

1015: 

1016: 

1017: \subsection{Abstract Model Checking and Strong Preservation}\label{amc}

1018: 

1019: Standard temporal languages like $\CTL$, $\CTLS$, $\ACTL$, the

1020: $\mu$-calculus, $\LTL$, etc., are interpreted on models specified as

1021: Kripke structures.  Given a set $\mathit{AP}$ of atomic propositions

1022: (of some language), a Kripke structure $\cK= (\Sigma ,\sra,\ell)$ over

1023: $\mathit{AP}$ consists of a transition system $(\Sigma ,\sra)$ together

1024: with a state labeling function $\ell:\Sigma \ra \wp(\mathit{AP})$. We

1025: use the following notation: for any $s\in \Sigma$, $[s]_\ell \ud

1026: \{s'\in \Sigma~|~ \ell(s)=\ell(s')\}$, while $P_\ell \ud \{[s]_\ell~|~

1027: s\in \Sigma\}\in \Part(\Sigma)$ denotes the state partition that is induced by

1028: $\ell$.  The notation $s \ok{\models^\cK} \varphi$ means

1029: that a state $s\in \Sigma$ satisfies in $\cK$ a state formula $\varphi$ of

1030: some language $\fL$, where the specific definition of the satisfaction

1031: relation $\ok{\models^\cK}$ depends on the language $\fL$

1032: (interpretations of standard logical/temporal operators can be found

1033: in \cite{cgp99}).

1034: 

1035: Standard abstract model checking \cite{cgl94,cgp99} 

1036: relies on abstract Kripke structures that are defined

1037: over partitions of the concrete state space $\Sigma$.

1038: A set $A$ of abstract states is related to $\Sigma$ 

1039: by a surjective abstraction $h:\Sigma \ra A$ that maps concrete states into

1040: abstract states and thus gives rise to a state partition

1041: $P_h \ud \{h^{-1}(a)~|~a\in A\} \in

1042: \Part(\Sigma)$. 

1043: Thus, in standard abstract model checking, formulae are interpreted on

1044: an abstract Kripke structure $\cA = (A, \ok{\sra^\sharp},

1045: \ok{\ell^\sharp})$ whose states are an abstract

1046: representation in $A$ of some block of the partition $P_h$.  Given a

1047: specification language $\fL$ of state formulae, a weak preservation result for $\fL$

1048: guarantees that if a formula in $\fL$ holds on an abstract Ktipke structure

1049: $\cA$ then it also holds on the corresponding concrete structure

1050: $\cK$: for any $\varphi\in \fL$, $a\in A$ and $s\in \Sigma$ such that

1051: $h(s)=a$, if $a

1052: \ok{\models^{\cA}} \varphi$ then

1053: $s \ok{\models^{\cK}} \varphi$.  Moreover, 

1054: strong preservation (s.p.\ for short) for $\fL$ encodes the equivalence of

1055: abstract and concrete validity for formulae in $\fL$:

1056: for any $\varphi\in \fL$, $a\in A$ and $s\in \Sigma$ such that

1057: $h(s)=a$, $a

1058: \ok{\models^{\cA}} \varphi$ if and only if

1059: $s \ok{\models^{\cK}} \varphi$.

1060:  

1061: The definition of weakly/strongly preserving  

1062: abstract Kripke structures depends on the language $\fL$. 

1063: Let us recall some well-known examples \cite{cgl94,cgp99,gl94}.

1064: Let $\cK= (\Sigma ,\sra,\ell)$ be a concrete Kripke

1065: structure

1066: $h: \Sigma \ra A$ be a surjection. 

1067: \begin{itemize}

1068: \item[{\rm (i)}] Consider the language $\ACTLS$. If $P_h\preceq

1069: P_\ell$ then the abstract Kripke

1070: structure $\cA = (A, \ok{\sra_h^{\exists\exists}}, \ell_h)$

1071: weakly preserves $\ACTLS$,

1072: where $\ell_h (a) =\cup \{\ell(s)~|~s\in \Sigma,\: h(s)=a\}$ and

1073: $\ok{\sra_h^{\exists\exists}}\subseteq A\times A$ is defined as: 

1074: $h(s_1)\, \ok{\sra_h^{\exists\exists}}\, h(s_2)  \;\,\Lra\;\,\exists

1075: s_1',s_2'.\: h(s_1')=h(s_1) \:\;\&\;\: h(s_2')=h(s_2) \:\;\&\;\:

1076: s_1' \sra s_2'$.

1077: \item[{\rm (ii)}] Let

1078: $P_{\mathrm{sim}}\in \Part(\Sigma)$ be the partition induced by 

1079: simulation equivalence on

1080: $\cK$. If $P_h =

1081: P_{\mathrm{sim}}$ (this also holds when $P_h \preceq P_{\mathrm{sim}}$)

1082: then the abstract Kripke

1083: structure $\cA = (A, \ok{\sra_h^{\forall\exists}},\ell_h)$ strongly preserves

1084: $\ACTLS$, where 

1085: $h(s_1)\,\ok{\sra_h^{\forall\exists}} \, h(s_2) \;\,\Lra\;\,\forall

1086: s_1'.\: h(s_1')=h(s_1).\: \exists s_2'.\: h(s_2')=h(s_2) \;\&\;

1087: s_1'\sra s_2'$.

1088: %In this case, Bustan and Grumberg \cite{bg03} 

1089: %show that there exists a smallest (in the number of transitions) 

1090: %abstract transition relation on $A$  and provide an

1091: %algorithm for computing it.

1092: \item[{\rm (iii)}] Let

1093: $P_{\mathrm{bis}}\in \Part(\Sigma)$ 

1094: be the partition induced by bisimulation equivalence on $\cK$. 

1095: If $P_h = P_{\mathrm{bis}}$ (this also holds when $P_h \preceq P_{\mathrm{bis}}$)

1096: then the abstract Kripke

1097: structure $\cA = (A, \ok{\sra_h^{\exists\exists}},

1098: \ell_h)$ strongly preserves $\CTLS$. 

1099: \end{itemize}

1100:  

1101: 

1102: Following Dams \cite[Section~6.1]{dams96} 

1103: and Henzinger et al.~\cite[Section~2.2]{hmr05},

1104: the notion of strong preservation  can be also given w.r.t.\ a mere

1105: state partition  rather than w.r.t.\ an abstract Kripke structure. 

1106: Let $\ok{\grasse{\cdot}_\cK}: \fL \ra \wp(\Sigma)$ be the semantic

1107: function of state formulae in $\fL$ w.r.t.\ a Kripke structure

1108: $\cK = (\Sigma ,\sra,\ell)$, i.e., $\ok{\grasse{\varphi}_\cK} \ud \{s\in \Sigma~|~

1109: s\ok{\models^\cK} \varphi\}$.  

1110: Then,  the semantic interpretation of $\fL$ on $\cK$ induces

1111: the following logical equivalence $\ok{\equiv_\fL^\cK}\: \subseteq \Sigma 

1112: \times \Sigma $:~ $$s\,\ok{\equiv^\cK_\fL}\, s' \text{~~iff~~} 

1113: \forall \varphi \in \fL.\, s\in

1114: \ok{\grasse{\varphi}_\cK} \: \Lra \: s' \in \ok{\grasse{\varphi}_\cK}.$$

1115: Let

1116: $\ok{P_\fL} \in \Part(\Sigma)$ be the partition induced by

1117: $\ok{\equiv^\cK_\fL}$  (the

1118: index $\cK$ denoting the Kripke structure is omitted). Then, a

1119: partition $P\in \Part(\Sigma)$ is strongly preserving\footnote{Dams 

1120: \cite{dams96} uses the term ``fine'' instead of ``strongly

1121: preserving''.} for $\fL$

1122: (when interpreted on $\cK$) if $P \preccurlyeq \ok{P_\fL}$. Thus,

1123: $\ok{P_\fL}$ is the coarsest partition that is strongly preserving for

1124: $\fL$. 

1125: For a number of well known temporal languages, like 

1126: $\ACTLS$, $\CTLS$ (see, respectively, the above points~(ii) and (iii)), $\CTLSX$ and

1127: the fragments of the $\mu$-calculus described by Henzinger et al.~\cite{hmr05}, 

1128: it turns out that if $P$ is

1129: strongly preserving for $\fL$ then the abstract

1130: Kripke structure $(P, \ok{\sra^{\exists\exists}},

1131: \ell_\fL)$ is strongly

1132: preserving for $\fL$, where, for any $B\in P$, $\ell_\fL (B) =

1133: \cup_{s\in B} \ell(s)$.

1134: In particular,  $(P_\fL, \ok{\sra^{\exists\exists}},

1135: \ell_\fL)$  is strongly preserving for $\fL$ and, additionally, $P_\fL$ is the

1136: smallest possible abstract state space, namely   

1137: if $\cA = (A, \ok{\sra^\sharp}, \ok{\ell^\sharp})$ is an abstract Kripke structure that

1138: strongly preserves $\fL$ then $|P_\fL| \leq |A|$. 

1139: %Also, Henzinger et al.~\cite[Section~2.2]{hmr05} give the following definition:

1140: %a generic temporal

1141: %language $\fL$ admits abstraction when the abstract Kripke structure 

1142: %$(P_\fL, \ok{R^{\exists\exists}}, \mathit{AP}, \ell_\fL)$ is strongly

1143: %preserving for $\fL$. 

1144: 

1145: 

1146: However, given a language $\fL$ and a  Kripke structure 

1147: $\cK$ where formulae of $\fL$ are interpreted, 

1148: the following example shows that  it is not always possible to

1149: define an abstract Kripke structure $\cA$ on the partition

1150: $P_\fL$ such that $\cA$ strongly preserves $\fL$.

1151: 

1152: \begin{figure}[t]

1153:   \centering

1154:   \mbox{

1155:     \xymatrix  { 

1156:      *+[o][F-]{\phantom{Y}R\phantom{Y}}\ar[r] ^(0.40){\color{red}\mathit{stop}} &  	    

1157:       *+[o][F-]{\phantom{Y}RY\phantom{Y}} \ar[r] ^(0.33){\color{red}\mathit{stop}} & 

1158:       *+[o][F-]{\phantom{Y}G\phantom{Y}}\ar[r] ^(0.33){\color{green}\mathit{go}}  &

1159:       *+[o][F-]{\phantom{Y}Y\phantom{Y}}\ar@(ul,ur)[lll] _(0.12){\color{green}\mathit{go}}

1160: 	\\

1161:     }

1162:   }

1163: \caption{A U.K.\ traffic light.}

1164:   \label{figsem}

1165: \end{figure}

1166: 

1167: 

1168: \begin{example2}\label{semaforo}

1169: Consider the following simple language $\fL$:

1170: $$\fL\ni \varphi ::= \mathit{stop} ~|~ \mathit{go} ~|~ \mathrm{AXX} \varphi$$

1171: and the Kripke structure $\cK$ depicted in Figure~\ref{figsem}, where

1172: superscripts determine the labeling function.

1173: $\cK$ models a four-state traffic light controller (like in the U.K.\ and in

1174: Germany): Red $\rightarrow$ RedYellow $\rightarrow$ Green

1175: $\rightarrow$ Yellow. 

1176: According to the standard semantics of $\mathrm{AXX}$, 

1177: we have that $s\ok{\models^\cK} \mathrm{AXX}\varphi$ iff for any path

1178: $s_0 s_1 s_2\ldots $

1179: starting from $s_0=s$, it happens that $s_2 \ok{\models^\cK} \varphi$. 

1180: It turns out that

1181: $\ok{\grasse{\mathrm{AXX}\mathit{stop}}_\cK}=\{G,Y\}$ and 

1182: $\ok{\grasse{\mathrm{AXX}\mathit{go}}_\cK}=\{R,RY\}$. Thus, we have

1183: that $\ok{P_\fL} =

1184: \ok{\{\{R,RY\},\{G,Y\}\}}$. 

1185: However, let us show that there exists no abstract transition relation $\ok{\sra^\sharp}

1186: \subseteq \ok{P_\fL \times P_\fL}$ such that the abstract Kripke structure

1187: $\ok{\cA}= (\ok{P_\fL},

1188: \ok{\sra^\sharp} ,\ok{\ell_\fL})$  strongly preserves $\ok{\fL}$. Assume

1189: by contradiction that such an abstract Kripke structure $\cA$

1190: exists. Let $B_1 = \{R,RY\}\in \ok{P_\fL}$ and $B_2 = \{G,Y\}\in \ok{P_\fL}$.

1191: Since $R \ok{\models^\cK}

1192: \mathrm{AXX}\mathit{go}$ and

1193: $G \ok{\models^\cK} \mathrm{AXX}\mathit{stop}$,   by strong preservation,

1194: it must be that $B_1 \ok{\models^\cA} \mathrm{AXX}\mathit{go}$ 

1195: and $B_2 \ok{\models^\cA} \mathrm{AXX}\mathit{stop}$. Hence, necessarily,

1196: $B_1 \ok{\sra^\sharp} B_2$ and $B_2 \ok{\sra^\sharp} B_1$. This leads to the

1197: contradiction

1198: $B_1 \ok{{\not\models}^\cA}

1199: \mathrm{AXX}\mathit{go}$. In fact, 

1200: if $\ok{\sra^\sharp} = 

1201: \{(B_1,B_2),(B_2,B_1)\}$ then we would have that $B_1 \ok{{\not\models}^\cA}

1202: \mathrm{AXX}\mathit{go}$. On the other hand, if, instead, $B_1

1203: \ok{\sra^\sharp} B_1$ (the case $B_2 \ok{\sra^\sharp} B_2$ is

1204: analogous), then  we would still

1205: have that 

1206: $B_1 \ok{{\not\models}^\cA}

1207: \mathrm{AXX}\mathit{go}$. Even more, along the same lines it is not hard

1208: to show that no proper abstract Kripke structure that strongly preserves

1209: $\fL$ can

1210: be defined,  because even if either $B_1$ or $B_2$ is split

1211: we still cannot define an abstract transition relation that is strongly

1212: preserving for $\fL$. 

1213: %In this case, a safety property like

1214: %$\mathrm{AG}(\mathit{stop}\rightarrow \mathrm{AXX} \mathit{go})$ cannot

1215: %be proved on some abstract Kripke structure that properly abstracts the concrete

1216: %model $\cK$.

1217: \qed

1218: \end{example2}

1219: 

1220: 

1221: 

1222: \section{Partitions as Abstract Domains}\label{paa}

1223: 

1224: Let $\Sigma$ be any (possibly infinite) set of states.  Following

1225: \cite[Section~5]{CC94}, a  partition

1226: $P\in \Part(\Sigma)$ can be viewed as an abstraction of

1227: $\wp(\Sigma)_\subseteq$ as follows:  

1228: any $S\subseteq

1229: \Sigma$ is over approximated by the unique minimal cover of $S$ in $P$, 

1230: namely by the 

1231: union of all the  blocks $B\in P$ such that $B\cap S\neq

1232: \varnothing$. A graphical example is depicted on the 

1233: left-hand side of Figure~\ref{figuco}. This abstraction is formalized

1234: by a GI $(\alpha_P,\wp(\Sigma)_\subseteq,\wp(P)_\subseteq, \gamma_P)$

1235: where: 

1236: $$\alpha_P(S) \ud \{B\in P~|~ B \cap S\neq \varnothing\}~~~~~~~

1237: \gamma_P(\mathcal{B})\ud \cup_{B\in \mathcal{B}} B.$$

1238: Hence, any partition $P\in \Part(\Sigma)$ induces an abstract domain

1239: $\adp(P)\in \Abs(\wp(\Sigma))$, and an 

1240: abstract domain $A\in \Abs(\wp(\Sigma))$ is called \emph{partitioning} when $A$ is

1241: equivalent to $\adp(P)$ for some partition $P$. 

1242: Observe that the closure 

1243: $\adp(P)=\gamma_P\circ

1244: \alpha_P$

1245: associated to a partitioning abstract domain is

1246: defined as $\adp(P)

1247: = \lambda S.\cup \{B\in P~|~ B \cap S\neq \varnothing\}$. 

1248: Accordingly, a closure $\mu\in \uco(\wp(\Sigma))$ that coincides with 

1249: $\gamma_P \circ \alpha_P$, for some

1250: partition $P$, is called partitioning. 

1251:   We denote by $\Absp(\wp(\Sigma))$ and $\ucop(\wp

1252: (\Sigma ))$  the sets of, respectively, partitioning abstract

1253: domains and closures on $\wp(\Sigma)$. As noted in

1254: \cite{CC99}, a 

1255: surjective abstraction $h:\Sigma \ra A$ used in standard abstract

1256: model checking  that maps concrete states into

1257: abstract states (cf.\ Section~\ref{amc}) gives rise to a partitioning Galois insertion

1258: $(\alpha_h, \wp(\Sigma)_\subseteq,\wp(A)_\subseteq,\gamma_h)$  where $\alpha_h \ud \lambda

1259: S\subseteq \Sigma. \{h(s)\in A~|~ s\in S\}$ and $\gamma_h \ud \lambda X \subseteq

1260: A. \{s \in \Sigma~|~h(s)\in X\}$.

1261: 

1262: Partitions can be also viewed as dual abstractions

1263: when a set $S$ is under approximated by the union of all the blocks

1264: $B\in P$ such that $B\subseteq S$. A graphical example of this under approximation is

1265: depicted on the right-hand side of

1266: Figure~\ref{figuco}. This dual abstraction is formalized

1267: by the GI

1268: $(\widetilde{\alpha}_P,\wp(\Sigma)_\supseteq,\wp(P)_\supseteq,

1269: \widetilde{\gamma}_P)$ 

1270: where the ordering on the concrete domain $\wp(\Sigma)$ is given by

1271: the subset relation and  

1272: $$\widetilde{\alpha}_P(S) \ud \{B\in P~|~ B \subseteq S\}~~~~~~~

1273: \widetilde{\gamma}_P(\mathcal{B})\ud \cup_{B\in \mathcal{B}} B.$$

1274: In the following, we will be interested in viewing partitions as over

1275: approximations, that is partitions as abstract domains of

1276: $\wp(\Sigma)_\subseteq$.

1277: 

1278: 

1279: \begin{figure}[t]

1280: \begin{center}

1281: \begin{tabular}{ccc}

1282: \mbox{

1283: \setlength{\unitlength}{.65cm}

1284: \begin{picture}(6,5)

1285: \linethickness{0.1mm}

1286: \multiput(0,0)(1,0){7}

1287: {\line(0,1){5}}

1288: \multiput(0,0)(0,1){6}

1289: {\line(1,0){6}}

1290: %\put(0.5,0.5){\line(1,5){0.5}}

1291: %\put(1,3){\line(4,1){2}}

1292: %\put(2.5,2){\line(2,-1){3}}

1293: %\put(5.5,0.5){\line(-1,5){0.5}}

1294: %\linethickness{1.5mm}

1295: \thicklines

1296: {\color{magenta}

1297: \qbezier(1.5,1.5)(1.2,3)(2,4.5)

1298: \qbezier(2,4.5)(2.5,4.75)(3.2,4.2)

1299: \qbezier(3.2,4.2)(3,2.5)(4.5,2.5)

1300: \qbezier(4.5,2.5)(5,2.5)(5.5,2)

1301: \qbezier(5.5,2)(4,1.5)(1.5,1.5)

1302: \color{blue}

1303: \thicklines

1304: \put(1,1){\line(0,1){4}}

1305: \put(1,5){\line(1,0){3}}

1306: \put(4,5){\line(0,-1){2}}

1307: \put(4,3){\line(1,0){2}}

1308: \put(6,3){\line(0,-1){2}}

1309: \put(1,1){\line(1,0){5}}

1310: }

1311: \end{picture}

1312: }

1313: &

1314: \mbox{~~~~~~~~~~~~~}

1315: &

1316: \mbox{

1317: \setlength{\unitlength}{.67cm}

1318: \begin{picture}(6,5)

1319: \linethickness{0.1mm}

1320: \multiput(0,0)(1,0){7}

1321: {\line(0,1){5}}

1322: \multiput(0,0)(0,1){6}

1323: {\line(1,0){6}}

1324: %\put(0.5,0.5){\line(1,5){0.5}}

1325: %\put(1,3){\line(4,1){2}}

1326: %\put(2.5,2){\line(2,-1){3}}

1327: %\put(5.5,0.5){\line(-1,5){0.5}}

1328: %\linethickness{1.5mm}

1329: \thicklines

1330: {\color{magenta}

1331: \qbezier(1.5,1.5)(1.2,3)(2,4.5)

1332: \qbezier(2,4.5)(2.5,4.75)(3.2,4.2)

1333: \qbezier(3.2,4.2)(3,2.5)(4.5,2.5)

1334: \qbezier(4.5,2.5)(5,2.5)(5.5,2)

1335: \qbezier(5.5,2)(4,1.5)(1.5,1.5)

1336: \color{red}

1337: \thicklines

1338: \put(2,2){\line(0,1){2}}

1339: \put(2,4){\line(1,0){1}}

1340: \put(3,4){\line(0,-1){2}}

1341: \put(3,2){\line(-1,0){1}}

1342: }

1343: \end{picture}

1344: }

1345: \end{tabular}

1346: \end{center}

1347: \caption{Partitions as abstract domains: over-approximation on

1348: the left and under-approximation on the right.}\label{figuco}

1349: \end{figure}

1350: %

1351: 

1352: 

1353: Thus, partitions can be viewed as representations of abstract domains. On the other hand,

1354: it turns out that abstract domains can be abstracted to partitions. 

1355: An abstract domain $A\in \Abs(\wp(\Sigma)_\subseteq)$ 

1356: induces a state equivalence $\equiv_A$ on $\Sigma$ by

1357: identifying those states that cannot be distinguished by $A$:

1358: $$s \equiv_A s' \text{~~~iff~~~} \alpha(\{s\}) = \alpha(\{s'\}).$$

1359: For any $s\in \Sigma$, $[s]_A \ud \{s'\in \Sigma~|~

1360: \alpha(\{s\}) = \alpha(\{s'\})\}$ is a block of the state partition $\pr(A)$

1361: induced by $A$:

1362: $$\pr(A) \ud \{[s]_A ~|~ s\in \Sigma\}.$$ 

1363: Thus, $\pr:

1364: \Abs(\wp(\Sigma)) \ra \Part(\Sigma)$ is a mapping from abstract domains to

1365: partitions.

1366: 

1367: \begin{example2}\label{simple}

1368: Let $\Sigma =\{1,2,3,4\}$ and let us specify  abstract domains as

1369: uco's on $\wp(\Sigma)$. The uco's

1370: $\mu_1 = \{\varnothing, 12, 3,4,1234\}$, $\mu_2 = \{\varnothing, 12,

1371: 3, 4, 34, 1234\}$, $\mu_3 = \{\varnothing, 12, 3, 4, 34, 123, 124,

1372: 1234\}$, 

1373: $\mu_4 = \{ 12,

1374: 123, 124, 1234\}$ and $\mu_5 = \{\varnothing, 12,

1375: 123, 124, 1234\}$ all  induce the same

1376: partition $P=\pr(\mu_i) = \{12,3,4\}\in \Part(\Sigma)$. For example, 

1377: $\mu_5(\{1\})=\mu_5 (\{2\})=\{1,2\}$, $\mu_5(\{3\})=\{1,2,3\}$ and

1378: $\mu_5 (\{4\})=\{1,2,3,4\}$ so that $\pr(\mu_5)=P$. 

1379: Observe that $\mu_3$ is the

1380: only partitioning abstract domain because $\adp(P)=\mu_3$.  \qed

1381: \end{example2}

1382: 

1383: Abstract domains of $\wp(\Sigma)$ carry

1384: additional information other than the underlying state

1385: partition and this additional information allows us to distinguish

1386: them. It turns out that this can be precisely stated by

1387: abstract interpretation since the above mappings $\pr$ and $\adp$ allows us to show that

1388: the whole lattice of partitions of

1389: $\Sigma$ can be viewed as a (``higher-order'') abstraction of the lattice of abstract

1390: domains of $\wp(\Sigma)$.

1391: 

1392: \begin{theorem}\label{teoGI}

1393: $(\pr, \Abs(\wp(\Sigma))_\sqsupseteq,\Part(\Sigma)_\succeq,

1394: \adp)$ is a Galois insertion.

1395: \end{theorem}

1396: \begin{proof}

1397: Let $A \in \Abs(\wp(\Sigma))$ and $P\in

1398: \Part(\Sigma)$ and let $\mu_A\in \uco(\wp(\Sigma))$ be the closure

1399: associated with the abstract domain $A$. Let us prove that  

1400: $P\preceq \pr(A) \; \Lra\; \adp(P) \sqsubseteq

1401: \mu_A$. \\

1402: $(\Rightarrow)$~For $S\in \wp(\Sigma)$ we have to prove that

1403: $\adp(P)(S) \subseteq \mu_A(S)$. Consider $s\in \adp(P)(S)$. Hence,

1404: there exists some $B\in P$ such that $s\in B$ and $B\cap S\neq

1405: \varnothing$. Let $q\in B\cap S$. Since $P\preceq \pr(A)$, there

1406: exists some block $[r]_A \in \pr(A)$ such that $B\subseteq

1407: [r]_A$. Thus, for any $x,y\in B$,

1408: $\alpha(\{x\})=\alpha(\{r\})=\alpha(\{y\})$, in particular,

1409: $\alpha(\{s\})=\alpha(\{q\})$. Consequently, 

1410: since $q\in S$ and therefore 

1411: $\mu_A(\{q\})\subseteq \mu_A(S)$, we have that $\mu_A(\{s\}) =

1412: \mu_A(\{q\}) \subseteq \mu_A(S)$, so that $s\in \mu_A(S)$. \\

1413: $(\Leftarrow)$~ Consider a block $B\in P$ and some $s\in B$. We show

1414: that $B\subseteq [s]_A$, namely if $s',s''\in B$ then $\alpha(\{s'\}) =

1415: \alpha(\{s''\})$. Since $\adp(P) \sqsubseteq \mu_A$,

1416: if $s',s''\in B$ then $\adp(P)(\{s'\})=B \subseteq \mu_A(\{s'\})$ so that

1417: $s''\in \mu_A(\{s'\})$ and therefore $\mu_A(\{s''\})\subseteq

1418: \mu_A(\{s'\})$. Likewise, $\mu_A(\{s'\})\subseteq

1419: \mu_A(\{s''\})$ so that $\mu_A(\{s'\}) = \mu_A(\{s''\})$ and in turn

1420: $\alpha(\{s'\}) =

1421: \alpha(\{s''\})$.

1422: \\

1423: Finally, observe that $\adp$ is 1-1 so that the above adjunction

1424: is indeed a Galois insertion. 

1425: \end{proof}

1426: 

1427: Let us observe that, as recalled in Section~\ref{aic}, the

1428: adjoint maps $\pr$ and $\adp$ give rise to an order isomorphism

1429: between the lattices $\tuple{\Part(\Sigma),\preceq}$ and

1430: $\tuple{\Absp(\wp(\Sigma)),\sqsubseteq}$.

1431: 

1432: 

1433: \begin{corollary}\label{coropart} Let $A \in \Abs(\wp(\Sigma))$. The

1434: following statements are equivalent:\\

1435: {\rm (1)} $A$ is partitioning.\\

1436: {\rm (2)} $\gamma$ is

1437: additive and $\{\gamma (\alpha (\{s\}))\}_{s\in \Sigma }$ is a partition of $\Sigma$.

1438: In this case, $\pr(A) =

1439: \{\gamma(\alpha(\{s\}))\}_{s\in \Sigma }$. \\

1440: {\rm (3)} $A$ is

1441: forward complete for the complement operator

1442: $\complement$.

1443: \end{corollary}

1444: \begin{proof} 

1445: Let $A\in \Abs(\wp(\Sigma))$ and let $\mu_A =\gamma\circ \alpha \in

1446: \uco(\wp(\Sigma))$ be the corresponding uco.\\

1447: (1) $\Ra$ (2) By Theorem~\ref{teoGI},  $A\in \Absp(\wp (\Sigma ))$ iff

1448: $\adp(\pr(A)) =A$. Thus, if $\adp(\pr(A))=A$ then $\mu_A=\gamma\circ

1449: \alpha$ is obviously additive. Moreover, $s\equiv_A s'$ iff

1450: $\alpha(\{s\}) = \alpha(\{s'\})$ iff $\gamma(\alpha(\{s\})) =

1451: \gamma(\alpha(\{s'\}))$, so that, for any $s\in \Sigma$,

1452: $[s]_A=\gamma(\alpha(\{s\}))$ and therefore $\pr(A) =

1453: \{\gamma(\alpha(\{s\}))\}_{s\in \Sigma }$.\\

1454: (2) $\Ra$ (1) Since

1455: $\{\gamma (\alpha (\{s\}))\}_{s\in \Sigma } = P\in \Part(\Sigma)$ we

1456: have that

1457: for any $s\in \Sigma$,

1458: $[s]_A=\gamma(\alpha(\{s\}))$: in fact, if $s'\in

1459: \gamma(\alpha(\{s\}))$ then $\alpha(\{s'\}) \leq \alpha(\{s\})$, hence

1460: $\gamma(\alpha(\{s'\})) \subseteq \gamma(\alpha(\{s\}))$ and therefore

1461: $\gamma(\alpha(\{s'\})) = \gamma(\alpha(\{s\}))$. Thus, 

1462: $\pr(A)=P$. Moreover, since $\gamma$ is additive, for any $S\subseteq

1463: \Sigma$, $\cup_{s\in S}

1464: \gamma(\alpha(\{s\}))= \gamma(\vee_{s\in S}

1465: \alpha(\{s\}))=\gamma(\alpha(S))\in \mu_A$. Hence, since

1466: $\adp(P)= \{ \cup_{s\in S}

1467: \gamma(\alpha(\{s\}))~|~ S \subseteq \Sigma \}$ we have that 

1468: $\adp(\pr (A))=A$. \\

1469: %

1470: (1) $\Ra$ (3) Assume that $A \in \Absp(\wp(\Sigma))$. It is

1471: enough to prove that for any $s\in \Sigma $, $\complement(\mu_A(\{s\}))\in \mu_A$:

1472:   in fact, by (1) $\Ra$ (2), $\gamma$ is additive and

1473: therefore $\mu_A$ is additive (because it is a composition of additive

1474: maps) and therefore

1475:  if $S\in\mu_A$ then $S=\cup_{s\in S}\mu_A(\{s\})$ so that

1476:   $\complement (S)=\cap_{s\in S}\complement(\mu_A(\{s\}))$.

1477: Let us observe the following fact~$(*)$: for any $s,s'\in \Sigma $, $s\not\in

1478: \mu_A(\{s'\}) \Leftrightarrow \mu_A(\{s\})\cap \mu_A(\{s'\})=\varnothing$;

1479: this is a consequence of the fact that, by (1) $\Ra$ (2),

1480: $\{\mu_A(\{s\})\}_{s\in \Sigma }$ is a partition. 

1481: For any $s\in \Sigma $, we have that

1482: $\complement(\mu_A(\{s\}))\in\mu_A$ because:

1483:   \begin{align*}

1484:     \mu_A(\complement(\mu_A(\{s\})))

1485:     & = \mu_A(\{s'\in \Sigma ~|~s'\not\in\mu_A(\{s\})\}  & \text{[by

1486: additivity of  $\mu_A$]}  \\

1487:     &=\cup \{ \mu_A(\{s'\})~|~s'\not \in \mu_A(\{s\})\}  & 

1488: \text{[by the above fact $(*)$]}\\

1489:     & = \cup \{ \mu_A(\{s'\})~|~\mu_A(\{s'\})\cap \mu_A(\{s\})=\varnothing\}   &\\

1490:     &= \cup \{ \mu_A(\{s'\})~|~\mu_A(\{s'\})\subseteq \complement(

1491: \mu_A(\{s\})) \} & \\

1492:    &\subseteq \complement(\mu_A(\{s\}))

1493:   \end{align*}

1494: (3) $\Ra$ (1) 

1495: Assume that $\mu_A$ is  

1496:   forward complete for $\complement$, i.e.\ $\mu_A$ is closed under

1497: complements.  By (2)~$\Ra$~(1),

1498: it is enough to

1499: prove that $\gamma$ is additive and that

1500:   $\{\mu_A(\{s\})\}_{s\in \Sigma }\in\Part(\Sigma)$. \\

1501: (i) $\gamma$ is additive. Observe that $\gamma$ is additive iff

1502: $\mu_A$ is additive iff $\mu_A$ is closed under arbitrary unions. 

1503: If $\{S_i\}_{i\in I}\subseteq \mu_A$ then

1504:     $\cup_i S_i = \complement(\cap_i \complement(S_i))\in\mu_A$,

1505:     because, $\mu_A$ is closed under complements (and arbitrary intersections). \\

1506: (ii) $\{\mu_A(\{s\})\}_{s\in \Sigma }\in\Part(\Sigma)$.

1507: Clearly, we have that $\cup_{s\in \Sigma }

1508: \mu_A(\{s\})=\Sigma $. Consider now $s,r\in \Sigma $ such that 

1509: $\mu_A(\{s\})\cap\mu_A(\{r\})\neq \varnothing$. Let us show that

1510: $\mu_A(\{s\})=\mu_A(\{r\})$. In order to show this, let us prove that

1511: $s\in\mu_A(\{r\})$. Notice that

1512: $\mu_A(\{s\})\smallsetminus\mu_A(\{r\})=\mu_A(\{s\})\cap\complement(\mu_A(\{r\}))\in\mu_A$,

1513: because $\mu_A$ is closed under complements.  If

1514: $s\not\in\mu_A(\{r\})$ then we would have that $s\in

1515: \mu_A(\{s\})\smallsetminus \mu_A(\{r\})\in \mu_A$, and this would imply 

1516: $\mu_A(\{s\})\subseteq \mu_A(\{s\})\smallsetminus \mu_A(\{r\}) \subseteq

1517: \mu_A(\{s\})$, namely $\mu_A(\{s\}) =  \mu_A(\{s\})\smallsetminus

1518: \mu_A(\{r\})$. Thus, we would obtain the contradiction

1519: $\mu_A(\{s\})\cap

1520: \mu_A(\{r\}) = \varnothing$. 

1521: Hence, we have that $s\in \mu_A(\{r\})$ and therefore

1522: $\mu_A(\{s\})\subseteq \mu_A(\{r\})$. By swapping the roles of $s$ and

1523: $r$, we also

1524: obtain that $\mu_A(\{r\})\subseteq \mu_A(\{s\})$, so that

1525: $\mu_A(\{s\})=\mu_A(\{r\})$. 

1526: \end{proof}

1527: 

1528: 

1529: 

1530: Let us remark that $\bP \ud \adp \circ \pr$ is a lower closure operator on

1531: $\tuple{\Abs(\wp(\Sigma)),\sqsubseteq}$ and that for any $A \in

1532: \Abs(\wp(\Sigma))$, $A$ is partitioning iff $\bP(A)=A$. 

1533: Hence, $\bP$ is exactly the partitioning-shell refinement, namely

1534: $\bP(A)$ is the most abstract refinement of $A$ that is partitioning.

1535: 

1536: \section{Abstract Semantics of Languages}

1537: \subsection{Concrete Semantics}\label{cs}

1538: We consider temporal specification languages $\fL$ whose

1539: state formulae $\varphi$ are inductively defined by: 

1540: $$\fL\ni \varphi ::= p ~|~ f(\varphi_1, ...,\varphi_n) $$

1541: where $p$ ranges over a (typically finite) set of atomic propositions $\AP$, while $f$

1542: ranges over a finite set $\mathit{Op}$ of operators. $\AP$ and $\Op$

1543: are also denoted, respectively, by $\AP_\fL$ and $\Op_\fL$. Each

1544: operator $f\in \mathit{Op}$ has an arity\footnote{It would be

1545: possible to consider generic operators whose arity is any

1546: possibly infinite ordinal, thus allowing, for example, infinite

1547: conjunctions or disjunctions.} 

1548: $\sharp(f) >0$. 

1549: 

1550: Formulae in $\fL$ are interpreted on a \emph{semantic structure} $\cS

1551: = (\Sigma, I)$ where $\Sigma$ is 

1552: any (possibly

1553: infinite) set of states and $I$ is an interpretation function $I: \AP

1554: \cup \mathit{Op} \ra \Fun(\wp(\Sigma))$ that

1555: maps $p\in \AP$ to $I(p)\in \wp(\Sigma)$ and $f\in \mathit{Op}$ to 

1556: $I(f): \wp(\Sigma)^{\sharp(f)} \ra \wp(\Sigma)$. 

1557: $I(p)$ and $I(f)$ are also denoted by, respectively,

1558: $\boldsymbol{p}$ and $\boldsymbol{f}$. Moreover, $\boldsymbol{AP}\ud

1559: \{\boldsymbol{p} \in \wp(\Sigma)~|~ p \in \AP\}$ and $\boldsymbol{Op}

1560: \ud \{ \boldsymbol{f}:\wp(\Sigma)^{\sharp(f)}\ra \wp(\Sigma)~|~ f\in \Op\}$.

1561: Note that the interpretation $I$ induces

1562: a state labeling $\ell_I: \Sigma \ra \wp(\mathit{AP})$ by

1563: $\ell_I(s)\ud \{ p\in \AP~|~ s \in I(p)\}$.  

1564: The 

1565: \emph{concrete state semantic function} $\grasse{\cdot}_\cS: \fL\ra

1566: \wp(\Sigma)$ evaluates a formula $\varphi\in \fL$ to the set of states making

1567: $\varphi$ true w.r.t.\ the semantic structure $\cS$:

1568: %

1569: $$\grasse{p}_\cS = \boldsymbol{p} \mbox{{\rm ~~~and~~~ }}

1570: \grasse{f(\varphi_1,...,\varphi_n)}_\cS =

1571: \boldsymbol{f}(\grasse{\varphi_1}_\cS,...,\grasse{\varphi_n}_\cS).$$

1572: %

1573: Semantic structures generalize the role of Kripke

1574: structures. In fact, in standard model checking a semantic structure

1575: is usually defined through a Kripke structure $\cK$ so that the

1576: interpretation of logical/temporal operators is defined in terms of

1577: standard logical operators and paths in $\cK$. 

1578: In the following, we freely use standard logical and temporal

1579: operators together with their corresponding usual interpretations: for

1580: example, $I(\wedge)= \cap$, $I(\vee)= \cup$, $I(\neg)=

1581: \complement$, $I(\mathrm{EX})= \pre_R$, $I(\mathrm{AX})=\pret_R$,

1582: etc. As an example, consider the

1583: standard semantics of $\CTL$: 

1584: %

1585: $$

1586: \CTL \ni \varphi ::=  p ~|~ \varphi_1 \wedge \varphi_2 ~|~ \neg \varphi ~|~ \mathrm{AX}\varphi ~|~ \mathrm{EX}\varphi

1587: ~|~ \mathrm{AU}(\varphi_1,\varphi_2) ~|~

1588: \mathrm{EU}(\varphi_1,\varphi_2) ~|~ \mathrm{AR}(\varphi_1,\varphi_2) ~|~

1589: \mathrm{ER}(\varphi_1,\varphi_2) 

1590: $$

1591: with respect to a Kripke structure $\cK= (\Sigma

1592: ,R,\ell)$. Hence, $\cK$ determines a corresponding

1593: interpretation $I$ for atoms in $\AP$ and

1594: operators of $\Op_{\CTL}$, namely $I(\mathrm{AX})=\pret_R$,

1595: $I(\mathrm{EX})=\pre_R$, etc., and this defines the concrete semantic

1596: function  $\grasse{\cdot}_\cK: \CTL \ra

1597: \wp(\Sigma)$. 

1598: 

1599: %

1600: If $g$ is any operator with arity $\sharp(g)=n>0$ whose

1601: interpretation is given by $\boldsymbol{g}:\wp(\Sigma)^{n} \ra \wp

1602: (\Sigma )$ and $\cS=(\Sigma,I)$ is a semantic structure then we say

1603: that a language $\fL$ is \emph{closed under} $g$ for $\cS$ when for any

1604: $\varphi_1, ...,\varphi_{n} \in \fL$ there exists some $\psi\in\fL$

1605: such that $\boldsymbol{g}(\grasse{\varphi_1}_\cS,...,\grasse{\varphi_{n}}_\cS)

1606: = \grasse{\psi}_\cS$. For instance, if $\Op_\fL$ includes 

1607: $\mathrm{EX}$ and negation with their standard

1608: interpretations, i.e.\

1609: $I(\mathrm{EX})=\pre_R$ and

1610: $I(\neg)=

1611: \complement$, then

1612: $\fL$ is closed under $\mathrm{AX}$ with its standard interpretation $\pret_R$ 

1613: because $\pret_R = \complement \circ \pre_R \circ \complement$. 

1614: This notion can be extended in a straightforward

1615: way to infinitary operators: for instance, $\fL$ is closed under

1616: infinite logical conjunction for $\cS$ iff for any $\Phi\subseteq \fL$, there

1617: exists some $\psi\in\fL$ such that $\bigcap_{\varphi\in

1618: \Phi}\grasse{\varphi}_\cS = \grasse{\psi}_\cS$. In particular, let us

1619: remark that if $\fL$ is

1620: closed under infinite logical conjunction then it must exist some

1621: $\psi\in \fL$ such that $\cap \varnothing

1622: = \Sigma  = \grasse{\psi}_\cS$, namely $\fL$ is able to express the tautology

1623: $\mathit{true}$. Let us remark that 

1624: if the state space $\Sigma$ is finite and 

1625: $\fL$ is closed under logical conjunction then we always

1626: mean that there exists some $\psi\in \fL$ such that $\cap \varnothing

1627: = \Sigma  = \grasse{\psi}_\cS$. Finally, note that $\fL$ is

1628: closed  under negation and infinite logical conjunction if and only if

1629: $\fL$ includes propositional logic.  

1630: 

1631: \subsection{Abstract Semantics}\label{as}

1632: In the following, we apply the standard abstract interpretation approach for

1633: defining abstract semantics \cite{CC77,CC79}. Let $\fL$ be a language

1634: and $\cS=(\Sigma,I)$ be a semantic structure for $\fL$.  An

1635: \emph{abstract semantic structure} $\cS^\sharp = (A,I^\sharp)$ is

1636: given by an abstract domain $A\in 

1637: \Abs(\wp(\Sigma)_\subseteq)$ and by an abstract interpretation function

1638: $I^\sharp: \AP \cup \Op \ra \Fun(A)$. An abstract

1639: semantic structure $\cS^\sharp$ therefore induces an \emph{abstract

1640: semantic function} $\grasse{\cdot}_{\cS^\sharp}: \fL\ra A$

1641: that evaluates formulae in $\fL$ to

1642: abstract values in $A$.

1643: The abstract interpretation $I^\sharp$  is a

1644: correct over-approximation (respectively, under-approximation) of $I$ on $A$ when 

1645: for any $p\in \AP$, $\gamma(I^\sharp(p)) \supseteq 

1646: I (p)$ (respectively, $\gamma(I^\sharp(p)) \subseteq 

1647: I (p)$) 

1648: and for any $f\in \Op$,  $\gamma \circ I^\sharp (f) \sqsupseteq 

1649: I(f) \circ \gamma$ (respectively, $\gamma \circ I^\sharp (f) \sqsubseteq 

1650: I(f) \circ \gamma$).

1651: If $I^\sharp$  is a

1652: correct over-approximation (respectively, under-approximation) 

1653: of $I$ and the semantic operations in

1654: $\boldsymbol{Op}$ are monotone then the

1655: abstract

1656: semantics is an over-approximation (respectively, under-approximation)

1657: of the concrete semantics, namely

1658: for any $\varphi\in \fL$, 

1659:  $\gamma(\grasse{\varphi}_{\cS^\sharp}) \supseteq

1660: \grasse{\varphi}_\cS$

1661: (respectively, $\gamma(\grasse{\varphi}_{\cS^\sharp}) \subseteq

1662: \grasse{\varphi}_\cS$).  

1663: 

1664: In particular, the abstract domain $A$ always induces an abstract

1665: semantic structure $\cS^A=(A,I^A)$ where $I^A$ is the best correct

1666: approximation of $I$ on $A$, i.e.\ $I^A$ interprets atoms $p$ and

1667: operators $f$ as best correct approximations on $A$ of,

1668: respectively, 

1669: $\boldsymbol{p}$ and $\boldsymbol{f}$: for any $p\in \AP$ and $f\in \Op$, 

1670: $$I^A (p)\ud \alpha(\boldsymbol{p}) ~~~\text{ and }~~~ I^A (f) \ud

1671: \boldsymbol{f}^A.$$

1672: Thus, the abstract domain $A$ systematically induces an abstract

1673: semantic function $\grasse{\cdot}_{\cS^A}: \fL\ra A$,   

1674: also denoted by $\grasse{\cdot}_\cS^A$, which is therefore defined by:

1675: $$\grasse{p}_\cS^A = \alpha(\boldsymbol{p})

1676: ~~~\text{ and }~~~

1677: \grasse{f(\varphi_1,...,\varphi_n)}_\cS^A =

1678: \boldsymbol{f}^A(\grasse{\varphi_1}^A_\cS,...,\grasse{\varphi_n}^A_\cS).$$

1679: 

1680: \noindent

1681: As usual in abstract interpretation, observe that the concrete semantics

1682: is a particular abstract semantics, namely it is the abstract

1683: semantics induced by the ``identical abstraction'' $(\id,\wp(\Sigma),\wp(\Sigma),\id)$.

1684: 

1685: %Let us also stress the following key point

1686: %of the abstract interpretation approach. In order to define an

1687: %abstract semantics we  need precisely an abstract domain $A\in

1688: %\Abs(\wp(\Sigma))$. In fact, since $\gdca$ is a GI, for any

1689: %$S\in \wp(\Sigma)$, $\alpha(S)$ is exactly the most precise approximation

1690: %in $A$ of the set $S$ and this basic property allows us to approximate

1691: %concrete semantic functions by their best

1692: %correct approximations on $A$.  

1693: 

1694: 

1695: \begin{figure}[t]

1696: \begin{center}

1697: \begin{tabular}{ccc}

1698:  \mbox{\xymatrix{

1699:       *++[o][F]{1} \ar[d] \ar[r]^(0.3){p} ^(1.3){p} &

1700:       *++[o][F]{2} \ar@(ul,ur)[] \ar[ld] &  \\ 

1701:       *++[o][F]{3}\ar[r] ^(0.35){p,q} & *++[o][F]{4}\ar@/^/[r] ^(0.24){r}

1702: & *++[o][F]{5} \ar@/^/[l] ^(0.24){q} 

1703:     }

1704:   }

1705: &

1706: \mbox{~~~~~~~~~~~~~}

1707: &

1708: \mbox{\small

1709:     \xymatrix@C=4pt@R=7pt{

1710:       &   & \top & &  \\

1711:         &   a_4\ar@{-}[ru]   &  & a_5\ar@{-}[lu] &\\

1712:      a_1 \ar@{-}[ru] & &   a_2\ar@{-}[ru]\ar@{-}[lu]      & & a_3\ar@{-}[lu] \\

1713:          && \bot\ar@{-}[llu]\ar@{-}[u]\ar@{-}[rru] &&  

1714:     }

1715:   }

1716: \end{tabular}

1717: \end{center}

1718: \caption{A Kripke structre on the left and an abstract domain on the right.}\label{figuco2}

1719: \end{figure}

1720: %

1721: 

1722: 

1723: \begin{example2}

1724:   \label{ex1}

1725: Let $\fL \ni

1726: \varphi::=p~|~q~|~r~|~\varphi_1\wedge\varphi_2~|~\EX\varphi$.

1727: Let us consider the Kripke structure

1728: $\cK=(\Sigma,\shortrightarrow,\ell)$ 

1729: and the lattice $A$ both

1730: depicted in Figure~\ref{figuco2}.

1731: Let $\cS$ be the

1732: semantic structure induced by the Kripke structure $\cK$ so

1733: that $\boldsymbol{\EX}=\pre_{\shortrightarrow}$. Let us consider the

1734: formulae $\EX r$ and $\EX (p \wedge q)$, whose concrete semantics are

1735: as follows: $\grasse{\EX r}_\cS = \{3,5\}$ and $\grasse{\EX (p \wedge

1736: q)}_\cS= \{1,2\}$. 

1737: $A$ is an abstract domain of $\wp(\Sigma)$ where the 

1738: Galois insertion $\gdcas$ is determined by the following

1739: concretization map: 

1740: \begin{align*}

1741: &\gamma(\bot)=\varnothing;~~\gamma(a_1)=\{1,2\};~~\gamma(a_2)=\{3\};

1742: ~~\gamma(a_3)=\{3,4\};\\ 

1743: &\gamma(a_4)=\{1,2,3\};~~ \gamma(a_5

1744: )=\{3,4,5\};~~ \gamma(\top)=\{1,2,3,4,5\}.

1745: \end{align*}

1746: Note that, by Corollary~\ref{coropart}, 

1747: $A$ is not partitioning because $\gamma$ is not additive: $\gamma(a_2)

1748: \cup \gamma(a_3) =\{3,4\} \subsetneq \{3,4,5\} = \gamma(a_2

1749: \vee a_3)$. It turns out that:

1750: $$ 

1751: \begin{array}{ll}

1752: \grasse{\EX r}_\cS^A

1753:     &= \alpha (\pre_{\shortrightarrow} ( \gamma(\grasse{r}_\cS^A)) 

1754:     = \alpha (\pre_{\shortrightarrow} ( \gamma (\alpha(\boldsymbol{r})))) 

1755:     = \alpha (\pre_{\shortrightarrow} ( \gamma( a_3) )) \\ 

1756:     & = \alpha (\pre_{\shortrightarrow} (\{3,4\}))  

1757:     = \alpha (\{1, 2, 3, 5\} )  = \top; \\[7.5pt]

1758: \grasse{\EX (p \wedge q)}_\cS^A

1759:     & = \alpha (\pre_{\shortrightarrow} ( \gamma( \grasse{p}_\cS^A \wedge

1760: \grasse{q}_\cS^A))) 

1761:     = \alpha (\pre_{\shortrightarrow} ( \gamma (\alpha(\boldsymbol{p}) \wedge

1762: \alpha(\boldsymbol{q}))))\\ 

1763:     & = \alpha (\pre_{\shortrightarrow} ( \gamma( a_4 \wedge a_5 ))) 

1764: = \alpha (\pre_{\shortrightarrow} ( \gamma( a_2 ))) 

1765: = \alpha (\pre_{\shortrightarrow} (3)) 

1766: = \alpha (\{1,2\}) = a_1 . 

1767: \end{array}

1768: $$

1769: Observe that 

1770: the abstract semantics $\grasse{\EX r}_\cS^A$ is 

1771:   a proper over-approximation of

1772: $\grasse{\EX r}_\cS$ because $\grasse{\EX r}_\cS \subsetneq 

1773: \gamma(\grasse{\EX r}_\cS^A)$. On the other hand,

1774: the concrete semantics  

1775: $\grasse{\EX (p \wedge q)}_\cS$ is precisely represented in $A$

1776: because $\gamma( \grasse{\EX (p

1777: \wedge q)}_\cS^A ) = \grasse{\EX (p \wedge q)}_\cS$.

1778: \qed

1779: \end{example2}

1780: 

1781: 

1782: 

1783: \section{Generalized Strong Preservation} 

1784: 

1785: We showed in Section~\ref{paa} how a state partition

1786: $P$ can be viewed as a partitioning abstract domain  $\adp(P)$

1787: specified by the GI $(\alpha_P,

1788: \wp(\Sigma)_\subseteq,\wp(P)_\subseteq,\gamma_P)$.  

1789: Thus, given a language $\fL$ and a corresponding

1790: semantic structure $\cS=(\Sigma,I)$, it turns out that 

1791: any partition  $P\in \Part(\Sigma)$ systematically induces

1792: a corresponding abstract semantics $\ok{\grasse{\cdot}_\cS^P}\ud 

1793: \ok{\grasse{\cdot}_\cS^{\adp(P)}}

1794: :\fL \ra \adp(P)$ that evaluates a formula in $\fL$ to a (possibly

1795: empty) union of blocks of $P$.  

1796: Strong preservation for a partition $P$ can be characterized in terms of the corresponding

1797: abstract domain $\adp(P)$ as follows. 

1798: 

1799: \begin{lemma}\label{char}

1800: $P\in \Part(\Sigma)$ is s.p.\ for $\fL$ iff $\forall \varphi \in

1801: \fL$ and $S\subseteq \Sigma $, $\alpha_P(S)

1802: \subseteq \grasse{\varphi}_\cS^P \: \Lra \: S\subseteq\grasse{\varphi}_\cS$.  

1803: \end{lemma}

1804: \begin{proof}

1805: $(\Rightarrow)$: 

1806:   Let us first observe that for any $\varphi\in \fL$, 

1807: $\gamma_P(\alpha_P(\grasse{\varphi}_\cS)) = \grasse{\varphi}_\cS$: in fact, 

1808: for any $s\in \grasse{\varphi}_\cS$, $\alpha_P(\{s\})$ is the block of 

1809: $P$ containing $s$; since $P\preceq P_\fL$, we have that $\alpha_P(\{s\})\subseteq

1810: \grasse{\varphi}_\cS$, and from this $\alpha_P(\grasse{\varphi}_\cS) \subseteq

1811: \grasse{\varphi}_\cS$ and in turn $\gamma_P(\alpha_P(\grasse{\varphi}_\cS)) =

1812: \grasse{\varphi}_\cS$.\\ 

1813: Let us now prove by 

1814: structural induction on $\varphi\in \fL$ that

1815: $\grasse{\varphi}_\cS=\gamma_P(\grasse{\varphi}^P_\cS)$:

1816: 

1817: \begin{itemize}

1818: \item[--] $\varphi\equiv p\in \AP_\fL$: by using the above observation, 

1819:   $\grasse{p}_\cS=\gamma_P(\alpha_P(\grasse{p}_\cS))=\gamma_P(\grasse{p}_\cS^P)$. 

1820: 

1821: \item[--] $\varphi\equiv f(\varphi_1,\ldots,\varphi_n)$: 

1822:   \begin{align*}

1823:     \grasse{f(\varphi_1,\ldots,\varphi_n)}_\cS = & \text{~~~[by

1824: the above observation]}\\

1825:     \gamma_P(\alpha_P(\grasse{f(\varphi_1,\ldots,\varphi_n)}_\cS)) = &

1826: \text{~~~[by definition]}  \\ 

1827:     \gamma_P(\alpha_P(\boldsymbol{f}

1828: (\grasse{\varphi_1}_\cS,\ldots,\grasse{\varphi_n}_\cS))) = &

1829: \text{~~~[by inductive hypothesis]} \\

1830:     \gamma_P(\alpha_P(\boldsymbol{f}

1831: (\gamma_P(\grasse{\varphi_1}_\cS^P),\ldots,\gamma_P(\grasse{\varphi_n}_\cS^P))))

1832: = &  \text{~~~[by definition]} \\

1833: \gamma_P( \grasse{f(\varphi_1,\ldots,\varphi_n)}_\cS^P). \phantom{=}&

1834:   \end{align*}

1835: \end{itemize}

1836: Now, consider any $\varphi\in

1837: \fL$. If $S\subseteq \grasse{\varphi}_\cS$ then 

1838:   $\alpha_P(S) \subseteq \alpha_P(\grasse{\varphi}_\cS) =

1839: \alpha_P(\gamma_P (\grasse{\varphi}_\cS^P)) = \grasse{\varphi}_\cS^P$.

1840:   Conversely, if

1841: $\alpha_P(S)\subseteq\grasse{\varphi}_\cS^P$ 

1842: then 

1843:   $S\subseteq \gamma_P(\grasse{\varphi}_\cS^P)= \grasse{\varphi}_\cS$. \\

1844: %    

1845: $(\Leftarrow)$:

1846:    Consider a block $B\in P$ and $s,s'\in B$ so that

1847: $\alpha_P(\{s\})=B=\alpha_P(\{s'\})$. By hypothesis, for any $\varphi\in

1848: \fL$, we have that  

1849:   $s\in\grasse{\varphi}_\cS$ iff $\alpha_P(\{s\})

1850:   \subseteq\grasse{\varphi}_\cS^P$ iff $\alpha_P(\{s'\})

1851:   \subseteq\grasse{\varphi}_\cS^P$ iff 

1852:   $s'\in\grasse{\varphi}_\cS$. Thus,

1853:   $s\equiv_\fL s'$. 

1854: \end{proof}

1855: 

1856: 

1857: This

1858: states that a partition $P\in \Part(\Sigma)$ is s.p.\ for $\fL$ 

1859: if and only if to check whether some set $S$ of states satisfies some

1860: formula $\varphi\in \fL$, i.e.\ $S\subseteq\grasse{\varphi}_\cS$, is equivalent to

1861: check whether the abstract state $\alpha_P(S)$ is more precise than the abstract semantics

1862: $\grasse{\varphi}_\cS^P$, that is $S$ is over-approximated by $\grasse{\varphi}_\cS^P$.

1863: The key observation here is that in our

1864: abstract interpretation-based framework partitions are particular

1865: abstract domains. This allows us to generalize

1866: the notion of strong preservation from partitions to generic abstract

1867: semantic functions as follows.

1868: 

1869: 

1870: \begin{definition2}\label{spd}

1871:   Let $\fL$ be a language, $\cS=(\Sigma,I)$ be a semantic structure for

1872: $\fL$ and $\cS^\sharp =(A,I^\sharp)$ be a corresponding abstract

1873: semantic structure. The abstract semantics

1874:   $\ok{\grasse{\cdot}_{\cS^\sharp}}$ is \emph{strongly preserving} for $\fL$ (w.r.t.\

1875: $\cS$) if for any $\varphi\in \fL$ and $S\subseteq \Sigma $,

1876:   $$\alpha(S)\leq_A \ok{\grasse{\varphi}_{\cS^\sharp}} \;\; \Lra \;\; S\subseteq

1877:   \grasse{\varphi}_\cS. \qed$$

1878: \end{definition2} 

1879: 

1880: 

1881: Definition~\ref{spd} generalizes standard strong preservation from partitions, as

1882: characte\-rized by Lem\-ma~\ref{char}, both to an arbitrary abstract

1883: domain $A\in \Abs(\wp(\Sigma))$ and to a corresponding abstract

1884: interpretation function $I^\sharp$. 

1885: Likewise, standard weak preservation can be generalized as follows. Let

1886: $\cK=(\Sigma,R,\ell)$ be a concrete Kripke structure that induces the

1887: concrete semantics

1888: $\ok{\grasse{\varphi}_\cK} = \{ s\in

1889: \Sigma~|~ s \ok{\models^\cK } \varphi\}$.

1890: Let $h:\Sigma

1891: \ra A$ be a surjective abstraction and let

1892: $(\alpha_h,\wp(\Sigma),\wp(A),\gamma_h)$ be the corresponding

1893: partitioning abstract domain. Let $\cA = (A,\ok{R^\sharp},

1894: \ok{\ell^\sharp})$ be an abstract Kripke structure on

1895: $A$ that gives rise to  the abstract semantics $\ok{\grasse{\varphi}_\cA} = \{ a\in

1896: A~|~ a \ok{\models^\cA } \varphi\}$. Then, $\cA$ weakly preserves  $\fL$

1897: when 

1898: $$\forall \phi\in \fL.\forall S\subseteq \Sigma.\; \alpha_h(S)

1899: \subseteq \ok{\grasse{\varphi}_\cA} \;\; \Ra \;\; S\subseteq

1900: \ok{\grasse{\varphi}_\cK}.$$ 

1901: Hence, weak preservation can be generalized to generic abstract domains and

1902: abstract semantics accordingly to Definition~\ref{spd}. 

1903: 

1904: \subsection{Strong Preservation is an Abstract Domain Property}

1905: Definition~\ref{spd} is a direct and natural generalization of the standard

1906: notion of strong preservation in abstract model checking. It can be

1907: equivalently stated as follows.   

1908: \begin{lemma}\label{charsp}

1909: $\grasse{\cdot}_{\cS^\sharp}$ is s.p.\ for $\fL$ iff for any $\varphi

1910: \in \fL$, $\grasse{\varphi}_\cS =

1911: \gamma(\grasse{\varphi}_{\cS^\sharp})$. 

1912: \end{lemma}

1913: \begin{proof}

1914: $(\Rightarrow)$ On the one hand,  $\gamma(\grasse{\varphi}_{\cS^\sharp})

1915: \subseteq \grasse{\varphi}_\cS$ iff 

1916: $\alpha(\gamma(\grasse{\varphi}_{\cS^\sharp}))

1917: \leq \grasse{\varphi}_{\cS^\sharp}$ iff 

1918: $\grasse{\varphi}_{\cS^\sharp} \leq \grasse{\varphi}_{\cS^\sharp}$,

1919: which is trivially true. On the other hand,  

1920: $\grasse{\varphi}_\cS \subseteq \gamma(\grasse{\varphi}_{\cS^\sharp})$

1921: iff $\alpha(\grasse{\varphi}_\cS) \leq \grasse{\varphi}_{\cS^\sharp}$

1922: iff $\grasse{\varphi}_\cS \subseteq \grasse{\varphi}_\cS$, that

1923: is trivially true. \\

1924: $(\Leftarrow)$ We have that $S\subseteq \grasse{\varphi}_\cS$ iff $S\subseteq

1925: \gamma(\grasse{\varphi}_{\cS^\sharp})$ iff $\alpha(S) \leq

1926: \grasse{\varphi}_{\cS^\sharp}$. 

1927: \end{proof}

1928: 

1929: \noindent

1930: In particular, it is worth noting that if   $\ok{\grasse{\cdot}_{\cS^\sharp}}$ is s.p.\ for

1931: $\fL$ then $\ok{\grasse{\cdot}_{\cS^\sharp}} = \alpha \circ

1932: \grasse{\cdot}_\cS$ holds. 

1933: 

1934: \begin{lemma}\label{spadp} Let $A\in \Abs(\wp(\Sigma))$.\\

1935: {\rm (1)} Let $\cS^\sharp_1 =(A,I^\sharp_1)$ and $\cS^\sharp_2

1936: =(A,I^\sharp_2)$ be abstract semantic structures on $A$.  If

1937: $\ok{\grasse{\cdot}_{\cS_1^\sharp}}$ and

1938: $\ok{\grasse{\cdot}_{\cS_2^\sharp}}$ are both s.p.\ for $\fL$ then

1939: $\ok{\grasse{\cdot}_{\cS_1^\sharp}}=

1940: \ok{\grasse{\cdot}_{\cS_2^\sharp}}$. \\

1941: {\rm (2)} Let $\cS^\sharp =(A,I^\sharp)$ 

1942: be an abstract semantic structure on $A$. 

1943: If $\ok{\grasse{\cdot}_{\cS^\sharp}}$

1944: is s.p.\ for $\fL$ then

1945: $\ok{\grasse{\cdot}_\cS^A}$ 

1946: is s.p.\ for $\fL$. 

1947: \end{lemma}

1948: \begin{proof}

1949: (1) By Lemma~\ref{charsp}, for any $\varphi\in \fL$, 

1950: $ \gamma(\ok{\grasse{\varphi}_{\cS_1^\sharp}}) = \grasse{\varphi}_\cS 

1951: = \gamma(\ok{\grasse{\varphi}_{\cS_2^\sharp}})$, so that, by applying

1952: $\alpha$, 

1953: $\ok{\grasse{\varphi}_{\cS_1^\sharp}} = \alpha(

1954: \gamma(\ok{\grasse{\varphi}_{\cS_1^\sharp}}))  = \alpha(\grasse{\varphi}_\cS) 

1955: = \alpha(\gamma(\ok{\grasse{\varphi}_{\cS_2^\sharp}})) 

1956: =\ok{\grasse{\varphi}_{\cS_2^\sharp}}$.

1957: \\

1958: %

1959: (2) Let us first observe that 

1960: for any $\varphi\in\fL$, $\gamma(\alpha(\grasse{\varphi}_\cS)) =

1961: \grasse{\varphi}_\cS$. In fact, 

1962: $\gamma(\alpha(\grasse{\varphi}_\cS)) \subseteq

1963: \grasse{\varphi}_\cS \Lra \alpha(\gamma(\alpha(\grasse{\varphi}_\cS)))

1964: \leq \ok{\grasse{\varphi}_{\cS^\sharp}} \Lra 

1965: \alpha(\grasse{\varphi}_\cS)

1966: \leq \ok{\grasse{\varphi}_{\cS^\sharp}} \Lra \grasse{\varphi}_\cS \subseteq

1967: \grasse{\varphi}_\cS$.  

1968: As a consequence of this

1969: fact, by structural

1970: induction  on $\varphi\in \fL$, analogously to the proof

1971: of Lemma~\ref{char}, it is easy to prove that 

1972: $\gamma(\grasse{\varphi}_\cS^A)=\grasse{\varphi}_\cS$. Thus, by

1973: Lemma~\ref{charsp}, $\grasse{\cdot}_\cS^A$ is s.p.\ for $\fL$.

1974: \end{proof}

1975: 

1976: Thus, it turns out that strong preservation is an

1977: \emph{abstract domain property}. This means that given any abstract domain $A\in

1978: \Abs(\wp(\Sigma))$, it is possible to define an abstract semantic

1979: structure $\cS^\sharp=(A,I^\sharp)$ on $A$ such that the corresponding

1980: abstract

1981: semantics $\ok{\grasse{\cdot}_{\cS^\sharp}}$ is s.p.\ for $\fL$ if and

1982: only if the induced abstract semantics $\ok{\grasse{\cdot}^A_\cS}:\fL

1983: \ra A$ is s.p.\ for $\fL$.  In

1984: particular, this also holds for the standard approach: if $\cA =

1985: (A,\ok{R^\sharp}, 

1986: \ok{\ell^\sharp})$ is an abstract Kripke structure for $\fL$, 

1987: where $h:\Sigma \ra A$ is the corresponding surjection, then the

1988: standard abstract semantics $\grasse{\cdot}_\cA$ 

1989: strongly preserves $\fL$ if and only if the abstract semantics induced

1990: by the partitioning abstract domain $(\alpha_h, \wp(\Sigma),

1991: \wp(A),\gamma_h)$ strongly preserves $\fL$, and in this case this

1992: abstract semantics coincides with 

1993: the standard abstract semantics $\ok{\grasse{\cdot}_\cA}$.  

1994: Strong preservation is an abstract domain property and therefore can be 

1995: defined without loss of generality as follows. 

1996: \begin{definition2}

1997: An abstract domain  $A\in

1998: \Abs(\wp(\Sigma))$ is \emph{strongly preserving for} $\fL$ (w.r.t.\ a

1999: semantic structure $\cS$) when

2000: $\grasse{\cdot}_\cS^A$ is s.p.\ for $\fL$ (w.r.t.\ $\cS$). 

2001: We denote by $\SP_\fL\subseteq \Abs(\wp(\Sigma))$ the set of abstract

2002: domains that are s.p.\ for $\fL$. 

2003: \qed

2004: \end{definition2}

2005: 

2006: \begin{example2}

2007: Let us consider Example~\ref{ex1}. It turns out that the abstract

2008: domain $A$ is not s.p.\ for $\fL$ because, by Lemma~\ref{charsp}, $\grasse{\EX

2009: r}_\cS = \{3,5\} \subsetneq \{1,2,3,4,5\} =\gamma(\top)=

2010: \gamma(\grasse{\EX r}_\cS^A)$. \qed 

2011: \end{example2}

2012: 

2013: \begin{figure}[t] 

2014: \begin{center}

2015: \begin{tabular}{ccc}

2016:     \mbox{

2017:       \xymatrix@C=25pt@R=15pt{

2018:        *++[o][F]{1}\ar[r]^(0.3){p} & *++[o][F]{2}\ar[r]^(0.3){p} &

2019: *++[o][F]{3} \ar@(ur,dr)[]^(0.15){p} 

2020:        }

2021:      }

2022: &

2023: \mbox{~~~~~~~~~~~~~~~}

2024: &

2025:     \mbox{

2026:       \xymatrix@C=10pt@R=10pt{

2027:        *++[o][F]{[12]}\ar[rr]^(0.3){p} & & *++[o][F]{\;[3]\;} \ar@(ur,dr)[]^(0.18){p}  

2028:        }

2029:      }

2030: \end{tabular}

2031: \end{center}

2032: \caption{A Kripke structure $\cK$ on the left and an abstract Kripke

2033: structure $\cA$ on the right.}\label{figk} 

2034: \end{figure}

2035: 

2036: 

2037: \begin{example2}\label{esnu}

2038: Let us consider the simple language

2039:   $\cL\ni \varphi ::= p ~|~ \EX \varphi$ and the Kripke 

2040: structure $\cK$ depicted in Figure~\ref{figk}.

2041:  The Kripke structure $\cK$

2042: induces the semantic structure $\cS=(\{1,2,3\},I)$ such that

2043: $I(p)=\{1,2,3\}$ and $I(\EX)=\pre_\sra$. Hence, we

2044: have that $\grasse{p}_\cS=\{1,2,3\}$, $\grasse{\EX p}_\cS

2045: =\{1,2,3\}$ and, for $k>1$, $\grasse{\EX^k p}_\cS

2046: =\{1,2,3\}$. Let us  consider the

2047: partitioning abstract domain 

2048: $A$ induced by the partition $P=\{[12],[3]\}$ and related to

2049: $\wp(\Sigma)$ by $\alpha$ and $\gamma$.

2050: Let us  consider two different abstract semantic structures on $A$.

2051: \begin{itemize}

2052: \item[--] The abstract semantic structure $\cS^A=(A,I^A)$ is induced

2053: as best correct approximation of $I$ by $A$.

2054: \item[--] The abstract semantic structure $\cS^\cA=(A,I^\cA)$ is instead

2055: induced by the abstract Kripke structure

2056: $\cA=(A,\sra^\sharp,\ell^\sharp)$ in Figure~\ref{figk}. Hence, 

2057: $I^\cA(p) = \{[12],[3]\}$ and $I^\cA(\EX)=\pre_{\sra^\sharp}$. 

2058: \end{itemize}

2059: $\cS^A$ is different from $\cS^\cA$ because  $I^A(\EX)\neq I^\cA(\EX)$. In fact, 

2060: $I^A(\EX)(\{[12]\}) = 

2061: \alpha (\pre_\sra (\gamma(\{[12]\}))) =

2062: \alpha (\pre_\sra (\{1,2\})) 

2063: = \ok{\alpha (\{1\})} = \ok{\{[12]\}}$, while

2064: $I^\cA(\EX)(\{[12]\}) = 

2065: \pre_{\sra^\sharp}(\{[12]\}) = \varnothing$. \\

2066: Let us show  that both the abstract semantics 

2067: $\grasse{\cdot}_{\cS}^A$ and $\grasse{\cdot}_{\cS^\sharp}$ are s.p.\

2068: for $\fL$. 

2069: \begin{itemize}

2070: \item[--]

2071: We have that  

2072: $\grasse{p}_\cS^A=\{[12],[3]\}$, $\grasse{\EX p}_\cS^A =\alpha

2073: (\pre_\sra (\{1,2,3\})) = \alpha(\{1,2,3\})=

2074: \{[12],[3]\}$ and, for

2075: $k>1$, $\grasse{\EX^k p}_\cS^A =\{[12],[3]\}$. Thus,

2076: for any $\varphi \in \cL$, $\grasse{\varphi}_\cS = \gamma

2077: (\grasse{\varphi}_\cS^A)$. 

2078: \item[--] We have that  

2079: $\grasse{p}_{\cS^\cA}=\{[12],[3]\}$, $\grasse{\EX p}_{\cS^\cA}

2080: =\pre_{\sra^\sharp} (\{[12],[3]\})=\{[12],[3]\}$ and, for

2081: $k>1$, $\grasse{\EX^k p}_{\cS^\cA} =\{[12],[3]\}$. Thus,

2082: for any $\varphi \in \cL$, $\grasse{\varphi}_\cS = \gamma

2083: (\grasse{\varphi}_{\cS^\cA})$. 

2084: \end{itemize}

2085: Consequently, by Lemma~\ref{charsp}, 

2086: both abstract semantics are s.p.\ for $\fL$. 

2087: \qed 

2088: \end{example2}

2089: 

2090: 

2091: \subsection{The Most Abstract Strongly Preserving Domain}

2092: As recalled in Section~\ref{amc}, a language $\fL$ and a

2093: semantic structure $\cS$ for $\fL$ induce a corresponding logical partition

2094: $P_\fL\in \Part(\Sigma)$.  By Lemma~\ref{char}, it turns out that

2095: $P_\fL$ is the coarsest strongly preserving partitioning abstract

2096: domain for $\fL$. This can be generalized to arbitrary abstract domains

2097: as follows. Let us define  $\AD_\fL$ by:

2098: $$\AD_\fL \ud  \cM(\{\grasse{\varphi}_\cS~|~\varphi\in\fL\}).$$

2099: Hence, $\AD_\fL$ is the closure under arbitrary intersections of the set

2100: of concrete semantics of formulae in $\fL$.

2101: Observe that $\AD_\fL \in \Abs(\wp(\Sigma))$ because it 

2102: is a Moore-family of $\wp(\Sigma)$. 

2103: 

2104: \begin{theorem}\label{spchar}

2105: For any 

2106: $A \in \Abs(\wp(\Sigma))$, $A \in \SP_\fL$ iff $A \sqsubseteq

2107:   \AD_\fL$.

2108: \end{theorem}

2109: \begin{proof}

2110: Let $\mu=\gamma\circ \alpha\in \uco(\wp(\Sigma))$ and let $\mu_\fL\in \uco(\wp(\Sigma))$ be

2111: the uco associated to $\AD_\fL$, that is $\mu_\fL (S) = \cap \{

2112: \grasse{\varphi}_\cS~|~ \varphi \in \fL,\: S \subseteq

2113: \grasse{\varphi}_\cS\}$. Recall that $A\sqsubseteq \AD_\fL$ iff for any

2114: $\varphi\in \fL$, $\grasse{\varphi}_\cS \in \mu$.  \\

2115: ($\Ra$)~ For any $\varphi\in \fL$, we have that 

2116: $\gamma(\alpha(\grasse{\varphi}_\cS))= \grasse{\varphi}_\cS$ because, 

2117: by Lemma~\ref{charsp},

2118: $\gamma(\alpha(\grasse{\varphi}_\cS)) 

2119: = \gamma(\alpha(\gamma(\grasse{\varphi}_{\cS}^A))) =

2120: \gamma(\grasse{\varphi}_{\cS}^A) = \grasse{\varphi}_\cS$.\\

2121: ($\Leftarrow$)~By hypothesis, $\gamma(\alpha(\grasse{\varphi}_\cS))=

2122: \grasse{\varphi}_\cS$ for any $\varphi$. Let us show  

2123: by structural induction on $\varphi\in \fL$ that

2124: $\grasse{\varphi}_\cS=\gamma(\grasse{\varphi}_\cS^A)$.

2125: \begin{itemize}

2126: \item[--] $\varphi\equiv p\in \AP_\fL$: by using the hypothesis, 

2127:   $\grasse{p}_\cS=\gamma_P(\alpha_P(\grasse{p}_\cS))=\gamma_P(\grasse{p}_\cS^A)$. 

2128: 

2129: \item[--] $\varphi\equiv f(\varphi_1,\ldots,\varphi_n)$: 

2130:   \begin{align*}

2131:     \grasse{f(\varphi_1,\ldots,\varphi_n)}_\cS = & \text{~~~[by

2132: hypothesis]}\\

2133:     \gamma(\alpha(\grasse{f(\varphi_1,\ldots,\varphi_n)}_\cS)) = &

2134: \text{~~~[by definition]}  \\ 

2135:     \gamma(\alpha(\boldsymbol{f}

2136: (\grasse{\varphi_1}_\cS,\ldots,\grasse{\varphi_n}_\cS))) = &

2137: \text{~~~[by inductive hypothesis]} \\

2138:     \gamma(\alpha(\boldsymbol{f}

2139: (\gamma(\grasse{\varphi_1}_\cS^A),\ldots,\gamma(\grasse{\varphi_n}_\cS^A))))

2140: = &  \text{~~~[by definition]} \\

2141: \gamma( \grasse{f(\varphi_1,\ldots,\varphi_n)}_\cS^A). \phantom{=}&

2142:   \end{align*}

2143: \end{itemize}

2144: Thus, by Lemma~\ref{charsp}, $A \in \SP_\fL$.  

2145: \end{proof}

2146: 

2147: 

2148: Thus, $\ok{\AD_\fL}$ is the  most abstract domain that is s.p.\ for

2149: $\fL$ w.r.t.\ $\cS$. As a consequence, it turns out  that

2150: $A$ is s.p.\ for $\fL$  if and only if $A$ represents with no loss of precision

2151: the concrete semantics of any formula in $\fL$, that is

2152: $\forall \varphi\in \fL.\; \gamma(\alpha(\grasse{\varphi}_\cS)) =

2153: \grasse{\varphi}_\cS$. Lemma~\ref{spadp} states that if a s.p.\ abstract

2154: semantics on a given abstract domain exists then this is

2155: unique. Nevertheless, 

2156: Example~\ref{esnu} shows that this unique s.p.\ abstract semantics may

2157: be induced from different abstract semantic structures, i.e.\

2158: different abstract interpretation functions. However, 

2159: when $\fL$ is closed

2160: under conjunction,

2161: it turns out

2162: that on the most abstract s.p.\ domain  $\AD_\fL$,  the abstract interpretation

2163: function is unique and is given by the best correct approximation

2164: $I^{\AD_\fL}$.  

2165: \begin{theorem}\label{unique}

2166: Let $\fL$ be closed under infinite logical conjunction and let 

2167: $\cS^\sharp = (\AD_\fL, I^\sharp)$ be an abstract semantic structure

2168: on $\AD_\fL$. If $\grasse{\cdot}_{\cS^\sharp}$ is s.p.\ for $\fL$ then

2169: $I^\sharp = I^{\AD_\fL}$. 

2170: \end{theorem}

2171: \begin{proof}

2172: Since $\fL$ is closed under arbritrary logical conjunctions 

2173: we have that $\AD_\fL = \{\grasse{\varphi}_\cS ~|~ \varphi \in

2174: \fL\}$. Thus, for any $a\in \AD_\fL$, there exists some

2175: $\varphi\in \fL$ such that

2176: $a=\grasse{\varphi}_{\cS^\sharp}=\grasse{\varphi}_\cS^{\AD_\fL}$. In fact, if

2177: $a\in \AD_\fL$ then $a= \grasse{\varphi}_\cS$, for some $\varphi\in

2178: \fL$, so that, by Lemmata~\ref{charsp} and~\ref{spadp}, $a=\grasse{\varphi}_\cS =

2179: \gamma(\grasse{\varphi}_{\cS^\sharp})=

2180: \grasse{\varphi}_{\cS^\sharp} = \grasse{\varphi}_\cS^{\AD_\fL}$. \\

2181: Let $p\in \AP$. Then, by Lemma~\ref{spadp}, $\grasse{p}_{\cS^\sharp}

2182: =\grasse{p}_{\cS}^{\AD_\fL}$ so that

2183: $I^\sharp(p)=  I^{\AD_\fL}(p)$.\\

2184: Let $f\in \Op$. Then, 

2185: \begin{align*}

2186: I^\sharp (f) (a_1,...,a_n) = & \text{~~~~~~[by

2187: the observation above]}\\

2188:     I^\sharp (f) (\grasse{\varphi_1}_{\cS^\sharp},...,\grasse{\varphi_n}_{\cS^\sharp}) = &

2189: \text{~~~~~~[by definition]}  \\ 

2190:    \grasse{f(\varphi_1,...,\varphi_n)}_{\cS^\sharp}  = &

2191: \text{~~~~~~[by Lemma~\ref{spadp}]} \\

2192:    \grasse{f(\varphi_1,...,\varphi_n)}_{\cS}^{\AD_\fL}  = &\text{~~~~~~[by definition]}  \\ 

2193: I^{\AD_\fL} (f)

2194: (\grasse{\varphi_1}_{\cS}^{\AD_\fL},...,\grasse{\varphi_n}_{\cS}^{\AD_\fL})

2195: = & \text{~~~~~~[by

2196: the observation above]}\\

2197: I^{\AD_\fL} (f) (a_1,...,a_n).\phantom{=}&

2198:   \end{align*}

2199: Thus, $I^\sharp=I^{\AD_\fL}$.

2200: \end{proof}

2201: 

2202: \noindent

2203: Hence, in the most abstract s.p.\ domain $\AD_\fL$ there is a unique

2204: choice for interpreting  

2205: atoms and operations of $\fL$. 

2206: 

2207: In our generalized framework, strong preservation for partitions

2208: becomes 

2209: a particular instance through the Galois insertion $\pr\!/\!\adp$. 

2210: Moreover, when $\fL$ is closed under infinite conjunction,

2211: it turns out that the most abstract s.p.\ domain $\AD_\fL$ is 

2212: partitioning if and only if $\fL$ is also closed under negation. 

2213: 

2214: \begin{proposition}\label{onetwo}\ \\ \

2215: {\rm (1)} $P_\fL = \pr(\AD_\fL)$ and $\adp(P_\fL)=\bP(\AD_\fL)$. \\

2216: {\rm (2)} $P$ is strongly preserving

2217: for $\fL$ iff $P \preccurlyeq \pr(\AD_\fL)$ iff $\adp(P)

2218: \sqsubseteq \AD_\fL$.\\

2219: {\rm (3)} Let $\fL$ be closed under conjunction. Then, 

2220: $\AD_\fL$ is partitioning iff $\fL$ is closed under logical negation. 

2221: \end{proposition}

2222: \begin{proof}

2223: (1)~ Let $\mu_\fL\in \uco(\wp(\Sigma))$ be

2224: the uco associated to $\AD_\fL$.

2225: We have that $\pr(\AD_\fL) =\{[s]_{\AD_\fL}~|~s\in \Sigma\}$, where

2226: $[s]_{\AD_\fL} = \{s'\in \Sigma~|~ \mu_\fL(\{s'\}) = \mu_\fL

2227: (\{s\})\}$. We also have that 

2228: $s\equiv_{\fL} s'$ iff $\forall \varphi\in

2229: \fL. s\in  \grasse{\varphi}_\cS \Lra s'\in

2230: \grasse{\varphi}_\cS$ iff 

2231: $\mu_\fL(\{s\}) = \mu_\fL(\{s'\})$, so that

2232: $P_\fL = \pr(\AD_\fL)$. Moreover, 

2233: $\adp(P_{\fL}) = \adp(\pr(\AD_\fL))=\bP(\AD_\fL)$. \\

2234: (2)~ $P$ is s.p.\ for $\fL$ iff $P\preccurlyeq P_\fL$ iff, by 

2235: Point~(1), $P\preccurlyeq \pr(A_{\fL})$ iff, by Theorem~\ref{teoGI},

2236:   $\adp(P)\sqsubseteq \AD_\fL$. \\

2237: (3)~   Since $\fL$ is closed under infinite logical conjunction, 

2238: $\AD_\fL

2239: =\{\grasse{\varphi}_\cS~|~\varphi\in\fL\}$.  Thus, 

2240: $\fL$ is closed under logical

2241:   negation iff $\AD_\fL$ is closed under complementation

2242: $\complement$ and this exactly means that

2243:   $\AD_\fL$ is forward complete for the complement $\complement$.  By

2244:   Corollary~\ref{coropart}, 

2245: this latter fact happens iff $\AD_\fL$ is partitioning. 

2246: \end{proof}

2247: 

2248: 

2249: In particular, when $\fL$ is closed under conjunction but not under

2250: negation, it turns out that $\adp(P_\fL) \sqsubset \AD_\fL$, i.e.\ a

2251: proper loss of information occurs when the domain $\AD_\fL$ is

2252: abstracted 

2253: to the partition $\pr(\AD_\fL)=P_\fL$. On the other hand, when 

2254: $\fL$ is closed under conjunction and negation, we have that

2255: $\adp(P_\fL)=\AD_\fL$ and therefore, by Theorem~\ref{unique}, the

2256: abstract interpretation function on the partitioning abstract domain

2257: $\adp(P_\fL)$ is uniquely determined.  

2258: 

2259: 

2260: \begin{example2}\label{exefex}

2261: Let us consider the traffic light controller $\cK$ in

2262: Example~\ref{semaforo}. As already observed, 

2263: formulae of $\fL$ have the following semantics in $\cK$:

2264: \begin{align*}

2265: \ok{\grasse{\mathit{stop}}_\cK} = \{ R,RY\};~~~

2266: \ok{\grasse{\mathit{go}}_\cK} = \{ G,Y\};~~~

2267: \ok{\grasse{\mathrm{AXX}\mathit{stop}}_\cK}=\{G,Y\};~~~

2268: \ok{\grasse{\mathrm{AXX}\mathit{go}}_\cK}=\{R,RY\}

2269: \end{align*}

2270: so that $$\AD_\fL =\cM(\{

2271: \ok{\grasse{\varphi}_\cK}~|~ \varphi\in \fL\}) 

2272: = \{ \varnothing, \{R,RY\}, \{G,Y\}, \{R,RY,G,Y\} \}$$ 

2273: and $P_\fL = \pr(\AD_\fL)=

2274: \{ \{R,RY\},\{G,Y\}\}$. We denote by $\mu_\fL$ the uco associated to

2275: $\AD_\fL$.  As shown in Example~\ref{semaforo}, it turns

2276: out  that 

2277: no abstract Kripke structure that properly abstracts $\cK$ and

2278: strongly preserves $\fL$ can be defined. In our approach, the

2279: abstract domain $\AD_\fL$ induces a corresponding  strongly preserving

2280: abstract semantics $\ok{\grasse{\cdot}_\cK^{\AD_\fL}}: \fL \ra

2281: \AD_\fL$, where the best correct approximation

2282: of the operator $\mathbf{AXX}:\wp(\Sigma)\ra \wp(\Sigma)$ on $\AD_\fL$

2283: is:

2284: %

2285: \begin{align*}

2286: \mu_\fL \circ \mathbf{AXX} =&~ \{\varnothing \mapsto \varnothing, \{R,RY\} \mapsto \{G,Y\}, 

2287: \{G,Y\} \mapsto \{R,RY\},  \\

2288: &~~~\{R,RY,G,Y\}  \mapsto \{R,RY,G,Y\}\}. \\[-35pt]

2289: \end{align*}

2290: %

2291: \mbox{~~}\qed

2292: \end{example2}

2293: 

2294: 

2295: \begin{figure}[t]

2296: \begin{center}

2297: \begin{tabular}{ccc}

2298:   \mbox{\xymatrix{

2299:       *++[o][F]{1} \ar[d] \ar[r]^(0.3){p} ^(1.3){p} &

2300:       *++[o][F]{2} \ar@(ul,ur)[] \ar[ld] &  \\ 

2301:       *++[o][F]{3}\ar[r] ^(0.3){p} & *++[o][F]{4}\ar@/^/[r] ^(0.24){p}

2302: & *++[o][F]{5} \ar@/^/[l] ^(0.24){q} \\

2303:     }

2304:   }

2305: & \mbox{~~~~~~~~~~~~~~~~~~~~} &

2306:   \mbox{\xymatrix  {

2307:       *++[o][F]{\![12]\!} \ar[d] ^(0.32){p} \ar@(ul,ur)[] & &  \\ 

2308:       *++[o][F]{\,[3]\,}\ar[r] ^(0.28){p} & *++[o][F]{\,[4]\,}\ar@/^/[r] ^(0.26){p}

2309: & *++[o][F]{\,[5]\,} \ar@/^/[l] ^(0.26){q} \\

2310:     }

2311:   }

2312: \end{tabular}

2313: \end{center}

2314: \caption{Concrete (on the left) and abstract (on the right) Kripke structures.}\label{fig1}

2315: \end{figure}

2316: 

2317: 

2318: \begin{example2}\label{exef}

2319: Consider the language $\CTL$ and the Kripke structure 

2320: $\cK=(\Sigma,R, \ell)$ depicted in

2321: Figure~\ref{fig1}, where

2322: the interpretation of temporal 

2323: operators of $\CTL$ on $\cK$ is standard. 

2324: It is well known that the coarsest s.p.\

2325: partition $P_{\mathrm{CTL}}$ can

2326: be obtained by refining the initial partition $P=\{1234,5\}$ induced

2327: by the labeling $\ell$ through the Paige-Tarjan \cite{pt87}

2328: algorithm, since $P_{\mathrm{CTL}}$

2329: coincides with bisimulation equivalence on $\cK$.  

2330: It is easy to check that

2331: $P_{\mathrm{CTL}}= \{12,3,4,5\}$. This partition

2332: determines (see point~(2) in Section~\ref{amc}) 

2333: the s.p.\ abstract Kripke structure depicted in

2334: Figure~\ref{fig1}. 

2335: Since $\CTL$ is closed under conjunction and negation, 

2336: by Proposition~\ref{onetwo}~(1) and~(3), it turns out that  the most abstract s.p.\

2337: domain $A_{\mathrm{CTL}}$ is partitioning and 

2338: coincides with the following partitioning closure: 

2339: $$\adp (P_{\mathrm{CTL}}) = \{\varnothing, 12,3,4,5,34, 35, 45, 122,

2340: 124, 125, 345, 1234, 1235, 1245, 12345\}.$$

2341: 

2342: 

2343: Let us now consider the following language 

2344: $\fL\ni \varphi ::= p ~|~ q~|~ \varphi_1\wedge \varphi_2~|~

2345: \mathrm{EF}_{[0,2]} \varphi$, 

2346: where $\mathrm{EF}_{[0,2]}$ is a time bounded reachability

2347: operator that is useful for quantitative temporal analysis \cite{emss90},

2348: e.g., of discrete real-time systems \cite[Chapter~16]{cgp99}. The standard 

2349: interpretation of $\mathrm{EF}_{[0,2]}$ is as follows:

2350: $s\ok{\models^\cK} \mathrm{EF}_{[0,2]} \varphi$ iff there exists a path

2351: $s_0 s_1 s_2 s_3\ldots$ in $\cK$

2352: starting from $s=s_0$ and some $n\in [0,2]$ such that  

2353: $s_n \ok{\models^\cK} \varphi$. 

2354: Let us characterize the semantics of formulae in $\fL$:

2355: \begin{align*}

2356: & \ok{\grasse{p}_\cK} = \{ 1,2,3,4\};~~~

2357:  \ok{\grasse{q}_\cK} = \{ 5\};~~~

2358: \ok{\grasse{\mathrm{EF}_{[0,2]} p}_\cK} = \{ 1,2,3,4,5\};\\

2359: & \ok{\grasse{\mathrm{EF}_{[0,2]}q}_\cK} = \{ 3,4,5\};~~~

2360: \ok{\grasse{\mathrm{EF}_{[0,2]}(\mathrm{EF}_{[0,2]}q)}_\cK} =

2361: \{1,2,3,4,5\};\\

2362: & \ok{\grasse{p \wedge \mathrm{EF}_{[0,2]}q }_\cK} =

2363: \{3,4\};~~~

2364: \ok{\grasse{\mathrm{EF}_{[0,2]}(p \wedge \mathrm{EF}_{[0,2]}q) }_\cK} =

2365: \{1,2,3,4,5\}.

2366: \end{align*}

2367: Thus, $\AD_\fL =\cM(\{

2368: \ok{\grasse{\varphi}_\cK}~|~ \varphi\in \fL\}) = \{\varnothing, 5, 34,

2369: 345,

2370: 1234, 12345\}$. On the other hand, by Proposition~\ref{onetwo}~(1),

2371: $P_\fL = \pr(\AD_\fL)= \{12, 34, 5\}$.

2372: In this case, it turns out that $\adp(P_\fL) \sqsubset

2373: \AD_\fL$. Moreover, analogously to Example~\ref{semaforo}, 

2374: let us show that there exists no abstract transition relation $\sra^\sharp

2375: \subseteq P_\fL \times P_\fL$ that determines an abstract Kripke structure

2376: $\cA= (P_\fL,

2377: \sra^\sharp,\ell_\fL)$  which strongly preserves $\fL$. 

2378: Let $B=\{1,2\}$, $B'=\{3,4\}$ and $B''=\{5\}$ be the blocks in

2379: $P_\fL$. Assume

2380: by contradiction that such an abstract Kripke structure $\cA$

2381: exists.  

2382: \begin{itemize}

2383: \item[{\rm (i)}] 

2384: On the concrete model $\cK$ we have that 

2385: $3 \ok{{\models^\cK}} \mathrm{EF}_{[0,2]}q$. Thus, by strong

2386: preservation, it must be that $B' \ok{\models^\cA}

2387: \mathrm{EF}_{[0,2]}q$.

2388: On the other hand, if $B' \sra^\sharp B$ and 

2389: $B \sra^\sharp B''$

2390: then $B \ok{\models^\cA} \mathrm{EF}_{[0,2]}q$ and therefore, by weak preservation, we

2391: would have that

2392: $ 1\ok{\models^\cK} \mathrm{EF}_{[0,2]}q$, which is a contradiction. 

2393: Thus, necessarily,

2394:  $B' \sra^\sharp B''$. 

2395: \item[{\rm (ii)}] 

2396: Let us observe that  $1 \ok{{\models^\cK}}

2397: \mathrm{EF}_{[0,2]}\mathrm{EF}_{[0,2]}q$.  Hence, by strong

2398: preservation, $B \ok{\models^\cA}

2399: \mathrm{EF}_{[0,2]}\mathrm{EF}_{[0,2]}q$. If $B \sra^\sharp B''$

2400: then, as in point~(i), we would still have that  

2401: $ 1\ok{\models^\cK} \mathrm{EF}_{[0,2]}q$, i.e.\ a

2402: contradiction. Hence, necessarily, $B \sra^\sharp B'$.

2403: \item[{\rm (iii)}] From $B \sra^\sharp  B'$ and $B'

2404: \sra^\sharp  B''$, we would obtain that 

2405: $B \ok{\models^\cA}\mathrm{EF}_{[0,2]}q$ that, as observed in

2406: point~(ii), is a contradiction. 

2407: \end{itemize}

2408: 

2409: \noindent 

2410: Thus, this shows that it is not possible to define an abstract Kripke structure on the

2411: abstract state space $P_\fL$ that strongly preserves $\fL$. The

2412: abstract domain $\AD_\fL$ induces a corresponding  

2413: abstract semantics $\ok{\grasse{\cdot}_\cK^{\AD_\fL}}$ that

2414: instead strongly preserves $\fL$. In this case, the best correct approximation

2415: of the operator $\mathbf{EF}_{[0,2]}$ on $\AD_\fL$

2416: is:

2417: \begin{align*}

2418: \mu_\fL \circ \mathbf{EF}_{[0,2]} =&~ \{\varnothing \mapsto \varnothing,\, 5 \mapsto 345,\, 

2419: 34 \mapsto 12345,\, 345 \mapsto 12345, \\ 

2420: &~~~1234  \mapsto 12345,\, 12345 \mapsto 12345\}. \\[-35pt]

2421: \end{align*}

2422: \mbox{~~}\qed

2423: \end{example2}

2424: 

2425: \section{Strong Preservation and Completeness}\label{csp}

2426: In this section we establish a precise correspondence between 

2427: generalized strong preservation of abstract models  and

2428: completeness of abstract interpretations, so that the problem of

2429: minimally refining an abstract model in order to get strong

2430: preservation can be formulated as a complete domain refinement in abstract

2431: interpretation. 

2432: 

2433: \subsection{Forward Complete Shells}\label{fcs-section}

2434: Let us consider forward completeness of abstract domains $A\in \Abs(C)$ for

2435: generic $n$-ary concrete operations $f:C^n \ra C$, with $n\geq

2436: 0$. Hence, $A$  is forward complete for $f$, or simply $f$-complete,

2437: when $f\circ \tuple{\mu_A,...,\mu_A} =\mu_A \circ f \circ

2438: \tuple{\mu_A,...,\mu_A}$, that is, for any

2439: $\vec{x}\in C^n$, $f(\mu_A(x_1),...,\mu_A(x_n)) = 

2440: \mu_A(f(\mu_A(x_1),...,\mu_A(x_n)))$. Equivalently, $A$ is

2441: $f$-complete when  

2442: for any

2443: $\vec{a}\in A^n$, $f(\gamma(a_1),...,\gamma(a_n)) = 

2444: \gamma(\alpha(f(\gamma(a_1),...,\gamma(a_n))))$.

2445: For a set of operations $F\subseteq

2446: \Fun(C)$, $A$ is $F$-complete when $A$ is $f$-complete for each

2447: $f\in F$. Observe that $F$-completeness for an abstract domain $A$ means that

2448: the associated closure $\mu_A$ is

2449: closed under the image of functions in $F$, namely  

2450: $F(\mu_A)\subseteq \mu_A$. 

2451: Also note that when $k:C^0\ra C$, i.e.\ $k\in C$ is a constant, $A$ is 

2452: $k$-complete iff $k$ is precisely represented in $A$, i.e.\

2453: $\gamma(\alpha(k)) = k$. 

2454: Let us also note that an abstract domain $A\in \Abs(C)$ is always

2455: forward meet-complete

2456: because any uco is Moore-closed.  

2457: 

2458: Let us first note that forward $F$-complete shells

2459: always exist. Let $\sS_F:\Abs(C)\ra \Abs(C)$ be defined as 

2460: $\sS_F (A)\ud \sqcup \{ X\in \Abs(C)~|~ X \sqsubseteq A ,\,

2461: X \text{ is $F$-complete}\}$.

2462: 

2463: \begin{lemma}\label{fcs}

2464: $\sS_F(A)$ is the $F$-complete shell of $A$. 

2465: \end{lemma}

2466: \begin{proof}

2467: Let $\eta = \sqcup \{\rho  \in \uco(C)~|~ \rho \sqsubseteq \mu_A,\,

2468: \rho \text{ is $F$-complete}\} = \cap \{\rho  \in \uco(C)~|~ \rho \sqsubseteq \mu_A,\,

2469: \rho \text{ is $F$-complete}\}$.

2470:   Let $f\in F$, with $\sharp(f)=n >0$ (if $\sharp(f)=0$ then, trivially, $f\in \eta$) 

2471: and $\ok{\vec{c}}\in \ok{\eta^{n}}$.

2472:   Consider any $\rho \in\uco(C)$ that is $F$-complete and such that

2473:   $\rho \sqsubseteq \mu$. Since $\eta\subseteq \rho$, we have that $\ok{\vec{c}}\in

2474:   \ok{\rho^{n}}$ and therefore $\ok{f(\vec{c})}\in\rho$ because

2475:   $\rho$ is $F$-complete.  Thus, $\ok{f(\vec{c})}\in\eta$, i.e., $\eta$ is $F$-complete.

2476: \end{proof}

2477: 

2478: A forward complete shell $\sS_F(A)$ is a more concrete abstraction

2479: than $A$. How to characterize $\sS_F(A)$? 

2480: It is here useful to view abstract domains as closure

2481: operators on the concrete domain, i.e.\ as subsets of $C$.  Hence, $A$

2482: is viewed as the

2483: subset $\img(\mu_A)=\gamma(A)$ of the concrete domain $C$ so that 

2484: $\sS_F(A)$ can be characterized as the least Moore-closed subset of $C$ that 

2485: contains $\img(\mu_A)$ and is forward $F$-complete. 

2486: We need to characterize the least amount of

2487: concrete information that must be added to $\gamma(A)$ in order to get

2488: forward completeness. 

2489: It turns out that forward complete shells admit a constructive

2490: fixpoint characterization. Let $\ok{F^{\uco}}: \uco(C)\ra \uco(C)$ be defined as follows:

2491: $\ok{F^{\uco}}(\rho)\ud\cM(F(\rho))$, namely $\ok{F^{\uco}} (\rho)$ is the most

2492: abstract domain that contains the image of $F$ on $\rho$. 

2493: Observe that the operator $\lambda \rho .\mu_A\sqcap

2494: \ok{F^{\uco}}(\rho):\uco(C)\ra \uco(C)$ is monotone.

2495: 

2496: \begin{lemma}\label{itera}

2497: $\sS_F (A) =

2498: \gfp (\lambda \rho. \mu_A \sqcap \ok{F^{\uco}} (\rho))$. 

2499: \end{lemma}

2500: \begin{proof}

2501: Observe that a uco $\rho$ is $F$-complete iff $F(\rho) \subseteq \rho$

2502: iff $\cM(F(\rho))=\ok{F^{\uco}} (\rho)\subseteq \rho$ iff $\rho

2503: \sqsubseteq \ok{F^{\uco}}(\rho)$. Thus, we have that

2504: $\sS_F (A) = \sqcup \{ \rho \in \uco(C)~|~ \rho \sqsubseteq \mu_A ,\:

2505: \rho \text{ is $F$-complete}\} = \sqcup \{ \rho \in \uco(C)~|~ \rho \sqsubseteq \mu_A ,\:

2506: \rho \sqsubseteq \ok{F^{\uco}}(\rho) \} = 

2507: \sqcup \{ \rho \in \uco(C)~|~ \rho \sqsubseteq \mu_A \sqcap \ok{F^{\uco}}(\rho) \}

2508: = \gfp ( \lambda \rho. \mu_A \sqcap \ok{F^{\uco}} (\rho))$. 

2509: \end{proof}

2510: 

2511: \noindent

2512: Thus, it turns

2513: out that the lower iteration sequence of $\lambda \rho. \mu_A \sqcap

2514: \ok{F^{\uco}} (\rho)$ 

2515: in $\uco(C)$

2516: converges to the complete shell $\sS_F(\mu_A)$.

2517: 

2518: \begin{example2}

2519: Let us consider the square operator on sets of integers

2520: $\sq:\wp(\mathbb{Z})\ra \wp(\mathbb{Z})$, i.e.\ $\sq(X)=X^2=\{x^2~|~

2521: x\in X\}$, and the abstract domain

2522: $\mathit{Sign}=\{\varnothing,\bZ_{<0},\{0\},\bZ_{>0},\bZ\}$. As observed in

2523: Section~\ref{secco}, $\mathit{Sign}$ is not forward complete for the

2524: square operator. Let us apply Lemma~\ref{itera} in order to 

2525: compute the forward complete shell

2526: $\sS_{\sq}(\mathit{Sign})$.  Observe that

2527: $$\varnothing^2 =\varnothing \in\Sign;~~~ \{0\}^2 = \{0\}\in \Sign;~~~

2528: \bZ_{<0}^2=\bZ_{>0}^2 =\bZ^2

2529: \not\in \Sign.$$

2530: Thus, the first step of iteration refines $\Sign$ to $\Sign\cup

2531: \ok{\{\bZ^2\}}$ (notice that this is an abstract domain because it is

2532: Moore-closed).  Then, $\ok{(\bZ^2)^2} =\ok{\bZ^{2^2}} \not\in \Sign

2533: \cup \{\ok{\bZ^2}\}$, so that on

2534: the second step of iteration we obtain $\Sign \cup

2535: \{\ok{\bZ^2},\ok{\bZ^{2^2}}\}$. In general, for $n\geq 1$,  the $n$-th step of

2536: iteration provides $\Sign \cup \{\ok{\bZ^{2^k}}~|~ k\in [1,n]\}$, so that the complete

2537: shell $\sS_{\sq}(\Sign)$ coincides with the least fixpoint $\Sign\cup \{\ok{\bZ^{2^n}}~|~

2538: n\geq 1\}$.

2539: \qed

2540: \end{example2}

2541: 

2542: Finally, the following easy observation will be useful later on. 

2543: \begin{lemma}\label{shellequiv}

2544: Let $F,G\subseteq \Fun(C)$. Then, $\sS_F = \sS_G$ if and only if for any $A \in

2545: \Abs(C)$, $A$ is $F$-complete $\Lra$ $A$ is $G$-complete. 

2546: \end{lemma}

2547: \begin{proof}

2548: ($\Ra$) If $A$ is $F$-complete then $A=\sS_F(A) = \sS_G(A)$

2549: and therefore $A$ is $G$-complete as well. \\

2550: ($\Leftarrow$) This follows from

2551: $\sS_F (A)= \sqcup \{ X \in \Abs(C)~|~ X \sqsubseteq A ,\,

2552: X \text{ is $F$-complete}\} = \sqcup \{ X \in \Abs(C)~|~ X \sqsubseteq A ,\,

2553: X \text{ is $G$-complete}\} = \sS_G (A)$.   

2554: \end{proof}

2555: 

2556: \subsection{Strong Preservation and Complete Shells}

2557: Let $\fL$ be a language with atoms in $\AP_{\fL}$ and operators in

2558: $\Op_{\fL}$ and let $\cS=(\Sigma,I)$ be a semantic structure for

2559: $\fL$ so that $\APb_{\fL}$ and $\Opb_\fL$ denote, respectively, the

2560: corresponding sets of semantic interpretations of atoms and operators.

2561: It turns out that forward completeness

2562: for $\APb_{\fL}$ and $\Opb_\fL$

2563: implies strong preservation for $\fL$.

2564: \begin{lemma}

2565: If $A\in \Abs(\wp(\Sigma))$ is forward complete for $\APb_{\fL}$ and

2566: $\Opb_\fL$ then $A$ is s.p.\ for $\fL$.

2567: \end{lemma}

2568: \begin{proof}

2569: By Theorem~\ref{spchar}, we show that $A\sqsubseteq \AD_\fL$. Let

2570: us show by

2571: induction that

2572: for any $\varphi\in \fL$,

2573: $\grasse{\varphi}_\cS=\gamma(\alpha(\grasse{\varphi}_\cS))$. 

2574: \begin{itemize}

2575: \item[--] $\varphi\equiv p\in \AP_\fL$: since $A$ is forward

2576: complete for $\boldsymbol{p}$, 

2577:   $\grasse{p}_\cS=\boldsymbol{p}= \gamma(\alpha(\boldsymbol{p})) =

2578: \gamma(\alpha(\grasse{p}_\cS))$. 

2579: 

2580: \item[--] $\varphi\equiv f(\varphi_1,\ldots,\varphi_n)$ with $f\in \Op_\fL$: 

2581:   \begin{align*}

2582:     \grasse{f(\varphi_1,...,\varphi_n)}_\cS = & \text{~~~[by

2583: definition]}\\

2584:     \boldsymbol{f}

2585: (\grasse{\varphi_1}_\cS,...,\grasse{\varphi_n}_\cS) = &

2586: \text{~~~[by inductive hypothesis]} \\

2587:     \boldsymbol{f}

2588: (\gamma(\alpha(\grasse{\varphi_1}_\cS)),...,\gamma(\alpha(\grasse{\varphi_n}_\cS)))

2589: = &  \text{~~~[since $A$ is forward complete for $\boldsymbol{f}$]} \\

2590:     \gamma(\alpha(\boldsymbol{f}

2591: (\gamma(\alpha(\grasse{\varphi_1}_\cS)),...,\gamma(\alpha(\grasse{\varphi_n}_\cS)))))

2592: = &  \text{~~~[by inductive hypothesis and by definition]} \\

2593:     \gamma(\alpha(\grasse{f(\varphi_1,...,\varphi_n)}_\cS)).\phantom{=} &

2594:   \end{align*}

2595: \end{itemize}

2596: \end{proof}

2597: 

2598: On the other hand, the converse is not true, that is 

2599: strong preservation does not imply forward

2600: completeness, as shown by the following example. 

2601: 

2602: \begin{example2}

2603: Let us consider again Example~\ref{esnu} where we showed that the partitioning abstract

2604: domain $A=\wp(P)_\subseteq$ is s.p.\ for $\fL$. However, $A$ is not

2605: forward complete for $\boldsymbol{Op}_\fL = \{\pre_\sra\}$.  In fact: 

2606: $\gamma(\alpha ( \pre_\sra (\gamma (\alpha (\{3\}))))) =

2607: \gamma(\alpha ( \pre_\sra (\{3\}))) 

2608: = \gamma (\alpha (\{2,3\})) = \{1,2,3\}$ while 

2609: $\pre_\sra (\gamma (\alpha (\{3\})))= \pre_\sra (\{3\}) =

2610: \{2,3\}$. 

2611: \qed

2612: \end{example2}

2613: 

2614: Instead, it turns out that most abstract s.p.\ domains can be

2615: characterized as forward complete shells.  

2616: \subsubsection{Complete Shells as Strongly Preserving Abstract Domains} \label{cssp}

2617: 

2618: Partition refinement

2619: algorithms for computing behavioural equivalences like bisimulation

2620: \cite{pt87}, simulation equivalence \cite{bg03,hhk95,TC01} and (divergence

2621: blind) stuttering equivalence \cite{gv90} are used

2622: in standard abstract model checking to

2623: compute the coarsest strongly preserving partition of temporal languages

2624: like $\CTLS$ or the

2625: $\mu$-calculus for the case of bisimulation equivalence, $\ACTLS$ for simulation

2626: equivalence and $\CTLSX$ for stuttering equivalence.

2627: 

2628: Given a language $\fL$ and a concrete state space $\Sigma$, 

2629: these partition refinement algorithms work by

2630: iteratively refining an initial partition $P$ within the lattice of

2631: partitions $\Part(\Sigma)$ until the fixpoint $P_\fL$ is reached.

2632: The input partition $P$ determines the set

2633: $\AP_P$ 

2634: of atoms

2635: and

2636: their interpretation $I_P$ as follows: $\AP_P\ud \{p_B~|~B\in P\}$ and

2637: $I_P(p_B) \ud B$. 

2638: More in general, any $\cX\subseteq \wp(\Sigma)$ determines a 

2639: set $\{p_X\}_{X\in \cX}$ of atoms with interpretation

2640: $I_\cX( p_X) =X$. In particular, this can be done for an abstract domain

2641: $A \in \Abs(\wp(\Sigma))$ by considering its concretization 

2642: $\gamma(A)\subseteq \Sigma$, namely $A$ is viewed as a set of atoms 

2643: with interpretation 

2644: $I_A (a) = \gamma(a)$. Thus, an abstract domain $A\in

2645: \Abs(\wp(\Sigma))$ 

2646: together with a set of functions $F\subseteq

2647: \Fun(\wp(\Sigma))$ determine a language $\fL_{A,F}$, with atoms in

2648: $A$, operations in $F$ and endowed with a semantic structure

2649: $\cS_{A,F}=(\Sigma,I_A \cup I_F)$ such that  for any $a\in A$, $I_A(a)=\gamma(a)$

2650: and for any $f\in F$, $I_F(f)=f$.   

2651: Therefore, the most abstract s.p.\ domain $\AD_{\fL_{A,F}}$ generalizes in

2652: our framework the

2653: output of a partition refinement algorithm for some language. Accordingly, 

2654: we aim at

2655: characterizing $\AD_{\fL_{A,F}}$ as the output of a

2656: refinement process of the initial domain $A$ within the lattice 

2657: $\Abs(\wp(\Sigma))$

2658: of abstract domains. The following 

2659: result shows that forward

2660: completeness for the operations in $F$ is the right

2661: notion of refinement to be used for the case of abstract

2662: domains. 

2663: 

2664: \begin{theorem}\label{main2} Let

2665: $A \in \Abs(\wp (\Sigma ))$, $F\subseteq \Fun(\wp(\Sigma))$ 

2666: and assume that $\fL_{A,F}$ is closed under infinite logical conjunction. Then,

2667: $\AD_{\fL_{A,F}} = \sS_{F}(A)$. 

2668: \end{theorem}

2669: \begin{proof}

2670: Since $\fL_{A,F}$ is closed under conjunction we 

2671:  have that $\AD_{\fL_{A,F}} =

2672: \{\grasse{\varphi}_{\cS_{A,F}}~|~\varphi\in\fL_{A,F}\}$.

2673:   Let us first prove that

2674:   $\{\grasse{\varphi}_{\cS_{A,F}}~|~\varphi\in\fL_{A,F}\} 

2675: \subseteq\sS_{F}(A)$ by structural

2676: induction on $\varphi\in \fL_{A,F}$:

2677:   \begin{itemize}

2678:   \item[--] $\varphi\equiv a\in A$: $\grasse{a}_{\cS_{A,F}} = I_A(a)=\gamma(a)

2679: \in \gamma(A) \subseteq

2680:     \sS_{F}(A)$.

2681:   \item[--] $\varphi\equiv f(\varphi_1,...,\varphi_n)$ with $f\in F$: 

2682:      $\grasse{f(\varphi_1,...,\varphi_n)}_{\cS_{A,F}}=

2683:     f(\grasse{\varphi_1}_{\cS_{A,F}},...,

2684: \grasse{\varphi_n}_{\cS_{A,F}})$,  where,

2685: by inductive hypothesis, 

2686: $\grasse{\varphi_i}_{\cS_{A,F}}\in \sS_{F}(A)$. 

2687: Therefore, since $\sS_{F}(A)$ is 

2688: forward $f$-complete, we have that

2689: $f(\grasse{\varphi_1}_{\cS_{A,F}},...,\grasse{\varphi_n}_{\cS_{A,F}})\in

2690: \sS_{F}(A)$.   

2691:   \end{itemize}

2692: 

2693: %

2694: \noindent

2695: Let us now prove the opposite inclusion. 

2696: Let us first observe that $\AD_{\fL_{A,F}}$

2697: is forward

2698: $F$-complete. For simplicity of notation, 

2699: consider  $f\in F$ with

2700: $\sharp(f)=1$. If $\grasse{\varphi}_{\cS_{A,F}} \in

2701: \AD_{\fL_{A,F}}$, where $\varphi\in \fL_{A,F}$, then, $f(\varphi)\in

2702: \fL_{A,F}$ and $f(\grasse{\varphi}_{\cS_{A,F}}) =

2703: \grasse{f(\varphi)}_{\cS_{A,F}} \in \AD_{\fL_{A,F}}$. 

2704: By Lemma~\ref{itera}, we know that 

2705:   $\sS_{A}(A)=\sqcap_{\alpha \in\Ord} (\lambda \rho. \mu_A

2706: \sqcap \cM(F(\rho)))^{\alpha,\downarrow} (\top_{\uco(\wp(\Sigma))})$, so that

2707:   it is sufficient to prove by transfinite induction on $\alpha \in

2708: \Ord$ that

2709:   $$(\lambda \rho. \mu_A

2710: \sqcap \cM(F(\rho)))^{\alpha,\downarrow} 

2711: (\top_{\uco(\wp(\Sigma))}) \subseteq \AD_{\fL_{A,F}}.$$

2712:   \begin{itemize}

2713: 

2714:   \item[--] $\alpha = 0$:  $(\lambda \rho. \mu_A

2715: \sqcap \cM(F(\rho)))^{0,\downarrow} (\top_{\uco(\wp(\Sigma))})

2716: =\top_{\uco(\wp(\Sigma))}=\{\Sigma \} \in \gamma(A) \subseteq \AD_{\fL_{A,F}}$.

2717:   \item[--] $\alpha +1$: By inductive

2718: hypothesis, $(\lambda \rho. \mu_A

2719: \sqcap \cM(F(\rho)))^{\alpha,\downarrow} (\top_{\uco(\wp(\Sigma))}) 

2720: \subseteq\AD_{\fL_{A,F}}$. Moreover, $\AD_{\fL_{A,F}}$ is Moore-closed

2721: and forward

2722: $F$-complete (hence closed under $F$).

2723: Thus, $\cM(F ( (\lambda \rho. \mu_A

2724: \sqcap \cM(F(\rho)))^{\alpha,\downarrow} (\top_{\uco(\wp(\Sigma))}))) \subseteq

2725: \AD_{\fL_{A,F}}$,  namely 

2726: $(\lambda \rho. \mu_A

2727: \sqcap \cM(F(\rho)))^{\alpha+1,\downarrow} (\top_{\uco(\wp(\Sigma))})\subseteq

2728: \AD_{\fL_{A,F}}$.

2729: \item[--] limit ordinal $\alpha$: 

2730: This follows from 

2731: $$ (\lambda \rho. \mu_A

2732: \sqcap \cM(F(\rho)))^{\alpha,\downarrow}

2733: (\top_{\uco(\wp(\Sigma))}) =

2734: \sqcap_{\beta < \alpha} (\lambda \rho. \mu_A

2735: \sqcap \cM(F(\rho)))^{\beta,\downarrow}

2736: (\top_{\uco(\wp(\Sigma))}) $$

2737: because, by inductive hypothesis, $(\lambda \rho. \mu_A

2738: \sqcap \cM(F(\rho)))^{\beta,\downarrow} (\top_{\uco(\wp(\Sigma))}) 

2739: \subseteq \AD_{\fL_{A,F}}$, for any

2740: $\beta< \alpha$.

2741:   \end{itemize}

2742: \end{proof}

2743: 

2744: 

2745: \subsubsection{Strongly Preserving Abstract Domains as Complete Shells} 

2746: 

2747: Let us consider a language $\fL$, with atoms in $\AP_\fL$ and

2748: operators in $\Op_\fL$, and a semantic structure $\cS=(\Sigma,I)$.  

2749: As an immediate consequence of Theorem~\ref{main2}, 

2750: the most abstract s.p.\ domain 

2751: $\AD_{\fL}$ for $\fL$ w.r.t.\ $\cS$ can be characterized as the

2752: forward $\boldsymbol{AP}_\fL \cup \boldsymbol{Op}_\fL$-complete shell

2753: of the most abstract domain $\{\Sigma\}$.

2754: 

2755: \begin{corollary}\label{strai}

2756:   Let $\fL$ be closed under infinite

2757: logical conjunction.

2758: Then, $\AD_\fL=\sS_{\boldsymbol{AP}_\fL\cup\boldsymbol{Op}_\fL}(\{\Sigma\})$.

2759: \end{corollary}

2760: 

2761: Let us also observe that

2762: $\AD_\fL$ can be equivalently characterized as 

2763: the

2764: forward $\boldsymbol{Op}_\fL$-complete shell

2765: of an initial abstract

2766: domain $\cM(\boldsymbol{AP}_\fL)$ induced by atoms: 

2767: $\AD_\fL=\sS_{\boldsymbol{Op}_\fL}(\cM(\boldsymbol{AP}_\fL))$.

2768: 

2769: 

2770: \subsubsection{Strongly Preserving Partitions} 

2771: 

2772: 

2773: %It is also worth remarking that, as 

2774: %a consequence of Proposition~\ref{onetwo}~(1), 

2775: %the state equivalence induced by the language

2776: %$\fL_\mu$ can be

2777: %retrieved from the closure $\sS_{\boldsymbol{Op}}(\mu)$: 

2778: %$\equiv_{\sS_{\boldsymbol{Op}}(\mu)} \: =\: \equiv_{\fL_\mu}$.

2779: 

2780: 

2781: 

2782: Theorem \ref{main2} and Corollary~\ref{strai} 

2783: provide an elegant generalization of 

2784: partition refinement algorithms for strong

2785: preservation from an

2786: abstract interpretation perspective. 

2787: 

2788: Given a language $\fL$ with operators in $\Op_\fL$ and a corresponding

2789: semantic

2790: structure $\cS=(\Sigma,I)$, as recalled in Section~\ref{cssp}, 

2791: an input partition $P\in \Part(\Sigma)$ for a partition refinement

2792: algorithm determines the set

2793: $\AP_\fL = \{p_B~|~B\in P\}$ 

2794: of atoms of $\fL$ 

2795: and

2796: their interpretation $I (p_B)=B$. Thus, $\cM(\boldsymbol{\AP}_\fL) =

2797: \cM(P)=P\cup \{\varnothing,\Sigma\}$. 

2798: It turns out that the coarsest s.p.\ partition $P_\fL$ for $\fL$ 

2799: can be characterized in our abstract domain-based approach as

2800: follows. 

2801: 

2802: 

2803: 

2804: \begin{corollary}\label{spcb}

2805:   Let $\fL$

2806: be closed under infinite logical conjunction. \\

2807:   {\rm (1)}  $P_\fL = \pr(\sS_{\boldsymbol{Op}_\fL}(\cM(P)))$.\\

2808:   {\rm (2)} Let $\fL$ be closed under logical negation. Then, 

2809:   $\adp(P_{\fL}) =

2810: \sS_{\boldsymbol{Op}_\fL}(\cM(P))$.

2811: \end{corollary}

2812: \begin{proof}

2813:   \noindent {\rm (1)} 

2814: By Corollary~\ref{strai}, 

2815: $\AD_\fL=\sS_{\boldsymbol{Op}_\fL}(\cM(P))$ and by

2816: Proposition~\ref{onetwo}~(1), $P_\fL=\pr(\AD_\fL)=

2817: \pr(\sS_{\boldsymbol{Op}_\fL}(\cM(P)))$.\\ 

2818: %

2819: {\rm (2)} By Proposition~\ref{onetwo}~(1) and~(3),

2820: Corollary~\ref{strai} and point~(1), 

2821: $\adp(P_\fL)=\adp(\pr(\AD_\fL))=\AD_\fL=\sS_{\boldsymbol{Op}_\fL}(\cM(P))$. 

2822: \end{proof}

2823: 

2824: It is worth remarking that when $\cL$ is not closed under negation, by

2825: Proposition~\ref{onetwo}~(3) and Corollary~\ref{spcb}~(2), it turns out

2826: that $\adp(P_\fL) \sqsubset \sS_{\boldsymbol{Op}_\fL}(\cM(P))$.  This

2827: means that when $\fL$ is not closed under negation the output

2828: partition $P_\fL$ of any partition refinement algorithm for achieving

2829: strong preservation for $\fL$ is not optimal within the lattice of

2830: abstract domains.

2831: 

2832: 

2833: \begin{example2}

2834: Let us consider the language $\fL$ and 

2835: the concrete Kripke structure $\cK$ in Example~\ref{exef}.

2836: The labeling determines the initial partition

2837: $P=\{\boldsymbol{p}=1234, \boldsymbol{q}=5\}\in \Part(\Sigma)$, so

2838: that $\cM(P)= \{\varnothing, 1234,5,12345\}\in \Abs(\wp(\Sigma))$. 

2839: Here, $\Op_\fL = \{\wedge, \mathrm{EF}_{[0,2]}\}$. Abstract domains

2840: are Moore-closed so that $\sS_{\boldsymbol{Op}_\fL}=

2841: \sS_{\mathbf{EF}_{[0,2]}}$. Let us compute

2842: $\sS_{\mathbf{EF}_{[0,2]}}(\cM(P))$. 

2843: \begin{align*} 

2844: A_0 & = \cM(P)= \{\varnothing, 1234,5,12345\}\\

2845: A_1 & = A_0 \sqcap \cM(\mathbf{EF}_{[0,2]}(A_0))= \cM(A_0 \cup \mathbf{EF}_{[0,2]}(A_0)) \\ 

2846: & =

2847: \cM(\{\varnothing, 1234,5,12345\} \cup \{

2848: \mathbf{EF}_{[0,2]}(\{5\})=345\}) = \{\varnothing, 5, 34,

2849: 1234,12345\}\\

2850: A_2 & = A_1 \text{~~~~(fixpoint)}

2851: \end{align*}

2852: As already observed in Example~\ref{exef}, $P_\fL = \{12,34,5\}$ is

2853: such that $\adp(P_\fL)\sqsubset \mu_\fL$ and it is not possible

2854: to define a strongly

2855: preserving abstract Kripke

2856: structure on the abstract space $P_\fL$.

2857: \qed

2858: \end{example2}

2859: 

2860: 

2861: 

2862: \section{An Application to some Behavioural Equivalences}\label{abse}

2863: It is well known that some temporal

2864: languages like $\CTL$, $\ACTL$ and $\CTLX$ induce state logical equivalences that

2865: coincide with standard behavioural equivalences 

2866: like bisimulation equivalence for $\CTL$, 

2867: (divergence blind) stuttering equivalence for $\CTLX$ and

2868: simulation equivalence for

2869: $\ACTL$. 

2870: We derive here

2871: a novel characterization of these behavioural equivalences

2872: in terms of forward completeness of abstract

2873: interpretations. 

2874: %Moreover, we also show how our approach allows to

2875: %obtain a simple characterization of

2876: %the smallest (w.r.t.\ the number of states and transitions) 

2877: %abstract Kripke structures that strongly

2878: %preserve $\CTL$ and $\ACTL$.

2879: 

2880: 

2881: \subsection{Bisimulation Equivalence}

2882: Let $\cK = (\Sigma ,\sra,\ell)$ be a Kripke structure over some set

2883: $\AP$ of atomic propositions. A

2884: relation $R  \subseteq \Sigma \times \Sigma $ is a bisimulation on

2885: $\cK$ if for any

2886: $s,s'\in \Sigma $ such that $s R s'$:

2887: \begin{itemize}

2888: \item[{\rm (1)}] $\ell(s) =\ell (s')$; 

2889: \item[{\rm (2)}] For

2890: any $t\in \Sigma $ such that $\ok{s \sra t}$, there exists $t'\in \Sigma $

2891: such that $\ok{s'\sra t'}$

2892: and $t R t'$;

2893: \item[{\rm (3)}] $s' R s$, i.e.\ $R$ is symmetric. 

2894: \end{itemize}

2895: Since the empty

2896: relation is a bisimulation and bisimulations are closed under union,

2897: it turns out that the 

2898: largest (as a set) bisimulation relation exists. This largest

2899: bisimulation is an equivalence relation called bisimulation

2900: equivalence and is 

2901: denoted by $\sim_{\mathrm{bis}}$ while $P_{\mathrm{bis}}\in \Part(\Sigma)$ denotes

2902: the corresponding partition. 

2903: Thus,  a partition $P\in \Part(\Sigma)$ is a bisimulation on $\cK$

2904: when $P\preceq P_{\mathrm{bis}}$.

2905: 

2906: It is well known~\cite{bcg88} that

2907: when $\cK$ is finitely branching, bisimulation

2908: equivalence coincides with the state

2909: equivalence induced by $\CTL$, i.e.,

2910: $P_{\mathrm{bis}}= P_\CTL$ (the same holds

2911: for $\CTLS$ and the $\mu$-calculus, see e.g.\

2912: \cite[Lemma~6.2.0.5]{dams96}). 

2913: Moreover, it is known (see e.g.\ \cite[Section~12]{vg90}) that it is enough

2914: to consider finitary Hennessy-Milner logic \cite{hm85}, i.e.\ a language

2915: $\fL_1$ including propositional logic 

2916: and the existential next operator in order to have that

2917: $P_{\fL_1} = P_{\mathrm{bis}}$: 

2918: $$\fL_1 \ni \varphi ::= p ~|~ \varphi_1 \wedge \varphi_2 ~|~

2919: \neg \varphi ~|~

2920: \mathrm{EX}\varphi 

2921: $$ where, as usual, 

2922: the interpretation $\mathbf{EX}$ of $\mathrm{EX}$ in $\cK$ is 

2923: $\pre_\sra$.  A number of algorithms for computing bisimulation

2924: equivalence exists \cite{bfh90,dpp04,ly92,pt87}. The

2925: Paige-Tarjan algorithm \cite{pt87}  runs in $O(|\sra|\log(|\Sigma

2926: |))$-time and 

2927: is the most time-efficient

2928: algorithm that computes bisimulation equivalence.  

2929: 

2930: We recalled above that $P_{\fL_1} = P_\CTL$. In our framework,

2931: this can be obtained as a consequence of the fact 

2932: that the most

2933: abstract s.p.\ domains for $\CTL$ and $\fL_1$ coincide.

2934: 

2935: \begin{lemma}\label{ctlequiv}

2936: Let $\cK$ be finitely branching. Then, $\AD_\CTL  = \AD_{\fL_1}=\adp(P_{\mathrm{bis}})$. 

2937: \end{lemma}

2938: \begin{proof}

2939: Let $\boldsymbol{Op}_{\CTL} =   

2940: \{\cap,  \complement, \mathbf{AX}, \mathbf{EX},

2941: \mathbf{AU},\mathbf{EU}, \mathbf{AR},  \mathbf{ER}\}$ be the

2942: set of standard interpretations of the operators of $\CTL$ on $\cK$, 

2943: so that $\mathbf{AX}=\pret_\sra$ and

2944: $\mathbf{EX}=\pre_\sra$.   

2945: We show

2946: that $\mu\in \uco(\wp(\Sigma))$ is forward complete  for 

2947: $\boldsymbol{Op}_{\CTL}$ 

2948:  iff

2949: $\mu$ is forward complete  for $\{\complement , \pre_\sra\}$. 

2950: Assume that $\mu$ is forward complete  for $\{\complement ,

2951: \pre_\sra\}$. Let us first prove that $\mu$ is forward

2952: complete for $\pret_\sra = \mathbf{AX}$: 

2953: \begin{align*}

2954: \mu \circ \pret_\sra \circ \mu &= \text{~~~~~[by definition of $\pret_\sra$]}\\

2955: \mu \circ \complement \circ \pre_\sra \circ \complement \circ \mu & = 

2956: \text{~~~~~[as $\mu$ is complete for $\complement$]}\\

2957: \mu \circ \complement \circ \pre_\sra \circ \mu \circ \complement \circ \mu & = 

2958: \text{~~~~~[as $\mu$ is complete for $\pre_\sra$]}\\

2959: \mu \circ \complement \circ \mu \circ \pre_\sra \circ \mu \circ \complement \circ \mu & = 

2960: \text{~~~~~[as $\mu$ is complete for $\complement$]}\\

2961: \complement \circ \mu \circ \pre_\sra \circ \mu \circ \complement \circ \mu & = 

2962: \text{~~~~~[as $\mu$ is complete for $\pre_\sra$]}\\

2963: \complement \circ \pre_\sra \circ \mu \circ \complement \circ \mu & = 

2964: \text{~~~~~[as $\mu$ is complete for $\complement$]}\\

2965: \complement \circ \pre_\sra \circ \complement \circ \mu & = 

2966: \text{~~~~~[by definition of $\pret_\sra$]}\\

2967: \pret_\sra \circ \mu &

2968: \end{align*}

2969: The following fixpoint

2970: characterizations are well known~\cite{cgp99}: 

2971: \begin{itemize}

2972: \item[--] $\mathbf{AU}(S_1,S_2) = \lfp(\lambda Z. S_2 \cup (S_1 \cap

2973: \pret_\sra(Z)))$; 

2974: \item[--] $\mathbf{EU}(S_1,S_2) = \lfp(\lambda Z. S_2 \cup (S_1 \cap

2975: \pre_\sra(Z)))$;

2976: \item[--] $\mathbf{AR}(S_1,S_2) = \gfp(\lambda Z. S_2 \cap (S_1 \cup

2977: \pret_\sra(Z)))$; 

2978: \item[--] $\mathbf{ER}(S_1,S_2) = \gfp(\lambda Z. S_2 \cap (S_1 \cup

2979: \pre_\sra(Z)))$.

2980: \end{itemize}

2981: Let us show that $\mu$ is forward complete for $\mathbf{AU}$. The proofs

2982: for the remaining operators in $\boldsymbol{Op}_{\CTL}$

2983: are analogous. 

2984: We need to show that $\mu (\lfp(\lambda Z. \mu(S_2) \cup (\mu(S_1) \cap

2985: \pret_\sra(Z)))) = \lfp(\lambda Z. \mu(S_2) \cup (\mu(S_1) \cap

2986: \pret_\sra(Z)))$. Let us  show that $\mu$ is forward

2987: complete for the function $\lambda Z. \mu(S_2) \cup (\mu(S_1) \cap

2988: \pret_\sra(Z))$: 

2989: \begin{align*}

2990: \mu( \mu(S_2) \cup (\mu(S_1) \cap \pret_\sra (\mu (Z)))) &= 

2991: \text{~~~~~[as $\mu$ is complete for $\pret_\sra$]}\\

2992: \mu( \mu(S_2) \cup (\mu(S_1) \cap \mu (\pret_\sra (\mu (Z))))) &= 

2993: \text{~~~~~[as $\mu$ is  complete for $\cap$]}\\

2994: \mu( \mu(S_2) \cup \mu(\mu(S_1) \cap \mu (\pret_\sra (\mu (Z))))) &=

2995: \text{~~~~~[as $\mu$ is complete for $\cup$]}\\

2996: \mu(S_2) \cup \mu(\mu(S_1) \cap \mu (\pret_\sra (\mu (Z)))) &=

2997: \text{~~~~~[as $\mu$ is  complete for $\cap$]}\\

2998: \mu(S_2) \cup (\mu(S_1) \cap \mu (\pret_\sra (\mu (Z)))) &=

2999:  \text{~~~~~[as $\mu$ is  complete for $\pret_\sra$]}\\

3000: \mu(S_2) \cup (\mu(S_1) \cap \pret_\sra (\mu (Z))).&

3001: \end{align*}

3002: Observe that since $\mu$ is additive (and therefore continuous)

3003: we have that 

3004: $\mu(\varnothing)=\varnothing$. 

3005: Moreover, let us show that from the hypothesis that 

3006: $\cK$ is finitely branching it follows  that

3007: $\pret_\sra$ is continuous. First, notice that

3008: $\pret_\sra$ is continuous iff $\pre_\sra$ is co-continuous. Hence,

3009: let us check that $\pre_\sra$ is co-continuous. Let

3010: $\{X_i\}_{i\in \mathbb{N}}$ be a decreasing chain of subsets of $\Sigma$ and let

3011: $x\in \cap_{i\in \mathbb{N}} \pre_\sra (X_i)$. Since $\cK$ is

3012: finitely branching, $\post_\sra(\{x\})$ is finite so that 

3013: there exists some $k\in \mathbb{N}$ such that for any

3014: $j>0$, $\post_\sra(\{x\})\cap X_k = \post_\sra(\{x\}) \cap

3015: X_{k+j}$. Hence, there exists some $z\in \cap_{i\in \mathbb{N}} X_i

3016: \cap \post_\sra(\{x\})$, so that $x\in \pre_\sra (\cap_{i\in \mathbb{N}}X_i)$.

3017: Therefore, since $\pret_\sra$ is continuous we also have that    

3018: $\lambda Z. \mu(S_2) \cup (\mu(S_1) \cap

3019: \pret_\sra(Z))$ is continuous. 

3020: We can therefore apply Lemma~\ref{fixrem2} so that

3021: $\mu (\lfp(\lambda Z. \mu(S_2) \cup (\mu(S_1) \cap

3022: \pret_\sra(Z)))) = \lfp(\lambda Z. \mu(S_2) \cup (\mu(S_1) \cap

3023: \pret_\sra(Z)))$.\\

3024: Thus, 

3025: by Lemma~\ref{shellequiv}, $\sS_{\{\complement ,

3026: \pre_\sra\}} = \sS_{\boldsymbol{Op}_{\CTL}}$, so that, by

3027: Corollary~\ref{strai}, $\AD_{\fL_1} = \AD_\CTL$. Finally, since

3028: $\cK$ is finitely branching and 

3029: $\fL_1$ is closed under conjunction and negation, $\adp(P_{\fL_1})=

3030: \adp(P_{\mathrm{bis}}) = \adp(P_{\fL_1})= \AD_{\fL_1}$.

3031: \end{proof}

3032: 

3033: 

3034: As a consequence of this and of the results in Section~\ref{csp}

3035: (in particular of Corollary~\ref{spcb}), any partition refinement

3036: algorithm $\Algbis$ for computing bisimulation equivalence on a

3037: finitely branching Kripke structure, like those in

3038: \cite{bfh90,dpp04,ly92,pt87}, can be characterized as a complete shell

3039: refinement as follows:

3040: $$\Algbis(P) = \pr (\sS_{\{\complement , \pre_\sra\}}

3041: (\cM(P))).$$

3042: Thus, $\Algbis$ is viewed as an algorithm for computing a particular

3043: abstraction, that is $\pr$, of a particular complete shell, that is  

3044: $\sS_{\{\complement , \pre_\sra\}}$. In particular, this holds for the

3045: Paige-Tarjan algorithm~\cite{pt87} and leads to design a generalized

3046: Paige-Tarjan-like procedure for computing most abstract strongly preserving

3047: domains~\cite{rt05}. 

3048: 

3049: 

3050: 

3051: %Therefore, 

3052: %the equality $P_{\fL_1} = P_\CTL$ can be obtained as a consequence of

3053: %Proposition~\ref{onetwo}~(1): $P_{\fL_1} = \pr(\mu_{\fL_1}) =

3054: %\pr(\mu_\CTL) = P_\CTL$.  

3055: 

3056: Finally, our abstract intepretation-based approach allows us to give the

3057: following nice

3058: characterization of 

3059: bisimulation for a partition $P$ in terms of forward completeness for

3060: the corresponding partitioning abstract domain $\adp(P)$. 

3061: \begin{theorem}\label{thbis}

3062: Let $P\in \Part(\Sigma)$. Then, $P$ is a bisimulation on $\cK$ iff $\adp (P)$

3063: is forward complete for $\{\boldsymbol{p}~|~p\in \mathit{AP}\} \cup

3064: \{\pre_\sra\}$.

3065: \end{theorem}

3066: \begin{proof}

3067: We view $\adp(P)$ as a uco so that $\adp(P)= \{\cup_i B_i \in \wp(\Sigma)~|~

3068: \{B_i\} \subseteq P\}$. Let

3069: us first observe that $P\preceq P_\ell$ iff $\adp(P)$ is forward complete for 

3070: $\{\boldsymbol{p}\subseteq \Sigma~|~p\in AP\}$.  On the one hand,

3071: since $\boldsymbol{p}=\{s\in \Sigma ~|~p\in \ell (s)\}$, 

3072: if $s\in \boldsymbol{p}$ and $s\in B$, for some $B\in P$, then

3073: $B\subseteq [s]_\ell \subseteq \boldsymbol{p}$. Hence, 

3074: $\boldsymbol{p}$ is a union of some blocks of $P$ and therefore

3075: $\boldsymbol{p}\in \adp(P)$. On the other hand, 

3076: if $\adp(P)$ contains $\{\boldsymbol{p}\subseteq \Sigma~|~p\in AP\}$ then,

3077: for any $p\in AP$, $\boldsymbol{p}$ is a union of some blocks in

3078: $P$. Thus, for any $B\in P$, either $B\subseteq \boldsymbol{p}$ or $B\cap

3079: \boldsymbol{p}=\varnothing$. Consequently, if 

3080: $s \in B$ then  $B\subseteq [s]_\ell \in P_\ell$.

3081: \\

3082: %

3083: Let us now note that $\ok{\adp(P)}$ is forward complete for $\ok{\pre_\sra}$ iff

3084:     for any block $B\in P$, $\ok{\pre_\sra(B)}$ is a (possibly empty) union of

3085: blocks of $P$:

3086: this holds because $\ok{\pre_\sra}$ is additive, and therefore if $\ok{\{B_i\}}\subseteq

3087: P$ then $\ok{\pre_\sra(\cup_i B_i)}=\cup_i \ok{\pre_\sra(B_i)}$. 

3088: The fact that, for some  $B\in P$, $\ok{\pre_\sra(B)}= \ok{\cup_i

3089: B_i}$, for some blocks $\ok{\{B_i\}}\subseteq P$, 

3090: implies that if $s\in

3091: \ok{\pre_\sra(B)}$, i.e., $s \sra t$ for some $t\in B$, then

3092: $s\in \ok{B_j}$, for some $j$, and if $s'\in \ok{B_j}$ then $s'\in \ok{\pre_\sra(B)}$,

3093: i.e., $s' \sra t'$ for some $t'\in B$, namely

3094: condition~(2) of bisimulation for $P$ holds. On the other hand, if

3095: condition~(2) of bisimulation for $P$ holds then if $s,s'\in B'$ and

3096: $s\in \ok{\pre_\sra(B)}$, for some $B,B'\in P$, then $s'\sra t'$ 

3097: for some $t\in B$, i.e., $s'\in \ok{\pre_\sra(B)}$,

3098: and therefore $\ok{\pre_\sra(B)}$ is a union of blocks of $P$. This closes

3099: the proof.

3100: \end{proof}

3101: 

3102: 

3103: 

3104: \subsubsection{On the Smallest Abstract Transition Relation}\label{str1} 

3105: As recalled in Section~\ref{amc},

3106: the abstract Kripke structure $\cA = (P_{\mathrm{bis}},\ok{\sra^{\exists \exists}},

3107: \ok{\ell^\exists})$ strongly

3108: preserves $\CTL$,  where 

3109: $B_1 \ok{{\sra^{\exists\exists}}} B_2$ iff there exist

3110: $s_1\in B_1$ and $s_2 \in B_2$ such that $s_1 \sra s_2$, 

3111: and $\ok{\ell^\exists (B)} = \cup_{s\in B} \ell(s)$. 

3112: As a simple and  elegant 

3113: consequence of our approach, it is easy to show that $\ok{\sra^{\exists

3114: \exists}}$ is the \emph{unique} (and therefore the smallest)

3115: abstract transition relation  on $P_{\mathrm{bis}}$

3116: that induces strong preservation for $\CTL$. 

3117: 

3118: Let $\cK=(\Sigma,\sra,\ell)$ be finitely branching so that, by

3119: Lemma~\ref{ctlequiv}, $\AD_{\fL_1}=\adp(P_{\mathrm{bis}})=\wp(P_{\mathrm{bis}})$. Recall that

3120: the concrete interpretation $I$ induced by $\cK$ is such that

3121: $I(\EX)=\pre_\sra$. 

3122: By

3123: Theorem~\ref{unique}, the unique interpretation of atoms

3124: and operations in $\fL_1$ on the

3125: abstract domain $\wp(P_{\mathrm{bis}})$ that gives rise to a s.p.\

3126: abstract semantics is the best correct approximation

3127: $I^{\wp(P_{\mathrm{bis}})}$.  

3128: Hence, if $\ok{\cA} =

3129: (P_{\mathrm{bis}},\ok{\sra^{\sharp}}, 

3130: \ok{\ell^\sharp})$ is strongly preserving for $\CTL$ then the

3131: interpretation $\ok{\pre_{\sra^{\sharp}}}$ of $\EX$ 

3132: induced by $\cA$ must coincide with $\ok{I^{\wp(P_{\mathrm{bis}})}(\EX)}$.  

3133: Consequently, $\ok{\pre_{\sra^{\sharp}}} = \ok{\alpha \circ \pre_\sra \circ

3134: \gamma}$ so that for any $B_1,B_2 \in \ok{P_{\mathrm{bis}}}$, we have that 

3135: $\ok{B_1 \sra^\sharp B_2}$ iff $B_1 \in \ok{\alpha(\pre_\sra

3136: (\gamma(\{B_2\})))}$. Therefore, we conclude by observing that 

3137: $B_1 \in \ok{\alpha(\pre_\sra

3138: (\gamma(\{B_2\})))}$ iff $B_1 \ok{{\sra^{\exists\exists}}} B_2$. 

3139: 

3140: We believe that a similar reasoning could be also useful for other

3141: languages $\fL$ in order to prove that the smallest abstract

3142: transition relation on $P_{\fL}$ that induces strong preservation

3143: exists. For example, this has been proved for the case of

3144: $\ACTL$ by Bustan and Grumberg~\cite{bg03}.

3145: 

3146: 

3147: \subsection{Stuttering Equivalence}

3148: Lamport's criticism \cite{lam83} of the next-time operator $\mathrm{X}$

3149: in $\CTL$/$\CTLS$ is well known. This motivated the study of  temporal

3150: logics $\CTLX$/$\CTLSX$ 

3151: obtained  from $\CTL$/$\CTLS$ by removing the next-time operator and this led to

3152: study notions of behavioural \emph{stuttering}-based equivalences

3153: \cite{bcg88,dnv95,gv90}. We are interested here in

3154: \emph{divergence blind stuttering} (dbs for short) equivalence. 

3155: Let $\cK = (\Sigma ,\sra ,\ell)$ be a Kripke structure over a set

3156: $\AP$ of atoms. 

3157: A

3158: relation $R \subseteq \Sigma \times \Sigma $ is a divergence blind 

3159: stuttering relation on $\cK$ if for any

3160: $s,s'\in \Sigma $ such that $sR s'$: 

3161: \begin{itemize}

3162: \item[{\rm (1)}] $\ell(s) =\ell (s')$;

3163: \item[{\rm (2)}] If

3164: $\ok{s\sra t}$ 

3165: then there exist $t_0,...,t_k\in \Sigma$, with $k\geq 0$, such that: (i)

3166: $t_0=s'$; (ii)  for all $i\in [0,k-1]$, $\ok{t_i

3167: \sra  t_{i+i}}$ and $s R t_i$; 

3168: (iii) $t R t_k$;

3169: \item[{\rm (3)}] $s'Rs$, i.e.\ $R$ is symmetric. 

3170: \end{itemize}

3171: Observe that condition~(2) allows the case $k=0$

3172: and this simply boils down to requiring that $t R s'$.  

3173: Since the empty

3174: relation is a dbs relation and dbs relations are closed under union,

3175: it turns out that the 

3176: largest dbs  relation relation exists. It turns out that this largest

3177: dbs relation  is an equivalence relation called dbs equivalence  and is 

3178: denoted by $\sim_{\mathrm{dbs}}$ while $P_{\mathrm{dbs}}\in \Part(\Sigma)$ denotes

3179: the corresponding partition.  In particular, a partition $P\in \Part(\Sigma)$ is a

3180: dbs relation on $\cK$ when 

3181: when $P\preceq P_{\mathrm{dbs}}$.

3182: 

3183: 

3184: De Nicola and Vaandrager \cite[Theorem~3.2.5]{dnv95} showed that for

3185: finite Kripke structures and for an interpretation of 

3186: universal/existential path quantifiers over all the, possibly finite,

3187: prefixes, dbs equivalence coincides with 

3188: the state equivalence induced from the language $\CTLX$

3189: (this also holds for $\CTLSX$), that is $P_{\mathrm{dbs}} =

3190: P_{\CTLX}$. This is not true with the standard interpretation of path

3191: quantifiers over infinite paths, since this requires a

3192: divergence sensitive notion of stuttering (see the details in

3193: \cite{dnv95}). Groote and Vaandrager \cite{gv90} presented a partition

3194: refinement algorithm that computes the partition $P_{\mathrm{dbs}}$

3195: in $O(|\Sigma| |\sra|)$-time.

3196: 

3197: 

3198: We provide a characterization of divergence blind stuttering equivalence

3199: as the state equivalence induced by 

3200: the following language $\fL_2$ that includes propositional logic and 

3201: the existential until operator $\mathrm{EU}$, where the interpretation

3202: of the existential path quantifier is standard, i.e.\ over infinite paths:

3203: $$\fL_2 \ni \varphi ::= 

3204: ~p ~|~ \varphi_1 \wedge \varphi_2 ~|~ \neg \varphi ~|~ 

3205: \mathrm{EU}(\varphi_1,\varphi_2)

3206: $$  

3207: %

3208: %

3209: Since the transition relation $\sra$ is assumed to be total, 

3210: let us recall that the standard semantics $\beu:\wp(\Sigma)^2\ra

3211: \wp(\Sigma)$ of the existential until operator

3212: is as

3213: follows:

3214: \begin{tabbing} 

3215: ~~~~$\beu(S_1,S_2) = S_2 \cup \{s\in S_1 ~|~$\=$\exists s_0,...,s_n \in

3216: \Sigma, \text{ with } n\geq 0, \text{ such that~(i)~} s_0=s,$\\

3217: \>${\rm ~(ii)~} \forall i\in [0,n-1].\,

3218: s_i\in S_1 \text{ and } s_i  \sra  s_{i+1},$

3219: ${\rm ~(iii)~} s_n\in S_2\}$.

3220: \end{tabbing}

3221: \noindent

3222: The following result characterizes

3223: a dbs partition $P$ in terms of forward completeness for the

3224: corresponding partitioning abstract domain $\adp(P)$. 

3225: 

3226: \begin{theorem}\label{chardbs}

3227: Let $P\in \Part(\Sigma)$. Then, $P\in\Part(\Sigma)$ is a dbs partition on $\cK$ iff 

3228: $\adp(P)$ is forward complete for $\{ \boldsymbol{p}~|~ p\in \AP\}

3229: \cup \{ \beu\}$. 

3230: \end{theorem}

3231: \begin{proof}

3232: As already shown in the proof of Theorem~\ref{thbis}, it

3233: turns out that $P\preceq P_\ell$ iff $\adp(P)$ is forward complete for

3234: $\{\boldsymbol{p} \subseteq \Sigma~|~ p\in \AP\}$. 

3235: Thus, it remains to

3236: show $P\in \Part(\Sigma)$ satisfies condition~(2) of the definition of

3237: dbs relation iff

3238: $\adp(P)$ is forward complete for $\beu$. 

3239:     Let us first observe that $P\in\Part(\Sigma)$ satisfies this 

3240: condition~(2) 

3241:   iff for any $B_1,B_2\in P$, $\beu(B_1,B_2) = B_1 \cup B_2$.\\

3242: $(\Rightarrow)$ 

3243:    If $B_1=B_2$ then $\beu(B_1,B_1)=B_1$. 

3244:   Otherwise, assume that $B_1\neq B_2$. If $B_2 \subsetneq

3245: \beu(B_1,B_2) \subseteq B_1 \cup B_2$ then there exists $s\in

3246: \beu(B_1,B_2)$ such that $s\in B_1$. Thus, if $s'\in B_1$ then, by

3247: condition~(2), $s'\in \beu(B_1,B_2)$. This implies that $\beu(B_1,B_2)

3248: = B_1 \cup B_2$.    \\

3249:  %

3250:  $(\Leftarrow)$

3251:   Let $B\in P$, $s,s'\in B$ and $s \sra  t$. If $t\in B$

3252: then condition~(2) is satisfied. Otherwise, $t\in B'$, for some $B'\in

3253: P$, with $B\neq B'$. Thus, $s\in \beu(B,B')$ and therefore

3254: $\beu(B,B')=B\cup B'$. This means that condition~(2) is

3255: satisfied for $P$. \\

3256: %

3257:   To complete the proof it is now sufficient to show that if, 

3258:  for any $B_1,B_2\in P$, $\beu(B_1,B_2)= B_1 \cup B_2$ then

3259: $\adp(P)$ is forward complete for $\beu$, i.e., for any

3260: $\{B_i\}_{i\in I},\{B_j\}_{j\in J} \subseteq P$, $\beu(\cup_i B_i,

3261: \cup_j B_j) = \cup_k B_k$, for some $\{B_k\}_{k\in K}\subseteq P$. 

3262: The function $\beu$ is additive in its second argument, thus we only need to show

3263: that, for any $B\in P$, 

3264: $\beu(\cup_i B_i,B)=\cup_k B_k$, namely if $s\in \beu(\cup_i

3265: B_i,B)$ and $s\in B'$, for some $B'\in P$, then $B'\subseteq

3266: \beu(\cup_i B_i, B)$. 

3267:   If $s\in\beu(\cup_i B_i, B)$ and $s\in B'$, for some $B'\in \{B_i\}_i$, then there exist

3268:   $n\geq 0$ and   $s_0,...,s_n \in

3269: \Sigma $ such that $s_0=s$, $\forall

3270: j\in [0,n-1]. s_j\in \cup_i B_i$ and  $s_j  \sra s_{j+1}$, and   $s_n\in B$. 

3271:   Let us prove by induction on $n\in\mathbb{N}$ that if $s'\in B'$ then 

3272:   $s'\in\beu(\cup_i B_i, B)$.\\[5pt]

3273: ($n=0$):

3274:     In this case $s\in \cup_i B_i$ and $s\in B=B'$. Hence, for some

3275: $k$, $s\in B_k=B=B'$ and therefore $s\in \beu(B,B)$. By hypothesis,

3276: $\beu(B,B)=B$. Moreover, $\beu$ is monotone on its first component and

3277: therefore $B'=B=\beu(B,B)\subseteq \beu(\cup_i B_i,B)$. \\[5pt]

3278: ($n+1$):

3279:     Suppose that 

3280: there exist

3281:   $s_0,...,s_{n+1} \in

3282: \Sigma $ such that $s_0=s$, $\forall

3283: j\in [0,n]. s_j\in \cup_i B_i$ and  $s_j  \sra 

3284: s_{j+1}$, and   $s_{n+1}\in B$. Let $s_n \in B_k$, for some $B_k\in

3285: \{B_i\}_{i\in I}$. Then, $s\in \beu(\cup_i B_i,B_k)$ and $s=s_0 \sra

3286: s_1 \sra  ... \sra 

3287: s_n$. Since this finite path has length $n$, 

3288: by inductive hypothesis, $s'\in \beu(\cup_i B_i,B_k)$. Hence,

3289: there exist $r_0,...,r_m \in \Sigma $, with $m\geq 0$, such that 

3290: $s'=r_0$, $\forall

3291: j\in [0,m-1]. r_j\in \cup_i B_i$ and  $r_j  \sra 

3292: r_{j+1}$, and   $r_{m}\in B_k$. Moreover, since $s_n \sra 

3293: s_{n+1}$, we have that $s_n\in \beu(B_k,B)$. By

3294: hypothesis, $\beu(B_k,B)=B_k\cup B$, and therefore $r_m\in

3295: \beu(B_k,B)$. Thus, there exist $q_0,...,q_l \in \Sigma $, with $l\geq 0$, such that 

3296: $r_m=q_0$, $\forall

3297: j\in [0,l-1]. q_j\in B_k$ and  $q_j  \sra 

3298: q_{j+1}$, and   $q_{l}\in B$. We have thus found the following finite path: 

3299: $s'=r_0 \sra  r_1 \sra 

3300: ... \sra  r_m = q_0 \sra  q_1 \sra  ... \sra  q_l$, where all the

3301: states in the sequence but the last one $q_l$  belong to $\cup_i B_i$,

3302: while $q_l\in B$. This means that $s'\in \beu(\cup_i B_i,B)$.  

3303: \end{proof}

3304: 

3305: 

3306: As a consequence, we obtain a characterization of dbs equivalence as

3307: the state equivalence induced by the standard interpretation of the

3308: language $\fL_2$.

3309: 

3310: 

3311: \begin{corollary}\label{coro7}

3312: Let $\Sigma$ be finite. Then, $P_{\mathrm{dbs}}= P_{\fL_2}$.

3313: \end{corollary}

3314: \begin{proof}

3315: By definition, $P_{\mathrm{dbs}} = 

3316: \curlyvee_{\Part(\Sigma)} \{P\in

3317: \Part(\Sigma)~|~ P$ is a dbs relation on  $\cK \}$. 

3318: By Theorem~\ref{chardbs}, $P_{\mathrm{dbs}} = 

3319: \curlyvee_{\Part(\Sigma)} \{P\in

3320: \Part(\Sigma)~|~ \adp(P)$ is complete for  

3321: $\{ \boldsymbol{p}~|~ p\in \AP\}

3322: \cup \{ \beu\}\}$. 

3323: By Theorem~\ref{teoGI}, $\adp$ is co-additive on

3324: $\Part(\Sigma)_\succeq$, that is $\adp$ preserves lub's in

3325: $\Part(\Sigma)_\preceq$. Hence, $\adp(P_{\mathrm{dbs}}) = 

3326: \sqcup_{\Abs(\wp(\Sigma))}  \{\adp(P)\in

3327: \Abs(\wp(\Sigma))~|~ P\in \Part(\Sigma),\, 

3328: \adp(P)$ is complete for  $\{ \boldsymbol{p}~|~ p\in \AP\}

3329: \cup \{ \beu\}\}$. By Theorem~\ref{teoGI}, 

3330: $\Absp(\wp(\Sigma)) = \{\adp(P)~|~P\in \Part(\Sigma)\}$ so that

3331:  $\adp(P_{\mathrm{dbs}}) = 

3332: \sqcup_{\Abs(\wp(\Sigma))}  \{A \in

3333: \Absp(\wp(\Sigma))~|~ 

3334: A$  is complete for  $\{ \boldsymbol{p}~|~ p\in \AP\}

3335: \cup \{ \beu\}\}$. By Corollary~\ref{coropart}, $A \in

3336: \Absp(\wp(\Sigma))$ iff $A$ is forward complete for $\complement$,

3337: so that $\adp(P_{\mathrm{dbs}}) = 

3338: \sqcup_{\Abs(\wp(\Sigma))}  \{A \in

3339: \Abs(\wp(\Sigma))~|~ 

3340: A$ is complete for  $\{ \boldsymbol{p}~|~ p\in \AP\}

3341: \cup \{\complement, \beu\}\}$. Then, we note that $A$ is forward

3342: complete for $\{ \boldsymbol{p}~|~ p\in \AP\}$ iff $A \sqsubseteq \cM(\{

3343: \boldsymbol{p}~|~ p\in \AP\})$. Hence, 

3344:  $\adp(P_{\mathrm{dbs}}) = 

3345: \sqcup_{\Abs(\wp(\Sigma))}  \{A \in

3346: \Abs(\wp(\Sigma))~|~ A \sqsubseteq \cM(\{ \boldsymbol{p}~|~ p\in \AP\}), \, 

3347: A$ is complete for 

3348: $\{\complement, \beu\}\} = \sS_{\{\complement, \beu\}} (\cM(\{

3349: \boldsymbol{p}~|~ p\in \AP\}))$. Finally, since $\Sigma$ is finite and

3350: therefore closure under infinite conjunction boils down to closure

3351: under finite conjunction,  by Corollary~\ref{strai}, 

3352: $\sS_{\{\complement, \beu\}} (\cM(\{

3353: \boldsymbol{p}~|~ p\in \AP\}))=\AD_{\fL_2}$. Thus,  by Proposition~\ref{onetwo}~(1),

3354: $\adp(P_{\mathrm{dbs}}) = \AD_{\fL_2}$, so that 

3355: $P_{\mathrm{dbs}} = \pr(\adp( P_{\mathrm{dbs}})) = \pr(\AD_{\fL_2}) =

3356: P_{\fL_2}$.   

3357: \end{proof}

3358: 

3359: 

3360: As a consequence of Corollary~\ref{spcb}, the Groote-Vaandrager

3361: algorithm~\cite{gv90} $\GV$ for computing dsb equivalence on a finite

3362: Kripke structure  can be characterized as a complete shell

3363: refinement as follows:

3364: $$\GV(P) = \pr (\sS_{\{\complement , \beu\}}

3365: (\cM(P))).$$

3366: 

3367: \subsection{Simulation Preorder and Equivalence}\label{simeq}

3368: Simulations are possibly nonsymmetric bisimulations, that is

3369: $R\subseteq \Sigma \times \Sigma $ is a

3370: simulation on a Kripke structure $\cK=(\Sigma,\sra,\ell)$ 

3371: if for any $s,s'\in \Sigma $ such that $s R s'$: 

3372: \begin{itemize}

3373: \item[{\rm (1)}] $\ell(s') \subseteq \ell (s)$; 

3374: \item[{\rm (2)}] For

3375: any $t\in \Sigma $ such that $\ok{s \sra t}$, there exists $t'\in \Sigma $

3376: such that $\ok{s'\sra t'}$

3377: and $t R t'$.

3378: \end{itemize}

3379: The empty

3380: relation is a simulation and simulation relations are closed under

3381: union, so that the 

3382: largest simulation relation exists. It turns out that the largest

3383: simulation is a preorder relation called similarity preorder and

3384: denoted by $R_{\mathrm{sim}}\in \PreOrd(\Sigma)$. 

3385: Therefore,  a preorder relation $R\in \PreOrd(\Sigma)$ is a simulation on $\cK$

3386: when $R \subseteq  R_{\mathrm{sim}}$. Simulation equivalence 

3387: $\sim_{\mathrm{simeq}}\,\subseteq

3388: \Sigma \times \Sigma $ is the symmetric closure of $R_{\mathrm{sim}}$:

3389: $s\sim_{\mathrm{simeq}}s'$ iff there exist two simulation

3390: relations $R_1$ and $R_2$ such that $s R_1 s'$ and $s' R_2s$. 

3391: $P_{\mathrm{simeq}}\in \Part(\Sigma)$ denotes

3392: the partition corresponding to $\sim_{\mathrm{simeq}}$. 

3393: 

3394: A number of algorithms for computing simulation equivalence

3395: have been proposed

3396: \cite{bp95,bg03,cps93,gpp03,hhk95} and some of them like

3397: \cite{bp95,hhk95} first compute the similarity preorder and then

3398: from it they obtain simulation equivalence.    The problem of 

3399: computing simulation equivalence is important in model checking

3400: because, as recalled in Section~\ref{amc}, simulation equivalence

3401: strongly preserves $\ACTL$ so that

3402: $P_{\mathrm{simeq}} = P_\ACTL$  (see \cite[Section~4]{gl94}).

3403: Recall that $\ACTL$ is 

3404: obtained by restricting $\CTL$, as defined in Section~\ref{cs}, to

3405: universal quantifiers and by allowing negation on atomic propositions only:

3406: $$

3407: \ACTL \ni \varphi ::=  p ~|~ \neg p ~|~ \varphi_1 \wedge \varphi_2 ~|~

3408: \varphi_1 \vee \varphi_2 ~|~ \mathrm{AX}\varphi 

3409: ~|~ \mathrm{AU}(\varphi_1,\varphi_2) ~|~

3410: \mathrm{AR}(\varphi_1,\varphi_2)$$

3411: %

3412: 

3413: It turns out that the most abstract s.p.\ domain for $\ACTL$

3414: can be obtained as the most abstract s.p.\ domain for 

3415: the following sublanguage $\fL_3$:

3416: $$\fL_3 \ni \varphi ::= p ~|~ \neg p ~|~ 

3417: \varphi_1 \wedge \varphi_2 ~|~ \varphi_1 \vee \varphi_2 ~|~

3418: \mathrm{AX}\varphi $$

3419: %

3420: \begin{lemma}\label{lem2}

3421: Let $\cK$ be finitely branching. Then, $\AD_{\ACTL} = \AD_{\fL_3}$.

3422: \end{lemma}

3423: \begin{proof}

3424: Let $\boldsymbol{Op}_{\ACTL} =  

3425: \{\cap,\cup,  \mathbf{AX}, 

3426: \mathbf{AU}, \mathbf{AR} \}$ be the

3427: set of standard interpretations of the operators of $\ACTL$ on $\cK$,

3428: so that $\mathbf{AX}=\pret_\sra$.  

3429: Analogously to the proof of Lemma~\ref{ctlequiv}, as a consequence of

3430: the least/greatest fixpoint characterizations of $\mathbf{AU}$ and

3431: $\mathbf{AR}$, it turns out that

3432: for any $A \in \Abs(\wp(\Sigma))$, $A$ is forward complete for  

3433: $\boldsymbol{Op}_{\ACTL}$ iff $A$ is forward complete for $\{\cup,

3434: \pret_\sra\}$. Thus, by Lemma~\ref{shellequiv}, $\sS_{\{\cup ,

3435: \pret_\sra\}} = \sS_{\boldsymbol{Op}_{\ACTL}}$, so that, by

3436: Corollary~\ref{strai}, $\AD_{\fL_3} = \AD_\ACTL$. 

3437: \end{proof}

3438: 

3439: Thus, by Proposition~\ref{onetwo}~(1), 

3440: $P_\ACTL = \ok{\pr(\AD_{\ACTL})} =

3441: \pr(\AD_{\fL_3}) = P_{\fL_3}$, so that $P_{\mathrm{simeq}} =

3442: P_{\fL_3}$.  As a further consequence, by Corollary~\ref{spcb}, 

3443:  any algorithm $\Algsimeq$ that computes simulation equivalence can be

3444: viewed  as a partitioning abstraction of the

3445: $\{\cup,\pret_\sra\}$-complete shell refinement: 

3446: 

3447: $$\Algsimeq(P) = \pr (\sS_{\{\cup , \pre_\sra\}}

3448: (\cM(P))).$$

3449: 

3450: An instantiation of the generalized Paige-Tarjan-like procedure in \cite{rt05} for

3451: the complete shell $\sS_{\{\cup , \pre_\sra\}}$ allows to design a new efficient

3452: abstract intepretation-based 

3453: algorithm for computing simulation equivalence \cite{rt06} whose space and

3454: time complexity is comparable with that of state-of-the-art

3455: algorithms  like \cite{bg03,gpp03}.

3456: 

3457: 

3458: 

3459: \subsubsection{Preorders as Abstract Domains}

3460: 

3461: Simulations give rise to preorders rather than equivalences like in

3462: the case of bisimulations and dbs relations. Thus, in

3463: order to characterize simulation for preorders as forward

3464: completeness for abstract domains we need to view preorders as

3465: abstract domains. This can be obtained by generalizing the abstraction

3466: in Section~\ref{paa} from partitions to preorders. 

3467: 

3468: Let $R\in \PreOrd(\Sigma)$ and for any $x\in \Sigma$ let us define 

3469: $R^{\pre} \ud \{ \pre_R(\{x\})

3470: \subseteq \Sigma~|~ x\in \Sigma\}$. The preorder $R$ gives rise to

3471: an abstract domain $\wp(R^{\pre})_\subseteq$ which is related to $\wp(\Sigma)_\subseteq$

3472: through the following abstraction and concretization maps: 

3473: $$\alpha_R(S)\ud\{\pre_R(\{x\}) \subseteq \Sigma~|~ x\in S\}

3474: ~~~~~~~

3475: \gamma_R(\mathcal{X})\ud \cup_{X\in \mathcal{X}} X.$$

3476: It is easy to check that from the hypothesis that $R$ is a

3477: preorder it follows that $(\alpha_R,

3478: \wp(\Sigma)_\subseteq, \wp(R^{\pre})_\subseteq,\gamma_R)$ is indeed a

3479: GI. 

3480: Hence, any $R\in \PreOrd(\Sigma)$ induces an abstract domain

3481: denoted by

3482: $\add(R) \in \Abs(\wp(\Sigma))$. Also, note that $\gamma_R\circ

3483: \alpha_R = \pre_R$, namely $\pre_R$ is the closure associated to

3484: $\add(R)$. 

3485: The notation $\add$

3486: comes from the fact that an abstract domain $A$ is equivalent to some

3487: $\add(R)$ if and only if

3488: $A$

3489: is disjunctive. 

3490: \begin{lemma}\label{lemmadisj}

3491: $\{\add(R)\in \Abs(\wp(\Sigma))~|~ R\in

3492: \PreOrd(\Sigma)\}=\{A\in \Abs(\wp(\Sigma))~|~ A~ \text{{\rm is disjunctive}}\}$. 

3493: \end{lemma}

3494: \begin{proof}

3495: Observe that $\gamma_R$ is trivially additive, so that any $\add(R)$

3496: is disjunctive. On the other hand, let $A\in \Abs(\wp(\Sigma))$ be

3497: disjunctive and consider the relation $R^A = \{(x,y) ~|~ \alpha(\{x\})

3498: \leq_A \alpha(\{y\})\}$ which is trivially a preorder. Thus,

3499: $\add(R^A)$ is disjunctive so that in order to conclude that $\add(R^A)$

3500: is equivalent to $A$ it is enough to observe that for any $y\in \Sigma$,

3501: $\pre_{R^A}(\{y\}) = \gamma(\alpha(\{y\}))$: this is true because

3502: $\gamma(\alpha(\{y\})) = \{x\in \Sigma~|~ \alpha(\{x\})\leq_A

3503: \alpha(\{y\})\}=\pre_{R^A}(\{y\})$. 

3504: \end{proof}

3505: 

3506: Let us observe that $\add$ indeed generalizes $\adp$ from partitions

3507: to preorders because for any $P\in \Part(\Sigma)$, $\adp(P)=\add(R)$:

3508: this is a simple consequence of the fact that for a partition $P$

3509: viewed as an equivalence relation and

3510: for $x\in \Sigma$,

3511: $P_x$ is exactly a block of $P$ so that

3512: $\alpha_P(S)=\{\pre_P(\{x\})~|~ x\in S\}$.  

3513: On the other hand, an abstract domain $A\in \Abs(\wp(\Sigma))$ induces

3514: a preorder relation $\preord(A)\in \PreOrd(\Sigma)$ as follows:

3515: $$(x,y)\in \preord(A)  \text{~~~iff~~~} \alpha(\{x\}) \leq_A \alpha(\{y\}).$$

3516: It turns out that the maps $\add$ and $\preord$ allows to view the lattice of

3517: preorder relations as an abstraction of the lattice of abstract

3518: domains. 

3519: \begin{theorem}

3520: $(\preord,\Abs(\wp(\Sigma))_\sqsupseteq,\PreOrd(\Sigma)_\supseteq,

3521: \add)$. 

3522: \end{theorem}

3523: \begin{proof}

3524: Let $A \in \Abs(\wp(\Sigma))$ and $R\in

3525: \PreOrd(\Sigma)$. Let us prove that  

3526: $R\subseteq \preord(A) \; \Lra\; \add(R) \sqsubseteq

3527: \gamma\circ \alpha$. \\

3528: $(\Rightarrow)$~Let $S\subseteq \Sigma$ and let us show that

3529: $\add(R)(S)=\pre_R(S)\subseteq \gamma(\alpha(S))$. If $x\in

3530: \pre_R(S)$ then $xRy$ for some $y\in S$, so that $(x,y) \in

3531: \preord(A)$, i.e.\ $\alpha(\{x\}) \leq_A \alpha(\{y\})$. Thus, by

3532: applying $\gamma$, $x\in \gamma(\alpha(\{x\})) \subseteq 

3533: \gamma(\alpha (\{y\}))\subseteq \gamma(\alpha(S))$. \\

3534: $(\Leftarrow)$~Let $(x,y) \in R$ and let us show that $\alpha(\{x\})

3535: \leq \alpha(\{y\})$. Note that $x\in \pre_R(\{y\}) =\add(R)(\{y\})

3536: \subseteq \gamma(\alpha(\{y\}))$, so that $\alpha(\{x\}) \leq_A

3537: \alpha(\{y\})$, namely $(x,y)\in \preord(A)$. 

3538: \end{proof}

3539: 

3540: Let us remark that $\mathbb{D}\ud \add \circ \preord$ is a lower closure operator on

3541: $\tuple{\Abs(\wp(\Sigma)),\sqsubseteq}$ and that, by

3542: Lemma~\ref{lemmadisj}, 

3543: for any $A \in

3544: \Abs(\wp(\Sigma))$, $A$ is disjunctive iff $\mathbb{D}(A)=A$. 

3545: Hence, $\mathbb{D}$ coincides with the disjunctive-shell refinement,

3546: also known as disjunctive completion \cite{CC79}, namely

3547: $\mathbb{D}(A)$ is the most abstract disjunctive refinement of $A$.

3548: 

3549: 

3550: We can now provide a characterization of simulation preorders in terms of forward

3551: completeness. 

3552: \begin{theorem}

3553: Let $R\in \PreOrd(\Sigma)$. Then, $R$ is a simulation on $\cK$ iff

3554: $\add(R)$ is forward complete for $\{\boldsymbol{p}~|~p\in \AP\}\cup \{\pret_\sra\}$.

3555: \end{theorem}

3556: \begin{proof}

3557: Recall that $\pre_R$ is the closure associated to $\add(R)$. We first

3558: observe that 

3559: $(sRs' \: \Ra\: \ell(s') \subseteq \ell(s))$ iff $\pre_R$ 

3560: is forward complete for  $\boldsymbol{\AP}$. On the one hand, if

3561: $\boldsymbol{p}\in \boldsymbol{\AP}$ and $s\in \pre_R(\boldsymbol{p})$

3562: then $sR s'$ for some $s' \in \boldsymbol{p}$, so that, from

3563: $\ell(s')\subseteq \ell(s)$, we obtain $s\in \boldsymbol{p}$, and

3564: therefore $\pre_R(\boldsymbol{p}) =\boldsymbol{p}$. On the other hand,

3565: if $sRs'$ and $s'\in \boldsymbol{p}$, for some $\boldsymbol{p}\in

3566: \boldsymbol{\AP}$, then $s'\in \boldsymbol{p}=\pre_R(\boldsymbol{p})$

3567: so that $\pre_R(\{s'\})\subseteq \pre_R(\pre_R (\boldsymbol{p}) )

3568: = \pre_R(\boldsymbol{p}) = \boldsymbol{p}$ and therefore from $s\in

3569: \pre_R(\{s'\})$ we obtain $s\in \boldsymbol{p}$. \\

3570: Thus, it remains to show that $R$ satisfies condition (2) of the

3571: definition of simulation iff $\pre_R$ is forward complete for

3572: $\pre_\sra$. \\

3573: $(\Ra)$ We prove that for any $S$, $\pre_R (\pret_\sra

3574: (\pre_R (S))) \subseteq \pret_\sra (\pre_R (S))$. Let $x\in  \pre_R (\pret_\sra

3575: (\pre_R (S)))$ so that there exists some $y\in \pret_\sra (\pre_R

3576: (S))$ such that $xRy$. If $x\sra x'$, for some $x'$, then, by

3577: simulation, there exists some $y'$ such that $y\sra y'$ and $x'R

3578: y'$. Hence, $y'\in \pre_R (S)$ and this together with $x'R y'$, as $R$

3579: is transitive, gives $x'\in \pre_R(S)$. Therefore, $x\in \pret_\sra

3580: (\pre_R(S))$. 

3581: %

3582: \\

3583: $(\Leftarrow)$  Observe that in order to show that $R$ is a simulation it is

3584: enough to show that if $xR y$ then $x\in \pret_\sra (\pre_R (\post_\sra

3585: (\{y\})))$. The following implications hold, where

3586: $\post_\sra (\{y\}) \subseteq \pre_R (\post_\sra (\{y\}))$ holds

3587: because $\pre_R$ is a uco:

3588: \begin{align*}

3589: \post_\sra (\{y\}) \subseteq

3590: \pre_R (\post_\sra (\{y\})) & ~~\Ra &

3591: \text{~~~[as $\pret_\sra$ is monotone]}\\

3592:  \pret_\sra(\post_\sra (\{y\})) \subseteq

3593: \pret_\sra (\pre_R (\post_\sra (\{y\}))) & ~~\Ra &

3594: \text{~~~[as $y\in \pret_\sra(\post_\sra(\{y\}))$]} \\

3595: \{y\} \subseteq \pret_\sra (\pre_R (\post_\sra (\{y\}))) & ~~\Ra &

3596: \text{~~~[as $\pre_R$ is monotone]} \\

3597: \pre_R(\{y\}) \subseteq \pre_R(\pret_\sra (\pre_R (\post_\sra

3598: (\{y\})))) & ~~\Ra &

3599: \text{~~~[as $\pre_R$ is forward complete for $\pret_\sra$]} \\

3600: \pre_R(\{y\}) \subseteq \pret_\sra (\pre_R (\post_\sra (\{y\}))) & ~~\Ra

3601: &

3602: \text{~~~[as $x\in \pre_R(\{y\})$]}\\

3603: x \in \pret_\sra (\pre_R (\post_\sra (\{y\}))) & &

3604: \end{align*}

3605: and this closes the proof.

3606: \end{proof}

3607: 

3608: 

3609: 

3610: \section{Related work} 

3611: Loiseaux et al.~\cite{loi95} generalized the standard approach to

3612: abstract model checking to more general abstract models where an

3613: abstraction relation $\sigma

3614: \subseteq \States \times A$  is used instead of a surjective

3615: function $h:\States \ra A$. However,

3616: the results of strong preservation given there (cf.~\cite[Theorems~3

3617: and~4]{loi95}) require the hypothesis that the relation $\sigma$ is

3618: difunctional, i.e.\ $\sigma = \sigma

3619: \sigma^{-1}\sigma$. In this case the

3620: abstraction relation $\sigma$ can indeed be derived from a function, so

3621: that the class of strongly preserving abstract models in Loiseaux et al.'s 

3622: framework is not really

3623: larger than the class of standard partition-based abstract models (see the

3624: detailed discussion by Dams et al.~\cite[Section~8.1]{dgg97}). \\

3625: %

3626: \indent

3627: Giacobazzi and Quintarelli~\cite{GQ01} first noted that

3628: strong preservation is related to

3629: completeness in abstract interpretation  by 

3630: studying the relationship between  complete abstract interpretations and

3631: Clarke et al.'s \cite{cgjlv00,cgjlv03,cjlv02} spurious counterexamples. 

3632: %The stream of

3633: %work by Clarke et al.\ on spurious counterexamples originated from the

3634: %idea of systemically refining abstract models in order to enhance

3635: %their precision. 

3636: Given a formula $\varphi$ of $\ACTL$, a model checker running on a

3637: standard abstract Kripke structure defined over a state partition $P$ may

3638: provide a spurious counterexample $\ok{\pi^\sharp}$ for $\varphi$, 

3639: namely a path of abstract

3640: states, namely blocks of $P$, which does not correspond to a real concrete

3641: counterexample.  

3642: In this case, by exploiting the spurious

3643: counterexample $\ok{\pi^\sharp}$, 

3644: the partition $P$ is refined to $\ok{P'}$ by splitting a

3645: single block of $P$.    As a result, 

3646: this refined partition $\ok{P'}$ does not admit the spurious counterexample

3647: $\ok{\pi^\sharp}$ for $\varphi$ 

3648:   so that $\ok{P'}$ is given as a new refined 

3649: abstract model for $\varphi$ to the model checker.  Giacobazzi and

3650: Quintarelli \cite{GQ01} cast spurious counterexamples for a partition

3651: $P$ as a lack of

3652: (standard) completeness in the abstract interpretation sense for the

3653: corresponding partitioning

3654: abstract domain $\adp(P)$. Then, by applying the results in

3655: \cite{jacm} they put forward a

3656: method for systematically refining abstract domains in order to

3657: eliminate spurious counterexamples. The relationship

3658: between completeness and spurious counterexamples was further studied

3659: in \cite{dp03}, where it is also shown that a 

3660: block splitting operation in 

3661: Paige and Tarjan~\cite{pt87} partition refinement algorithm  can be characterized

3662: in terms of complete abstract interpretations.

3663: More in general, the idea of

3664: systematically enhancing the precision of abstract interpretations by

3665: refining the underlying abstract domains dates back to the early works

3666: by Cousot and Cousot~\cite{CC79}, and evolved to the systematic design

3667: of abstract interpretations by abstract domain refinements

3668: \cite{fgr96,GR97,jacm}.  

3669: 

3670: 

3671: 

3672: \section{Conclusion}

3673: 

3674: This work shows how the abstract interpretation technique

3675: allows to generalize the notion of strong preservation from standard

3676: abstract models specified as abstract Kripke structures to generic

3677: domains in abstract interpretation. For any inductively defined

3678: language $\fL$, it turns out that strong preservation of $\fL$ in

3679: a standard abstract model checking framework based on partitions of

3680: the space state $\Sigma$ becomes a particular instance of the property

3681: of forward completeness of abstract domains w.r.t.\ the semantic

3682: operators of the language $\fL$. In particular, a

3683: generalized abstract model can always be refined through a

3684: fixpoint iteration to the most abstract domain that strongly

3685: preserves $\fL$.  This generalizes in our framework the idea of

3686: partition refinement algorithms that reduce the state space $\Sigma$

3687: in order to obtain a minimal abstract Kripke structure that is

3688: strongly preserving for some temporal language.

3689: 

3690: This work deals with generic temporal languages consisting of

3691: state formulae only. As future work, it would be interesting to

3692: study whether the ideas of our abstract interpretation-based approach

3693: can be applied to linear languages like $\mathrm{LTL}$ consisting of 

3694: formulae that are interpreted as

3695: sets of paths of a Kripke structure. The idea here is to investigate

3696: whether standard strong preservation of $\mathrm{LTL}$ can be

3697: generalized to abstract interpretations of the powerset

3698: of traces and to the corresponding completeness

3699: properties.  Fairness can be also an interesting topic of

3700: investigation, namely to study whether our abstract

3701: interpretation-based framework allows to handle fair semantics and 

3702: fairness constraints \cite{cgp99}. 

3703: 

3704: Finally, let us mention that the results

3705: presented in this paper led to design a generalized Paige-Tarjan

3706: refinement algorithm based on abstract interpretation for computing

3707: most abstract strongly preserving domains~\cite{rt05}. 

3708: As shown in Section~\ref{csp}, a most abstract strongly preserving

3709: domain can be characterized as a greatest

3710: fixpoint computation in $\Abs(\wp(\Sigma))$.

3711: It is shown in \cite{rt05} that the Paige-Tarjan algorithm

3712: \cite{pt87} can be viewed exactly 

3713: as a corresponding abstract greatest fixpoint computation in

3714: $\Part(\Sigma)$. This

3715: leads to an   abstract

3716: interpretation-based Paige-Tarjan-like refinement algorithm  that is parameteric on any

3717: abstract interpretation of the lattice $\Abs(\wp(\Sigma))$ of abstract

3718: domains of $\wp(\Sigma)$ and on any generic inductive language $\fL$. 

3719: 

3720: 

3721: \paragraph*{{\it Acknowledgements.}} We wish to thank Mila Dalla

3722: Preda and Roberto Giacobazzi who contributed to the early stage of

3723: this work. This paper is an extended and revised version of \cite{rt04a}.

3724: This work was partially supported by the FIRB Project

3725: ``Abstract interpretation and model checking for the verification of

3726: embedded systems'' and by the COFIN2004

3727: Project ``AIDA: Abstract Interpretation Design and Applications''.

3728: 

3729: {\small  

3730: \begin{thebibliography}{99}

3731: 

3732: \bibitem{ap86}

3733: K.R.~Apt and G.D.~Plotkin.

3734: \newblock Countable nondeterminism and random assignment.

3735: \newblock \emph{J.\ ACM}, 33(4):724--767, 1986.

3736: 

3737: \bibitem{bp95}

3738: B.~Bloom and R.~Paige. 

3739: \newblock Transformational design and implementation of a new

3740: efficient solution to the ready simulation problem.

3741: \newblock \emph{Sci.\ Comp.\ Program.}, 24(3):189--220, 1995.

3742: 

3743: \bibitem{bfh90}

3744: A.~Bouajjani, J.-C.~Fernandez and N.~Halbwachs. 

3745: \newblock Minimal model generation. 

3746: \newblock  In \emph{Proc.\ of the 2nd Internat.\ Conf.\ on Computer

3747: Aided Verification (CAV'90)}, LNCS~531, pp.~197--203, Springer, 1990.

3748: 

3749: \bibitem{bcg88}

3750: M.C.~Browne, E.M.\ Clarke and O.~Grumberg.

3751: \newblock Characterizing finite {K}ripke structures in propositional

3752: temporal logic.

3753: \newblock \emph{Theoret.\ Comp.\ Sci.}, 59:115--131, 1988.

3754: 

3755: \bibitem{bg03}

3756: D.~Bustan and O.~Grumberg.

3757: \newblock Simulation-based minimization.

3758: \newblock \emph{ACM Trans.\ Comput.\ Log.},

3759: 4(2):181--204, 2003.

3760: 

3761: \bibitem{cgjlv00}

3762: E.M.~Clarke, O.~Grumberg,  S.~Jha, Y.~Lu and H.~Veith.

3763: \newblock Counterexample-guided abstraction refinement.

3764: \newblock In \emph{Proc.\ of the 12th Internat.\ Conf.\ on Computer

3765: Aided Verification (CAV'00)},  LNCS 1855, pp.~154--169, Springer, 2000.

3766: 

3767: \bibitem{cgjlv03}

3768: E.M.~Clarke, O.~Grumberg,  S.~Jha, Y.~Lu and H.~Veith.

3769: \newblock Counterexample-guided abstraction refinement for symbolic

3770: model checking.

3771: \newblock \emph{J.\ ACM}, 50(5):752--794, 2003.

3772: 

3773: \bibitem{cjlv02}

3774: E.M.~Clarke, S.~Jha, Y.~Lu and H.~Veith.

3775: \newblock Tree-like counterexamples in model checking.

3776: \newblock In \emph{Proc.\ of the 

3777: 17th IEEE Symp.\ on Logic in Computer Science (LICS'02)}, 

3778: pp.~19--29, IEEE Press, 2002.

3779: 

3780: 

3781: \bibitem{cgl94}

3782: E.M.~Clarke, O.~Grumberg and D.~Long.

3783: \newblock Model checking and abstraction.

3784: \newblock \emph{ACM Trans.\ Program.\ Lang.\ Syst.}, 16(5):1512--1542, 1994.

3785: 

3786: \bibitem{cgp99}

3787: E.M.~Clarke, O.~Grumberg and D.A.~Peled.

3788: \newblock \emph{Model checking}.

3789: \newblock The {M}{I}{T} Press, 1999.

3790: 

3791: 

3792: %\bibitem{clarke02}

3793: %E.M.~Clarke, S.~Jha, Y.~Lu, and H.~Veith.

3794: %\newblock Tree-like counterexamples in model checking.

3795: %\newblock In \emph{Proc.\ of the 17th IEEE Symp.\  on Logic in Computer

3796: %Science (LICS'02)},  pp.~19--29, IEEE Computer Society, 2002.

3797: 

3798: \bibitem{cpy95}

3799: R.~Cleaveland,  S.P.~Iyer, D.~Yankelevich.

3800: \newblock  Optimality in abstractions of model checking. 

3801: \newblock In \emph{Proc.\ 2nd Intern.\ Static Analysis

3802: Symposium (SAS'95)}, LNCS~983,

3803: pp.~51--63, Springer, 1995.

3804: 

3805: \bibitem{cps93}

3806: R.~Cleaveland, J.~Parrow and B.~Steffen.

3807: \newblock The Concurrency Workbench: a semantics based tool for the

3808: verification of concurrent systems. 

3809: \newblock \emph{ACM Trans.\ Program.\ Lang.\ Syst.}, 15(1):36--72, 1993.

3810: 

3811: 

3812: 

3813: \bibitem{CC77}

3814: P.~Cousot and R.~Cousot.

3815: \newblock Abstract interpretation: a unified lattice model for static analysis

3816:   of programs by construction or approximation of fixpoints.

3817: \newblock In \emph{Proc.\ 4th ACM POPL}, pp.~238--252, 1977.

3818: 

3819: \bibitem{CC79}

3820: P.~Cousot and R.~Cousot.

3821: \newblock Systematic design of program analysis frameworks.

3822: \newblock In \emph{Proc.\ 6th ACM POPL}, pp.~269--282, 1979.

3823: 

3824: \bibitem{CC94}

3825: P.~Cousot and R.~Cousot.

3826: \newblock Higher-order abstract interpretation (and application to

3827: comportment analysis generalizing strictness, termination, projection

3828: and PER analysis of functional languages).

3829: \newblock In \emph{Proc.\ IEEE Int.\ Conf.\ on Computer Languages

3830: (ICCL'94)}, pp.~95--112, 1994.

3831: 

3832: \bibitem{CC99}

3833: P.~Cousot and R.~Cousot.

3834: \newblock Refining model checking by abstract interpretation. 

3835: \newblock \emph{Automated Software Engineering Journal}, 6(1):69--95, 1999.

3836: 

3837: \bibitem{CC00}

3838: P.~Cousot and R.~Cousot.

3839: \newblock Temporal abstract interpretation.

3840: \newblock In \emph{Proc.\ 27th ACM POPL}, pp.~12--25, 2000.

3841: 

3842: \bibitem{dp03}

3843: M.~Dalla Preda. 

3844: \newblock \emph{Completeness and stability in abstract model 

3845: checking}. 

3846: \newblock Laurea Thesis (in Italian), Univ.\ of Verona, Italy, 2003.  

3847: 

3848: 

3849: \bibitem{dams96}

3850: D.~Dams. 

3851: \newblock \emph{Abstract interpretation and partition refinement for

3852: model checking}. 

3853: \newblock Ph.D.\ Thesis, Eindhoven University of Technology, The

3854: Netherlands, 1996.  

3855: 

3856: %\bibitem{dams99}

3857: %D.~Dams. 

3858: %\newblock Flat fragments of  $\CTL$ and $\CTLS$: separating the expressive

3859: %and distinguishing powers. 

3860: %\newblock \textit{Logic J.\ of the IGPL}, 7(1):55--78, 1999.

3861: 

3862: 

3863: \bibitem{dgg97}

3864: D.~Dams, O.~Grumberg and R.~Gerth.

3865: \newblock Abstract interpretation of

3866: reactive systems.

3867: \newblock \emph{ACM Trans.\ Program.\ Lang.\ Syst.}, 16(5):1512--1542, 1997.

3868: 

3869: \bibitem{db83}

3870: J.W.~De Bakker, J.-J.C.~Meyer and J.I.~Zucker.

3871: \newblock On infinite computations in denotational semantics.

3872: \newblock \emph{Theoret.\ Comp.\ Sci.}, 26(1-2):53--82, 1983.

3873: 

3874: 

3875: \bibitem{dnv95}

3876: R.~De Nicola and F.~Vaandrager.

3877: \newblock Three logics for branching bisimulation.

3878: \newblock \emph{J.\ ACM}, 42(2):458--487, 1995

3879: 

3880: \bibitem{dpp04}

3881: A.~Dovier, C.~Piazza and A.~Policriti. 

3882: \newblock An efficient algorithm for computing bisimulation

3883: equivalence. 

3884: \newblock \emph{Theoret.\ Comp.\ Sci.}, 311(1-3):221--256, 2004.

3885: 

3886: 

3887: \bibitem{emss90}

3888: E.A.~Emerson, A.K.~Mok, A.P.~Sistla and J.~Srinivasen.

3889: \newblock Quantitative temporal reasoning.

3890: \newblock In \emph{Proc.\ of the 2nd Internat.\ Conf.\ on Computer

3891: Aided Verification (CAV'90)},  LNCS~531, pp.~136--145, Springer, 1990.

3892: 

3893: 

3894: \bibitem{ec80}

3895: E.A.~Emerson and E.M.~Clarke.

3896: \newblock Characterizing correctness properties of parallel programs

3897: using fixpoints. 

3898: \newblock In \emph{Proc.\ ICALP'80}, 

3899: LNCS~85, pp.~169--181, Springer, 1980.

3900: 

3901: \bibitem{fgr96}

3902: G.~Fil\'e, R.~Giacobazzi and F.~Ranzato.

3903: \newblock A unifying view of abstract domain design.

3904: \newblock \emph{ACM Comput.\ Surv.}, 28(2):333--336, 1996.

3905: 

3906: %\bibitem{gpp02}

3907: %R.~Gentilini, C.~Piazza and A.~Policriti.

3908: %\newblock Simulation as coarsest partition problem.

3909: %\newblock In In \emph{Proc.\ 8th Intern.\ Conf.\ on Tools and Algorithms

3910: %for the Construction and Analysis of Systems (TACAS'02)}, LNCS~2280,

3911: %pp.~415-430,

3912: %Springer, 2002.

3913: 

3914: \bibitem{gpp03}

3915: R.~Gentilini, C.~Piazza and A.~Policriti.

3916: \newblock From bisimulation to simulation: coarsest partition problems.

3917: \newblock \emph{J.\ Automated Reasoning}, 31(1):73-103, 2003. 

3918: 

3919: 

3920: \bibitem{GQ01}

3921: R.~Giacobazzi and E.~Quintarelli.

3922: \newblock Incompleteness, counterexamples and refinements

3923: in abstract model checking.

3924: \newblock In \emph{Proc.\ 8th Intern.\ Static Analysis

3925: Symposium (SAS'01)}, LNCS~2126,

3926: pp.~356--373, Springer, 2001.

3927: 

3928: \bibitem{GR97}

3929: R.~Giacobazzi and F.~Ranzato.

3930: \newblock Refining and compressing abstract domains.

3931: \newblock In \emph{Proc.\ 24th ICALP}, LNCS~1256, pp.~771--781,

3932: Springer, 1997.

3933: 

3934: \bibitem{gr98}

3935: R.~Giacobazzi and F.~Ranzato.

3936: \newblock Optimal domains for disjunctive abstract interpretation. 

3937: \newblock \emph{Sci.\ Comp.\ Program.}, 32:177--210, 1998.

3938: 

3939: \bibitem{jacm}

3940: R.~Giacobazzi, F.~Ranzato and F.~Scozzari.

3941: \newblock Making abstract interpretations complete.

3942: \newblock \emph{J.\ ACM}, 47(2):361--416, 2000.

3943: 

3944: \bibitem{gv90}

3945: J.F.~Groote and F.~Vaandrager.

3946: \newblock An efficient algorithm for branching bisimulation and

3947: stuttering equivalence.

3948: \newblock In \emph{Proc.\ ICALP'90}, 

3949: LNCS~443, pp.~626-638, Springer, 1990.

3950: 

3951: \bibitem{gl94}

3952: O.~Grumberg and D.E.~Long.

3953: \newblock Model checking and modular verification.

3954: \newblock \emph{ACM Trans.\ Program.\ Lang.\ Syst.}, 16(3):843--871, 1994.

3955: 

3956: \bibitem{hm85}

3957: M.~Hennessy and R.~Milner.

3958: \newblock Algebraic laws for nondeterminism and concurrency.

3959: \newblock \emph{J.\ ACM}, 32(1):137--161, 1985.

3960: 

3961: \bibitem{hhk95}

3962: M.R.~Henzinger, T.A.~Henzinger and P.W.~Kopke.

3963: \newblock Computing simulations on finite and infinite graphs.

3964: \newblock In \emph{Proc.\ 36th FOCS}, pp.~453--462, IEEE Press, 1995.

3965: 

3966: \bibitem{hmr05}

3967: T.A.~Henzinger, R.~Maujumdar and J.-F.~Raskin.

3968: \newblock A classification of symbolic transition systems.

3969: \emph{ACM Trans.\ Comput.\ Log.}, 6(1), 2005.

3970: 

3971: \bibitem{lam83}

3972: L.~Lamport. 

3973: \newblock What good is temporal logic?

3974: \newblock In \emph{Information Processing '83}, pp.~657--668,

3975: IFIP North-Holland, 1983.

3976: 

3977: \bibitem{ly92}

3978: D.~Lee and M.~Yannakakis.

3979: \newblock Online minimization of transition systems. 

3980: \newblock In \emph{Proc.\ 24th ACM STOC}, pp.~264--274, 1992.

3981: 

3982: \bibitem{loi95}

3983: C.~Loiseaux, S.~Graf, J.~Sifakis, A.~Bouajjani and S.~Bensalem.

3984: \newblock Property preserving abstractions for the verification of

3985: concurrent systems.

3986: \newblock \emph{Formal Methods in System Design}, 6:1--36, 1995.

3987: 

3988: \bibitem{mas02}

3989: D.~Mass\'e. 

3990: \newblock Semantics for abstract interpretation-based static analyzes

3991: of temporal properties. 

3992: \newblock In \emph{Proc.\ 9th Intern.\ Static Analysis

3993: Symposium (SAS'02)}, LNCS~2477,

3994: pp.~428--443, Springer, 2002.

3995: 

3996: 

3997: \bibitem{mas04}

3998: D.~Mass\'e. 

3999: \newblock Abstract domains for property checking driven analysis of

4000: temporal properties. 

4001: \newblock In \emph{Proc.\ 10th Intern.\ Conf.\ on Algebraic 

4002: Methodology and Software Technology (AMAST'04)}, LNCS~3116,

4003: pp.~349--363, Springer, 2004.

4004: 

4005: \bibitem{pt87}

4006:   R.~Paige and R.E.~Tarjan.

4007:   \newblock Three partition refinement algorithms.

4008:   \newblock \emph{SIAM J.\ Comput.}, 16(6):973--989, 1987

4009: 

4010: \bibitem{RT02}

4011: F.~Ranzato and F.~Tapparo.

4012: \newblock Making abstract model checking strongly preserving.

4013: \newblock In \emph{Proc.\ 9th Intern.\ Static Analysis

4014: Symposium (SAS'02)}, LNCS~2477,

4015: pp.~411--427, Springer, 2002.

4016: 

4017: \bibitem{rt04a}

4018: F.~Ranzato and F.~Tapparo.

4019: \newblock Strong preservation as completeness in abstract interpretation.

4020: \newblock In \emph{Proc.\ 13th European

4021: Symposium on Programming (ESOP'04)}, LNCS.~2986, pp.~18--32, Springer,

4022: 2004. 

4023: 

4024: \bibitem{rt05}

4025: F.~Ranzato and F.~Tapparo.

4026: \newblock An abstract interpretation-based refinement algorithm for

4027: strong preservation. 

4028: \newblock In \emph{Proc.\ 11th Intern.\ Conf.\ on Tools and Algorithms

4029: for the Construction and Analysis of Systems (TACAS'05)}, LNCS~3440, pp.~140--156,

4030: Springer, 2005.

4031: 

4032: 

4033: \bibitem{rt06}

4034: F.~Ranzato and F.~Tapparo.

4035: \newblock An efficient algorithm for computing

4036: simulation equivalence based on abstract interpretation. 

4037: \newblock In preparation, 2006. 

4038: 

4039: 

4040: \bibitem{sch04}

4041: D.A.~Schmidt.

4042: \newblock Closed and 

4043: logical relations for over- and under-approximation of powersets. 

4044: \newblock In \emph{Proc.\ 11th Intern.\ Static Analysis

4045: Symposium (SAS'04)}, LNCS~3148,

4046: pp.~22--37, Springer, 2004.

4047: 

4048: \bibitem{TC01}

4049: L.~Tan and R.~Cleaveland.

4050: \newblock Simulation revisited.

4051: \newblock In In \emph{Proc.\ 7th Intern.\ Conf.\ on Tools and Algorithms

4052: for the Construction and Analysis of Systems (TACAS'01)}, LNCS~2031,

4053: pp.~480-495,

4054: Springer, 2001.

4055: 

4056: 

4057: \bibitem{vg90}

4058: R.J.~van Glabbeek.

4059: \newblock The linear time - branching time spectrum. 

4060: \newblock In \emph{Handbook of Process Algebra}, pp.~3--99, Elsevier, 2001. 

4061: 

4062: \end{thebibliography}

4063: }

4064: 

4065: \end{document}

4066: 

4067: 

4068: 

4069: 

4070: