# TAI-GAN: A Temporally and Anatomically Informed Generative Adversarial
Network for early-to-late frame conversion in dynamic cardiac PET inter-frame
motion correction

Xueqi Guo<EMAIL_ADDRESS>Luyao Shi Xiongchao Chen Qiong Liu Bo Zhou
Huidong Xie Yi-Hwa Liu Richard Palyo Edward J. Miller Albert J. Sinusas
Lawrence Staib Bruce Spottiswoode Chi Liu<EMAIL_ADDRESS>Nicha C. Dvornek
<EMAIL_ADDRESS>Department of Biomedical Engineering, Yale University,
New Haven, CT, USA.  IBM Research, San Jose, CA, USA.  Department of Internal
Medicine, Yale University, New Haven, CT, USA  Yale New Haven Hospital, New
Haven, CT, USA.  Department of Radiology and Biomedical Imaging, Yale School
of Medicine, New Haven, CT, USA  Siemens Medical Solutions USA, Inc.,
Knoxville, TN, USA.

###### Abstract

Inter-frame motion in dynamic cardiac positron emission tomography (PET) using
rubidium-82 (82Rb) myocardial perfusion imaging impacts myocardial blood flow
(MBF) quantification and the diagnosis accuracy of coronary artery diseases.
However, the high cross-frame distribution variation due to rapid tracer
kinetics poses a considerable challenge for inter-frame motion correction,
especially for early frames where intensity-based image registration
techniques often fail. To address this issue, we propose a novel method called
Temporally and Anatomically Informed Generative Adversarial Network (TAI-GAN)
that utilizes an all-to-one mapping to convert early frames into those with
tracer distribution similar to the last reference frame. The TAI-GAN consists
of a feature-wise linear modulation layer that encodes channel-wise parameters
generated from temporal information and rough cardiac segmentation masks with
local shifts that serve as anatomical information. Our proposed method was
evaluated on a clinical 82Rb PET dataset, and the results show that our TAI-
GAN can produce converted early frames with high image quality, comparable to
the real reference frames. After TAI-GAN conversion, the motion estimation
accuracy and subsequent myocardial blood flow (MBF) quantification with both
conventional and deep learning-based motion correction methods were improved
compared to using the original frames.

###### keywords:

###### MSC:

41A05, 41A10, 65D05, 65D17 Early-to-late Frame Conversion, Dynamic Cardiac
PET, Inter-frame Motion Correction

††journal: Medical Image Analysis

##  1 Introduction

Dynamic cardiac positron emission tomography (PET) myocardial perfusion
imaging is more accurate in detecting coronary artery disease compared to
other non-invasive imaging procedures [49]. A dynamic frame sequence is
obtained after the injection of the radioactive tracer rubidium-82 (82Rb),
which lasts several minutes until the myocardium is sufficiently perfused.
Regions of interest (ROIs) of the myocardium tissue and left ventricle blood
pool (LVBP) are labeled from the reconstructed frames to collect time-activity
curves (TACs) for the following kinetic modeling and the estimation of
myocardial blood flow (MBF) and myocardial flow reserve (MFR). MBF and MFR
quantification have demonstrated improved diagnostic and prognostic
effectiveness [56].

However, in dynamic cardiac PET, subject motion originating from respiratory,
cardiac, and voluntary body movements can seriously impact both voxel-based
and ROI-based MBF quantification [28]. On the one hand, the intra-frame motion
can cause blurriness in reconstructed frames and incorrect activity
measurements. On the other hand, the inter-frame motion introduces spatial
mismatch across the dynamic frames, resulting in attenuation mismatch,
incorrect TAC measurements, and subsequent MBF estimation errors. Current
inter-frame motion correction approaches for dynamic PET include external
motion tracking systems [47, 39], data-driven motion estimation algorithms
[51, 14, 40, 42], and non-rigid registration using conventional optimization
[46, 31, 21, 63] or deep learning-based methods [71, 24, 23, 72, 22]. However,
few studies have specifically addressed the challenges in inter-frame motion
correction for cardiac dynamic PET with the rapid tracer kinetics of 82Rb. In
the early phases of tracer perfusion, 82Rb concentrates in the right ventricle
blood pool (RVBP) first and subsequently in LVBP; in the late scans, 82Rb is
well distributed in myocardial tissue. This significant change in tracer
distribution can substantially complicate inter-frame motion correction since
intensity-based frame registration typically depends on the resemblance
between the two frames that are to be registered, especially between the early
and late frames [41, 58]. In 82Rb dynamic cardiac PET, most existing motion
correction research and clinical software focuses exclusively on the later
frames in the myocardial perfusion stage [4, 68, 55, 41]. A blood pool
isolation strategy was proposed for the blood pool phase [34] but not for the
late myocardium phase frames. A frame registration method using normalized
gradient fields instead of original intensities was proposed to narrow the
gap, but unidentifiable boundaries in the transition phase frames and the
usage of the blurred summed tissue phase frame as the reference might
introduce additional errors to motion estimation [35]. A motion correction
framework under supervised learning was proposed for 82Rb dynamic cardiac PET
under simulated translational motion [58], but the network requires the
training of two separate models to address the variation between early and
late frames, which can be computationally expensive and inconvenient in
clinical practice.

An alternative solution is using frame conversion to generate mapped early
frames that appear similar in tracer distribution to the corresponding late
frame to assist standard motion correction methods. Recent studies have
indicated that utilizing modality conversion through image synthesis can
enhance optimization in multi-modality image registration by simplifying it to
intra-modality [29, 69]. For instance, image synthesis methods have been
utilized to convert magnetic resonance (MR) to computed tomography (CT) images
[54, 5], MR T1-weighted (T1w) to T2-weighted (T2w) images [6, 38], and MR to
X-ray mammography [44]; however, few studies involve PET images.

Such medical image synthesis tasks have largely utilized convolutional neural
networks (CNNs) [57, 38, 73]. In molecular imaging, CNNs have been
successfully implemented in the generation of attenuation maps [61, 62, 8],
cross-tracer images [67], and parametric $K_{i}$ images [45], mostly deploying
the structure of a 3-D U-Net [9]. Generative adversarial networks (GANs) [17]
and their derivatives are a group of CNNs including a generator and a
discriminator which are trained in a process of competition under an
adversarial loss. GAN-based image synthesis from MR T1w images has been
implemented to generate CT images [36, 1], T2w images [11], and fluid-
attenuated inversion recovery images [70]. In nuclear medicine imaging, recent
works have investigated attenuation map generation for single-photon emission
computed tomography (SPECT) [60] and the direct SPECT attenuation correction
deploying conditional GANs (cGANs), a GAN variation with conditional restraint
for specific mapping. A 3-D cGAN with self-attention and spectral
normalization mechanism was proposed to synthesize brain PET from MR in an
Alzheimer’s disease database [33]. A cGAN with visual information fidelity
loss was developed for generating synthetic CT images for the attenuation
correction of small animal PET [37]. A short-to-long acquisition conversion
module using a cGAN was included in a motion correction and reconstruction
framework for accelerated PET [72].

A closely related work to improve inter-frame motion correction in dynamic PET
deployed a cGAN to convert low-count early frames to the high-count late frame
of brain [64] and total-body dynamic scans [65]. In this way, the low-count
limitation and the different tracer uptake patterns of early frames are
addressed, and the motion correction using the standard multi-scale mutual
information method is successfully improved. However, this approach involves
training one-to-one mappings between each specific early frame and the
reference frame, which may not generalize well to new acquisitions and can be
challenging to implement in clinical practice settings. Additionally, the
backbone of the generator is a simple 3-D U-Net, and the tracer kinetics and
related temporal analysis are not incorporated in network training. This
method was originally developed on 2-deoxy-2-[18F]fluoro-D-glucose (FDG) PET
scans, while 82Rb kinetics is substantially more rapidly changing than FDG.
This is a potential limitation of their approach when directly applied to 82Rb
scans. Recently, feature-wise linear modulation (FiLM) [48] has been reported
to be effective in encoding conditional information and vision reasoning. FiLM
layers have been incorporated into GAN models to encode text or semantic
information for natural images, specifically fashion image generation [2, 43,
3]. In MRI generation, the FiLM layer was proposed to process metadata [50].
Similarly, [12] proposed to use the FiLM layer as a conditional embedding in a
GAN for deformable template generation in MRI registration. However, such a
structure has not been proposed either for tracer kinetics information
encoding or in dynamic PET synthesis.

Fig. 1: The architecture of the proposed temporally and anatomically informed
generative adversarial network (TAI-GAN).

Thus, in this work, we introduce a new framework named Temporally and
Anatomically Informed GAN (TAI-GAN), an all-to-one mapping approach that
converts all early frames into those with the appearance of the last reference
frame. To provide the temporal information to the generator, we incorporate a
FiLM layer that embeds channel-wise parameters generated from the temporal
frame index and blood pool TACs. To inform the network with auxiliary
anatomical locators, we utilize rough segmentation masks of RVBP, LVBP, and
myocardium with local shifts as the additional image input channel. TAI-GAN is
the first work for dynamic cardiac PET frame conversion that addresses the
challenges of both high tracer distribution variability and spatial mismatch
by incorporating both temporal and anatomical information, effectively
handling the variations in tracer distribution over time and ensuring accurate
spatial alignment in the generated frames. Using a 5-fold cross-validation, we
evaluated TAI-GAN in terms of frame conversion similarity, motion correction
accuracy, and MBF quantification errors.

##  2 Methods

###  2.1 Clinical cardiac dataset and pre-processing

A total of 104 anonymized clinical dynamic cardiac 82Rb PET scans from 73
subjects at Yale New Haven Hospital were included in this study, with the
approval of the Yale Institutional Review Board. Each scan was acquired using
a GE Discovery 690 PET/CT scanner after 82Rb generation using a Bracco
Diagnostics Inc. commercial generator and weight-based 82Rb delivery using a
programmed infusion. In each scan, the list-mode data of the first 6 minutes
and 10 seconds were rebinned into a sequence of 27 dynamic frames (14×5s,
6×10s, 3×20s, 3×30s, 1×90s) in total. All the frames were reconstructed into
128 × 128 × 47 volumes with a voxel size of 3.125 × 3.125 × 3.270 mm3 using
the ordered subset expectation maximization algorithm (OSEM, 2 iterations, and
24 subsets) with the corrections of isotope decay, attenuation, scatter,
random and prompt-gamma coincidences, detector efficiency, and deadtime, and
then filtered with a Butterworth filter (cutoff frequency = 21 mm-1, order =
5). The intensities of the dynamic frames were calibrated as activity
concentration (Bq/mL). With the Corridor 4DM software in the clinical setting,
technologists manually performed frame-by-frame motion correction and
identified each scan as either motion-free (total motion no more than 3 mm,
[28, 58]) or with moderate to significant motion. The demographic information
and characteristics of the dataset are summarized in Table 1.

Table 1: The demographic information and characteristics of the cardiac
dataset.

Group | A (motion-free) | B (with motion)
---|---|---
Scan time | Dec. 2019 to Jan. 2020 | Oct. 2022
| Number of scans
---
(rest/stress)
85 (55/30) | 19 (10/9)
| Number of patients
---
(female/male)
59 (34/25) | 14 (9/5)
| Age (year, mean $\pm$
---
standard deviation)
62.9 $\pm$ 11.3 | 65.8 $\pm$ 10.9
| Body mass index ($kg/m^{2}$,
---
mean $\pm$ standard deviation)
37.1 $\pm$ 10.9 | 32.3 $\pm$ 7.3

The rough segmentations of RVBP, LVBP, and LV myocardium were manually
annotated on all scans using the last dynamic frame as a reference for the
generation of TAC and subsequent quantification of MBF. The location of the LV
inferior wall center was manually labeled for each scan on the last dynamic
frame for cardiac central cropping [58].

###  2.2 Proposed network

The model architecture of the proposed TAI-GAN is illustrated in Figure 1. The
generator maps the input early frame to its corresponding late frame, and the
discriminator takes either the true or synthesized late frame as the input and
encodes it to determine whether it is real or fake. The backbone structure of
the generator is a 3-D U-Net with skip connections between the 4 downsample or
upsample levels in both the encoder and decoder, with modifications
specifically designed for auxiliary guidance in terms of temporal and
anatomical information. The backbone structure of the discriminator is a
PatchGAN [30, 64] with 3 encoding levels and 1 linear output layer.

Given the significant discrepancy in the tracer distribution across the
various dynamic frame phases, the model is temporally informed by the
auxiliary input of the concatenated RVBP and LVBP TACs along with the one-hot
coded temporal frame index. Considering the recent success in implementing
long short-term memory (LSTM) networks [27] in 1-D biomedical sequential data
analyses [25, 13, 20], we deploy an LSTM to analyze the concatenated temporal
input. Subsequently, a 1-D convolutional layer and a linear layer encode the
LSTM output to the manipulation parameters $\gamma$ and $\beta$ for the
following channel-wise linear modulation, formulated as:

$[\gamma,\beta]=f(x),$ (1)

