Runtime verification (RV) is a lightweight approach to detecting temporal errors of system at runtime. It confines the verification on observed trajectory which avoids state explosion problem. To predict the future violation, some work proposed the predictive RV which uses the information from models or static analysis. But for software whose models and codes cannot be obtained, or systems running under uncertain environment, these predictive methods cannot take effect. Meanwhile, RV in general takes multi-valued logic as the specification languages, for example the true, false and inconclusive in three-valued semantics. They cannot give accurate quantitative description of correctness when inconclusive is encountered. We in this paper present a RV method which learns probabilistic model of system and environment from history traces and then generates probabilistic runtime monitor to quantitatively predict the satisfaction of temporal property at each runtime state. In this approach, Hidden Markov Model (HMM) is firstly learned and then transformed to Discrete Time Markov Chain (DTMC). To construct incremental monitor, the monitored LTL property is translated into Deterministic Rabin Automaton (DRA). The final probabilistic monitor is obtained by generating the product of DTMC and DRA, and computing the probabilities for each state. With such a method, one can give early warning once the probability of correctness is lower than a pre-defined threshold, and have the chance to do adjustment in advance. The method has been implemented and experimented on real UAS (Unmanned Aerial Vehicle) simulation platform.
Citation: Ge Zhou, Chunzheng Yang, Peng Lu, Xi Chen. Runtime verification in uncertain environment based on probabilistic model learning[J]. Mathematical Biosciences and Engineering, 2022, 19(12): 13607-13627. doi: 10.3934/mbe.2022635
[1] | Shiqiang Feng, Dapeng Gao . Existence of traveling wave solutions for a delayed nonlocal dispersal SIR epidemic model with the critical wave speed. Mathematical Biosciences and Engineering, 2021, 18(6): 9357-9380. doi: 10.3934/mbe.2021460 |
[2] | Wenhao Chen, Guo Lin, Shuxia Pan . Propagation dynamics in an SIRS model with general incidence functions. Mathematical Biosciences and Engineering, 2023, 20(4): 6751-6775. doi: 10.3934/mbe.2023291 |
[3] | Tong Li, Zhi-An Wang . Traveling wave solutions of a singular Keller-Segel system with logistic source. Mathematical Biosciences and Engineering, 2022, 19(8): 8107-8131. doi: 10.3934/mbe.2022379 |
[4] | Ran Zhang, Shengqiang Liu . Traveling waves for SVIR epidemic model with nonlocal dispersal. Mathematical Biosciences and Engineering, 2019, 16(3): 1654-1682. doi: 10.3934/mbe.2019079 |
[5] | Danfeng Pang, Yanni Xiao . The SIS model with diffusion of virus in the environment. Mathematical Biosciences and Engineering, 2019, 16(4): 2852-2874. doi: 10.3934/mbe.2019141 |
[6] | Xixia Ma, Rongsong Liu, Liming Cai . Stability of traveling wave solutions for a nonlocal Lotka-Volterra model. Mathematical Biosciences and Engineering, 2024, 21(1): 444-473. doi: 10.3934/mbe.2024020 |
[7] | M. B. A. Mansour . Computation of traveling wave fronts for a nonlinear diffusion-advection model. Mathematical Biosciences and Engineering, 2009, 6(1): 83-91. doi: 10.3934/mbe.2009.6.83 |
[8] | Felicia Maria G. Magpantay, Xingfu Zou . Wave fronts in neuronal fields with nonlocal post-synaptic axonal connections and delayed nonlocal feedback connections. Mathematical Biosciences and Engineering, 2010, 7(2): 421-442. doi: 10.3934/mbe.2010.7.421 |
[9] | Maryam Basiri, Frithjof Lutscher, Abbas Moameni . Traveling waves in a free boundary problem for the spread of ecosystem engineers. Mathematical Biosciences and Engineering, 2025, 22(1): 152-184. doi: 10.3934/mbe.2025008 |
[10] | Guo Lin, Shuxia Pan, Xiang-Ping Yan . Spreading speeds of epidemic models with nonlocal delays. Mathematical Biosciences and Engineering, 2019, 16(6): 7562-7588. doi: 10.3934/mbe.2019380 |
Runtime verification (RV) is a lightweight approach to detecting temporal errors of system at runtime. It confines the verification on observed trajectory which avoids state explosion problem. To predict the future violation, some work proposed the predictive RV which uses the information from models or static analysis. But for software whose models and codes cannot be obtained, or systems running under uncertain environment, these predictive methods cannot take effect. Meanwhile, RV in general takes multi-valued logic as the specification languages, for example the true, false and inconclusive in three-valued semantics. They cannot give accurate quantitative description of correctness when inconclusive is encountered. We in this paper present a RV method which learns probabilistic model of system and environment from history traces and then generates probabilistic runtime monitor to quantitatively predict the satisfaction of temporal property at each runtime state. In this approach, Hidden Markov Model (HMM) is firstly learned and then transformed to Discrete Time Markov Chain (DTMC). To construct incremental monitor, the monitored LTL property is translated into Deterministic Rabin Automaton (DRA). The final probabilistic monitor is obtained by generating the product of DTMC and DRA, and computing the probabilities for each state. With such a method, one can give early warning once the probability of correctness is lower than a pre-defined threshold, and have the chance to do adjustment in advance. The method has been implemented and experimented on real UAS (Unmanned Aerial Vehicle) simulation platform.
The quality of the proteome, or proteostasis, is challenged during the ageing process inducing the accumulation of damaged proteins. Proteostasis is maintained by a complex network of cellular mechanisms that monitors folding, concentration, cellular localization, and interactions of proteins from their synthesis through their degradation [1]. Chaperones assure the proper folding of proteins throughout their life cycle [2,3]. When the activity of chaperones is insufficient to maintain proteome stability, damaged and misfolded proteins may accumulate. These proteins impair cell function and tissue homeostasis and must, therefore, be scavenged. Damaged, misfolded or aggregated proteins are degraded by the proteasome or through autophagy-lysosome [4,5]. In the proteasome-mediated degradation proteins are first targeted by the ubiquitination machinery and then recognized, unfolded and proteolyzed by the proteasome [6]. In autophagy-mediated proteolysis, proteins are degraded by the lysosome. Although lysosomal proteolysis was initially considered to be a non-selective system, it has been shown that molecular chaperones and other cargo-recognition molecules such as ubiquitin determine the degradation of specific proteins by the lysosome [5].
Loss of proteostasis is considered one of the hallmarks of ageing [7] and contributes to multiple age-related diseases such as Alzheimer’s (AD) [8], Parkinson’s (PD) [9] or Huntington’s disease (HD) [10]. Both proteasome functionality and autophagic-lysosomal potential decline during the ageing process and trigger the onset of age-related diseases [5,11,12,13]. In addition, longevity-promoting pathways, such as reduced insulin/IGF-1 signaling pathway (IIS)or dietary restriction (DR), impact on protein clearance mechanisms and increase the stability of the proteome, thus protecting from the symptoms associated to AD, PD or HD [14]. Here, we discuss the mechanistic links between neurodegenerative diseases and loss of protein clearance mechanisms.
The ubiquitin-proteasome system (UPS)is critical for maintaining the proper concentration of many regulatory proteins involved in signal transduction, metabolism, cell cycle, development, stem cell function, apoptosis, gene transcription, DNA repair, senescence, inflammation and other biological processes [4,5,6,15,16,17]. The UPS is not only necessary to degrade regulatory proteins but it is also a key component of the proteostasis network to terminate damaged proteins [4,5,6]. The first step of the UPS-mediated degradation is the conjugation of ubiquitin, a highly conserved 76 amino acid residue polypeptide, to the substrate protein [6]. The attachment of ubiquitin is achieved through a sequential enzymatic mechanism (Figure 1). First, the ubiquitin-activating enzyme (E1) activates the C-terminal glycine residue of an ubiquitin in an ATP-dependent manner. Activated ubiquitin is next transferred to a cysteine site of an ubiquitin-conjugating enzyme (E2). In the third step, a ubiquitin ligase (E3) links ubiquitin from the E2 enzyme by its C-terminus to the ε-amino group of a lysine residue of the target protein. While apparently there are only two E1, there are several E2 enzymes and many E3 ubiquitin ligases, each of which recognizes one or several specific protein motifs, being responsible for the selectivity of the process [6]. Additional molecules of ubiquitin are linked to the primary ubiquitin via internal ubiquitin lysines, forming a chain. Ubiquitin has seven lysine residues, all of which can form polymer chains [18]. A chain of at least four lysine 48-linked ubiquitins is the primary signal for degradation [19], while other linear ubiquitin chains participate in different processes such as signal transduction [4]. The polyubiquitylated protein is subsequently recognized by the proteasome, which will be responsible of its degradation.
The proteasome is a proteolytic machine formed by the assembly of several subunits [6] (Figure 1). The core particle (20S) of the proteasome exhibits a barrel-like structure in which the 28 subunits are assembled into four seven membered rings [6]. The two outer rings are composed by seven α-subunits (α1 to α7), while the two inner rings are composed by seven β-subunits (β1 to β7) [6]. β-rings contain the proteolytic active sites, β1, β2 and β5, which present caspase-like, trypsin-like and chymotrypsin-like activities, respectively [6]. The entrance of the substrate into the catalytic cavity is controlled by the α-rings. Although existing in a free form, 20S particles are by default closed and need the binding of the proteasome activators to degrade polyubiquitylated proteins [20]. However, it is important to remark that free 20S particles have a detectable activity independent of ATP/ubiquitination towards small proteins and could play a significant role in the degradation of oxidized proteins [11,21].
Active proteasome exists in several forms, but is mainly formed through the assembly of the 20S and the 19S (26S if it is single and 30S if it is double capped) [6] (Figure 1). The 19S modulates the activity of the holo-complex by recognizing polyubiquitylated proteins, unfolding and translocating these proteins to the 20S for degradation in an ATP dependent process [4,6]. The 19S is composed of a base adjacent to the 20S and a lid that sits on top of the base [6]. The base contains six ATPases (Rpt1-Rpt6), which are members of the AAA family of ATPases [6] and three non ATPases subunits (Rpn1, Rpn2 and Rpn10). The lid complex is critical for substrate recognition and deubiquitination [6]. The 19S lid is formed by eight subunits (Rpn3, Rpn5, Rpn6, Rpn7, Rpn8, Rpn9, Rpn11, and Rpn12). In addition to regulation by 19S, the core particle can be activated by other regulatory particles, like PA28 (also known as 11S) [4], which is formed by hetero-heptameric rings of 28-kDa proteins (PA28α and PA28β)or homo-heptameric rings of PA28γ [11]. PA28 opens the channel by binding to the core particle [22,23]. In contrast to the 19S regulatory particle, PA28 lacks ATPase activity and the ability to bind to ubiquitin conjugates [24,25]. PA28αβ is inducible by interferon-γ [26] and modulates the presentation and generation of specific viral antigens [27]. PA28γ is involved in cell cycle regulation and promotes the degradation of small proteins such as p21 [28]. The 20S proteasome is also activated by Blm10/PA200, a monomeric protein of 250 kDa [11]. Blm10/PA200 forms hybrid complexes in which this protein binds to one end of the 20S proteasome and the 19S to the opposite end [29,30].
Autophagy is an intracellular catabolic process in which cytosol fractions, organelles and macromolecules are degraded through the lysosome. Autophagy acts as a bulk intracellular degradation system that degrades many different substrates to provide energy during metabolic stress, growth factor depletion, oxidative stress, DNA damage, endoplasmic reticulum stress or hypoxia [31,32]. These substrates include macromolecules that are degraded to nutrients during starvation [33]. Autophagy also has a key role as a quality control mechanism of proteins and organelles and is required for maintaining cellular homeostasis by, for example, degrading misfolded and aggregated proteins [34], such as the neurodegenerative-associated proteins tau, α-synuclein and polyglutamine-exp and ed molecules [35]. Moreover, due to the capacity to engulf whole cellular regions, autophagy is critical in every process that requires extensive cellular remodelation, such as embryogenesis or cellular death [36,37].
Lysosomes are the catalytic compartment of the autophagic degradation system. Lysosomes are single membrane vesicles that contain a large variety of cellular hydrolases such as proteases, lipases, nucleotidases and glycosidases, and which work optimally at the acidic pH of the lysosomal lumen. Lysosomal proteases convert proteins into small di- and tri-peptides and free aminoacids that are released into the cytosol and either used to obtain energy or recycled to synthesize the novo proteins [33,38].
There are different types of autophagy depending on the nature of the cargo and the way it is delivered to the lysosomes. In mammalian cells, the best-characterized types of autophagy are macroautophagy (Figure 1), microautophagy and chaperone-mediated autophagy (CMA) [37,39,40]. Macroautophagy (herein after called autophagy)is a self-catabolic process in which cytoplasm portions are engulfed into double membrane vesicles, known as autophagosomes. The gene, which participate in autophagy are known as autophagy-related genes (ATG) (Table 1) [41]. Atg proteins organize into complexes that regulate each of the steps of autophagy (Box 1). After the autophagosome is formed with the sequestered cargo inside, it is transported to the lysosome, where its outer membrane fuses with the lysosome membrane and both the sequestered material and the inner membrane of the autophagosome are degraded. In microautophagy, a pathway characterized to a much lesser extent, small components of the cytoplasm are engulfed directly by the lysosome membrane [42,43,44]. In CMA, particular cytoplasmic proteins are recognized by chaperones through a consensus sequence and transferred to the lysosome for their degradation via the lysosomal-membrane-protein type 2A (LAMP-2A) receptor [45]. Autophagy and microautophagy can degrade both organelles and proteins, whereas CMA only participates in the degradation of proteins [39].
Autophagy step involved | Yeast | Mammals |
Formation of phagophore | Atg1 | ULK1/2 |
Atg13 | Atg13 | |
Atg17 | FIP200 | |
Atg14 | Atg14 | |
Atg6 | Beclin-1 | |
Elongation of phagophore | Atg12 | Atg12 |
Maturation of phagophore | Atg5 | Atg5 |
Atg16 | Atg16L | |
Atg7 | Atg7 | |
Atg10 | Atg10 | |
Maturation of phagophore | Atg8 | LC3/ MAP1LC3A |
Atg3 | Atg3 | |
Atg4 | Atg4 |
Autophagy is modulated by many signaling pathways such as adenosine monophosphate-activated protein kinase (AMPK), Sirtuin 1 (SIRT1) and mTOR, a serine/threonine kinase which exists in two complexes (mTORC1 and mTORC2). mTORC1, the mammalian target of rapamycin, modulates the assembly of the Atg complex to form the autophagosomes [46]. Under fed conditions, mTORC1 is activated upon the binding of growth factors to the insulin-like growth factor receptor (IGF1R) [32] and inactivates the Atg1 complex by phosphorylation. Conversely, under starving conditions mTOR is inhibited and the autophagosoms are formed upon Atg1 complex trigger [32]. In contrast, mTORC2 is insensitive to rapamycin inhibition and activates autophagy.
A hallmark of ageing is the progressive decline in cellular proteostasis and the accumulation of misfolded and damaged proteins [7]. As one of the key components of the cellular proteostasis network, proteasome function declines during ageing (Figure 1). This dysfunction can occur at different levels such as decreased expression of proteasome subunits [47,48], alteration and/or replacement of proteasome subunits [49], disassembly of proteasomes [50] or inactivation by interaction with protein aggregates [51]. This later mechanism could, in addition, induce a collapse proteostasis feedback during ageing, since inhibition of proteostasis itself can induce the accumulation of protein inclusions, which in turn can obstruct and further inhibit proteasome activity [52]. Several mammalian tissues present a decline in proteasome function during ageing and senescence, such as human skin, epidermal cells, fibroblasts and lymphocytes [53,54,55,56], bovine eye lens [57] and rat liver, lung, heart, kidney, spinal cord, hippocampus, cerebral cortex and muscle tissues [58,59,60,61,62,63]. Notably, a transgenic mouse with decreased proteasomal chymotrypsin-likeactivity exhibits a shortened lifespan, premature age-related phenotypes and aggravation of age-related metabolic disorders such as obesity or excessive accumulation of triglycerides in hepatic cells [64].
Similarly to proteasome activity, autophagic-lysosomal potential also declines during ageing and senescence [65,66,67,68,69], through a decline in ATG proteins, autophagy inductors or the cellular response to hormones that trigger autophagic degradation [32]. Autophagy of organelles is also impaired in ageing, particularly that of defective mitochondria [51,65,70,71]. Clearance of autophagosomes is equally altered in ageing, with the consequent accumulation of undigested cargos inside the lysosome [68]. The molecular mechanism mediating this decline is not fully established, although in the aged human brain Atg5, Atg7 and Beclin-1 are downregulated [72]. Furthermore, the levels of ULK1 (the human orthologue of Atg1), Beclin-1 and LC3 are reduced in age-related pathologies, such as osteoarhrtitis [73]. In the liver, age-dependent decrease in autophagy may be the consequence of an inefficient clearance of the autophagosome cargo by the lysosome [68] and reduced hormonal (mainly glucagon and insulin)regulation of the pathway [74]. Several genetic studies have suggested a casual effect of a decrease in autophagy and ageing. In yeast, a genetic screen searching for ageing factors identified multiple short-lived mutants with autophagy defects [75]. In C. elegans, loss of function of several autophagic genes (Atg7, Atg12, Atg1, Beclin-1, Atg18 and Atg12) shortens lifespan, supporting the role of autophagy in longevity [76,77]. In Drosophila melanogaster, the expression of autophagy genes is decreased in neurons from old flies [78]. Similar to C. elegans, loss of function of Atg1, Atg8 and sestrin1 (a protein required for autophagy)reduce lifespan while enhancing their expression can promote longevity, suggesting a causal role of autophagy in the ageing process [32]. In mice, constitutive knock-out of most ATG genes is lethal during the early postnatal period due to the incapacity of energy reserves mobilization [79,80]. Tissue specific deletion of several autophagy genes precipitates ageing and ageing-associated phenotypes [32]. Accordingly, the central nervous system-specific knockout of Atg5 or Atg7 induces the accumulation of ubiquitin positive inclusion bodies followed by neuronal loss and premature death [81,82]. Purkinje-cell specific knockout of Atg7 induces axonal dystrophy and degeneration of axon terminals with a subsequent Purkinje cell death and cerebellar ataxia [83]. Furthermore, central nervous system-specific knockout of Atg17/FIP200 induces the accumulation of ubiquitin positive inclusion bodies in Purkinje neurons, cerebellar cell loss and cortical spongiosis [84]. Skeleton-muscle specific knockout of Atg7 induces muscle atrophy, age-dependent decrease in force, accumulation of abnormal mitochondria, disorganization of sarcomeres and exacerbates muscle loss during denervation and fasting [85]. Hepatocyte-specific knockout of Atg7 triggers the accumulation of lipid droplets containing triglycerides and cholesterol, induces ER stress in these cells and causes insulin stress resistance [86,87]. β cell-specific deletion of Atg7 induces degeneration of pancreatic islets, impaired glucose tolerance, decreased serum insulin level, accumulation of ubiquitinylated proteins colocalized with p62, mitochondrial swelling and endoplasmic reticulum distension [88]. Another example is the specific knockout of Atg5 in podocytes that induces spontaneous age-dependent late onset of glomerulosclerosis with accumulation of oxidized and ubiquitinylated proteins, damaged mitochondria, ER stress and podocyte loss [89].
As it is the case for macroaupthagy, CMA rate also decreases with ageing [67,90] due to a decrease in the LAMP-2A receptor and a consequent reduction in the binding of proteins to the lysosome and their transport into the organelle [67,91]. Accordingly, an increase in the levels of LAMP-2A prevents ageing-associated dysfunctions in the liver of old mice [92]. The mechanism of LAMP-2A downregulation with ageing could be at the post-transcriptional level, since RNA levels of LAMP-2A remain unchanged in ageing [91]. The structure of the LAMP-2A revealed that heat shock protein 90 (Hsp90) was key for the assembly of the receptor [93]. Thus, the decline in availability of chaperones during ageing [94], and particularly, in Hsp90 in the aged liver [95] could explain the impairment in the trafficking and stability of LAMP-2A. Although merely correlative, these findings indicate that loss of proteasome and autophagy may contribute to the ageing process.
Neurodegenerative diseases associated to proteotoxicity, such as AD, HD, PD or amyotrophic lateral sclerosis (ALS) [5,8,9,10,11,14], have been associated with ageing [96,97]. A common characteristic of these disorders is the aggregation of aberrant proteins in neurons, even though different toxic proteins are involved in their onset [96]. The pathophysiological significance of protein aggregates is vaguely known. The accumulation of abnormal proteins may lead to perturbed cellular functions and eventually to neuronal death, ultimately manifesting as neurodegenerative disease. The inclusion bodies of AD, PD, HD and ALS contain abnormal amounts of ubiquitin, suggesting a link between neurodegeneration and dysfunction of proteasome and autophagy [12,34,98]. Changes in the proteolytic machinery with age may explain why ageing is a risk factor for AD, PD and HD [34,97,99]. Furthermore, loss-of-function experiments have shown that decreased proteasomal activity and autophagic potential enhance the neurodegenerative phenotype [34,99]. Unfolded monomeric proteins can be degraded through proteasome or CMA; while once aggregated into large macromolecules, bulk degradation through autophagy seems to be the key player in their removal [35]. In addition, there is a crosstalk between proteasome and autophagy: protein aggregated-induced proteasome or CMA impairment can activate macroautophagy, probably as a compensation mechanism [100]. Sequestration of autophagy repressors in these protein aggregates could partially mediate autophagy induction [101]. In proteopathies, after proteasome and /or CMA failure to degrade damaged proteins, autophagy may also end up collapsing and contributing to an enhanced accumulation of aggregates [102]. Therefore, therapies focused on increasing proteasome as well as autophagic activity could have a great impact in reducing aggregation-mediated toxicity.
The most common neurodegenerative disorders marked by protein misfolding and aggregation is AD, the hallmarks of which are progressive dementia and loss of memory, reasoning and language qualities [8]. AD is characterized by the deposition of two different protein aggregates: (i) extracellular senile (amyloid)plaques and (ii)intracellular neurofibrillary tangles [8]. The latter are mostly composed by hyperphosphorylated tau, a microtubule-associated protein [8]. Proteasome activity is decreased in brains from AD patients compared with age-matched controls [103], suggesting a connection between the proteasome and the disease. Indeed, an in vitro study has shown that tau protein can be degraded by the 20S proteasome in an ATP/ubiquitin independent manner [104], while other studies report that its degradation in cells is, at least partially, ubiquitin-dependent [105,106]. When tau is not bound to microtubules, it associates with the chaperone Hsp70. The ubiquitin ligase CHIP interacts directly with Hsp70 and promotes tau ubiquitination and degradation [105,106]. In addition, the proteasome activator Blm10 accelerates tau degradation in vitro [107]. Tau clearance is blocked by FK506 binding protein 51 (FKBP51), which forms a mature chaperone complex with Hsp90 that prevents tau degradation [108]. In mice, FKBP51 and HSP90 synergize to block tau clearance by the proteasome, resulting in tau oligomerization [109]. Notably, in humans, FKBP51 levels increase relative to age and higher FKBP51 levels are associated with AD progression [109]. These results suggest a model in which age-associated increases in FKBP51 and its interaction with Hsp90 would promote neurotoxic tau accumulation. Strikingly, aggregated tau can inhibit proteasome activity [103], which in turn could further contribute to the pathology of AD. Analysis of AD brain by electron microscopy revealed a link between autophagy and the pathogenesis of the disease, since autophagy vacuoles were abundant in neuritis and the perikarya of AD neurons [110]. Upregulation of autophagy is beneficial in AD, since flies expressing mutant aggregate-prone tau, activation of autophagy by rapamycin treatment increases the clearance of tau aggregates [111]. In a mouse model of AD, rapamycin also protects from tau pathology by increasing autophagy [112].
Senile plaques are mostly formed by aggregates of amyloid-β (Aβ), which is generated via proteolytic cleavage of the amyloid precursor protein (APP) [8]. Incorrect cleavage of APP leads to Aβ aggregation. Interestingly, intracellular Aβ oligomers can inhibit proteasome activity [113]. Autophagy vacuoles in AD neurons contain substantial amounts of β-amyloid [114]. Strikingly, upregulation of lysosomal-autophagic pathway occurs at early stages of the disease, when amyloid deposits are not visible [110]. This is achieved through increased lysosome proliferation and expression of lysosomal enzymes [115]. However, with the disease progression this pathway declines, contributing to the deposition of aggregated proteins as well as other intracellular components [114]. Many products are sequestered into autophagosomes but are never cleared by the lysosome, resulting in the accumulation of cargo-containing autophagosomes in neurons [110]. In AD, both the maturation and the transport of autophagosomes are impaired, and β-amyloid-containing autophagosomes consequently accumulate within neuritis [110,116]. In addition, impaired lysosomal proteolysis may also contribute to β-amyloid accumulation. Presenilin-1 (PS-1), the AD related protein involved in the early-onset of the disease, also regulates autophagy by acidificating autolysosomes and activating cathepsin. PS-1 hypomorphic mice present impaired clearance of autophagosomes [117]. Beclin-1 expression is reduced in AD brain with age. Beclin-1 heterozygous mice present defective autophagy and neuronal degeneration, while a decrease of beclin-1 in the APP AD model enhances β-amyloid deposition and neuronal degeneration [118]. In addition, beclin-1 deficiency reduces autophagy rate and alters APP metabolism [119], suggesting that reduced autophagy via beclin-1 contributes to the deposition of β-amyloid. Drugs that modulate autophagy have proven to be beneficial for the Aβ pathology. Accordingly, the mTOR inhibiting compound rapamycin ameliorates β-amyloid deposition via autophagy enhancement, thus improving the overall cognitive performance [112].
PD is a progressive neurodegenerative disorder that affects movements and that is characterized by the accumulation of Lewy Bodies in dopaminergic neurons [9]. Lewy bodies are mainly composed out of the protein α-synuclein, ubiquitin, the E3 ligase parkin and other UPS-related proteins, suggesting a connection of the proteasome and the disease. Different approaches have been undertaken to uncover the role of the proteasome in the pathology of PD. A rat model for this disease was established by treating animals with proteasome inhibitors [120]. These rats exhibited characteristics of PD, such as bradykinesia and tremor, which was accompanied at a molecular level by α-synuclein and ubiquitin-containing inclusions in dopaminergic neurons. However, other studies could not obtain a similar output [98]. As an alternative approach, proteasome subunits knock-out mouse models were generated. Since the constitutive deletion of most of the proteasome genes is embryonically lethal, conditional knock-out models had to be developed [4]. Deletion of the ATPase subunit Psmc1/Rpt2 specifically in dopaminergic neurons lead to ubiquitin and α-synuclein positive inclusions which resulted in neuronal death, thus resembling the hallmarks of PD [121]. Interestingly, variations in the gene PSMC4/Rpt3 correlate with the age of PD onset in patients [122], suggesting a role for the 26S/30S in α-synuclein degradation. α-synuclein monomers can also be degraded by free 20S in an ubiquitin-independent process [123]. In addition, ultrastrutctural analysis in PD brains pointed to a role of autophagy in the pathogenesis of the disease [124]. Later studies showed that α-synuclein is degraded via autophagy and CMA [125,126]. Mutant α-synuclein binds to the lysosome membrane with high affinity, but cannot be transported into the lysosome. Consequently, the irreversible binding of mutant α-synuclein to the lysosome blocks the binding of other substrates, resulting in a general impairment of the CMA pathway and further α-synuclein accumulation [127]. Activation of autophagy by rapamycin treatment increases clearance of α-synuclein aggregates in cells that express mutant α-synuclein [126]. Overexpression of beclin-1 ameliorates the accumulation of α-synuclein by enhancing lysosomal function and reducing the deficits in the autophagic pathway [128]. Another crucial role of autophagy in PD is in the clearance of defective mitochondria (mitophagy). Mutations in the ubiquitin E3 ligase parkin cause an early-onset familial PD. Parkin is recruited to dysfunctional mitochondria, where it ubiquitinates proteins leading to mitochondria engulfment into autophagosomes [129]. PINK1, a serine/threonine kinase also implicated in familiar PD, participates in this mitophagic pathway by accumulating in the outer mithocondrial membrane when mitochondrial membrane potential is dissipated, where it mediates parkin recruitment [129,130]. PINK1 and parkin knockout models accumulate increasing amounts of defective mitochondria, further confirming the role of these proteins on mitophagy. Altogether, these studies open a therapeutical window for mitochondria clearance, as a treatment for PD. ALS is another progressive neurodegenerative movement disorder, that affects motor neurons [9]. Impairment of the proteasome in these neurons by conditional knock-out of Psmc4/Rpt3 revealed loss of motor neurons, locomotor dysfunction and accumulation of aggregates of TDP-43 and FUS proteins, features typical of ALS [131]. In contrast, the motor neuron-specific KO of Atg7, results in only subtle cytosolic accumulation of p62 and ubiquitin, with no TDP-43 and FUS pathologies or motor dysfunctions [131]. Therefore, under these experimental settings, proteasome rather than autophagy seems to be governing the development of ALS.
HD is an autosomal dominant disease that affects muscle coordination and leads to progressive cognitive decline and psychosis [10]. HD displays selective neurodegeneration that occurs preferentially in the brain striatum [10,132,133]. The disorder is caused by the expansion of a CAG triplet repeat region in the huntingtin gene, which translates into a polyglutamine (polyQ) stretch in the N-terminal domain of the protein and results in fibril formation and aggregation [10,134,135]. An expansion of glutamines of over 40 can trigger the development of HD and the length of the CAG stretches correlates with the disease progression and types of symptoms [135,136]; unusually long CAG expansions (> 50)cause an early onset of the disease, known as juvenile HD [137]. Huntingtin inclusions contain ubiquitinated proteins, chaperones and components of the proteasome [138]. Enhancement of the proteasome machinery has been proven beneficial in HD models. Thus, increasing the expression of PA28γ in a cellular model of HD improves cell survival [139]. Furthermore, ectopic expression of PSMD11/Rpn6 in C. elegans [140] or Rpn11 in D. melanogaster suppresses exp and ed polyQ-induced progressive neurodegeneration [141]. In contrast to the soluble form of huntingtin, the aggregated form has been found to be ubiquitinated itself [142,143], suggesting an impairment of the capacity of the proteasome to degrade aberrant huntingtin [144,145,146]. In addition, proteasome activity is reduced in brains from HD patients and mice models [144]. The exact mechanisms of the toxicity of the aggregates remain, however, unsolved but a general impairment of the proteasomal function resulting in proteostasis collapse and cellular death has been proposed [147,148]. An in vitro study suggested that the proteasome is not able to cleave within PolyQ stretches and the occasional failure of these long undegradable sequences to exit the proteasome may interfere with its function [149]. Accordingly, incubation of proteasomes with mutant huntingtin exerts an inhibitory effect on the proteasome by directly impeding the entrance of other substrates [150]. However, other studies found that huntingtin aggregates do not affect proteasome activity suggesting that proteasomal dysfunction may be a consequence of a general proteostasis collapse [142,151]. Autophagy and its failure have also been shown to play an important role in HD. The first evidence for autophagy contribution to HD pathogenesis was the observation of autophagosomes in human HD brain [152]. Indeed, mutated huntingtin aggregates can be degraded through autophagy [153,154]. This link was further confirmed when it was shown that polyglutamine aggregates can sequester mTOR and consequently prevent autophagy inhibition [101]. Pharmacological autophagy activation also ameliorates HD phenotype, while autophagy inhibition enhances the disease [154,155]. The molecular base underlying autophagy dysfunction in HD has not been fully elucidated. In cells from HD patients, as well as HD mouse models, a defect in the effective cargo recognition by autophagosomes was demonstrated [156]. Additionally, mutant huntingtin can sequester beclin-1, and consequently inhibit autophagy, what further enhances huntingtin accumulation [157]. Age-induced reduction in beclin-1 expression would also contribute to the major accumulation of huntingtin in old neurons [157]. WT huntingtin has been proposed to participate in the induction of autophagy upon endoplasmic reticulum stress [158] and it can associate with endoplasmic reticulum and autophagic vesicles [159]. Consequently, mutant huntingtin expressing cells would have a perturbed endoplasmic reticulum function and increased autophagosomes [158]. Loss of dynein function experiments have strengthen the link between autophagy and HD. Mutations that affect the dynein motor machinery are sufficient to cause motor neuron disease and the accumulation of aggregates. Decreased dynein function impairs autophagic clearance of aggregate-prone proteins and enhances the toxicity of the mutation that causes HD in fly and mouse models [160].
Ageing is accompanied by an accumulation of misfolded, damaged proteins, which can severely compromise cell function and are, in turn, associated to late-onset neurodegenerative diseases such as AD, PD and HD. The two main cellular protein clearance mechanisms, the proteasome and autophagy, decline in several tissues with age, and might contribute to the age-associated accumulation of damaged proteins. Accordingly, genetic or chemical enhancement of proteasome function and autophagic potential decreases the loading of aberrant proteins and ameliorates the symptoms and incidence of age-related disorders [140,141,161,162]. Notably, longevity-promoting mechanisms, such as reduced insulin/IGF-1 signaling pathway (IIS)or dietary restriction (DR), induce increased functionality of protein clearance mechanisms and protect from the symptoms associated to AD, PD or HD [14]. Although these studies have been performed mostly in invertebrates, this could be translated into a valuable therapeutic approach for the treatment of progressive, age-related neurodegenerative diseases. However, further studies in mammals are required to strengthen the potential link between increased protein clearance mechanisms and delay of age-related neurodegenerative diseases.
Box 1. Autophagy (macroautophagy). The autophagic process is orchestrated via the Atg proteins (from Autophagy related Genes). These proteins are involved in the formation and maturation of the autophagosomes and its fusion with the lysosome. The Atg proteins were first discovered in yeast [163] and are highly conserved in mammals [164] (see Table 1 for differential nomenclature of Atg in yeast and mammals). The autophagic process can be divided into the following steps:
1. Formation of the phagophore
Autophagy starts with the formation of the phagophore, a double membrane which can be either newly synthesized or can be originated from the endoplasmic reticulum, mitochondria or plasma membrane. In these three sites of phagophore formation the Atg proteins act as a platform to recruit further Atg proteins. The key Atg protein for the formation of the phagophore is the Atg1 complex. The mammalian Atg1 homologues are the kinases Unc-51 like kinase 1 and 2 (ULK1 and ULK2). The ULK complex is formed, among others, by ULK1/2, Atg13 and FIP200. To promote the expansion of the phagophore, mammalian phosphoinositide 3-kinase (PI3K)Vps34 complex - Vps15, Vps34, ATG14, Beclin-1, UVRAG, Rubicon produces phosphatydilinositol-3-phosphate, which is crucial for the formation of the autophagosome.
2. Elongation of the phagophore
In the second part of the autophagic process, the cytoplasmic fraction is engulfed into the phagophore. The membrane then elongates until its edges fuse and give rise to the autophagosome [165]. The elongation of the membrane involves two sequential ubiqutin- like reactions of the complex Atg12-Atg5-Atg16L. In the first reaction, Atg7, which acts as an ubiquiting-activating enzyme, catalyzes the activation of Atg12. In the second step, Atg10, mimicking an ubiquitin-conjugating enzyme, mediates the binding of active Atg12 to Atg5. The Atg12-Atg5 conjugate interacts with Atg16L and this complex associates with phagophores while it dissociates from completed autophagosomes.
3. Maturation of the phagophore
Maturation of the phagophore comes with the conjugation of LC3 (the mammalian homologue to Atg8)to phosphatidylethanolamine (PE), a process known as LC3 lipidation. LC3 lipidation can occur either via assembly through the Atg12-Atg5-Atg16L complex [166] or via processing of the newly synthesized LC3 through Atg4 to the cytosolic LC3 form (LC3I), and subsequently to the membrane binding form (LC3II). These reactions are catalyzed through Atg7 and Atg3, again in an ubiquitin-like reaction [167,168]. LC3II positive autophagosomes are trafficked to the lysosomes through the microtubule network in a dynein-dependent manner [38].
This work was supported by the Deutsche Forschungsgemeinschaft (DFG) (CECAD), the University of Cologne Advanced Postdoc Grant and the European Commission (FP7-PEOPLE-2013-CIG).
All authors declare no conflicts of interest in this paper.
[1] | P. Zhang, Z. Su, Y. Zhu, W. Li, B. Li, Ws-psc monitor: A tool chain for monitoring temporal and timing properties in composite service based on property sequence chart, in International Conference on Runtime Verification, 6418 (2010), 485–489. https://doi.org/10.1007/978-3-642-16612-9_39 |
[2] |
I. O. Electrical, I. S. Board, IEEE standard for software verification and validation, Software Qual. Prof., 2005 (2005), 1–217. https://doi.org/10.1109/IEEESTD.2005.96278 doi: 10.1109/IEEESTD.2005.96278
![]() |
[3] | E. M. Clarke, Model checking-my 27-year quest to overcome the state explosion problem, in 2009 24th Annual IEEE Symposium on Logic In Computer Science, IEEE, (2008). https://doi.org/10.1109/LICS.2009.42 |
[4] | O. J. Dahl, E. W. Dijkstra, C. A. R. Hoare, Structured Programming, Academic Press, 1972. https://doi.org/10.5555/1243380 |
[5] | C. Zhao, W. Dong, J. Wang, P. Sui, Z. Qi, Software active online monitoring under anticipatory semantics, Shm, 2009. Available from: https://smcit.ecs.baylor.edu/2011/www-smcit09/abstracts-contri_papers/karsai/DongWei_SHM.pdf. |
[6] | K. Yu, Z. Chen, W. Dong, A predictive runtime verification framework for cyber-physical systems, in 2014 IEEE Eighth International Conference on Software Security and Reliability-Companion, (2014), 247–250. https://doi.org/10.1109/SERE-C.2014.43 |
[7] |
A. Bauer, M. Leucker, C. Schallhart, Comparing ltl semantics for runtime verification, J. Log. Comput., 20 (2010), 651–674. https://doi.org/10.1093/logcom/exn075 doi: 10.1093/logcom/exn075
![]() |
[8] | A. Naskos, E. Stachtiari, P. Katsaros, A. Gounaris, Probabilistic Model Checking at Runtime for the Provisioning of Cloud Resources, Springer International Publishing, 9333 (2015). https://doi.org/10.1007/978-3-319-23820-3_18 |
[9] | A. Filieri, G. Tamburrelli, Probabilistic verification at runtime for self-adaptive systems, in Assurances for Self-Adaptive Systems, 7740 (2013). https://doi.org/10.1007/978-3-642-36249-1_2 |
[10] | A. Nouri, B. Raman, M. Bozga, A. Legay, S. Bensalem, Faster statistical model checking by means of abstraction and learning, in Runtime Verification, 8734 (2014), 340–355. https://doi.org/10.1007/978-3-319-11164-3_28 |
[11] | U. Sammapun, I. Lee, O. Sokolsky, J. Regehr, Statistical runtime checking of probabilistic properties, Springer, Berlin Heidelberg, 2007 (2007). https://doi.org/10.1007/978-3-540-77395-5_14 |
[12] | V. C. Ngo, A. Legay, V. Joloboff, Pscv: A runtime verification tool for probabilistic systemc models, in International Conference on Computer Aided Verification, 9779 (2016). https://doi.org/10.1007/978-3-319-41528-4_5 |
[13] | J. Jayaputera, I. Poernomo, H. Schmidt, Runtime verification of timing and probabilistic properties using wmi and.net, in Proceedings. 30th Euromicro Conference, IEEE, (2004), 100–106. https://doi.org/10.1109/EURMIC.2004.1333361 |
[14] | C. Zhao, W. Dong, Z. Qi, Active monitoring for control systems under anticipatory semantics, in 2010 10th International Conference on Quality Software, (2010), 318–325. https://doi.org/10.1109/QSIC.2010.82 |
[15] | H. He, Z. Zou, "Black-box modeling of ship maneuvering motion using system identification method based on bp neural network, " in The 39th International Conference on Ocean, Offshore and Arctic Engineering, (2020). https://doi.org/10.1115/OMAE2020-18069 |
[16] | S. Kundu, A. Soyyigit, K. A. Hoque, K. Basu, "High-level modeling of manufacturing faults in deep neural network accelerators, " in 2020 IEEE 26th International Symposium on On-Line Testing and Robust System Design (IOLTS), (2020). https://doi.org/10.1109/iolts50870.2020.9159704 |
[17] |
D. Angluin, Learning regular sets from queries and counterexamples, Inf. Comput., 75 (1987), 87–106. https://doi.org/10.1016/0890-5401(87)90052-6 doi: 10.1016/0890-5401(87)90052-6
![]() |
[18] |
Y. Kan, K. Yue, H. Wu, X. Fu, Z. Sun, Online learning of parameters for modeling user preference based on bayesian network, Int. J. Uncertainty Fuzzines Knowledge Based Syst., 30 (2022), 285–310. https://doi.org/10.1142/S021848852250012X \newpage doi: 10.1142/S021848852250012X
![]() |
[19] |
S. Tao, J. Jiang, D. Lian, K. Zheng, E. Chen, Predicting human mobility with reinforcement-learning-based long-term periodicity modeling, ACM Tran. Intell. Syst. Technol., 12 (2021), 1–23. https://doi.org/10.1145/3469860 doi: 10.1145/3469860
![]() |
[20] | V. Forejt, M. Kwiatkowska, D. Parker, H. Qu, M. Ujma, Incremental runtime verification of probabilistic systems, in International Conference on Runtime Verification, 7687 (2012), 314–319. https://doi.org/10.1007/978-3-642-35632-2_30 |
[21] | A. Ferrando, G. Delzanno, Incrementally predictive runtime verification. in CILC, (2021), 92–106. https://doi.org/10.1007/978-3-642-28891-3_37 |
[22] | S. D. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund, S. A. Smolka, et al., Runtime verification with state estimation, in International Conference on Runtime Verification, (2011), 193–207. https://doi.org/10.1007/978-3-642-29860-8_15 |
[23] | E. Bartocci, R. Grosu, A. Karmarkar, S. A. Smolka, S. D. Stoller, E. Zadok, et al., Adaptive runtime verification, in International Conference on Runtime Verification. (2012), 168–182. https://doi.org/10.1007/978-3-642-35632-2_18 |
[24] | Z. Chen, O. Wei, Z. Huang, H. Xi, Formal semantics of runtime monitoring, verification, enforcement and control, in International Symposium on Theoretical Aspects of Software Engineering, (2015), 63–70. https://doi.org/10.1109/TASE.2015.11 |
[25] | D. Giannakopoulou, K. Havelund, Runtime analysis of linear temporal logic specifications, in IEEE International Conference on Automated Software Engineering, (2001). Available from: http://www.riacs.edu/trs/. |
[26] | S. M. Chu, T. S. Huang, An experimental study of coupled hidden markov models, in IEEE International Conference on Acoustics, Speech, and Signal Processing, (2002). https://doi.org/10.1109/ICASSP.2002.5745559 |
[27] | N. M. Abbasi, Hidden markov methods. algorithms and implementation, 2015. Available from: https://manualzz.com/doc/o/cklvd/. |
[28] | B. Motik, Y. Nenov, R. Piro, I. Horrocks, Incremental update of datalog materialisation: the backward/forward algorithm, in Twenty-Ninth AAAI Conference on Artificial Intelligence, (2015), 1560–1568. https://doi.org/10.5555/2886521.2886537 |
[29] | An simulation platform of unmanned aerial vehicle. Available from: https://www.ardupilot.org/. |
[30] | S. Safra, On the complexity of ω-automata, in Foundations of Computer Science, W. H. Freeman, (1988), 319–327. https://doi.org/10.1109/SFCS.1988.21948 |
[31] | P. Gastin, D. Oddoux, Fast LTL to Büchi automata translation, in International Conference on Computer Aided Verification, (2001), 53–65. https://doi.org/10.1007/3-540-44585-4_6 |
[32] | LTL to deterministic Streett and Rabin automata. Available from: https://www.ltl2dstar.de/. |
[33] |
W. Liu, F. Song, G. Zhou, Reasoning about periodicity on infinite words, Appl. Microbiol. Biotechnol., 2017 (2017), 200–215. https://doi.org/10.1007/978-3-319-69483-2_12 doi: 10.1007/978-3-319-69483-2_12
![]() |
1. | Thomas Behrsing, Glen B. Deacon, Jenny Luu, Peter C. Junk, Brian W. Skelton, Allan H. White, Structural diversity of lanthanoid salicylate hydrates, 2016, 120, 02775387, 69, 10.1016/j.poly.2016.05.047 |
Autophagy step involved | Yeast | Mammals |
Formation of phagophore | Atg1 | ULK1/2 |
Atg13 | Atg13 | |
Atg17 | FIP200 | |
Atg14 | Atg14 | |
Atg6 | Beclin-1 | |
Elongation of phagophore | Atg12 | Atg12 |
Maturation of phagophore | Atg5 | Atg5 |
Atg16 | Atg16L | |
Atg7 | Atg7 | |
Atg10 | Atg10 | |
Maturation of phagophore | Atg8 | LC3/ MAP1LC3A |
Atg3 | Atg3 | |
Atg4 | Atg4 |