where $f(\cdot)$ represents the temporal encoding module (concatenated LSTM,
1-D convolution, and linear layer), and $x$ represents the concatenated
auxiliary temporal inputs (RVBP TAC, LVBP TAC, and the one-hot frame index).
After this, the bottleneck feature map of the 3-D U-Net is modulated by the
channel-wise FiLM operator using $\gamma$ as the scale factor and $\beta$ as
the bias:

$FiLM(X_{i})=\gamma_{i}\cdot X_{i}+\beta_{i},$ (2)

where for the $i^{th}$ channel of the bottleneck feature map $X_{i}$,
$\gamma_{i}$ and $\beta_{i}$ are respectively the scale factor and the bias of
the corresponding channel, and $FiLM(\cdot)$ represents the FiLM operator.

The model is anatomically informed by the rough segmentations of the cardiac
ROIs as the anatomical locator. The rough segmentations of RVBP, LVBP, and
myocardium are concatenated with the early frame as the dual-channel input of
the generator. These labeled masks indicate the location of different ROIs
within the dynamic frames and provide anatomical information to the generator
about the location of each region. This is designed to introduce consistency
and prevent spatial mismatch artifacts of the myocardium in frame conversion,
which are particularly useful in distinguishing between the early RV and LV
phases. Without such anatomical guidance, the conversion result of an early
frame in the RV phase might have the artifact of myocardium located near the
RV instead of LV due to mistaking the RVBP as LVBP. To prevent errors
introduced by the misalignment between the early frame and the last frame
where the ROIs are labeled, during training, random local shifts of the
segmentations are deployed before concatenating with the early frame. In this
way, the robustness of the model is improved under weak guidance, and the
model is trained to be able to handle real-patient data when significant
motion may be present.

The loss function of the TAI-GAN model contains both a voxel-wise mean squared
error (MSE) loss as the image similarity penalty and the cross entropy
adversarial loss in the min-max game between the generator and the
discriminator. As in Eq. 3-5 below,

$\displaystyle L_{mse}$
$\displaystyle=\frac{1}{N}\sum\limits_{n=1}^{N}(G(F_{i})_{n}-(F_{L})_{n})^{2},$
(3)

$\displaystyle L_{adv}$ $\displaystyle=-\log(D(F_{L}))-\log(1-D(G(F_{i}))),$
(4)

$\displaystyle\hat{G},\hat{D}$
$\displaystyle=arg\min_{G}\max_{D}(L_{mse}+L_{adv}),$ (5)

where $L_{mse}$ is the MSE loss, $N$ is the total number of voxels in one
dynamic frame, $G$ is the generator, $G(F_{i})$ is the converted late frame of
the $i^{th}$ early input frame $F_{i}$, $F_{L}$ is the true last frame as the
reference, $L_{adv}$ is the adversarial loss, and $D$ is the discriminator.
Both the generator and the discriminator networks are trained end-to-end under
a min-max game with the goal of improving the quality of frame conversion.

###  2.3 Implementation details

All the early frames with tracer concentration greater than 10% of the maximal
activity in LVBP TAC are included in implementation to be converted to the
corresponding last frames. All the earlier frames are ignored since these very
early frames with LVBP activity lower than 10% maximum have no meaningful
impact on image-derived input function and consequently the MBF measurement
[58]. The EQ frame was defined as the first frame in which the LVBP activity
is equal to or higher than the RVBP activity [58] and automatically labeled
based on the LVBP and RVBP TACs, and the same temporal normalization process
as in Shi et al. [58] was applied to all the dynamic frames. The intensity
normalization of all the frames was applied individually to the range of
[-1,1] prior to the conversion network input to enhance GAN optimization. The
network training was based on patches with the size of (64,64,32) that are
randomly cropped near the center of the LV inferior wall, randomly rotated in
the xy plane in the range of [-45∘,45∘], and randomly shifted in the range of
[-5,5] voxels along the x, y, and z-axis for data augmentation.

Due to the low practicality of training each one-to-one mapping for all the
early frames, we trained two single-pair mappings using a vanilla GAN (3-D
U-Net generator) and only the adversarial loss to compare with Sundar et al.
[64]. The two single-pair mappings are one frame before and after the EQ
frame, which are respectively designated as EQ-1 and EQ+1. Additionally, we
implemented both the vanilla GAN and the MSE loss GAN as the two baselines of
all-to-one conversion. An ablation study was conducted to evaluate the
effectiveness of the auxiliary temporal and anatomic information analysis.

All frame conversion models are implemented using PyTorch and trained on an
NVIDIA A40 GPU with an Adam optimizer (learning rate $LR_{G}$=2e-4,
$LR_{D}$=5e-5). The training and evaluation are conducted under 5-fold cross-
validation on the 85 motion-free scans. Each fold contained 68 scans for
training and 17 scans that were randomly left out for inference. For one-to-
one mappings, the stopping epoch was 800, and for all-to-one models, the
stopping epoch was set to 100.

Fig. 2: Sample results of early-to-late frame conversion using each method
with overlaid RVBP (red), LVBP (blue), and myocardium (green) segmentation
contours, with arrows highlighting alignment or mismatch between the cardiac
segmentations and structures.

###  2.4 Frame mapping evaluation

The qualitative evaluation of frame generation results involves comparing the
visualizations of the generated last frames and the real last frames given the
real early frame inputs. The cardiac segmentations are overlaid on the
visualized frames as locators for the anatomical regions.

The quantitative evaluations of frame generation results are the normalized
mean absolute error (NMAE), MSE, structural similarity index (SSIM), and peak
signal-to-noise ratio (PSNR) calculated between the real and generated last
frames. As in Eq. 6-9,

$\displaystyle\mathrm{NMAE}$
$\displaystyle=\frac{1}{N}\sum\limits_{n=1}^{N}\frac{|(\hat{F_{L}})_{n}-(F_{L})_{n}|}{\max(F_{L})-\min(F_{L})},$
(6)

$\displaystyle\mathrm{MSE}$
$\displaystyle=\frac{1}{N}\sum\limits_{n=1}^{N}((\hat{F_{L}})_{n}-(F_{L})_{n})^{2},$
(7)

$\displaystyle\mathrm{SSIM}(F_{L},\hat{F_{L}})$
$\displaystyle=\frac{(2\mu(F_{L})\mu(\hat{F_{L}})+C_{1})(2\sigma(F_{L},\hat{F_{L}})+C_{2})}{(\mu^{2}(F_{L})+\mu^{2}(\hat{F_{L}})+C_{1})(\sigma^{2}(F_{L})+\sigma^{2}(\hat{F_{L}})+C_{2})},$
(8)

$\displaystyle\mathrm{PSNR}$
$\displaystyle=10\cdot\log_{10}\left(\frac{\max(F_{L})^{2}}{\mathrm{MSE}}\right),$
(9)

where $N$ is the total number of voxels in one dynamic frame, $\hat{F_{L}}$ is
the generated last frame, $F_{L}$ is the real last frame, $\max(F_{L})$ and
$\min(F_{L})$ are respectively the maximum and minimum values of the real last
frame, $max(\hat{F_{L}})$ and $min(\hat{F_{L}})$ are respectively the maximum
and minimum values of the generated last frame, $\mu(F_{L})$ and
$\mu(\hat{F_{L}})$ are respectively the mean values of the real and generated
last frame, $\sigma^{2}(F_{L})$ and $\sigma^{2}(\hat{F_{L}})$ are respectively
the variance of the real and generated last frame, $\sigma(F_{L},\hat{F_{L}})$
is the covariance of $F_{L}$ and $\hat{F_{L}}$, and $C_{1}=(0.01\cdot DR)^{2}$
and $C_{2}=(0.03\cdot DR)^{2}$ are the two constants to stabilize the ratio
when the denominator is weak, where $DR$ is the dynamic range of the voxel
values.

Table 2: Quantitative image similarity evaluation of early-to-late frame
conversion (mean $\pm$ standard deviation) with the best results marked in
bold.

Test set | Metric |  | Vanilla GAN
---
One-to-one
| Vanilla
---
GAN
| MSE loss
---
GAN
| TAI-GAN
---
(Proposed)
EQ-1 | NMAE | 0.068 $\pm$ 0.002∗ | 0.063 $\pm$ 0.005∗ | 0.059 $\pm$ 0.009 | 0.057 $\pm$ 0.005
MSE | 0.057 $\pm$ 0.001∗ | 0.050 $\pm$ 0.006∗ | 0.044 $\pm$ 0.011 | 0.040 $\pm$ 0.005
SSIM | 0.557 $\pm$ 0.017∗ | 0.640 $\pm$ 0.021 | 0.633 $\pm$ 0.053∗ | 0.657 $\pm$ 0.018
PSNR | 18.678 $\pm$ 0.116∗ | 19.370 $\pm$ 0.474∗ | 19.950 $\pm$ 0.949 | 20.335 $\pm$ 0.530
EQ+1 | NMAE | 0.050 $\pm$ 0.011 | 0.053 $\pm$ 0.003 | 0.051 $\pm$ 0.006 | 0.048 $\pm$ 0.003
MSE | 0.032 $\pm$ 0.014 | 0.034 $\pm$ 0.002 | 0.033 $\pm$ 0.006 | 0.032 $\pm$ 0.002
SSIM | 0.669 $\pm$ 0.061∗ | 0.679 $\pm$ 0.014 | 0.680 $\pm$ 0.011 | 0.691 $\pm$ 0.013
PSNR | 21.323 $\pm$ 1.800 | 21.014 $\pm$ 0.355 | 21.188 $\pm$ 0.757 | 21.361 $\pm$ 0.205
All Pre-EQ frames | NMAE | - | 0.072 $\pm$ 0.007∗ | 0.066 $\pm$ 0.011 | 0.062 $\pm$ 0.008
MSE | - | 0.063 $\pm$ 0.010∗ | 0.053 $\pm$ 0.016 | 0.046 $\pm$ 0.009
SSIM | - | 0.594 $\pm$ 0.012∗ | 0.596 $\pm$ 0.047∗ | 0.627 $\pm$ 0.025
PSNR | - | 18.507 $\pm$ 0.474∗ | 19.269 $\pm$ 1.036∗ | 19.834 $\pm$ 0.738
All frames | NMAE | - | 0.047 $\pm$ 0.004∗ | 0.044 $\pm$ 0.002 | 0.040 $\pm$ 0.002
MSE | - | 0.027 $\pm$ 0.002∗ | 0.024 $\pm$ 0.003 | 0.021 $\pm$ 0.002
SSIM | - | 0.708 $\pm$ 0.010∗ | 0.716 $\pm$ 0.007∗ | 0.733 $\pm$ 0.018
PSNR | - | 22.803 $\pm$ 0.530∗ | 23.241 $\pm$ 0.342∗ | 23.799 $\pm$ 0.466
∗P$\textless 0.05$ between the current method and TAI-GAN (paired two-tailed
t-test).

###  2.5 Simulated and real-patient motion correction

A motion simulation test was conducted on all the motion-free scans to assess
the benefit of frame conversion on motion correction. To generate motion
vector ground truth, we implemented non-rigid motion correction in BioImage
Suite [32] (BIS) on an independent 82Rb cardiac scan set classified as having
significant motion by the clinical team. Since the conventional BIS method
might fail on early frames with distinct tracer distribution differences, we
only utilized the motion field estimates from the late frames with realistic
characteristics of simulated motion and then scaled the motion magnitude by 2
as the motion magnitude from those late frames adjacent to the last frame
might be too small to show significant motion impact. Before motion
simulation, different frame mapping models were applied to all the early
frames before frame 27, and then the simulated motion vectors were applied to
both original and converted early frames. We applied two motion correction
methods: the conventional frame registration using BIS was implemented with
the same hyperparameter settings as in [21], and a multiple-frame deep
learning registration model (DL) that was well-trained on a whole-body FDG PET
dataset as in [24]. All the early frames were registered to frame 27 as the
reference frame. The frames before and after motion simulation were visualized
with overlaid cardiac segmentations as the qualitative evaluation. The mean
absolute error is computed as the measurement of motion prediction accuracy,
formulated as below,

$|\Delta\phi|=\frac{1}{T}\sum\limits_{n=1}^{T}(|\phi_{x_{n}}-\hat{\phi}_{x_{n}}|+|\phi_{y_{n}}-\hat{\phi}_{y_{n}}|+|\phi_{z_{n}}-\hat{\phi}_{z_{n}}|)*\frac{1}{3},$
(10)

where $T$ is the number of transformation control points in a frame,
($\phi_{x_{n}}$,$\phi_{y_{n}}$,$\phi_{z_{n}}$) is the ground-truth of the
motion field, and
($\hat{\phi}_{x_{n}}$,$\hat{\phi}_{y_{n}}$,$\hat{\phi}_{z_{n}}$) is the
predicted motion field. The normalized mutual information (NMI) between each
moving dynamic frame and the reference frame is also calculated as a
measurement of spatial alignment.

In the cross-validation of frame conversion, the motion simulation test was
implemented on the 17 test subjects of each fold, resulting in 85 motion
simulation cases.

For the independent dataset with significant motion (Group B), we directly
applied frame conversion on the early frames and then the same BIS and DL
motion correction methods on both the original and converted frame sequences.
Since the motion ground truth is lacking, we only visualized the frames with
overlaid segmentations as the qualitative evaluation and calculated frame NMI
as the quantitative spatial alignment evaluation.

For each motion correction group, the motion estimates are directly applied to
the motion-corrupted original frames before conversion and without intensity
normalization to preserve the tracer activities for the following MBF
quantification.

###  2.6 Myocardial blood flow analysis

The three-parameter one-tissue compartment model is fitted using the LVBP TAC
as the image-derived input function and the LV myocardium TAC for the
estimation of uptake rate constant $K_{1}$,

$\frac{dC_{t}(t)}{dt}=K_{1}C_{p}(t)-k_{2}C_{t}(t),$ (11)

where $C_{t}(t)$ is the tissue concentration, $C_{p}(t)$ is the plasma
concentration (input function), and $k_{2}$ is the clearance rate constant.
Weighted least squares fitting was applied in the model fitting for parameter
estimations, with the weights computed as in 12 [59, 58],

$w_{i}=\frac{dur_{i}^{2}}{T_{i}\times DCF^{2}},$ (12)

where for the $i^{th}$ frame, $w_{i}$ is the fitting weight, $dur_{i}$ is the
frame scan duration, $T_{i}$ is the sum of the activity of the entire frame,
and $DCF$ is the decay correction factor.

The MBF is then quantified from the $K_{1}$ estimate under the Renkin-Crone
Model [52, 53, 10] with the unit of mL/min/g,

$K_{1}=MBF\times(1-\alpha e^{-\beta/MBF}),$ (13)

where $\beta$ is the basal permeability-surface area (PS) product and $\alpha$
is the parameter of MBF-related PS changes [16]. Both $\alpha$ and $\beta$
were the same as in the previous 82Rb study ($\alpha$=0.74, $\beta$=0.51, Shi
et al. [58]).

The percentage differences for $K_{1}$ and $MBF$ are calculated between the
motion-corrected and original frames,

${K_{1}}_{diff}=(\hat{K_{1}}-K_{1})/K_{1},$ (14)
$MBF_{diff}=(\hat{MBF}-MBF)/MBF,$ (15)

where $\hat{K_{1}}$ and $\hat{MBF}$ are respectively the estimated parameters
after motion correction, and $K_{1}$ and $MBF$ are respectively the estimated
parameters before motion correction. For the motion simulation cases, the
percentage differences are calculated as estimation bias; for the cases with
real motion, since the motion-free ground truth is lacking, the percentage
differences are reported as the effect of motion correction.

##  3 Results

###  3.1 Frame conversion evaluation

Figure 2 displays sample slices from distinct cases of early-to-late frame
conversion results under each method. The models of one-to-one conversion were
trained with the most precise temporal mapping pairs, but the generation
results were generally unsatisfactory with several failure cases. This might
be due to the small sample size in the dataset and the possible overfitting of
the model since the dataset size of one specific mapping is substantially
smaller than the entire dataset. Also, although the model could learn the
anatomical information from one early frame, the kinetics-related temporal
information from only one early frame is insufficient for satisfactory
conversion. The Vanilla GAN was able to learn the conversion patterns in an
all-to-one manner, although with some aberrations and distortions in the
myocardium. The MSE loss GAN produced results with improved visual similarity.
The proposed TAI-GAN achieved the best visual performance with the least
amount of remaining mismatch and distortion after incorporating temporal and
anatomical information.

Table 2 summarizes the quantitative results of the image similarity evaluation
for frame conversion. Statistics are presented for different sets of test
data, including only EQ-1 frames; only EQ+1 frames; all pre-EQ frames, defined
as frames where LVBP activity is greater than RVBP activity; and all frames.
The quantitative results confirmed that the one-to-one trained models did not
perform better than the all-to-one trained models, possibly due to the lack of
inter-frame tracer kinetic dependencies. The TAI-GAN produced the best result
in each statistic across all evaluation sets. The proposed TAI-GAN showed the
greatest improvement in the pre-EQ frames, which are the most challenging
subgroup in frame conversion due to the significant tracer distribution
discrepancy between the input and output frames.

Fig. 3: Sample motion simulation and correction results with different methods
of frame conversion, with overlaid RVBP (red), LVBP (blue), and myocardium
(green) segmentation contours and arrows highlighting alignment or mismatch
between the cardiac segmentations and structures.

###  3.2 Motion simulation study

Table 3: Mean absolute motion prediction errors without and with each
conversion method (in mm, mean $\pm$ standard deviation) with the best results
marked in bold.

| Motion
---
correction
method
Test set |  | No
---
Conversion
| Vanilla GAN
---
One-to-one
Vanilla GAN |  | MSE loss
---
GAN
TAI-GAN
BIS | All frames | 5.30 $\pm$ 0.98∗ | - | 5.44 $\pm$ 0.90∗ | 5.06 $\pm$ 0.37∗ | 4.70 $\pm$ 0.46
EQ-1 | 5.36 $\pm$ 1.52∗ | 5.42 $\pm$ 1.21 | 5.36 $\pm$ 1.52∗ | 5.23 $\pm$ 1.10∗ | 5.17 $\pm$ 0.60
EQ+1 | 5.30 $\pm$ 1.18∗ | 4.74 $\pm$ 0.93 | 4.93 $\pm$ 1.02∗ | 4.90 $\pm$ 0.47∗ | 4.52 $\pm$ 1.02
DL | All frames | 3.84 $\pm$ 0.39∗ | - | 3.82 $\pm$ 0.40∗ | 3.81 $\pm$ 0.40∗ | 3.77 $\pm$ 0.38
EQ-1 | 3.87 $\pm$ 0.59∗ | 3.83 $\pm$ 0.53∗ | 3.80 $\pm$ 0.60 | 3.80 $\pm$ 0.57 | 3.78 $\pm$ 0.56
EQ+1 | 3.85 $\pm$ 0.53∗ | 3.79 $\pm$ 0.50∗ | 3.83 $\pm$ 0.54∗ | 3.72 $\pm$ 0.56 | 3.70 $\pm$ 0.54
${}^{*}P\textless 0.05$ between the current method and TAI-GAN (paired two-tailed t-test). |

Table 4: Mean frame NMI after motion correction without and with each
conversion method (mean $\pm$ standard deviation) with the best results marked
in bold.

| Motion
---
correction
method
Test set | No motion | Simulated motion |  | No
---
Conversion
| Vanilla GAN
---
One-to-one
Vanilla GAN |  | MSE loss
---
GAN
TAI-GAN
BIS | All frames | 0.933 $\pm$ 0.013∗ | 0.915 $\pm$ 0.015∗ | 0.887 $\pm$ 0.027∗ | - | 0.917 $\pm$ 0.035∗ | 0.918 $\pm$ 0.035∗ | 0.948 $\pm$ 0.009
EQ-1 | 0.925 $\pm$ 0.015∗ | 0.914 $\pm$ 0.015∗ | 0.884 $\pm$ 0.033∗ | 0.902 $\pm$ 0.033∗ | 0.906 $\pm$ 0.029∗ | 0.905 $\pm$ 0.067∗ | 0.948 $\pm$ 0.011
EQ+1 | 0.927 $\pm$ 0.014∗ | 0.914 $\pm$ 0.015∗ | 0.887 $\pm$ 0.034∗ | 0.902 $\pm$ 0.033∗ | 0.905 $\pm$ 0.029∗ | 0.903 $\pm$ 0.081∗ | 0.947 $\pm$ 0.010
DL | All frames | 0.933 $\pm$ 0.013∗ | 0.915 $\pm$ 0.015∗ | 0.937 $\pm$ 0.014∗ | - | 0.939 $\pm$ 0.013 | 0.938 $\pm$ 0.014∗ | 0.939 $\pm$ 0.013
EQ-1 | 0.925 $\pm$ 0.015∗ | 0.914 $\pm$ 0.015∗ | 0.936 $\pm$ 0.015∗ | 0.928 $\pm$ 0.018∗ | 0.938 $\pm$ 0.014∗ | 0.937 $\pm$ 0.014∗ | 0.966 $\pm$ 0.008
EQ+1 | 0.927 $\pm$ 0.014∗ | 0.914 $\pm$ 0.015∗ | 0.937 $\pm$ 0.015∗ | 0.929 $\pm$ 0.017∗ | 0.939 $\pm$ 0.014 | 0.938 $\pm$ 0.015∗ | 0.939 $\pm$ 0.015
∗P <0.05 between the current method and TAI-GAN (paired two-tailed t-test). |  |  |

The sample results of the motion simulation and the corrected motion are shown
in Figure 3. In the motion-free sample, the cardiac mask contours are well-
aligned with the corresponding anatomical structures. After introducing the
simulated non-rigid motion, part of the LVBP is misaligned under the
myocardium. When directly registering the original frames without frame
conversion, the resliced frame by BIS was more distorted, especially for the
LVBP, and the motion correction of DL showed an undercorrected result,
possibly because of the substantial tracer distribution differences in the
frame pair. In the Vanilla and MSE loss GAN results, the frame generation
results look similar to the last reference frame to some extent, but with
deformation and shape differences from conversion errors, additional
mismatches were observed after BIS motion correction. With the highest frame
similarity and minimal frame mapping errors, the conversion result of the
proposed TAI-GAN matched the relevant myocardium and ventricle locations with
the original early frame and had the cardiac shape most similar to the
original last frame. The registration result of BIS demonstrated the best
visual alignment of the cardiac ROIs and that of DL showed the best similarity
of the base cardiac regions. It is noted that all of the DL motion correction
results showed under-correction on top of the LV, possibly due to the gap
between the whole-body motion and cardiac motion; still, the result after TAI-
GAN conversion reduced this remaining mismatch the most.

Table 3 summarizes the mean absolute motion estimation error of both BIS and
DL motion correction without conversion and with all the conversion methods.
The early scan time of a dynamic frame is generally related to high motion
estimation errors, and the DL motion correction method achieved lower
estimation errors than the BIS method. In all the included early frames and
both EQ-1 and EQ+1 frames, for both BIS and DL motion correction methods, the
proposed TAI-GAN achieved the lowest motion estimation error among all the
methods. The TAI-GAN-aided BIS motion correction significantly reduced the
average prediction error compared to no conversion and all the other GAN
models ($p<0.05$), and the TAI-GAN-aided DL motion correction significantly
decreased the average prediction error for all frames compared to no
conversion and the one-to-one GAN mapping ($p<0.05$). This suggests that the
accuracy of motion correction would increase after successful frame
conversion.

Table 4 summarizes the average of frame NMI before and after each motion
correction method. For BIS motion correction, the TAI-GAN frame conversion
could successfully improve frame similarity measured by NMI compared to no
conversion and all the GAN baselines with significant differences ($p<0.05$).
For DL motion corrections, even without conversion, the frame NMI increased.
For the EQ-1 frame, the TAI-GAN significantly improved frame NMI compared with
all the other baselines ($p<0.05$), but for the EQ+1 frame and all the frames
the TAI-GAN achieved comparable improvement as Vanilla GAN ($p>0.05$). It
could be due to the limitation of the direct application of a well-trained
whole-body FDG model to the cardiac Rb-82 data, especially for later frames
with less tracer distribution difference, where the motion characteristics-
related generalization gap became more significant.

###  3.3 Parametric fitting results

Table 5: $K_{1}$ and MBF quantification results after BIS or DL motion
correction (mean $\pm$ standard deviation) with the best results marked in
bold.

|  | Mean $K_{1}$ percentage
---
difference (%)
| Mean MBF percentage
---
difference (%)
| Mean fitting
---
error ($\times$10-5)
Motion-free | - | - | 1.80 $\pm$ 2.06
With motion | 15.72 $\pm$ 26.24∗ | 4.43 $\pm$ 38.67∗ | 10.46 $\pm$ 6.55∗
BIS | 16.63 $\pm$ 32.13∗ | 14.45 $\pm$ 68.65∗ | 13.74 $\pm$ 19.49∗
Vanilla GAN+BIS | 11.73 $\pm$ 32.82∗ | 3.09 $\pm$ 39.09 | 9.60 $\pm$ 9.02∗
MSE loss GAN+BIS | 17.98 $\pm$ 24.54∗ | 3.32 $\pm$ 31.76 | 11.34 $\pm$ 12.29∗
TAI-GAN+BIS | 6.42 $\pm$ 35.82 | 2.21 $\pm$ 35.41 | 7.41 $\pm$ 7.81
DL | 17.43 $\pm$ 23.89∗ | 7.03 $\pm$ 40.37∗ | 8.35 $\pm$ 7.52∗
Vanilla GAN+DL | 17.34 $\pm$ 24.38∗ | 7.87 $\pm$ 40.82∗ | 8.29 $\pm$ 7.58∗
MSE loss GAN+DL | 18.54 $\pm$ 24.12∗ | 5.90 $\pm$ 32.36 | 7.97 $\pm$ 7.26
TAI-GAN+DL | 15.43 $\pm$ 26.04 | 3.40 $\pm$ 32.90 | 7.80 $\pm$ 6.77
∗P $\textless 0.05$ between the current method and TAI-GAN (paired two-tailed
t-test).

Table 5 summarizes the parametric fitting error as well as the percentage
difference in $K_{1}$ and MBF compared to no motion ground truth. The fitting
errors of both TAI-GAN+BIS and TAI-GAN+DL were the lowest among all the test
classes in each motion correction category, showing significant improvements
compared to fitting using frames with motion and all the motion correction
methods ($p<0.05$). The $K_{1}$ and MBF percentage differences of TAI-GAN+BIS
and TAI-GAN+DL were the lowest among all the groups. The TAI-GAN+BIS achieved
$K_{1}$ and MBF fitting results closer to those of the motion-free baseline
than the TAI-GAN+DL. Thus, we visualized the scatter plots of MBF fitting and
the TAC plots of the TAI-GAN+BIS. As in Figure 4, with simulated motion, the
scatters of MBF estimates versus the ground truth without motion were not
uniformly distributed and were distant from the identity line. With BIS MC but
without conversion, the fitted line was close to the identity line but for
some data points, the estimation bias even increased. The fitted lines of
motion correction with vanilla GAN and MSE loss GAN were closer to the
identity line but still with an under-estimation effect. The fitted line of
motion correction with the proposed TAI-GAN was the closest to the identity
line, suggesting the most improvement in MBF quantification. As in Figure 5,
after BIS MC with no conversion, the discrepancy between the two LVBP TACs
decreased in later frames but drastically increased in the very early blood
pool phase frames. The Vanilla GAN conversion improved the correction of later
frames but the early frames remained mismatched in the myocardium. The MSE
loss GAN corrected the later frames but showed remaining errors of under-
correction or miscorrection in the early and later frames. The TACs of TAI-
GAN-aided BIS motion correction were closest to the no-motion ground truth and
resulted in the lowest LV and myocardium MSE.

Fig. 4: Scatter plots of MBF results estimated from no motion frames vs. no
motion correction and BIS motion correction after different conversion
methods. Fig. 5: A comparison of LVBP and myocardium TACs of each conversion
method before and after BIS motion correction.

###  3.4 Real-motion evaluation

Fig. 6: Sample patient real motion correction results with different methods
of frame conversion, with overlaid RVBP (red), LVBP (blue), and myocardium
(green) segmentation contours and arrows highlighting alignment or mismatch
between the cardiac segmentations and structures.

A sample of the real-motion correction after frame conversion is shown in
Figure 6. The early and late frames are misaligned in the right ventricle,
left ventricle, and myocardium, with non-rigid motion. Without frame
conversion, the BIS method showed under correction and the DL method showed
motion estimation error in the myocardium region. The one-to-one model
conversion showed large errors and distortion, resulting in over-correction
after applying both BIS and DL. Both all-to-one baseline models produced more
realistic results but still with local spatial distortion. In the conversion
result of TAI-GAN, the myocardium shape is the closest to the reference with
the location matching with the motion-present early frame. The motion
correction result after TAI-GAN conversion was also the best among both the
BIS and DL methods.

Table 6: Mean frame NMI after motion correction without and with each
conversion method (mean $\pm$ standard deviation) on the real-patient motion
dataset with the best results marked in bold.

| Motion
---
correction
method
Test set | No motion correction |  | No
---
Conversion
| Vanilla GAN
---
One-to-one
Vanilla GAN |  | MSE loss
---
GAN
TAI-GAN
BIS | All frames | 0.970 $\pm$ 0.012∗ | 0.945 $\pm$ 0.013∗ | - | 0.939 $\pm$ 0.032∗ | 0.935 $\pm$ 0.037∗ | 0.961 $\pm$ 0.008
EQ-1 | 0.960 $\pm$ 0.014∗ | 0.940 $\pm$ 0.012∗ | 0.864 $\pm$ 0.031∗ | 0.906 $\pm$ 0.045∗ | 0.905 $\pm$ 0.052∗ | 0.961 $\pm$ 0.009
EQ+1 | 0.964 $\pm$ 0.011 | 0.942 $\pm$ 0.012∗ | 0.856 $\pm$ 0.024∗ | 0.924 $\pm$ 0.028∗ | 0.920 $\pm$ 0.038∗ | 0.962 $\pm$ 0.011
DL | All frames | 0.970 $\pm$ 0.012∗ | 0.982 $\pm$ 0.006∗ | - | 0.982 $\pm$ 0.006∗ | 0.982 $\pm$ 0.006∗ | 0.988 $\pm$ 0.004
EQ-1 | 0.960 $\pm$ 0.014∗ | 0.981 $\pm$ 0.006∗ | 0.981 $\pm$ 0.006∗ | 0.981 $\pm$ 0.006∗ | 0.981 $\pm$ 0.006∗ | 0.988 $\pm$ 0.004
EQ+1 | 0.964 $\pm$ 0.011∗ | 0.982 $\pm$ 0.006∗ | 0.982 $\pm$ 0.006∗ | 0.982 $\pm$ 0.006∗ | 0.982 $\pm$ 0.006∗ | 0.988 $\pm$ 0.004
∗P <0.05 between the current method and TAI-GAN (paired two-tailed t-test). |  |

Quantitative evaluations of real-motion cases are summarized in Table 6. Since
motion ground truth is not available in the real-motion cases, frame
similarity as measured by NMI was calculated to assess motion correction
results. Similar to the motion simulation test, the DL motion correction
achieved higher frame NMI than the BIS method. For the BIS method, the TAI-GAN
conversion improved motion correction the best in all frames and the EQ-1
frame set. For the EQ+1 set, though all the methods produced lower frame NMI
than the original frames, the TAI-GAN achieved the average frame NMI closest
to the original frames and the difference was not significant ($p<0.05$). For
the DL method, the motion correction results without conversion did not show a
significant difference compared with other frame conversion baselines. TAI-GAN
conversion results showed significant improvements compared to all the
baselines.

Table 7: $K_{1}$ and MBF quantification results after BIS or DL motion
correction (mean $\pm$ standard deviation) on the real-motion dataset with the
best results marked in bold.

|  | Mean $K_{1}$ percentage
---
difference (%)
| Mean MBF percentage
---
difference (%)
| Mean fitting
---
error ($\times 10^{-4}$)
Without MC | - | - | 2.53 $\pm$ 2.72∗
BIS | -5.23 $\pm$ 15.52 | -0.56 $\pm$ 7.75 | 3.48 $\pm$ 7.19∗
Vanilla GAN+BIS | -17.61 $\pm$ 11.41 | -6.99 $\pm$ 17.30 | 1.96 $\pm$ 2.70∗
MSE loss GAN+BIS | -20.98 $\pm$ 13.48 | -6.85 $\pm$ 21.87 | 2.53 $\pm$ 3.26∗
TAI-GAN+BIS | -12.20 $\pm$ 12.63 | -6.96 $\pm$ 15.61 | 1.21 $\pm$ 1.98
DL | -21.77 $\pm$ 35.52 | -25.40 $\pm$ 43.95 | 4.07 $\pm$ 5.07∗
Vanilla GAN+DL | -27.42 $\pm$ 32.31 | -33.65 $\pm$ 39.85 | 2.18 $\pm$ 2.55∗
MSE loss GAN+DL | -33.06 $\pm$ 30.47 | -40.91 $\pm$ 34.30 | 1.74 $\pm$ 2.02∗
TAI-GAN+DL | -27.46 $\pm$ 32.36 | -33.16 $\pm$ 37.76 | 1.54 $\pm$ 2.17
∗P $\textless 0.05$ between the current method and TAI-GAN (paired two-tailed
t-test).

Compared to the no motion correction real-motion dataset results, the
parametric fitting error as well as the percentage difference in both $K_{1}$
and MBF are summarized in Table 7. The DL showed more substantial differences
in $K_{1}$ and MBF estimations than BIS. Compared to no conversion motion
correction results, frame conversion also showed a more substantial difference
in both motion correction methods. The TAI-GAN conversion resulted in
significantly reduced fitting errors after either BIS or DL motion correction.

Fig. 7: A comparison of the current motion correction baselines on real-motion
cases, with overlaid RVBP (red), LVBP (blue), and myocardium (green)
segmentation contours and arrows highlighting alignment or mismatch between
the cardiac segmentations and structures.

A visual comparison of all the current motion correction pipelines on the
real-motion dataset is shown in Figure 7. The BIS method failed to correct the
misalignment. When well-trained on the whole-body FDG dataset and then
directly applied to the cardiac dataset, the DL method showed its limitation
in introducing new distortion to the myocardium region. The method of Shi et
al. [58] was able to correct the location-wise misalignment, but the method
was only for translational motion correction, and the shape of the left
ventricle was not perfectly aligned with the myocardium mask outline. Also,
note that Shi et al. trained two separate models for the early and late
frames, resulting in additional time and memory consumption. Among all the
frame-conversion-aided methods, the method of Sundar et al. [64] failed,
producing the most unrealistic motion prediction, possibly due to the errors
in the one-to-one frame conversion method. The TAI-GAN+BIS corrected the
motion in the right ventricle better, while the TAI-GAN+DL corrected the
mismatch in the left ventricle and myocardium better. With TAI-GAN frame
conversion, both the visual performance of BIS and DL motion correction
improved.

###  3.5 Ablation studies of temporal and anatomical information

Fig. 8: Sample results of the ablation study as the evaluation of the
introduced temporal and anatomic information with overlaid RVBP (yellow), LVBP
(orange), and myocardium (red) segmentations.

Figure 8 shows sample results with overlaid cardiac segmentations from the
ablation study as the evaluation of the introduced temporal and anatomic
information. The auxiliary anatomical information provided by the cardiac
masks further improved frame conversion in addition to the MSE loss, but some
of the misrepresentations related to insufficient temporal interdependence
still exist in the conversion results. The introduced temporal input informed
the model effectively with the kinetics information, especially improving
model performance in post-EQ frames, but it is noted that due to the lack of
anatomical information, for pre-EQ frame samples, the model might misidentify
the RVBP as LVBP and then cause incorrect myocardium prediction.

Table 8 summarizes the quantitative assessments of the complete ablation
studies. The anatomical information provided by the rough segmentation masks
showed substantial improvement in both all frames and all pre-EQ frame test
sets. The temporal information introduced by TACs and the FiLM model further
improved SSIM and PSNR on all the frames compared to MSE loss GAN, although on
all the pre-EQ frames the performance dropped possibly due to the lack of
anatomical guidance. With the combined auxiliary anatomical and temporal
information, the proposed TAI-GAN achieved the best performance.

Table 8: Quantitative image similarity evaluation results (mean $\pm$ standard
deviation) of the ablation study of the introduced temporal and anatomic
information with the best results marked in bold.

Test set | Metric | Vanilla GAN | MSE loss | MSE loss+Mask | MSE loss+FiLM |  | MSE loss+Mask+FiLM
---
(Proposed TAI-GAN)
All Pre-EQ frames | NMAE | 0.072 $\pm$ 0.007∗ | 0.066 $\pm$ 0.011 | 0.065 $\pm$ 0.008∗ | 0.079 $\pm$ 0.009∗ | 0.062 $\pm$ 0.008
MSE | 0.063 $\pm$ 0.010∗ | 0.053 $\pm$ 0.016 | 0.049 $\pm$ 0.010∗ | 0.081 $\pm$ 0.014∗ | 0.046 $\pm$ 0.009
SSIM | 0.594 $\pm$ 0.012∗ | 0.596 $\pm$ 0.047∗ | 0.621 $\pm$ 0.033 | 0.587 $\pm$ 0.021∗ | 0.627 $\pm$ 0.025
PSNR | 18.51 $\pm$ 0.47∗ | 19.27 $\pm$ 1.04∗ | 19.63 $\pm$ 0.72 | 17.42 $\pm$ 0.85∗ | 19.83 $\pm$ 0.74
All frames | NMAE | 0.047 $\pm$ 0.004∗ | 0.044 $\pm$ 0.002 | 0.042 $\pm$ 0.002 | 0.045 $\pm$ 0.003∗ | 0.040 $\pm$ 0.002
MSE | 0.027 $\pm$ 0.002∗ | 0.024 $\pm$ 0.003 | 0.021 $\pm$ 0.002 | 0.026 $\pm$ 0.003∗ | 0.021 $\pm$ 0.002
SSIM | 0.708 $\pm$ 0.010∗ | 0.716 $\pm$ 0.007∗ | 0.720 $\pm$ 0.015∗ | 0.723 $\pm$ 0.018∗ | 0.733 $\pm$ 0.018
PSNR | 22.80 $\pm$ 0.53∗ | 23.24 $\pm$ 0.34∗ | 23.57 $\pm$ 0.28 | 23.40 $\pm$ 0.36 | 23.80 $\pm$ 0.47
∗P <0.05 between the current method and TAI-GAN (subject-wise paired two-tailed t-test). |

##  4 Discussion

In this study, we propose the Temporally and Anatomically Informed GAN (TAI-
GAN), a new framework that uses an all-to-one mapping method to translate the
appearance of all early frames into the last reference frame to tackle the
tracer discrepancy problem in cardiac dynamic PET motion correction. We use a
FiLM layer to encode tracer kinetics-related temporal information and rough
cardiac structural segmentations to provide anatomical guidance. We evaluated
TAI-GAN in terms of frame conversion similarity, motion correction accuracy,
and MBF quantification errors using the five-fold cross-validation. On the
clinical 82Rb PET dataset, the TAI-GAN achieved desirable frame conversion and
improved current motion correction methods, as well as the downstream clinical
MBF quantification.

Currently, the anatomical information is provided by the cardiac ROIs as an
additional input channel. Note that in the current workflow, the need for
cardiac ROIs did not introduce additional labor since these cardiac
segmentations are already required in MBF quantification and constitute an
essential part of the current clinical workflow. In future work, we will
further automate this step by applying existing automatic labeling using the
clinical software 4DM (INVIA, Ann Arbor, Michigan; Ficaro et al. [15]) or deep
learning segmentation models. Given the challenge of acquiring manual dense
annotations as the labels for fully supervised training, weakly-supervised
models have been widely investigated in the field of medical image
segmentation [66, 18]. Also, utilizing non-contrast CT images as additional
guidance is another future direction to achieve a segmentation-free method.

Another potential limitation of the current work is that the frame conversion
method is developed using a clinical dataset that is identified by clinicians
as nearly motion-free. Since the cardiac ROIs are segmented based on the last
reference frame, the mismatch between the last frame ROI and the early frames
might introduce errors in frame conversion if motion is present. To overcome
this problem, we implemented random translation of cardiac ROIs during
training. Thus, the network is trained to handle any present mismatch between
the cardiac ROIs and the dynamic frames and only takes the anatomical input as
auxiliary guidance instead of fully relying on that information. This is
particularly useful in distinguishing between the early RV and LV phases and
preventing the model from predicting myocardium structure near the RV instead
of LV. Also, the residual minimal motion in the nearly motion-free dataset
might introduce errors in the motion simulation tests. Further investigations
including simulation studies on phantoms with motion ground truth are
warranted.

A comparison of the memory footprint and the average training time for each
frame conversion method is summarized in Supplementary Table S1. The average
training time for all the mappings needed to convert a whole sequence using
the vanilla GAN one-to-one model is the longest among all the frame conversion
methods and is 10 times longer than the all-to-one mapping methods, making it
infeasible to implement in practice. The training time of the TAI-GAN is still
comparable to the other two baselines, indicating the efficiency of the
incorporation of temporal and anatomical information. With an additional
channel, the memory footprint of the TAI-GAN is 1.5 times of other baselines.

There are several limitations and future directions of this study. First, this
method is implemented as a post-reconstruction method, taking only the inter-
frame motion into consideration. The attenuation mismatch and intra-frame
motion also degrade the quality of the reconstructed frames and introduce
errors to the MBF quantification. Future work includes correcting intra-frame
and attenuation mismatches in the workflow. Second, the current work only
includes ROI-based MBF quantification as clinical analysis. A future direction
for clinical-centric evaluation is validating the downstream clinical impact
using invasive catheterization as the clinical gold standard. Including post
hoc analysis of diagnostic accuracy and clinical experts’ reading reports is
also worth further investigation. Third, current predictions of the late
frames serve as the intermediate results as the input to the following motion
correction step. These outputs have comparable visual characteristics to the
real late frames but do not represent the actual tracer activities. This is
due to the intensity normalization in model training to benefit the
optimization process. Future work includes directly predicting motion-
compensated late frames with the actual intensities. This will reduce scan
time and further simplify the current protocol. Besides, currently, temporal
information is sent to the generator indirectly through encoding and FiLM.
Future work will investigate introducing more direct kinetics-based
optimization [23, 22] to the network to provide more realistic predictions.
Finally, we will investigate other advanced generative backbone structures
such as diffusion models [26] and neural ordinary differential equations [7]
to further improve conversion performance.

##  5 Conclusion

In conclusion, we propose a novel Temporally and Anatomically Informed GAN
(TAI-GAN) as an all-to-one mapping method to convert all the early frames to
the last frame to address the challenge of fast tracer distribution change in
cardiac dynamic PET inter-frame motion correction. The tracer kinetics-related
temporal information is incorporated by a FiLM layer into the generator
bottleneck, and cardiac segmentations are concatenated with the early frame
for network input to provide anatomical guidance. Under a 5-fold cross-
validation on the clinical 82Rb cardiac dataset, the TAI-GAN achieved
desirable frame conversion results with comparable visual quality to the real
late frames and the highest quantitative frame similarity measurements. In
both a motion simulation test and a real motion evaluation, the proposed TAI-
GAN increased the prediction accuracy of current motion correction methods and
demonstrated improvement in the MBF quantification.

## Declaration of competing interests

Bruce Spottiswoode is an employee of Siemens Medical Solutions USA, Inc. There
are no additional financial conflicts of interest that may be relevant to this
paper.

## CRediT authorship contribution statement

Xueqi Guo: Conceptualization, Methodology, Software, Visualization,
Validation, Formal analysis, Investigation, Data Curation, Writing - original
draft, review & editing. Luyao Shi: Data Curation, Visualization, Writing -
review & editing. Xiongchao Chen: Data Curation, Validation, Writing - review
& editing. Qiong Liu: Methodology, Writing - review & editing. Bo Zhou:
Methodology, Writing - review & editing. Huidong Xie: Methodology, Writing -
review & editing. Yi-Hwa Liu: Data Curation, Writing - review & editing.
Richard Palyo: Data Curation, Writing - review & editing. Edward J. Miller:
Writing - review & editing. Albert J. Sinusas: Writing - review & editing.
Lawrence Staib: Writing - review & editing. Bruce Spottiswoode:
Conceptualization, Writing - review & editing, Funding acquisition. Chi Liu:
Conceptualization, Methodology, Writing - review & editing, Supervision,
Funding acquisition. Nicha C. Dvornek: Conceptualization, Methodology, Writing
- review & editing, Supervision.

## Acknowledgments

This work was supported by the National Institutes of Health (NIH) under grant
R01 CA224140.

An early version of this work was initially accepted for publication by
Springer Nature at SASHIMI: Simulation and Synthesis in Medical Imaging, a
workshop of the International Conference on Medical Image Computing and
Computer-Assisted Intervention (MICCAI) 2023 [19]. Here, we included a more
comprehensive analysis of the complete evaluation using simulated motion and
ablation studies, a comparison of the conventional non-rigid and deep
learning-based motion correction methods, an evaluation of an independent
cohort of real-patient motion cases, additional background and implementation
details, and in-depth discussions considering the viability of clinical use
and prospective future directions.

## References

  * Abu-Srhan et al. [2021] Abu-Srhan, A., Almallahi, I., Abushariah, M.A., Mahafza, W., Al-Kadi, O.S., 2021.  Paired-unpaired unsupervised attention guided gan with transfer learning for bidirectional brain mr-ct synthesis.  Computers in Biology and Medicine 136, 104763.
  * Ak et al. [2019] Ak, K.E., Lim, J.H., Tham, J.Y., Kassim, A., 2019.  Semantically consistent hierarchical text to fashion image synthesis with an enhanced-attentional generative adversarial network, in: 2019 IEEE/CVF International Conference on Computer Vision Workshop (ICCVW), IEEE. pp. 3121–3124.
  * Ak et al. [2020] Ak, K.E., Lim, J.H., Tham, J.Y., Kassim, A.A., 2020.  Semantically consistent text to fashion image synthesis with an enhanced attentional generative adversarial network.  Pattern Recognition Letters 135, 22–29.
  * Burckhardt [2009] Burckhardt, D.D., 2009.  Cardiac positron emission tomography: Overview of myocardial perfusion, myocardial blood flow and coronary flow reserve imaging.  Mol. Imag .
  * Cao et al. [2018] Cao, X., Yang, J., Gao, Y., Wang, Q., Shen, D., 2018.  Region-adaptive deformable registration of ct/mri pelvic images via learning-based image synthesis.  IEEE Transactions on Image Processing 27, 3500–3512.
  * Chen et al. [2017] Chen, M., Carass, A., Jog, A., Lee, J., Roy, S., Prince, J.L., 2017.  Cross contrast multi-channel image registration using image synthesis for mr brain images.  Medical image analysis 36, 2–14.
  * Chen et al. [2018] Chen, R.T., Rubanova, Y., Bettencourt, J., Duvenaud, D.K., 2018.  Neural ordinary differential equations.  Advances in neural information processing systems 31.
  * Chen et al. [2022] Chen, X., Zhou, B., Xie, H., Shi, L., Liu, H., Holler, W., Lin, M., Liu, Y.H., Miller, E.J., Sinusas, A.J., et al., 2022.  Direct and indirect strategies of deep-learning-based attenuation correction for general purpose and dedicated cardiac spect.  European Journal of Nuclear Medicine and Molecular Imaging 49, 3046–3060.
  * Çiçek et al. [2016] Çiçek, Ö., Abdulkadir, A., Lienkamp, S.S., Brox, T., Ronneberger, O., 2016.  3d u-net: learning dense volumetric segmentation from sparse annotation, in: Medical Image Computing and Computer-Assisted Intervention–MICCAI 2016: 19th International Conference, Athens, Greece, October 17-21, 2016, Proceedings, Part II 19, Springer. pp. 424–432.
  * Crone [1963] Crone, C., 1963.  The permeability of capillaries in various organs as determined by use of the ‘indicator diffusion’method.  Acta physiologica scandinavica 58, 292–305.
  * Dar et al. [2019] Dar, S.U., Yurt, M., Karacan, L., Erdem, A., Erdem, E., Cukur, T., 2019.  Image synthesis in multi-contrast mri with conditional generative adversarial networks.  IEEE transactions on medical imaging 38, 2375–2388.
  * Dey et al. [2021] Dey, N., Ren, M., Dalca, A.V., Gerig, G., 2021.  Generative adversarial registration for improved conditional deformable templates, in: Proceedings of the IEEE/CVF international conference on computer vision, pp. 3929–3941.
  * Dvornek et al. [2017] Dvornek, N.C., Ventola, P., Pelphrey, K.A., Duncan, J.S., 2017.  Identifying autism from resting-state fmri using long short-term memory networks, in: International Workshop on Machine Learning in Medical Imaging, Springer. pp. 362–370.
  * Feng et al. [2017] Feng, T., Wang, J., Sun, Y., Zhu, W., Dong, Y., Li, H., 2017.  Self-gating: an adaptive center-of-mass approach for respiratory gating in pet.  IEEE transactions on medical imaging 37, 1140–1148.
  * Ficaro et al. [2007] Ficaro, E.P., Lee, B.C., Kritzman, J.N., Corbett, J.R., 2007.  Corridor4dm: the michigan method for quantitative nuclear cardiology.  Journal of nuclear cardiology 14, 455–465.
  * Germino et al. [2016] Germino, M., Ropchan, J., Mulnix, T., Fontaine, K., Nabulsi, N., Ackah, E., Feringa, H., Sinusas, A.J., Liu, C., Carson, R.E., 2016.  Quantification of myocardial blood flow with 82 rb: Validation with 15 o-water using time-of-flight and point-spread-function modeling.  EJNMMI research 6, 1–12.
  * Goodfellow et al. [2020] Goodfellow, I., Pouget-Abadie, J., Mirza, M., Xu, B., Warde-Farley, D., Ozair, S., Courville, A., Bengio, Y., 2020.  Generative adversarial networks.  Communications of the ACM 63, 139–144.
  * Guo et al. [2023a] Guo, X., Abdi, M., Shinagawa, Y., Jerebko, A., Farhand, S., 2023a.  Seam-stress: A weakly supervised framework for interstitial lung disease segmentation in chest ct, in: 2023 IEEE 20th International Symposium on Biomedical Imaging (ISBI), IEEE. pp. 1–4.
  * Guo et al. [2023b] Guo, X., Shi, L., Chen, X., Zhou, B., Liu, Q., Xie, H., Liu, Y.H., Palyo, R., Miller, E.J., Sinusas, A.J., et al., 2023b.  Tai-gan: Temporally and anatomically informed gan for early-to-late frame conversion in dynamic cardiac pet motion correction.
  * Guo et al. [2022a] Guo, X., Tinaz, S., Dvornek, N.C., 2022a.  Characterization of early stage parkinson’s disease from resting-state fmri data using a long short-term memory network.  Frontiers in Neuroimaging 1, 952084.
  * Guo et al. [2022b] Guo, X., Wu, J., Chen, M.K., Liu, Q., Onofrey, J.A., Pucar, D., Pang, Y., Pigg, D., Casey, M.E., Dvornek, N.C., et al., 2022b.  Inter-pass motion correction for whole-body dynamic pet and parametric imaging.  IEEE Transactions on Radiation and Plasma Medical Sciences 7, 344–353.
  * Guo et al. [2023c] Guo, X., Zhou, B., Chen, X., Chen, M.K., Liu, C., Dvornek, N.C., 2023c.  Mcp-net: Introducing patlak loss optimization to whole-body dynamic pet inter-frame motion correction.  IEEE Transactions on Medical Imaging .
  * Guo et al. [2022c] Guo, X., Zhou, B., Chen, X., Liu, C., Dvornek, N.C., 2022c.  Mcp-net: Inter-frame motion correction with patlak regularization for whole-body dynamic pet, in: Medical Image Computing and Computer Assisted Intervention–MICCAI 2022: 25th International Conference, Singapore, September 18–22, 2022, Proceedings, Part IV, Springer. pp. 163–172.
  * Guo et al. [2022d] Guo, X., Zhou, B., Pigg, D., Spottiswoode, B., Casey, M.E., Liu, C., Dvornek, N.C., 2022d.  Unsupervised inter-frame motion correction for whole-body dynamic pet using convolutional long short-term memory in a convolutional neural network.  Medical Image Analysis 80, 102524.  doi:10.1016/j.media.2022.102524.
  * Guo et al. [2019] Guo, Y., Dvornek, N., Lu, Y., Tsai, Y.J., Hamill, J., Casey, M., Liu, C., 2019.  Deep learning based respiratory pattern classification and applications in pet/ct motion correction, in: 2019 IEEE Nuclear Science Symposium and Medical Imaging Conference (NSS/MIC), IEEE. pp. 1–5.
  * Ho et al. [2020] Ho, J., Jain, A., Abbeel, P., 2020.  Denoising diffusion probabilistic models.  Advances in neural information processing systems 33, 6840–6851.
  * Hochreiter and Schmidhuber [1997] Hochreiter, S., Schmidhuber, J., 1997.  Long short-term memory.  Neural computation 9, 1735–1780.
  * Hunter et al. [2016] Hunter, C.R., Klein, R., Beanlands, R.S., deKemp, R.A., 2016.  Patient motion effects on the quantification of regional myocardial blood flow with dynamic pet imaging.  Medical physics 43, 1829–1840.
  * Iglesias et al. [2013] Iglesias, J.E., Konukoglu, E., Zikic, D., Glocker, B., Van Leemput, K., Fischl, B., 2013.  Is synthesizing mri contrast useful for inter-modality analysis?, in: Medical Image Computing and Computer-Assisted Intervention–MICCAI 2013: 16th International Conference, Nagoya, Japan, September 22-26, 2013, Proceedings, Part I 16, Springer. pp. 631–638.
  * Isola et al. [2017] Isola, P., Zhu, J.Y., Zhou, T., Efros, A.A., 2017.  Image-to-image translation with conditional adversarial networks, in: Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 1125–1134.
  * Jiao et al. [2014] Jiao, J., Searle, G.E., Tziortzi, A.C., Salinas, C.A., Gunn, R.N., Schnabel, J.A., 2014.  Spatio-temporal pharmacokinetic model based registration of 4d pet neuroimaging data.  Neuroimage 84, 225–235.
  * Joshi et al. [2011] Joshi, A., Scheinost, D., Okuda, H., Belhachemi, D., Murphy, I., Staib, L.H., Papademetris, X., 2011.  Unified framework for development, deployment and robust testing of neuroimaging algorithms.  Neuroinformatics 9, 69–84.
  * Lan et al. [2021] Lan, H., Initiative, A.D.N., Toga, A.W., Sepehrband, F., 2021.  Three-dimensional self-attention conditional gan with spectral normalization for multimodal neuroimaging synthesis.  Magnetic resonance in medicine 86, 1718–1733.
  * Lee et al. [2016] Lee, B., Moody, J., Murthy, V., Corbett, J., Ficaro, E., 2016.  Image-based motion correction of the blood pool phase of dynamic pet data using blood pool isolation.
  * Lee et al. [2020] Lee, B.C., Moody, J.B., Poitrasson-Rivière, A., Melvin, A.C., Weinberg, R.L., Corbett, J.R., Murthy, V.L., Ficaro, E.P., 2020.  Automated dynamic motion correction using normalized gradient fields for 82 rubidium pet myocardial blood flow quantification.  Journal of Nuclear Cardiology 27, 1982–1998.
  * Lei et al. [2019] Lei, Y., Harms, J., Wang, T., Liu, Y., Shu, H.K., Jani, A.B., Curran, W.J., Mao, H., Liu, T., Yang, X., 2019.  Mri-only based synthetic ct generation using dense cycle consistent generative adversarial networks.  Medical physics 46, 3565–3581.
  * Li et al. [2021] Li, J., Wang, Y., Yang, Y., Zhang, X., Qu, Z., Hu, S., 2021.  Small animal pet to ct image synthesis based on conditional generation network, in: 2021 14th International Congress on Image and Signal Processing, BioMedical Engineering and Informatics (CISP-BMEI), IEEE. pp. 1–6.
  * Liu et al. [2019] Liu, X., Jiang, D., Wang, M., Song, Z., 2019.  Image synthesis-based multi-modal image registration framework by using deep fully convolutional networks.  Medical & Biological Engineering & Computing 57, 1037–1048.
  * Lu et al. [2018] Lu, Y., Fontaine, K., Mulnix, T., Onofrey, J.A., Ren, S., Panin, V., Jones, J., Casey, M.E., Barnett, R., Kench, P., et al., 2018.  Respiratory motion compensation for pet/ct with motion information derived from matched attenuation-corrected gated pet data.  Journal of nuclear Medicine 59, 1480–1486.
  * Lu et al. [2019] Lu, Y., Gallezot, J.D., Naganawa, M., Ren, S., Fontaine, K., Wu, J., Onofrey, J.A., Toyonaga, T., Boutagy, N., Mulnix, T., et al., 2019.  Data-driven voluntary body motion detection and non-rigid event-by-event correction for static and dynamic pet.  Physics in Medicine & Biology 64, 065002.
  * Lu and Liu [2020] Lu, Y., Liu, C., 2020.  Patient motion correction for dynamic cardiac pet: Current status and challenges.  Journal of Nuclear Cardiology 27, 1999–2002.
  * Lu et al. [2020] Lu, Y., Naganawa, M., Toyonaga, T., Gallezot, J.D., Fontaine, K., Ren, S., Revilla, E.M., Mulnix, T., Carson, R.E., 2020.  Data-driven motion detection and event-by-event correction for brain pet: Comparison with vicra.  Journal of Nuclear Medicine 61, 1397–1403.
  * Mao et al. [2019] Mao, X., Chen, Y., Li, Y., Xiong, T., He, Y., Xue, H., 2019.  Bilinear representation for language-based image editing using conditional generative adversarial networks, in: ICASSP 2019-2019 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), IEEE. pp. 2047–2051.
  * Maul et al. [2021] Maul, J., Said, S., Ruiter, N., Hopp, T., 2021.  X-ray synthesis based on triangular mesh models using gpu-accelerated ray tracing for multi-modal breast image registration, in: Simulation and Synthesis in Medical Imaging: 6th International Workshop, SASHIMI 2021, Held in Conjunction with MICCAI 2021, Strasbourg, France, September 27, 2021, Proceedings 6, Springer. pp. 87–96.
  * Miao et al. [2023] Miao, T., Zhou, B., Liu, J., Guo, X., Liu, Q., Xie, H., Chen, X., Chen, M.K., Wu, J., Carson, R.E., et al., 2023.  Generation of whole-body fdg parametric ki images from static pet images using deep learning.  IEEE Transactions on Radiation and Plasma Medical Sciences .
  * Mourik et al. [2009] Mourik, J.E., Lubberink, M., van Velden, F.H., Lammertsma, A.A., Boellaard, R., 2009.  Off-line motion correction methods for multi-frame pet data.  European journal of nuclear medicine and molecular imaging 36, 2002–2013.
  * Noonan et al. [2015] Noonan, P., Howard, J., Hallett, W., Gunn, R., 2015.  Repurposing the microsoft kinect for windows v2 for external head motion tracking for brain pet.  Physics in Medicine & Biology 60, 8753.
  * Perez et al. [2018] Perez, E., Strub, F., De Vries, H., Dumoulin, V., Courville, A., 2018.  Film: Visual reasoning with a general conditioning layer, in: Proceedings of the AAAI Conference on Artificial Intelligence.
  * Prior et al. [2012] Prior, J.O., Allenbach, G., Valenta, I., Kosinski, M., Burger, C., Verdun, F.R., Bischof Delaloye, A., Kaufmann, P.A., 2012.  Quantification of myocardial blood flow with 82 rb positron emission tomography: clinical validation with 15 o-water.  European journal of nuclear medicine and molecular imaging 39, 1037–1047.
  * Rachmadi et al. [2019] Rachmadi, M.F., del C. Valdés-Hernández, M., Makin, S., Wardlaw, J.M., Komura, T., 2019.  Predicting the evolution of white matter hyperintensities in brain mri using generative adversarial networks and irregularity map, in: Medical Image Computing and Computer Assisted Intervention–MICCAI 2019: 22nd International Conference, Shenzhen, China, October 13–17, 2019, Proceedings, Part III, Springer. pp. 146–154.
  * Ren et al. [2017] Ren, S., Jin, X., Chan, C., Jian, Y., Mulnix, T., Liu, C., Carson, R.E., 2017.  Data-driven event-by-event respiratory motion correction using tof pet list-mode centroid of distribution.  Physics in Medicine & Biology 62, 4741.
  * Renkin [1955] Renkin, E.M., 1955.  Effects of blood flow on diffusion kinetics in isolated, perfused hindlegs of cats: a double circulation hypothesis.  American Journal of Physiology-Legacy Content 183, 125–136.
  * Renkin [1959] Renkin, E.M., 1959.  Transport of potassium-42 from blood to tissue in isolated mammalian skeletal muscles.  American Journal of Physiology-Legacy Content 197, 1205–1210.
  * Roy et al. [2014] Roy, S., Carass, A., Jog, A., Prince, J.L., Lee, J., 2014.  Mr to ct registration of brains using image synthesis, in: Medical Imaging 2014: Image Processing, SPIE. pp. 307–314.
  * Rubeaux et al. [2017] Rubeaux, M., Doris, M.K., Alessio, A., Slomka, P.J., 2017.  Enhancing cardiac pet by motion correction techniques.  Current cardiology reports 19, 1–8.
  * Sciagrà et al. [2021] Sciagrà, R., Lubberink, M., Hyafil, F., Saraste, A., Slart, R.H., Agostini, D., Nappi, C., Georgoulias, P., Bucerius, J., Rischpler, C., et al., 2021.  Eanm procedural guidelines for pet/ct quantitative myocardial perfusion imaging.  European Journal of Nuclear Medicine and Molecular Imaging 48, 1040–1069.
  * Sevetlidis et al. [2016] Sevetlidis, V., Giuffrida, M.V., Tsaftaris, S.A., 2016.  Whole image synthesis using a deep encoder-decoder network, in: Simulation and Synthesis in Medical Imaging: First International Workshop, SASHIMI 2016, Held in Conjunction with MICCAI 2016, Athens, Greece, October 21, 2016, Proceedings 1, Springer. pp. 127–137.
  * Shi et al. [2021] Shi, L., Lu, Y., Dvornek, N., Weyman, C.A., Miller, E.J., Sinusas, A.J., Liu, C., 2021.  Automatic inter-frame patient motion correction for dynamic cardiac pet using deep learning.  IEEE Transactions on Medical Imaging .
  * Shi et al. [2019a] Shi, L., Lu, Y., Wu, J., Gallezot, J.D., Boutagy, N., Thorn, S., Sinusas, A.J., Carson, R.E., Liu, C., 2019a.  Direct list mode parametric reconstruction for dynamic cardiac spect.  IEEE transactions on medical imaging 39, 119–128.
  * Shi et al. [2020] Shi, L., Onofrey, J.A., Liu, H., Liu, Y.H., Liu, C., 2020.  Deep learning-based attenuation map generation for myocardial perfusion spect.  European Journal of Nuclear Medicine and Molecular Imaging 47, 2383–2395.
  * Shi et al. [2019b] Shi, L., Onofrey, J.A., Revilla, E.M., Toyonaga, T., Menard, D., Ankrah, J., Carson, R.E., Liu, C., Lu, Y., 2019b.  A novel loss function incorporating imaging acquisition physics for pet attenuation map generation using deep learning, in: Medical Image Computing and Computer Assisted Intervention–MICCAI 2019: 22nd International Conference, Shenzhen, China, October 13–17, 2019, Proceedings, Part IV 22, Springer. pp. 723–731.
  * Shi et al. [2022] Shi, L., Zhang, J., Toyonaga, T., Shao, D., Onofrey, J.A., Lu, Y., 2022.  Deep learning-based attenuation map generation with simultaneously reconstructed pet activity and attenuation and low-dose application.  Physics in Medicine and Biology .
  * Sun et al. [2022] Sun, T., Wu, Y., Bai, Y., Wang, Z., Shen, C., Wang, W., Li, C., Hu, Z., Liang, D., Liu, X., et al., 2022.  An iterative image-based inter-frame motion compensation method for dynamic brain pet imaging.  Physics in Medicine & Biology 67, 035012.
  * Sundar et al. [2021a] Sundar, L.K.S., Iommi, D., Muzik, O., Chalampalakis, Z., Klebermass, E.M., Hienert, M., Rischka, L., Lanzenberger, R., Hahn, A., Pataraia, E., et al., 2021a.  Conditional generative adversarial networks aided motion correction of dynamic 18f-fdg pet brain studies.  Journal of Nuclear Medicine 62, 871–879.
  * Sundar et al. [2021b] Sundar, L.S., Iommi, D., Spencer, B., Wang, Q., Cherry, S., Beyer, T., Badawi, R., 2021b.  Data-driven motion compensation using cgan for total-body [18f] fdg-pet imaging.
  * Wang et al. [2019] Wang, C., Moriya, T., Hayashi, Y., Roth, H., Lu, L., Oda, M., Ohkubo, H., Mori, K., 2019.  Weakly-supervised deep learning of interstitial lung disease types on ct images, in: Medical Imaging 2019: Computer-Aided Diagnosis, SPIE. pp. 373–379.
  * Wang et al. [2021] Wang, R., Liu, H., Toyonaga, T., Shi, L., Wu, J., Onofrey, J.A., Tsai, Y.J., Naganawa, M., Ma, T., Liu, Y., et al., 2021.  Generation of synthetic pet images of synaptic density and amyloid from 18f-fdg images using deep learning.  Medical physics 48, 5115–5129.
  * Woo et al. [2011] Woo, J., Tamarappoo, B., Dey, D., Nakazato, R., Le Meunier, L., Ramesh, A., Lazewatsky, J., Germano, G., Berman, D.S., Slomka, P.J., 2011.  Automatic 3d registration of dynamic stress and rest 82rb and flurpiridaz f 18 myocardial perfusion pet data for patient motion detection and correction.  Medical physics 38, 6313–6326.
  * Xiao et al. [2020] Xiao, H., Ren, G., Cai, J., 2020.  A review on 3d deformable image registration and its application in dose warping.  Radiation Medicine and Protection 1, 171–178.
  * Yu et al. [2018] Yu, B., Zhou, L., Wang, L., Fripp, J., Bourgeat, P., 2018.  3d cgan based cross-modality mr image synthesis for brain tumor segmentation, in: 2018 IEEE 15th international symposium on biomedical imaging (ISBI 2018), IEEE. pp. 626–630.
  * Zhou et al. [2021] Zhou, B., Tsai, Y.J., Chen, X., Duncan, J.S., Liu, C., 2021.  Mdpet: A unified motion correction and denoising adversarial network for low-dose gated pet.  IEEE Transactions on Medical Imaging .
  * Zhou et al. [2023] Zhou, B., Tsai, Y.J., Zhang, J., Guo, X., Xie, H., Chen, X., Miao, T., Lu, Y., Duncan, J.S., Liu, C., 2023.  Fast-mc-pet: A novel deep learning-aided motion correction and reconstruction framework for accelerated pet.  arXiv preprint arXiv:2302.07135 .
  * Zhou et al. [2020] Zhou, T., Fu, H., Chen, G., Shen, J., Shao, L., 2020.  Hi-net: hybrid-fusion network for multi-modal mr image synthesis.  IEEE transactions on medical imaging 39, 2772–2781.

## Supplementary Material

Table S1: A comparison of the memory footprint and the average training time
for each frame conversion method.

Method |  | Memory
---
footprint (MB)
| Average training time for
---
all frame conversions (min)
| Vanilla GAN
---
one-to-one
2671 | 780
Vanilla GAN | 2671 | 89
MSE loss GAN | 2671 | 78
TAI-GAN (Proposed) | 3759 | 98


ifaamas [AAMAS ’22]Proc. of the 21st International Conference on Autonomous
Agents and Multiagent Systems (AAMAS 2022)May 9–13, 2022 OnlineP. Faliszewski,
V. Mascardi, C. Pelachaud, M.E. Taylor (eds.) 2022 2022 1 Faculty of
Mathematics and Computer Science, Nicolaus Copernicus University, Toruń,
Poland 2 Institute of Computer Science, Polish Academy of Sciences, Warsaw,
Poland 3 Interdisciplinary Centre for Security, Reliability and Trust, SnT,
University of Luxembourg, Luxembourg

# Towards Assume-Guarantee Verification of Strategic Ability

Extended Abstract

Łukasz Mikulski1,2, Wojciech Jamroga2,3, and Damian Kurpiewski2,1
<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

Formal verification of strategic abilities is a hard problem. We propose to
use the methodology of assume-guarantee reasoning in order to facilitate model
checking of alternating-time temporal logic with imperfect information and
imperfect recall.

###### Key words and phrases:

model checking, assume-guarantee reasoning, strategic ability

##  1\. Introduction

_Alternating-time temporal logic_ $\mathbf{ATL_{\mathrm{}}^{*}}$ Alur97ATL ;
Alur02ATL ; Schobbens04ATL  and _Strategy Logic_ $\mathbf{SL}$
Chatterjee10strategylogic ; Mogavero14behavioral  provide powerful tools to
reason about strategic aspects of MAS. Specifications in agent logics can be
used as input to algorithms and tools for _model checking_ Alur98mocha-cav ;
Chen13prismgames ; Busard14improving ; Huang14symbolic-epist ;
Cermak14mcheckSL ; Lomuscio17mcmas ; Cermak15mcmas-sl-one-goal ;
Belardinelli17publicActions ; Belardinelli17broadcasting ;
Jamroga19fixpApprox-aij ; Kurpiewski21stv-demo . However, verification of
strategic abilities suffers both from state-space and strategy-space
explosion. Even for the more restricted logic $\mathbf{ATL_{\mathrm{}}}$,
model checking of its imperfect information variants ranges from
$\mathbf{{\Delta_{{2}}^{\mathbf{{P}}}}}$–complete to undecidable
Bulling10verification ; Jamroga06atlir-eumas ; Schobbens04ATL ;
Dima11undecidable ; Guelev11atl-distrknowldge .

In this paper, we make the first step towards compositional model checking of
strategic properties in asynchronous multi-agent systems with imperfect
information and imperfect recall. To this end, we creatively expand the
assume-guarantee framework of Lomuscio10assGar ; Lomuscio13assGar . Instead of
searching through the states and strategies of the entire model, we
“factorize” it and perform most of the search locally, using _assume-guarantee
reasoning_ Pnueli84assGuar ; Clarke89assGuar . We illustrate the approach by
means of a simple voting scenario. Finally, we evaluate the practical gains
through verification experiments.

Related work. Compositional verification dates back to Hoare69axiomatic ;
Owicki76relyGuar ; Jones83relyGuar , and has been intensively studied for
temporal specifications Pnueli84assGuar ; Clarke89assGuar ; Henzinger98assGuar
; Devereux03compositionalRA ; Kwiatkowska10assGuar ; Lomuscio10assGar ;
Lomuscio13assGar ; Fijalkow20assGuar . Our approach is based on
Lomuscio10assGar ; Lomuscio13assGar , where assume-guarantee rules were
defined for liveness properties of MAS. A related scheme for
$\mathbf{ATL_{\mathrm{}}}$ with perfect information strategies and aspect-
oriented programs was considered in Devereux03compositionalRA .

##  2\. Models of Concurrent MAS

We use the MAS representations of Lomuscio10assGar ; Lomuscio13assGar , which
allow for asynchronous and synchronous composition of local transitions.

Modules. Let $D$ be a domain (for all variables used in the system). For any
set of variables $X$, let $D^{X}$ be a set of all valuation functions on $X$.
We follow Lomuscio13assGar , and divide the variables in a module into _state
variables_ and _input variables_. An agent can read and modify only its state
variables. The input variables are not a part of its state, but their values
limit the set of executable transitions.

######  Definition  (Module Lomuscio13assGar ).

A _module_ is $M=(X,I,Q,T,\lambda,q_{0})$, where: $X,I$ are finite sets of
state and input variables, respectively, with $X\cap I=\varnothing$; $Q$ is a
finite set of states; $\lambda:Q\to D^{X}$ labels each state with a valuation
of the state variables; $q_{0}\in Q$ is the initial state; $T\subseteq Q\times
D^{I}\times Q$ is a transition relation. We require that if
$(q,\alpha,q^{\prime})\in T,q\neq q^{\prime}$, then $(q,\alpha,q)\notin T$,
and for each pair $(q,\alpha)\in Q\times D^{I}$ there exists $q^{\prime}\in Q$
such that $(q,\alpha,q^{\prime})\in T$.

$?,?,?$start$1,?,?$$2,?,?$$1,1,?$$1,!,?$$2,!,?$$2,2,?$$1,1,T$$1,1,F$$1,!,F$$1,!,T$$2,!,T$$2,!,F$$2,2,F$$2,2,T$$\forall$$\forall$$\forall$$\forall$$\forall$$\forall$$T$$F$$F$$T$$T$$F$$F$$T$$?$$?$$?$$?$$\forall$$\forall$$\forall$$\forall$$\forall$$\forall$$\forall$$\forall$
---

Figure 1. Module of a voter deciding between two candidates

Basic modules of a voter and a coercer used in the leading example.

###### Example

We use a voting scenario, inspired by Jamroga19fixpApprox-aij ; JPSDM20 ,
consisting of modules $M^{(1)},\dots,M^{(n)}$ of voters and $M^{(c)}$ of a
coercer.

Every voter has three local variables in $X^{(i)}$: $vote^{(i)}$: the vote
being cast ($?,1$, or $2$); $reported^{(i)}$: the vote value presented to the
coercer ($?,1,2$ or $!$), where $!$ means that the voter decided not to show
her vote; $pstatus^{(i)}$: the punishment status ($?,T$ or $F$). Moreover,
$I^{(i)}$ consists of variable $pun^{(i)}$ controlled by the coercer. The
voter first casts her vote, then decides whether to share its value with the
coercer. Finally, she waits for the coercer’s decision to punish her or to
refrain from punishment. The module is shown in Figure 1.

The coercer has two available actions per voter: to punish the voter or to
refrain from punishment. He can execute them in any order, but only after the
respective voters decide to share or not.

Modules $M,M^{\prime}$ are _asynchronous_ if $X\cap X^{\prime}=\varnothing$.
Note that all the modules presented in Example 2 are asynchronous.

Composition of Modules. The model of a MAS is given by the asynchronous
composition $M=M^{(1)}|\dots|M^{(n)}$ that combines modules
$M^{(1)},\dots,M^{(n)}$ into a single module $M$ Lomuscio13assGar . The
composition is standard; it only requires the compliance of the valuations.

Traces and Words. A trace of a module $M$ is an infinite sequence of
alternating states and transitions
$\sigma=q_{0}\alpha_{0}q_{1}\alpha_{1}\ldots$, where $q_{0}$ is the initial
state and $(q_{i},\alpha_{i},q_{i+1})\in T$ for every $i\in\mathbb{N}$. An
infinite word $w=v_{0}v_{1},\ldots\in(D^{X})^{\omega}$ is _derived_ by module
$M$ with trace $\sigma=q_{0}\alpha_{0}q_{1}\alpha_{1}\ldots$ if
$v_{i}=\lambda(q_{i})$ for all $i\in\mathbb{N}$. An infinite word
$u=\alpha_{0}\alpha_{1},\ldots\in(D^{I})^{\omega}$ is _admitted_ by $M$ with
$\sigma$ if $\sigma=q_{0}\alpha_{0}q_{1}\alpha_{1}\ldots$ . Finally, $w$
(resp. $u$) is derived (resp. admitted) by $M$ if there exists a trace of $M$
that derives (resp. admits) it.

##  3\. What Agents Can Achieve

_Alternating-time temporal logic_ $\mathbf{ATL_{\mathrm{}}^{*}}$ Alur97ATL ;
Alur02ATL ; Schobbens04ATL  introduces _strategic modalities_
$\langle\\!\langle{C}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma$, expressing
that coalition $C$ can enforce the temporal property $\gamma$. In this paper,
we use the _imperfect information/imperfect recall_ variant without next step
operator $\mathrm{X}$ and nested strategic modalities, denoted
$\mathbf{sATL_{\mathrm{}}^{*}}$ (“simple $\mathbf{ATL_{\mathrm{}}^{*}}$”).

Syntax. Formally, the syntax of $\mathbf{sATL_{\mathrm{}}^{*}}$ is defined by:

$\phi::=p(Y)\mid\neg\phi\mid\phi\land\phi\mid\langle\\!\langle{C}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma;\quad\gamma::=p(Y)\mid\neg\gamma\mid\gamma\land\gamma\mid\gamma\,\mathrm{U}\,\gamma$.

where $p:Y\to D$ for some subset of domain variables $Y\subseteq X$. That is,
each atomic statement refers to the valuation of a subset of variables used in
the system. $\,\mathrm{U}\,$ is the “strong until” operator of $\mathbf{LTL}$.
The “sometime” and “always” operators $\mathrm{F}$ and $\mathrm{G}$ can be
defined as usual by $\mathrm{F}\gamma\equiv\top\,\mathrm{U}\,\gamma$ and
$\mathrm{G}\gamma\equiv\neg(\top\,\mathrm{U}\,\neg\gamma)$.

Semantics. A _memoryless imperfect information strategy_ for agent $i$ is a
function $s_{i}:Q_{i}\to T_{i}$. We say that a trace $\sigma$ (word derived
with $\sigma$) _implements_ a strategy $s_{i}$ if for any $j$ where
$q_{j}^{(i)}\neq q_{j+1}^{(i)}$ we have
$s_{i}(q_{j}^{(i)})=(q_{j}^{(i)},\alpha_{j},q_{j+1}^{(i)})$, where
$\alpha_{j}:I_{i}\to D$ and $\alpha_{j}(x)=\lambda(q_{j})(x)$.

Let $C\subseteq\\{1,\ldots,n\\}$ be a set of agent indices. We define _joint
strategies_ for $C$ as tuples of individual strategies, one per $i\in C$. The
semantics of strategic operators is given by the following clause:

$M,q\models\langle\\!\langle{C}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\gamma$:

if there exists a joint strategy $s_{C}$ for $C$ such that, for any word $w$
that implements $s_{C}$, we have $M,w\models\gamma$.

##  4\. Assumptions and Guarantees

We propose an assume-guarantee scheme, where one can reduce the complexity of
model checking $\mathbf{sATL_{\mathrm{}}^{*}}$ by verifying individual
strategic abilities of single agents against overapproximating abstractions of
its environment, i.e., the rest of the system. The general idea is that if an
agent has a successful strategy in a more nondeterministic environment, then
it can can use the same strategy to succeed in the original model. Moreover,
it often suffices to prepare the abstraction based only of the modules that
are connected with the agent by at most $k$ synchronization steps.

Assumptions and Guarantees. The environmental abstractions are formalized by
_assumptions_ $A=(M_{A},F)$, where $M_{A}$ is a module and $F$ is a set of
accepting states that provide Büchi-style accepting rules for infinite traces
derived by $M$. The assumption should be constructed so that it _guarantees_
that the set of computations accepted by $A$ covers the sequences of changes
in the input variables $I_{M}$ of module $M$. We capture those changes by the
notion of _curtailment_. Formally, a sequence $v=v_{1}v_{2}\ldots$ over
$D^{Y}$ is a curtailment of sequence $u=u_{1}u_{2}\ldots$ over $D^{X}$ (where
$Y\subseteq X$) if there exists an infinite sequence of indices
$j_{1}<j_{2}<...$ with $j_{1}=1$ such that $\forall_{i}\forall_{j_{i}\leq
k<j_{i+1}}v_{i}=u_{k}|_{Y}$.

The Scheme. Let $M=M_{1}|M_{2}|\dots|M_{n}$ be a system composed from modules
$M_{1},M_{2},\dots,M_{n}$, where $X_{M_{i}}\cap X_{M_{j}}=\varnothing$ for
$i\neq j$. By $\mathit{Comp}_{i}^{1}$ we denote the composition of all modules
directly related to $M_{i}$. Moreover, $\mathit{Comp}_{i}^{k}$ denotes the
composition of the modules in $\mathit{Comp}_{i}^{k-1}$ and the modules
directly related to them (except for $M_{i}$). Further, let $\psi_{i},i\in C$
be path formulas of $\mathbf{sATL_{\mathrm{}}^{*}}$, one for each agent in
$C$. Simple assume-guarantee reasoning for strategic ability is provided by
the following inference rule:

$\bf{R_{k}}\;\;\;\begin{array}[]{c}\forall_{i\in
C}\;M_{i}|A_{i}\,\models_{ir}\,\langle\\!\langle{i}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\psi_{i}\\\
\forall_{i\in C}\;\mathit{Comp}_{i}^{k}\,\models\,A_{i}\\\ \hline\cr
M_{1}|...|M_{n}\models_{ir}\langle\\!\langle{C}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\bigwedge_{i\in
C}\psi_{i}\end{array}$

##  5\. Experiments

V Monolithic model checking Assume-guarantee verification #st #tr DFS Apprx
#st #tr DFS Apprx 2 529 2216 ¡0.1 ¡0.1/Yes 161 528 ¡0.1 ¡0.1/Yes 3 1.22e4
1.28e5 ¡0.1 0.8/Yes 1127 7830 ¡0.1 ¡0.1/Yes 4 2.79e5 6.73e6 ¡0.1 30/Yes 7889
1.08e5 ¡0.1 0.5/Yes 5 6.43e6 3.42e8 timeout 5.52e4 1.45e6 ¡0.1 8/Yes 6 timeout
3.86e5 1.92e7 ¡0.1 135/Yes 7 timeout timeout

Table 1. Results of assume-guarantee verification for simple voting (times
given in seconds; timeout=2h)

Here, we present preliminary experimental results for the assume-guarantee
rule proposed in Section 4, using the voting scenario of Example 2 as the
benchmark. The assumptions are provided by a simplified module of the coercer,
where he only waits for the value reported by $\mathit{Voter}_{1}$, no matter
how he reacts to other voters’ choices. The algorithms have been implemented
in Python, and run on a server with 2.40 GHz Intel Xeon Platinum 8260 CPU, 991
GB RAM, and 64-bit Linux.

The verified formula was
$\varphi\equiv\langle\\!\langle{\mathit{Voter}_{1}}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{G}(\lnot\mathsf{{pstatus_{1}}}\lor\mathsf{{voted_{1}=1}})$.
The results are presented in Table 1. The first column describes the
configuration of the benchmark, i.e., the number of the voters. Then, we
report the performance of model checking algorithms that operate on the
explicit model of the whole system vs. assume-guarantee verification. _DFS_ is
a straightforward implementation of depth-first strategy synthesis. _Apprx_
refers to the method of fixpoint-approximation Jamroga19fixpApprox-aij ;
besides the time, we also report if the approximation was conclusive.

##  6\. Conclusion

In this paper, we sketch how assume-guarantee reasoning can be extended for
verification of strategic abilities. The main idea is to factorize coalitional
abilities by the abilities of the coalition members, and to verify the
individual abilities against Büchi-style abstractions of the agents’
environment of action. Preliminary experimental evaluation has produced very
promising results, showing noticeable improvement in the verification of large
models consisting of asynchronous agents with independent goals.

We acknowledge the support of the National Centre for Research and
Development, Poland (NCBR), and the Luxembourg National Research Fund (FNR),
under the PolLux/FNR-CORE project STV (POLLUX-VII/1/2019 –
C18/IS/12685695/IS/STV/Ryan).

## References

  * [1] R. Alur, T.A. Henzinger, and O. Kupferman.  Alternating-time Temporal Logic.  In Proc. of FOCS’97, pages 100–109. IEEE Comput. Soc. Press, 1997\.
  * [2] R. Alur, T.A. Henzinger, and O. Kupferman.  Alternating-time Temporal Logic.  J. of the ACM, 49:672–713, 2002.
  * [3] R. Alur, T.A. Henzinger, F.Y.C. Mang, S. Qadeer, S. Rajamani, and S. Tasiran.  MOCHA: Modularity in model checking.  In Proc. of CAV’98, volume 1427 of LNCS, pages 521–525. Springer, 1998.
  * [4] F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin.  Verification of broadcasting multi-agent systems against an epistemic strategy logic.  In Proc. of IJCAI’17, pages 91–97, 2017.
  * [5] F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin.  Verification of multi-agent systems with imperfect information and public actions.  In Proc. of AAMAS’17, pages 1268–1276, 2017.
  * [6] N. Bulling, J. Dix, and W. Jamroga.  Model checking logics of strategic ability: Complexity.  In Specification and Verification of Multi-Agent Systems, pages 125–159. Springer, 2010.
  * [7] S. Busard, C. Pecheur, H. Qu, and F. Raimondi.  Improving the model checking of strategies under partial observability and fairness constraints.  In Formal Methods and Software Engineering, volume 8829 of LNCS, pages 27–42. Springer, 2014.
  * [8] P. Cermák, A. Lomuscio, F. Mogavero, and A. Murano.  MCMAS-SLK: A model checker for the verification of strategy logic specifications.  In Proc. of CAV’14, volume 8559 of LNCS, pages 525–532. Springer, 2014.
  * [9] P. Cermák, A. Lomuscio, and A. Murano.  Verifying and synthesising multi-agent systems against one-goal strategy logic specifications.  In Proc. of AAAI’15, pages 2038–2044, 2015.
  * [10] K. Chatterjee, T.A. Henzinger, and N. Piterman.  Strategy Logic.  Inf. and Comp., 208(6):677–693, 2010.
  * [11] T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis.  PRISM-games: A model checker for stochastic multi-player games.  In Proc. of TACAS’13, volume 7795 of LNCS, pages 185–191. Springer, 2013.
  * [12] E.M. Clarke, D.E. Long, and K.L. McMillan.  Compositional model checking.  In Proc. of LICS’89, pages 353–362. IEEE Comput. Soc. Press, 1989.
  * [13] B. Devereux.  Compositional reasoning about aspects using alternating-time logic.  In Proc. of FOAL’03, pages 45–50, 2003.
  * [14] C. Dima and F.L. Tiplea.  Model-checking ATL under imperfect information and perfect recall semantics is undecidable.  CoRR, abs/1102.4225, 2011.
  * [15] N. Fijalkow, B. Maubert, A. Murano, and M.Y. Vardi.  Assume-guarantee synthesis for prompt linear temporal logic.  In Proc. of IJCAI’20, pages 117–123. ijcai.org, 2020.
  * [16] D.P. Guelev, C. Dima, and C. Enea.  An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking.  J. Appl. Non-Classical Log., 21(1):93–131, 2011.
  * [17] T.A. Henzinger, S. Qadeer, and S.K. Rajamani.  You assume, we guarantee: Methodology and case studies.  In Proc. of CAV’98, volume 1427 of LNCS, pages 440–451. Springer, 1998.
  * [18] C.A.R. Hoare.  An axiomatic basis for computer programming.  Commun. ACM, 12(10):576–580, 1969.
  * [19] X. Huang and R. van der Meyden.  Symbolic model checking epistemic strategy logic.  In Proc. of AAAI’14, pages 1426–1432, 2014.
  * [20] W. Jamroga and J. Dix.  Model checking ATLir is indeed $\Delta_{2}^{P}$-complete.  In Proc. of EUMAS’06, volume 223 of CEUR Workshop Proc., 2006.
  * [21] W. Jamroga, M. Knapik, D. Kurpiewski, and Ł. Mikulski.  Approximate verification of strategic abilities under imperfect information.  Artif. Int., 277, 2019.
  * [22] W. Jamroga, W. Penczek, T. Sidoruk, P. Dembiński, and A.W. Mazurkiewicz.  Towards partial order reductions for strategic ability.  J. Artif. Intell. Res., 68:817–850, 2020.
  * [23] C.B. Jones.  Specification and design of (parallel) programs.  In Proc. of IFIP’83, pages 321–332. North-Holland/IFIP, 1983\.
  * [24] D. Kurpiewski, W. Pazderski, W. Jamroga, and Y. Kim.  STV+Reductions: Towards practical verification of strategic ability using model reductions.  In Proc. of AAMAS’21, pages 1770–1772. ACM, 2021.
  * [25] M.Z. Kwiatkowska, G. Norman, D. Parker, and H. Qu.  Assume-guarantee verification for probabilistic systems.  In Proc. of TACAS’10, volume 6015 of LNCS, pages 23–37. Springer, 2010.
  * [26] A. Lomuscio, H. Qu, and F. Raimondi.  MCMAS: An open-source model checker for the verification of multi-agent systems.  Int. J. Soft. Tools Tech. Trans., 19(1):9–30, 2017.
  * [27] A. Lomuscio, B. Strulo, N.G. Walker, and P. Wu.  Assume-guarantee reasoning with local specifications.  In Proc. of ICFEM’10, volume 6447 of LNCS, pages 204–219. Springer, 2010.
  * [28] A. Lomuscio, B. Strulo, N.G. Walker, and P. Wu.  Assume-guarantee reasoning with local specifications.  Int. J. Found. Comput. Sci., 24(4):419–444, 2013.
  * [29] F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi.  Reasoning about strategies: On the model-checking problem.  ACM Trans. Comp. Log., 15(4):1–42, 2014.
  * [30] S.S. Owicki and D. Gries.  Verifying properties of parallel programs: An axiomatic approach.  Commun. ACM, 19(5):279–285, 1976.
  * [31] A. Pnueli.  In transition from global to modular temporal reasoning about programs.  In Logics and Models of Concurrent Systems, volume 13 of NATO ASI Series, pages 123–144. Springer, 1984.
  * [32] P.Y. Schobbens.  Alternating-time logic with imperfect recall.  Electr. Not. Theor. Comput. Sci., 85(2):82–93, 2004.