**Abstract**

Plant seeds, being sessile, are simultaneously exposed to favorable or adverse conditions from sowing to harvest. The physiological quality of the seed is affected by the type of biotic and abiotic stress to which the mother plant is exposed, especially in the stages of embryogenesis, development and seed filling. Therefore, the behavior of their progeny will be reflected when the seeds are capable of maintaining acceptable viability standards with a high-germination potential to generate a normal seedling and establish themselves without difficulties under field conditions. Most of the species cultivated under abiotic stress conditions reduce their physiological quality; however, some species are salt dependent, and prolonged absence of NaCl in the soil inhibits seed development, results in lower seed quality and thus limits progenyseedling growth as is the case of Suaeda salsa, and typical annual extreme halophytic herb with succulent leaves develops well and produces high-quality seeds when grown under high salinity conditions. Consequently, the response of the plant to adverse factors depends on the genotype and its stage of development at the time of stress, the duration and severity of the type of stress and the environmental factors that cause it. Depending on the severity and duration of the stress, plants could activate mechanisms to adapt or tolerate abiotic stress conditions at the molecular, morphological, physiological and cellular levels.

**Keywords:** abiotic factors, climate change, heat stress, seed germination, soil salinity, water stress

### **1. Introduction**

High-quality seed is the main input to obtain high crop yields, by producing healthy plants, resistant to diseases and to adverse conditions [1, 2]. The physical, physiological, genetic, and sanitary quality of the seeds depend on the genetic material used in sowing, management of the mother plant, climatic conditions, such as temperature, humidity, and solar intensity; likewise, the edaphic characteristics or the fertility of the soils, presence or absence of stress during the stage of germination, emergence, growth, reproduction (flowering and pollinization/fertilization, seed filling period), and harvest and post-harvest management [3–8].

Different environmental stress during seed formation that affects the final seed quality can be due to water, mineral deficiencies, salinity, and extreme temperatures among the most important; water deficiencies during grain filling, flowering, or pod formation can reduce germination potential and seed vigor [9–11]. The seed's quality is also affected when the water deficit is complemented by high temperatures, causing the production of a high proportion of small seeds with low germination and vigor [6, 12, 13]. Internal plant temperature increase causes stomatal closure and causes damage to the seed embryo due to the decrease in the thermoregulatory effect of water, thus influencing seed germination. Photosynthesis is reduced due to high temperatures and reduces the flow of the substances produced toward the seed; in this condition they are used to sustain respiration, creating an imbalance in the stage of spike formation or seed filling, and affecting the quality and size of the seeds.

On the other hand, high salinity levels generally cause a reduction in seed germination or may retard the germination process or affect plant growth by interfering with seed germination, as well as enzyme activity and unbalance mitosis mainly in glycophytic plants [14, 15]. Some species of halophyte-type plants can tolerate high levels of salinity, but the levels of germination and vigor of the seeds can be affected in the absence of salts.

In response to abiotic stress conditions, plants can activate various stress-sensitive systems, such as upregulation of stress-related proteins that function as molecular chaperones (heat shock, abundant late embryogenesis, and protein dehydrins), production of enzymatic antioxidants (catalase, superoxide dismutase, and ascorbate peroxidase), and accumulation of compatible solutes known as osmolytes (proline and glycine betaine) in plant cells subjected to osmotic stress [16]. In the case of extreme temperatures, plants show a broad structural and physiological plasticity that allows them to adapt to different temperatures [12, 17, 18].

### **2. Incidence of abiotic factors in seed quality**

When plants grow under adverse environmental conditions, the oxidative/reductive state in their cells is altered and allows the processing of a type of protein and its transport to the nucleus to regulate the expression of genes related to the homeostasis of nitric oxide (NO) and the response to abscisic acid (ABA), a key plant hormone in the response to numerous abiotic stresses (solar radiation, temperatures, humidity, and salinity); it is a survival mechanism against different abiotic stresses during seed germination or subsequent plant growth. High radiation is rarely a problem, as long as water and nutrients are available. To obtain high yields, leaves grow and cover the soil surface as soon as possible after planting; if this process is delayed, solar radiation is lost as heat embodied in bare soil, evaporating soil moisture [19]. With high temperatures, crops need a greater amount of inputs (nutrients, water, and solar radiation) to be able to maintain its level of metabolism. During the filling of the seed or grains and as the temperature increases, the development accelerates more than the growth; even under optimal management conditions, yield can be reduced by up to 4% for every 1°C increase in mean temperature due to shortening the grain-filling period [20].

The damage caused by high temperatures is commonly associated with water stress; therefore, the availability of water becomes a critical factor for the survival and initial growth of plants and in the formation and development of seeds. Consequently, to the extent that plants can transpire freely, they will also be able to cope with high temperatures; with enough water available they can withstand air temperatures of 40°C; however, if water is a limiting factor, leaves may die at that temperature.

Regarding salinity, salts can destroy the soil structure causing the expansion of clays and the dispersion of fine particles that clog the soil pores through which water and oxygen circulate [19]. The increase in salts causes very high values of osmotic pressure in the soil water, generally causes a reduction in seed germination or can slow down the germination process, interfering with the growth of most crops and other plants specialized [11, 15].

The environmental effects of seed production are complex, in that environment, the mother plant has a significant influence on seed traits including seed size, dormancy, and germination. In many species, factors such as the age of the mother plant and the position of the seed in the fruit, inflorescence, or canopy can affect seed properties, often accompanied by dimorphism of the seeds themselves or of the fruits themselves arise [6].

#### **2.1 Water stress**

#### *2.1.1 Effect of water stress on seed germination*

Crop production is highly influenced by the water level in the soil, one of the best conditions being field capacity. There are three degrees of water stress based on the relative water content (WRC), a measure that normalizes the real water content in the tissue with respect to the water potential that the tissue could have: (i) mild stress: decrease in the water potential of some bars (tenths of MPa) or WRC by 8–10% compared to well-watered plants under slight evaporative demand; (ii) moderate stress: decrease in water potential more pronounced, although less than −1.2 to −1.5 MPa or a decrease in WRC between 10 and 20%, and (iii) severe stress: when the decrease in water potential is greater than 15 bars (−1.5 MPa) or decrease in WRC greater than 20% [21].

Water deficit during grain filling, flowering, or seed coat formation reduces germination and seed vigor [10]. When water deficiency is complemented by high temperatures, the plant produces small seeds of poor physiological quality [12, 13].

Seed germination in *Citrullus lanatus* is extremely sensitive to water stress. An osmotic ψ of −430 kPa completely inhibits germination; compared to other cucurbits, the seeds of *C. lanatus* are the most sensitive [22]. However, the sensitivity of *C. lanatus* seeds to water stress is reduced when the seed coat and inner membrane are removed. Exposure to water stress causes secondary dormancy (lettuce seeds) when insufficient water potentials are present; when seeds are exposed to the environmental signal, secondary dormancy is overcome, which means that secondary dormancy is a reversible process for the seed [22].

#### *2.1.2 Effect of water stress on the agronomic characteristics of the mother plant*

Water stress causes a decrease in stomatal conductance that causes a reduction in transpiration and photosynthesis as a consequence of the decrease in total carbon (C) fixation. Water deficit also causes loss of starch reserves and nonstructural sugars that support the growth and development of the mother plant, due to the decrease in the activity of the photosynthetic enzyme galactinol synthase [23, 24]. Sucrose import is blocked and remobilization of starch reserves to the ovary walls occurs when water

**Table 1.**

*Water stress and its effect on the physiological quality of seeds.*

stress occurs 5 days before anthesis in the case of maize [25]. These water stress conditions directly affect the photosynthesis processes in the carbohydrate translocation from the leaves (source) to the seeds (sink) (**Table 1**) [27, 28].

In the seed filling stage of *Glycine max*, there is a reduction in yield due to water stress, in addition, in pre-flowering, the abortion of flowers occurs due to damage to the pistil (ovule) and not to the pollen, which reduces the number of pods and therefore seed yield; however, they are not affected in the physiological quality in terms of germination, vigor, and viability of the seeds [12, 26, 29, 30].

In the maize case (**Table 1**), the action of CWIN (cell wall invertase) and glucose concentrations lead to ovary abortion and yield loss in the face of permanent water deficit [25]. When water stress occurs during flower induction and inflorescence development, panicle development and anther dehiscence are delayed, resulting in a substantial reduction in rice and sorghum seed establishment [27].

#### **2.2 Temperature stress**

### *2.2.1 Effect of high-temperature stress on plant physiology*

Most plant species are sensitive to temperature stress and suffer when these are low or very high with respect to the thresholds defined for each one. There are few production environments with ideal temperatures (5–25°C). In response to these environmental constraints, plants display a broad structural and physiological plasticity that allows them to adapt to different temperatures caused by geography, diurnal, and seasonal rhythms [17, 18]. The answers vary if it is a temporary or permanent stress, due to high night temperatures, daytime temperatures, and the daily average, or if there is an interaction between day and night temperatures. In general, four types of heat stress

*Water Stress, Heat, and Salinity in the Physiological Quality of the Seeds DOI: http://dx.doi.org/10.5772/intechopen.107006*

are recognized in plants: that caused by sustained high temperatures; frequent episodes of high temperatures ("heat shock"); damage due to cooling (from 0 to 10°C) or "chilling injury" in numerous fruits, foliage, and tropical flowers; and freeze damage at temperatures below 0°C, which causes ice formation in plant tissues [17].

High temperatures generate anatomical, morphological, and functional changes in plants, some similar to those produced by water stress. The opening of the stomata is a response of plants to stress due to high temperatures to cool their leaves through transpiration, while in response to drought they close their stomata to reduce water loss and under conditions of combined stress due to high temperatures and lack of water the stomata remain closed [31]. Heat waves are generally accompanied by periods of drought, accelerating soil water loss, and increasing the H20 vapor pressure deficit in the air, decreasing stomatal conductance [32]. Meristems, fruits, seeds, and young leaves are closely associated with mature leaves and with the whole plant in general, through complex networks of source/sink relationships. When moderate stress occurs due to high temperatures, photosynthesis and the activity of sources and sinks are reduced simultaneously because the assimilates destined for the reproductive or conservation organs are destined to solve maintenance respiration and osmotic adjustment [33]. The photosynthetic apparatus is very susceptible to high-temperature stress; photosystem I, II, and carbon assimilation (Calvin Cycle) are the most affected processes. Consequently, the cumulative effects of these changes usually result in poor growth and reduced plant productivity [34, 35].

#### *2.2.2 High temperatures in the physiological seed quality*

The physiological seed quality can be altered due to a shorter time in the grain filling period caused by high temperatures. This stress type affects the transport and accumulation of reserve substances in the seed due to a greater fluidity of the lipids in the cell membranes of the seeds and a greater loss of electrolytes so that the seed produced under these conditions has less vigor by the low amount of reserve substances accumulated by the seeds [36, 37].

High temperatures affect the development of gametes and the double fertilization process and therefore the number of seeds formed. It also affects pollen production and viability, stigma receptivity, pollen germination, and pollen tube elongation. Therefore, exposing plants to high temperatures in early reproductive stage results in an irreversible loss of yield while in late agronomic stage losses can be reduced with some agronomic practices [38–40]. Likewise, high temperatures cause a greater production of superoxides (ROS) that could reduce the metabolic activity of the seed necessary for the germination process. Hydrogen peroxide plays important role in the germination process, however, high levels of H2O2 can be toxic to seeds [41, 42].

Reduction of the thermostability of the plasmatic membrane delays the activity of the Ca + 2 signaling, kinases, and heat shock factors are responsible for the decrease in germination and seed vigor due to thermal stress [43]. On the other hand, phytohormones related to the germination process, such as ABA and GA, have a negative interaction, especially in response to stress conditions [44]; exposure to high temperatures increases ABA concentration and decreases GA biosynthesis in seeds [45].

Likewise, substances from the group of polyamines, including putrescine, spermidine, and spermine, are recognized for their relationship with seed development and tolerance to high-temperature stress [46]. Glutathione has also been identified in tolerance to heat stress, in the regulation of redox signaling and defense processes in *Zea mays*, *Coleus blumei*, *Fagus sylvatica, Triticum aestivum,* and Vigna radiata [47–49].

#### **Table 2.**

*Temperature stress effect on physiological quality of seeds.*

High temperatures have favorable and in some cases favorable effects on the physiological quality of the seeds (**Table 2**). For example, in late pea, rice, and Lupinus sp. and in plants of the Brassica genus, stress due to high temperatures in the field affects crop phenology, fruit set, viability, germination, and the number of abnormal seedlings [41, 50, 54, 56]. In lentils (*Lens culinaris*), exposure to high temperatures reduces the grain filling period, as well as seed growth, the number of seeds per plant, seed weight, carbohydrate, protein, and mineral content; abnormalities in flowering reduce retention capacity of legumes, lower oil content in seeds in canola, and higher incidence of pathogens in seeds [53, 57–59].

In *Medicago truncatula*, the increase in temperature from 15 to 25°C favors the increase in the properties of the seed coat, regulating imbibition and physical dormancy [52]. Likewise, the stress environment with high temperatures in *Medicago* sp. is positive for faster and more uniform germination compared to seeds produced under optimal conditions [54]. In soybeans, exposure to high temperatures of 36/24°C and 42/26°C from the beginning of flowering to harvest, presents a lower accumulation of lipoxygenase, the β-conglycin, sucrose binding protein, and Bowman-Birk protease inhibitor compared to soybeans of the control under 28/22°C [62].

#### **2.3 Salinity**

Osmotic and water stress in plants generated by soil salinity is one of the main causes of the deterioration of arable land. It is estimated that there are more than 800 million hectares globally including 20% of cultivated land, with salinity being the cause of yield losses estimated at 20% worldwide in arid and semi-arid regions of the world [63–67].

*Water Stress, Heat, and Salinity in the Physiological Quality of the Seeds DOI: http://dx.doi.org/10.5772/intechopen.107006*

The process of accumulation of K and Na salts in soils, with a predominance of Ca and Mg, can be of natural origin or the product of anthropogenic activities, mainly due to the indiscriminate use of chemical fertilizers, inadequate irrigation practices, and flooding of soils with seawater in coastal regions are the main causes of soil salinization [15, 68].

There are plants that can tolerate or be completely susceptible to salinity. Most cultivated plants are salt-sensitive glycophytes. In contrast, halophytic species such as quinoa (*Chenopodium quinoa* Willd.) and *Suaeda aralocapsica*, are capable of reducing stomatal density when grown under hypersalinity conditions [5, 11, 69]. Quinoa can tolerate high levels of salinity (6 d S m -1), without a significant decrease in seed yield and total biomass [11].

Salt stress affects seed germination rate, germination initiation, and seedling establishment due to osmotic stress, ion toxicity, and oxidative stress [11, 14]. The presence of salts in the soil can reduce seed germination by decreasing the amounts

#### **Table 3.**

*Salinity stress effect on physiological quality of seeds.*

of gibberellic acids (GA), increasing the levels of abscisic acid (ABA), and altering cell membrane permeability and water behavior within the seed [64]. However, the presence of salts may not always be detrimental to all crops (**Table 3**); some species require salts from the germination stage [5, 11]. In halophytic plant types such as *S. salsa*, the prolonged absence of NaCl inhibits development and affects seed quality; as a consequence, it limits the growth of progeny seedlings in terms of biomass and seed yield [76, 81]. In C. quinoa and *S. aralocapsica* with 0.3 M NaCl and 1.5 M NaCl, the percentage of seed germination is reduced between 10 and 20% [5, 11, 69]. In the case of rice seeds, they are relatively tolerant during germination and very sensitive at the seedling stage; after establishment, plant tolerance increases progressively until panicle differentiation, and decreases again until the flowering stage [82].


**Thiamethoxam: An Inseticide that Improve Seed Rice Germination at Low Temperature**

Andréia da Silva Almeida, Francisco Amaral Villela, João Carlos Nunes, Geri Eduardo Meneghello and Adilson Jauer

Additional information is available at the end of the chapter

http://dx.doi.org/10.5772/53207


*2.3. Processing of Size-Fractionated Aerosol Concentration Data*

The utilization of portable aerosol instruments with different particle diameter ranges and cutoff diameters enables derivations of size-fractionated particle number and mass concentrations [47]: Super-micron (1–10 μm) particle number and mass concentrations, submicron (0.01–1 μm) particle number concentrations, PM2.5 mass concentrations, PM10 mass concentrations, and PM10–1 mass concentrations. Additionally, we derived the particle number size distribution *n*0 *N* = *dN dlog*(*Dp*) within eight diameter bins:

The particle mass size distribution was estimated from the particle number size distribution by assuming spherical particles:

$$m\_M^0 = \frac{dM}{d\log\left(D\_p\right)} = \frac{dN}{d\log\left(D\_p\right)}\frac{\pi}{6}D\_p^3\rho\_p = n\_N^0\frac{\pi}{6}D\_p^3\rho\_p\tag{1}$$

where *n*0 *M* is the particle mass size distribution, *dM* is the particle mass concentration within a certain diameter bin normalized to the width of the diameter range *dlog Dp* of that diameter bin, *dN* is the particle number concentration within that diameter bin (also normalized with respect to *dlog Dp* to obtain the particle number size distribution, *n*0 *N*), *Dp* is the particle diameter, and ρ*p* is the particle density, here assumed to be unit density (1 g cm−3). In practice, the particle density is size-dependent and variable for different aerosol populations (i.e., diesel soot vs. organic aerosol); therefore, size-resolved effective density functions should be used. However, there is limited empirical data on the effective densities of aerosols produced by indoor emission sources. Thus, the assumption of 1 g cm−3 for the particle density will result in uncertainties (over- or underestimates, depending on the source) in the estimated mass concentrations.

The size-fractionated particle number concentration was calculated as:

$$PN\_{D\_{p2} - D\_{p1}} = \bigcap\_{D\_{p1}}^{D\_{p2}} n\_N^0(D\_P) \cdot d\log(D\_P) \tag{2}$$

where *PNDp*2−*Dp*1 is the calculated size-fractionated particle number concentration within the particle diameter range *Dp*1*–Dp*2. Similarly, the size-fractionated particle mass concentration *PMDp*2−*Dp*1 was calculated as:

$$P M\_{D\_{p2} - D\_{p1}} = \int\_{D\_{p1}}^{D\_{p2}} n\_M^0(D\_P) \cdot d\log(Dp) = \int\_{D\_{p1}}^{D\_{p2}} n\_N^0(D\_P) \frac{\pi}{6} D\_p^3 \rho\_{p'} d\log(Dp) \tag{3}$$

PM2.5 and PM10 can be also calculated by using Equation (3) and integrating over the particle diameter range starting from 10 nm (i.e., the lower cutoff diameter according to our instrument setup) and up to 2.5 μm (for PM2.5) or 10 μm (for PM10).


**2. Evolution of ethics**

Evolution of biologically-centered ethical guidelines in medical or biomedical research has upgraded the understanding of ethics over the years. Various guidelines and declarations evolved over the period, including international and national, are mentioned as below:


Probabilistic programs extend traditional programs with the ability to flip coins or, more generally, sample values from probability distributions. These programs can be used to encode randomized algorithms and randomized mechanisms in security [7] in a natural way. The interest in probabilistic programs has significantly increased in recent years. To a large extent, this is due to the search in AI for more expressive and succinct languages than probabilistic graphical models for Bayesian inference [17]. Probabilistic programs have many applications [24]. They are used in, amongst others, machine learning, systems biology, security, planning and control, quantum computing, and software–defined networks. Probabilistic variants of many programming languages exist.

Procedural programs allow for declaration of procedures—small independent code blocks—and the ability to call procedures from one another, possibly in

This work is supported by the DFG research training group 2236 UnRAVeL and the ERC advanced research grant 787914 FRAPPANT.

Fig. 1. Recursive probabilistic program modeling the outbreak of an infectious disease. uniform(a, b) stands for the discrete uniform distribution on [a, b].

a recursive fashion. Most common programming languages such as C, Python, or Java support procedures. It is thus not surprising that recursion is a key ingredient in many modern probabilistic programming languages (PPL). In fact, many early approaches to extend Bayesian networks focused on incorporating recursion [26,19,11,27]. Randomized algorithms such as Hoare's quicksort with random pivot selection can be straightforwardly programmed using recursion. Recursion is also a first-class citizen in modeling rule-based dependencies between molecules or populations in systems biology (e.g., modeling reproduction).

This paper studies the automated verification of probabilistic pushdown automata [14] (pPDA) as an explicit-state operational model of procedural probabilistic programs against temporal specifications. As a motivating example, let us consider a simple epidemiological model for the outbreak of an infectious disease in a large population where the number of susceptible

Y 1.5 1 E 0.5 2 Fig. 2. Example infec-

Y E

tion rates by age groups. individuals can be assumed to be infinite. Our example model distinguishes young and elderly persons. Each affected individual infects a uniformly distributed number of others, with varying rates (expected values) according to the age groups (Figure 2). The fatality rate for infected elderly and young persons is 1% and 0%, respectively. Initially, we assume there is a single infected young person, i.e., the overall program is started by calling infectYoung(). It is an easy task for any working programmer to specify this model as a discrete probabilistic program with mutually recursive procedures (Figure 1). Note that this program can be easily amended to more realistic models involving, e.g., more age or gender groups, other distributions, hospitalization rate, etc.

The operational behavior of programs such as the one in Figure 1 can be naturally described by pPDA. The technical details of such a translation are beyond the scope of this paper but let us provide some intuition (more details can be found e.g. in [2]). Roughly, the local states of the procedures—the valuation of the local variables and the position of the program counter—constitute both the state space and the stack alphabet of the automaton. Procedure calls correspond to push transitions in the automaton in such a way that the program's procedure stack is simulated by the automaton's pushdown stack, i.e., the current local state is saved on top of the stack. Accordingly, returning from a procedure corresponds to taking a pop transition in order to restore the local state of the caller. Returning a value can be handled similarly. Clearly, if the reachable local state spaces of the involved procedures are finite, then the resulting automaton will be finite as well.

A number of relevant questions such as "Will the virus eventually become extinct?" (termination probability) or "What is the expected number of fatalities?" (expected costs) can be decided on finite pPDA (see [9] for a survey). In this work, we focus on temporal properties, e.g., questions that involve reasoning about the chronological order of certain events of interest during the epidemic. An example are chains of infection: For instance, we might ask

What is the probability that eventually a young person with only young persons in their chain of infection passes the virus on to an elderly person who then dies?

On the level of the program in Figure 1, this corresponds to the probability of reaching a global program configuration where the call stack only contains infectYoung() invocations and during execution of the current infectYoung(), the local variable f is eventually set to true. This requires reasoning about the nestings of calls and returns of a computation. In fact, in order to decide if f = true in the current procedure, we must "skip" over all calls within it and only consider their local return values. This requirement and many others can be rather naturally expressed in the logic CaRet [3], an extension of LTL:

$$
\Diamond^g \left( \Box^- p\_Y \wedge p\_Y \wedge \Diamond^a f \right) \Box
$$

Here, pY is an atomic proposition that holds at states which correspond to being in procedure infectYoung, and f indicates that f = true. Intuitively, the above formula states that eventually (outer ♦ g ), the computation reaches a (global) state where only infectYoung is on the call stack and the current procedure is infectYoung as well (−pY ∧ pY ), and moreover the local—aka abstract—path within in the current procedure reaches a state where f is true (♦ af). Such properties are in general context-free but not always regular and thus cannot be expressed in LTL [3].

Technical Contribution. We are given a (finite) pPDA ∆ and a CaRet formula ϕ and we are interested in determining the probability that a random trajectory of ∆ satisfies ϕ. In order for this problem to be decidable [13], we need to impose a mild visibility restriction on ∆, yielding a probabilistic visibly pushdown automaton (pVPA). Just like several previous works on model checking pPDA against ω-regular specifications [14,10,21], we follow the automata-based approach (see Figure 3). More specifically, we first translate ϕ into an equivalent non-deterministic B¨uchi visibly pushdown automaton [4] (VPA) A and then determinize it using a result of [22]. The resulting DVPA D uses a so-called stair-parity [22] acceptance condition that is strictly more expressive than standard parity or Muller DVPA [4]. Stair-parity differs from usual parity in that 452 T. Winkler, C. Gehnen, J.-P. Katoen

Fig. 3. Chain of reductions used in this paper. ETR stands for existential theory of the reals, i.e., the existentially quantified fragment of the FO-theory over (R, +, ·, ≤).

it only considers certain positions—called steps [22]—of an infinite word where the stack height never decreases again. We then construct a standard product ∆×D. Here, the visibility conditions ensure that the automata synchronize their stack actions, yielding a product automaton that uses a single stack instead of two independent ones, which would lead to undecidability [13]. Finally, we are left with computing a stair-parity acceptance probability in the product, which is itself a pPDA. This is achieved by constructing a specific finite Markov chain associated to ∆ × D, called step chain in this paper. Intuitively, the step chain jumps from one step of a run to the next, and therefore we only need to evaluate standard parity rather than stair-parity on the step chain. The idea of step chains is due to [14] where they were used to show decidability against deterministic non-pushdown B¨uchi automata. For constructing the step chain, certain termination probabilities of the pPDA need to be computed. These are in general algebraic numbers that cannot always be expressed by radicals [16], let alone by rationals. However, the relevant problems are still decidable via an encoding in the existential fragment of the FO-theory of the reals (ETR) [21].

The resulting main contributions of this paper are complexity results, summarized in Figure 4, and algorithms for quantitative model checking of pPDA against ω-VPL given in terms of either deterministic automata, non-deterministic automata, or as CaRet formulae. As common in the literature, we consider the special case of qualitative, or almost-sure (a.-s.), model checking separately. To the best of our knowledge, none of these problems was known to be decidable before. The work of [13] proved decidability of model checking against deterministic Muller VPA which capture a strict subset of the CaRet-definable languages [4]. As a lemma of independent interest, we show that the step chain can be used for checking all kinds of measurable properties defined on steps, even beyond parity.

Related work. We have already mentioned various works on recursion in probabilistic graphical models (and PPL) as well as on verifying pPDA and the equivalent model of recursive Markov chains [16]. The analysis of these models focuses on reachability probabilities, ω-regular properties or (fragments of) probabilistic CTL, expected costs, and termination probabilities. The computation of termination probabilities in recursive Markov chains and variations thereof with non-determinism is supported by the software tool PReMo [29]. Our paper can be seen as a natural extension from checking pPDA against ω-regular properties to ω-visibly pushdown languages. In contrast to these algorithmic approaches, various deductive reasoning methods have been developed for recursive

Fig. 4. Complexity results of this paper.

probabilistic programs. Proof rules for recursion were first provided in [20], and later extended to proof rules in a weakest-precondition reasoning style [23,25]. Olmedo et al. [25] also address the connection to pPDA and provide proof rules for expected run-time analysis. A mechanized method for proving properties of randomized algorithms, including recursive ones, for the Coq proof assistant is presented in [5]. The Coq approach is based on higher–order logic using a monadic interpretation of programs as probabilistic distributions.

Organization. We review the basics about VPA and CaRet in Section 2. Section 3 introduces probabilistic visibly pushdown automata (pVPA). The stair-parity DVPA model checking procedure is presented in Section 4, and the results for B¨uchi VPA and CaRet in Section 5. We conclude the paper in Section 6.

### 2 Visibly Pushdown Languages

We fix some general notation for words first. Given a non-empty alphabet Σ, let Σ∗ be the set of finite words (this includes the empty word ), and let Σω be the set of infinite words over Σ. For i ≥ 0, the i-th symbol of a word w ∈ Σ∗ ∪ Σω is denoted w(i) if it exists. |w| denotes the length of w.

### 2.1 Visibly Pushdown Automata

A finite alphabet Σ is called a pushdown alphabet if it is equipped with a partition Σ = Σcall ] Σint ] Σret into three—possibly empty—subsets of call, internal, and return symbols. A visibly pushdown automaton [4] (VPA) over Σ is like a standard pushdown automaton with the additional syntactic restriction that reading a call or return symbol triggers a push or a pop transition, respectively. Reading an internal symbol, on the other hand, does not affect the stack at all.

Definition 1 (VPA [4]). Let Σ be a pushdown alphabet. A visibly pushdown automaton (VPA) over Σ is a tuple A = (S, s0, Γ, ⊥, δ, Σ) with S a finite set of states, s0 ∈ S an initial state, Γ a finite stack alphabet, ⊥ ∈ Γ a special bottom-of-stack symbol, and δ = (δcall, δint, δret) a triple of relations

δcall ⊆ (S ×Σcall)×(S ×Γ-⊥) , δint ⊆ (S ×Σint)×S , δret ⊆ (S ×Σret ×Γ)×S

where Γ-⊥ = Γ \ { ⊥ }. For s, t ∈ S, Z ∈ Γ, and a ∈ Σ, we use the shorthand notations s a−→ tZ, s a−→ t, sZ a−→ t to indicate that there exist transitions (s, a, t, Z) ∈ δcall, (s, a, t) ∈ δint, (s, a, Z, t) ∈ δret, respectively. Note that e.g. s a−→ tZ implies implicitly that a ∈ Σcall and Z 6= ⊥, and similar for internal and return transitions. Intuitively, call transitions push a new symbol Z onto the stack, internal transitions ignore the stack, and return transitions pop the topmost symbol Z from the stack (unless Z = ⊥, in which case nothing is popped). A configuration of VPA A is a tuple (s, γ) ∈ S × Γ ∗ , written more succinctly as sγ in the sequel. Let w ∈ Σω be an infinite input word. An infinite sequence ρ = s0γ0, s1γ1 . . . of configurations is called a run of A on w if s0γ0 = s0⊥ and for all i ≥ 0, exactly one of the following cases applies:

$$\begin{aligned} & -\ w(i) \in \Sigma\_{\text{call}} \text{ and } \gamma\_{i+1} = \gamma\_i Z \text{ for some } Z \in \varGamma\_{\perp} \text{ such that } s\_i \xrightarrow{w(i)} s\_{i+1} Z; \text{or} \\ & -\ w(i) \in \Sigma\_{\text{int}} \text{ and } \gamma\_{i+1} = \gamma\_i \text{ and } s\_i \xrightarrow{w(i)} s\_{i+1}; \text{or} \\ & -\ w(i) \in \Sigma\_{\text{ret}} \text{ and } \gamma\_{i+1} Z = \gamma\_i \text{ for some } Z \in \varGamma\_{\perp} \text{ such that } s\_i Z \xrightarrow{w(i)} s\_{i+1}, \text{ or} \\ & \gamma\_i = \gamma\_{i+1} = \perp \text{ and } s\_i \xrightarrow{w(i)} s\_{i+1}. \end{aligned}$$

A B¨uchi acceptance condition for A is a subset F ⊆ S. A VPA equipped with a B¨uchi condition is called a B¨uchi VPA. An infinite word w ∈ Σω is accepted by a B¨uchi VPA if there exists a run s0γ0, s1γ1, . . . of A on w such that si ∈ F for infinitely many i ≥ 0. The ω-language of words accepted by a B¨uchi VPA A is denoted L(A) ⊆ Σω.

Definition 2 (ω-VPL [4]). Let Σ be a pushdown alphabet. L ⊆ Σω is an ω-visibly pushdown language (ω-VPL) if L = L(A) for a B¨uchi VPA A over Σ.

A VPA is deterministic (DVPA) if it has exactly one run on each input word. In this case, δcall, δint, and δret can be viewed as (total) functions. As for standard NBA, the class of languages recognized by B¨uchi DVPA is a strict subset of the languages recognized by non-deterministic B¨uchi VPA. Unlike in the nonpushdown case, DVPA with Muller or parity conditions are also strictly less expressive than non-deterministic B¨uchi VPA [4]. A deterministic automaton model for ω-VPL was given in [22]. It uses a so-called stair-parity acceptance condition which is the topic of the next subsection.

### 2.2 Steps and Stair-parity Conditions

Let us fix a pushdown alphabet Σ and a VPA A over Σ. Consider a run ρ = s0γ0, s1γ1, . . . of A on an infinite word w ∈ Σω. We define the stack height of the i-th configuration as sh(ρ(i)) = |γi | − 1 (the bottom symbol ⊥ does not count to the stack height). The stair-parity condition relies on the notion of steps:

Definition 3 (Step). Let ρ be a run of A. Position i ≥ 0 is a step of ρ if

$$\forall n \ge i \colon \quad sh(\rho(n)) \ge \; sh(\rho(i)) \; .$$

Fig. 5. Left: An example VPA (in fact, a DVPA) with Γ = {Z, ⊥ } over input alphabet Σ = { c } ] { τ } ] { r }. Transitions labeled c, Z are call transitions which push Z on the stack, the transitions labeled with τ are internal ones that ignore the stack, and those labeled Z, r and ⊥, r are return transitions that are only enabled if Z (⊥, resp.) is on top of the stack; when executing Z, r we also pop Z from the stack. However, the special bottom-of-stack symbol ⊥ can never be popped (see e.g. pos. 1). Right: The unique run of the DVPA on input word τ r c τ τ c r c2 r 2 c 3 r 3 . . .. Steps are underlined.

Abusing terminology, we may also refer to the configurations at the step positions of a run as steps.

Example 1. Figure 5 depicts a DVPA and the initial fragment of its unique run ρ on the input word τ r c τ τ c r c2 r 2 c 3 r 3 . . .. The step positions are underlined, i.e., positions 0-5, 7, 11, and 17 are steps. Note that if ρ(i) = s⊥ for some s ∈ S then i is a step, i.e., bottom configurations are always steps.

Steps play a central role in the rest of the paper. We therefore explain some of their fundamental properties.

Remark 1. One can also define the steps of a word w ∈ Σω as the positions where a run of any arbitrary VPA on w has a step. Due to the visibility restriction, the actual behaviour of the VPA does not influence the step positions [22]. In other words, the step positions are predetermined by the input word. Thus, we can also speak of the stack height sh(w(i)) of word w at position i.

We need one last notion before defining stair-parity. The footprint of an infinite run ρ = s0γ0, s1γ1, . . . is the infinite sequence ρ↓Steps = sn0 sn1 . . . ∈ S ω where for all i ≥ 0 the position ni is the i-th step of ρ. Phrased differently, ρ↓Steps is the projection of the run ρ onto the states occurring at its steps. For the example run in Figure 5 (right), ρ↓Steps = s0s1s1s0s ω 1 .

Definition 4 (Stair-parity [22]). Let A be a VPA over pushdown alphabet Σ. A stair-parity acceptance condition for A is defined in terms of a priority function Ω : S → N0. i.e. A word w ∈ Σω is accepted if A has a run ρ on ω s.t.

$$\min \left\{ k \in \mathbb{N}\_0 \: \mid \: \exists i \colon \ \Omega(\rho \downarrow\_{Steps}(i) \;) = k \right\}.$$

is even. The language accepted by A is denoted L(A).

Example 2. The DVPA in Figure 5 with Ω(s0) = 1 and Ω(s1) = 2 accepts

$$\mathcal{L}\_{repbda} = \left\{ w \in \Sigma^{\omega} \; | \; \exists B \ge 0, \; \exists i \ge 0 \colon sh(w(i)) \le B \right\},$$

the language of repeatedly bounded words [22], i.e., words whose stack height (cf. Remark 1) is infinitely often at most a constant B. It is known that Lrepbdd is not expressible by DVPA with usual parity conditions [4].

Theorem 1 ([22, Thm. 1]). For every non-deterministic B¨uchi VPA A there exists a deterministic stair-parity DVPA D with 2 O(|S| 2 ) states such that L(A) = L(D). Moreover, D can be constructed in exponential time in the size of A.

It was also shown in [22] that stair-parity DVPA characterize exactly the class of ω-VPL (and are thus not more expressive than non-deterministic B¨uchi VPA).

### 2.3 CaRet, a Temporal Logic of Calls and Returns

Specifying requirements directly in terms of automata is tedious in practice. CaRet [3] is an extension of Linear Temporal Logic (LTL) that can be used to describe ω-VPL. Its syntax is defined as follows:

Definition 5 (CaRet [3]). Let AP be a finite set of atomic propositions. The logic CaRet adheres to the grammar

$$\varphi \vDash = \begin{array}{c} p \mid \varphi \lor \varphi \mid \neg \varphi \mid \bigcirc^g \varphi \mid \varphi \mathcal{U}^g \varphi \mid \bigcirc^a \varphi \mid \varphi \mathcal{U}^a \varphi \mid \bigcirc^- \varphi \mid \varphi \mathcal{U}^- \varphi \mid \end{array}$$

where p ∈ AP ∪ { call, int,ret }.

Other common modalities such as ♦ b and b for b ∈ { g, a, − } are defined as usual via ♦ bϕ = true U b ϕ, and bϕ = ¬♦ b¬ϕ. We briefly explain the semantics of CaRet, the formal definition can be found in [3] or the full version [28]. We assume familiarity with LTL. CaRet formulae are interpreted over infinite words from the pushdown alphabet Σ = 2AP × { call, int,ret }. g and U g are the standard next and until modalities from LTL (called global next and until

Fig. 6. CaRet's various next modalities applied to the initial fragment of an example word. Call, internal, and return positions are depicted as boxes, circles, and rhombs, resp. Note that a of position 3 is undefined because g is a return.

in CaRet). CaRet extends LTL by two key operators, the caller modality − and the abstract successor a , see Figure 6. The former is a past modality that refers to the position of the last pending call. For internal and return symbols, the abstract successor a behaves like g unless the latter is a return, in which case a is undefined (e.g. pos. 3 in the example). On the other hand, the abstract successor of a call symbol is its matching return if it exists, or undefined otherwise. The until modalities U − and U a are defined over the paths induced by the callers and abstract successors, respectively. Note that the caller path is always finite and the abstract path can be either finite or infinite. A prime application of CaRet is to state Hoare-like total correctness of a procedure F [3]:

$$\begin{array}{rcl} \varphi\_{total} & = & \Box^g \left( \mathsf{call} \wedge p \wedge p\_F \to \Box^a q \right) \end{array}$$

where p and q are atomic propositions that hold at the states where the pre- and post-condition is satisfied, respectively, and pF is an atomic proposition marking the calls to F. Another example is the language of repeatedly bounded words from Example 2; it is Lrepbdd = L(♦ gg (call → a ret)). Further examples are given in [3]. The language defined by a CaRet formula ϕ is denoted L(ϕ).

Theorem 2 ([1, Thm. 5.1]). CaRet-definable languages are ω-VPL: For each CaRet formula ϕ there exists a (non-deterministic) B¨uchi VPA A such that L(ϕ) = L(A), and A can be constructed in time 2 O(|ϕ|) .

The above theorem is well-known in the literature [1,2] even though it is usually stated for Nested Word Automata (NWA) which are equivalent to VPA, and it is more common to state a space bound on A rather than a time bound for the construction. The theorem also applies to more expressive extensions of CaRet [1] which we do not consider here for the sake of simplicity.

### 3 Probabilistic Visibly Pushdown Automata

As explained in the introductory section, we employ probabilistic pushdown automata [14] (pPDA) as an operational model for procedural probabilistic programs. pPDA thus play a fundamentally different role in this paper than VPA (cf. Definition 1): While the former are used to model the system, the latter encode the specification. Consequently, our pPDA do not read an input word like VPA do, but instead take their transitions randomly, according to fixed probability distributions. In this way, they define a probability space over their possible traces, i.e., runs projected on their labeling sequence. These traces constitute the input words of the VPA. In order for the model checking problems to be decidable [13], a syntactic visibility restriction related—but not exactly analogous—to the one required by VPA needs to be imposed on pPDA. In a nutshell, the condition is that each state only has outgoing transitions of one type, i.e., push, internal, or pop. This means that the stack operation is visible in the states (recall that for VPA, the stack operation is visible in the input symbol). This restriction is not severe in the context of modeling programs (see Remark 2 further below) and leads to our notion of probabilistic visibly pushdown automata (pVPA) which we now define formally.

Given a finite set X, we write D(X) = { f : X → [0, 1] | P a∈X f(a) = 1 } for the set of probability distributions on X.

Definition 6 (pVPA). A probabilistic visibly pushdown automaton (pVPA) is a tuple ∆ = (Q, q0, Γ, ⊥, P, Σ, λ) where Q is a finite set of states partitioned into Q = Qcall]Qint]Qret, q0 ∈ Q is an initial state, Γ is a finite stack alphabet, ⊥ ∈ Γ is a special bottom-of-stack symbol, P = (Pcall, Pint, Pret) is a triple of functions with signature

Pcall : Qcall → D(Q × Γ-⊥) , Pint : Qint → D(Q) , Pret : Qret × Γ → D(Q) ,

Σ = Σcall ] Σint ] Σret is a pushdown alphabet, and λ: Q → Σ is a state labeling function consistent with the visibility condition, i.e., for all type ∈ {call, int,ret} and all q ∈ Q, we have that q ∈ Qtype iff λ(q) ∈ Σtype.

Intuitively, the behavior of a pVPA ∆ is as follows. If the current state q is a call state, then the probability distribution Pcall(q) determines a random successor state and stack symbol to be pushed on the stack (⊥ cannot be pushed). Similarly, if the current state is internal, then Pint(q) is the distribution over possible successor states and the stack is ignored completely. Lastly, if the current state is a return state and symbol Z ∈ Γ is on top of the stack, then Pret(q, Z) once again determines the probability distribution of successor states, and additionally Z is removed from the stack. Similar to VPA, the bottom symbol ⊥ is the only exception to this rule, it can never be removed. Thus, pVPA are a generalization of labeled Markov chains, which correspond to the special case Q = Qint.

We now define the semantics of pVPA more formally. For q, r ∈ Q, Z ∈ Γ and p > 0 we use the shorthand notations q p −→ rZ, q p −→ r, and qZ p −→ r to indicate that Pcall(q)(r, Z) = p, Pint(q)(r) = p, and Pret(q, Z)(r) = p, respectively. As for VPA, a configuration of a pVPA is an element qγ ∈ Q×Γ ∗ . An (infinite) run of a pVPA is a sequence of configurations ρ = q0γ0, q1γ1, . . . such that q0γ0 = q0⊥ and for all i ≥ 0 we have that either

$$1. \ q\_i \in Q\_{\mathsf{call}}, \ \gamma\_{i+1} = \gamma\_i Z \text{ for some } Z \in \Gamma\_{\ast \perp} \text{ and } q\_i \xrightarrow{p} q\_{i+1} Z;$$

Note that our pVPA only produce infinite runs and do not simply "terminate" upon reaching the empty stack as in e.g. [14]. In fact, in our case the stack cannot be empty due to the special bottom symbol ⊥ that can never be popped. We have chosen to avoid finite pVPA runs for compatibility with CaRet which describes ω-languages per definition. Nonetheless, terminating behavior can be easily simulated in our framework by moving to a dedicated sink state once the pVPA attempts to pop ⊥ for the first time.

The set of all runs of a pVPA ∆ is denoted Runs∆. We extend ∆'s labeling function λ to runs ρ ∈ Runs∆ by applying it to each state along ρ individually, yielding a word λ(ρ) ∈ Σω. Steps of pVPA runs are defined as in Definition 3. An example pVPA and its possible runs are depicted in Figure 7 on page 14.

We can view the set of all configurations Q × Γ ∗ as the (infinite) state space of a discrete-time Markov chain. In this way, we obtain a probability space (Runs∆, F, P) via the usual cylinder set construction [6, Ch. 10].

Remark 2. The visibility restriction of our pVPA is slightly different from the definition given in [13] which requires all incoming transitions to a state to be of the same type, i.e., call, internal, or return. Our definition, on the other hand, imposes the same requirement on the states' outgoing transitions. We believe that our condition is more natural for pVPA obtained from procedural programs, such as the one in Figure 1. In fact, programs where randomness is restricted to internal statements such as x := bernoulli(0.5) or x := uniform(0, 3) naturally comply with our visibility condition because all call and return states of such programs are deterministic and thus cannot violate visibility. However, the alternative condition of [13] is not necessarily fulfilled for such programs.

We can now formally state our main problem of interest:

Definition 7 (Probabilistic CaRet Model Checking). Let AP be a finite set of atomic propositions, ϕ be a CaRet formula over AP, ∆ be a pVPA with labels from the pushdown alphabet Σ = 2AP × { call, int,ret }, and θ ∈ [0, 1] ∩ Q. The quantitative CaRet Model Checking problem is to decide whether

$$\mathbb{P}(\{\rho \in Runs\_{\Delta} \mid \lambda(\rho) \in \mathcal{L}(\varphi)\}) \geq\_{?} \theta \ . $$

The qualitative CaRet Model Checking problem is the special case where θ = 1.

The probabilities in Definition 7 are well-defined as ω-VPL are measurable [22].

### 4 Model Checking against Stair-parity DVPA

In this section, we show that model checking pVPA (Definition 6) against VPL given in terms of a stair-parity DVPA (Definition 4) is decidable. This is achieved by first computing an automata-theoretic product of the pVPA and the DVPA and then evaluating the acceptance condition in the product automaton.

### 4.1 Products of Visibly Pushdown Automata

In general, pushdown automata are not closed under taking products as this would require two independent stacks. However, the visibility conditions on VPA and pVPA ensure that their product is again an automaton with just a single stack because the stack operations (push, nop, or pop) are forced to synchronize.

We now define the product formally. An unlabeled pVPA is a pVPA where the labeling function λ and alphabet Σ are omitted.

Definition 8 (Product ∆ × D). Let ∆ = (Q, q0, Γ, ⊥, P, Σ, λ) be a pVPA, and D = (S, s0, Γ0 , ⊥, δ, Σ) be a DVPA over pushdown alphabet Σ.

If the DVPA D is equipped with a priority function Ω : S → N0, then we extend Ω to Ω0 : Q × S → N0 via Ω0 (q, s) = Ω(s).

It is not difficult to show that ∆×D is indeed a well-defined pVPA and moreover satisfies the following property (the proof is standard, see [28]):

Lemma 1 (Soundness of ∆ × D). Let ∆ be a pVPA and D be a stairparity DVPA with priority function Ω, both over pushdown alphabet Σ. Then the product pVPA ∆ × D with priority function Ω0 as in Definition 8 satisfies

P({ ρ ∈ Runs∆ | λ(ρ) ∈ L(D) }) = P({ ρ ∈ Runs∆×D | ρ↓Steps ∈ ParityΩ0 }),

where ParityΩ0 denotes the set of words in (Q×S) ω satisfying the standard parity condition defined by Ω0 . Moreover, ∆×D can be constructed in polynomial time.

Remark 3. It is not actually important that the product satisfies the visibility condition. All techniques we apply to the product also work for general pPDA.

### 4.2 Stair-parity Acceptance Probabilities in pVPA

Lemma 1 effectively reduces model checking pVPA against stair-parity DVPA to computing stair-parity acceptance in the product, which is again an (unlabeled) pVPA. We therefore focus on pVPA in this section and do not consider DVPA.

Throughout the rest of this section, let ∆ = ( Q, q0, Γ, ⊥, P ) be an unlabeled pVPA. On the next pages we describe the construction of a finite Markov chain M∆ that we call the step chain of ∆. Loosely speaking, M∆ simulates jumping from one step (see Definition 3) of a run of ∆ to the next. A similar idea first appeared in [14]. Our construction, however, differs from the original one in various aspects. We discuss this in detail in Remark 5 further below.

Steps as events. For all n ∈ N0, we define a random variable V (n) on Runs∆ whose value is either the state q of ∆ at the n-th step, or the extended state q⊥ in the special case where the n-th step occurs at a bottom configuration of the form q⊥, for some q ∈ Q. We denote the set of all such extended states with Q⊥ = { q⊥ | q ∈ Q }. Formally, V (n) : Runs∆ → Q ∪ Q⊥ is defined as

$$V^{(n)}(\rho) \quad = \begin{cases} q & \text{if } \operatorname{step}\_n(\rho) = q\gamma \text{ and } \gamma \neq \bot \\ q \bot & \text{if } \operatorname{step}\_n(\rho) = q\bot \end{cases},$$

where stepn(ρ) denotes the configuration at the n-th step of ρ. Note that V (0) = q0⊥ because the first position of a run is always a step.

Lemma 2. For all n ∈ N0 and v ∈ Q ∪ Q⊥, the event V (n) = v is measurable, and thus V (n) is a well-defined random variable.

We can view the sequence V (0), V (1) . . . of random variables as a stochastic process. It is intuitively clear that for all n ∈ N0, the value of V (n+1) depends only on V (n) , but not on V (i) for i < n. This is due to the more general observation that the state q at any step configuration qγ (with γ 6= ⊥) fully determines the future of the run because being a step already implies that no symbol in γ can ever be read as reading it implies popping it from the stack. In particular, q determines the probability distribution over possible next steps. A similar observation applies to bottom configurations of the form q⊥. Phrased in probability theoretical terms, the process V (0), V (1) . . . has the Markov property, i.e.,

$$\mathbb{P}(V^{(n)}=v\_n \mid V^{(n-1)}=v\_{n-1} \land \dots \land V^{(0)}=v\_0) = \mathbb{P}(V^{(n)}=v\_n \mid V^{(n-1)}=v\_{n-1}) \tag{1}$$

holds for all values of v0, . . . , vn such that the above conditional probabilities are well-defined 1 . This was proved in detail in [14]. It is also clear that the Markov process is time-homogeneous in the sense that

$$\mathbb{P}(V^{(n+1)}=v \mid V^{(n)}=v') \quad = \quad \mathbb{P}(V^{(n'+1)}=v \mid V^{(n')}=v')$$

holds for all n, n0 ∈ N0 for which the two conditional probabilities are welldefined. The following example provides some intuition on these facts.

Example 3. Consider the pVPA in Figure 7 (left). The initial fragments of its two equiprobable runs are depicted in the middle. In this example, it is easy to read off the next-step probabilities P(V (n) = vn | V (n−1) = vn−1) for all n ∈ N0 and vn, vn−1 ∈ Q ∪ Q⊥. They are summarized in the Markov chain on the right. For example, V (0) = q0⊥ holds with probability 1, and V (1) = q1 and V (1) = q3⊥ hold with probability 1/2 each because the second step occurs either at position 1 with configuration q1⊥Z or at position 3 with configuration q3⊥,

1 A conditional probability is well-defined if the condition, i.e., the event on the right hand side of the vertical bar, has positive probability. Expressions like the one in (1) are thus not necessarily well-defined because the probability that V (n−1) = vn−1 might be zero for certain values of n and vn−1.

Fig. 7. Left: An example (unlabeled) pVPA ∆. Call, internal, and return states are depicted as squares, circles, and rhombs, respectively. The format of the transition labels is analogous to Figure 5 (left). Middle: Initial fragments of the two possible runs of ∆. Steps are underlined. Right: Its step Markov chain M∆ (Definition 10, page 15).

Fig. 8. Next-step probabilities of the step Markov chain. Ptype for type ∈ { call, int,ret } are the probabilities of the pVPA's call, internal, and return transitions, respectively. The values [r 0Z↓r] and [q↑] are the return and diverge probabilities from Definition 9.

and both options are equally likely. The case P(V (2) = q2 | V (1) = q1) = 1 is slightly more interesting: Given that a configuration q1γ with γ 6= ⊥ is a step, we know that the next state must be q2 (which is then also a step). Even though there is a transition from q1 to q3 in ∆, the next state cannot be q3 because the latter is a return state which would immediately decrease the stack height of γ. This shows that, intuitively speaking, conditioning on being a step influences the probabilities of a state's outgoing transitions.

Probabilities of next steps, returns, and diverges. Our next goal is to provide expressions for the next-step probabilities P(V (n+1) = v 0 | V (n) = v) as we did in Example 3. It turns out that those can be stated in terms of the return and diverge probabilities of ∆.

Definition 9. Let p, q ∈ Q, Z ∈ Γ, and γ ∈ Γ ∗ . We define

Note that [p↑] is indeed independent of Z because the only way to read Z is by popping it from the stack which decreases the stack height. The diverge probabilities are closely related to steps. Indeed, the probability that a configuration pγ with γ 6= ⊥ is a step is equal to [p↑]. For example, in the pVPA in Figure 7 the configuration q1⊥Z is a step with probability [q1↑] = 1/2.

It is known that the return and diverge probabilities are in general nonrational. As a minimal example, consider a pVPA that repeats the following steps until emptying its stack or getting stuck: (i) It pushes four symbols with probability 1/6, or (ii) pops one symbol with probability 1/2, or (iii) gets stuck otherwise. The resulting return probability is the least solution of x = (1/6)x 5 + 1/2, a non-rational number that is not even solvable by radicals [16, Thm. 3.2(1)].

Remark 4. The terms return and diverge are natural. When modeling procedural probabilistic programs as pVPA, [pZ↓q] is just the probability to eventually return from local state p of the current procedure to local state q of the calling procedure (the return address is stored on the stack in Z). Similarly, [p↑] is the probability that the current procedure diverges, i.e., it never returns to the calling context. Clearly, this is independent of the return address.

Lemma 3. The conditional next-step probabilities in Figure 8 are correct in the sense that if P(V (n+1) = v 0 | V (n) = v) is defined for n ∈ N0 and v, v0 ∈ Q ∪ Q⊥ then it is equal to the probability in the respective column " v → v 0 ".

Proof sketch. We only provide some intuition for two important cases; formal derivations are in [28]. Let r ∈ Q be arbitrary.

The step chain. It is convenient to view the stochastic process V (0), V (1) . . . as an explicit (graphical) Markov chain.

Definition 10 (The Step Chain M∆). M∆ is the Markov chain with states

$$M\_{\quad} = \{ q \in Q\_{\text{call}} \cup Q\_{\text{int}} \mid [q\uparrow] > 0 \} \cup Q\bot,$$

Fig. 9. Left: Example pVPA with the following return-diverge probabilities: [cZ↓c] = 1/6, [cZ↓r] = 1/12, [rZ↓r] = 1/3, [rZ↓c] = 2/3, and [c↑] = 3/4, [τ↑] = 1/2, [r↑] = 0. Even though it is the case here, these probabilities are not always rational [16]. Right: Its step Markov chain according to Definition 10. The transition probabilities can be computed using the return and diverge probabilities and Figure 8.

initial state q0⊥, and for all v, v0 ∈ M, the probability of transition v → v 0 is defined according to Figure 8.

Figure 9 depicts a non-trivial pVPA and its step chain. In this example, all return and diverge probabilities are rational. In general, however, the return and diverge probabilities (Definition 9) are algebraic numbers that are not always rational or even expressible by radicals [16]. As a consequence, one cannot easily perform numerical computations on the step chain. However, the probabilities can be encoded implicitly as the unique solution of an existential theory of the reals (ETR) formula, i.e. an existentially quantified FO-formula over (R, +, ·, ≤) [14]. Since the ETR is decidable, many questions about the step chain are still decidable as well. We will make use of this in Theorem 3 below.

The property of M∆ that is most relevant to us is given by the following Lemma 4. We call ρ⇓Steps = V (0)(ρ)V (1)(ρ). . . the extended footprint of run ρ.

Lemma 4 (Soundness of M∆). Let ∆ be a pVPA with step chain M∆. Let M be the states of the step chain and consider a measurable set R ⊆ Mω. Then

$$\mathbb{P}(\{\rho \in Runs\_{\Delta} \mid \rho \psi\_{Steps} \in R\}) \quad = \quad \mathbb{P}(R) \ .$$

Proof sketch. For basic cylinder sets of the form R = w · Mω for some w ∈ M∗ , the claim follows from the Markov property (1) together with the correctness of the transition probabilities of M∆ according to Lemma 3. For other measurable sets, it can be shown by induction over the levels of the Borel hierarchy [28].

Remark 5. The step chain as presented here differs from the original definition in [14] in at least two important aspects. First, we have to take the semantics of our special bottom symbol ⊥ into account. This is why our chain uses a subset of Q ∪ Q⊥ as states—it must distinguish whether a step occurs at a bottom configuration. The pPDA in [14], on the other hand, may have both finite and infinite runs, and this needs to be handled differently in the step chain. Second, we use step chains for a different purpose than [14], namely to show that general measurable properties defined on steps—this includes stair-parity—can be evaluated on pVPA (Lemma 4).

Fig. 10. Left: The product of the pVPA from Figure 9 (left) and the DVPA from Figure 5 (left) on page 7. Right: Its step chain according to Definition 10. The dashed region is the only BSCC. It violates the parity condition Ω(s0) = 1 and Ω(s1) = 2 inherited from the DVPA (see Example 2 on page 8) since every run reaching the BSCC visits cs0 infinitely often with probability 1. Only reachable states are depicted.

Putting it all together. We can now prove the main result of this section.

Theorem 3. Let ∆ be a pVPA and let D be a stair-parity DVPA, both over the same pushdown alphabet Σ. Then for all θ ∈ [0, 1] ∩ Q, the problem P({ρ ∈ Runs∆ | λ(ρ) ∈ L(D)}) ≥? θ is decidable in PSPACE.

Proof sketch. We first construct the product ∆ × D according to Definition 8. By Lemma 1 we need to compute the stair-parity acceptance probability of ∆×D. Lemma 4 reduces this to computing a usual parity acceptance probability in the step chain M∆×D. This can be achieved through finding the bottom strongly connected components (BSCC) of M∆×D, classifying them as good (the minimum priority of a BSCC state is even) or otherwise bad, and running a standard reachability analysis wrt. the good states. See Figure 10 for an example. The remaining technical difficulty is that the transition probabilities of M∆×D are not rational in general. However, this can be dealt with using the fact that these probabilities are expressible in the ETR [14] (see [28] for the details).

#### 4.3 Probabilistic One-counter Automata

A probabilistic visibly one-counter automaton (pVOC) is the special case of a pVPA with unary stack alphabet, i.e., |Γ-⊥| = 1. For example, the pVPA in Figure 9 (left) is a pVOC. For many problems, better complexity bounds are known for pVOC than for the general case. In particular, [p↑] > 0 can be decided in P [9, Thm. 4]. We can exploit this to improve Theorem 3 in the pVOC case:

Corollary 1. Let ∆ be a pVOC and D be a stair-parity DVPA over pushdown alphabet Σ. The problem P({ρ ∈ Runs∆ | λ(ρ) ∈ L(D)}) =? 1 is decidable in P.

Corollary 1 implies that there exist efficient algorithms for many properties of pVOC-expressible random walks on N0. In fact, a.-s. satisfaction of each fixed visibly-pushdown property can be decided in P. For instance, using the DVPA from Figure 5 we can decide if a random walk is a.-s. repeatedly bounded.

### 5 Model Checking against B¨uchi VPA and CaRet

With Theorems 1 and 3 it follows immediately that quantitative model checking of pVPA against non-deterministic B¨uchi VPA is decidable in EXPSPACE. We can improve the complexity in the qualitative case:

Theorem 4.  The problem P({ρ ∈ Runs∆ | λ(ρ) ∈ L(A)}) =? 1 is EXPTIME-complete.

In the above result, membership in EXPTIME relies on the fact that one can construct the underlying graph of a step chain M∆×D in time exponential in the size of ∆ but polynomial in the size of D; see [28]. EXPTIME-hardness follows from [15, Thm. 8]. In fact, qualitative model checking of pPDA against nonpushdown B¨uchi automata is also EXPTIME-complete [15]. With Theorems 1 to 4 we immediately obtain the following complexity results for CaRet model checking:

Theorem 5. The quantitative and qualitative probabilistic CaRet model checking problems (Def. 7) are decidable in 2EXPSPACE and 2EXPTIME, respectively.

Both problems are known to be EXPTIME-hard [30].

### 6 Conclusion

We have presented the first decidability result for model checking pPDA—an operational model of procedural discrete probabilistic programs—against CaRet, or more generally, against the class of ω-VPL. We heavily rely on the determinization procedure from [22] and the notion of a step chain used in previous works. These two constructions turn our to be natural match.

We conjecture that our complexity bounds are not the best possible which is often the case in purely automata-based model checking. Future work is thus to investigate whether the doubly-exponential complexity can be lowered to singlyexponential, e.g. by generalizing the automata-less algorithm from [30]. Other topics are to explore to what extent algorithms for probabilistic CTL can be generalized to the branching-time variant of CaReT [18], to consider more expressive logics such as visibly LTL [8] or OPTL [12], and to study the interplay of conditioning and recursion [27] through the lens of pPDA.

Acknowledgement. The authors thank Christof L¨oding for his pointer to stairparity VPA, and the anonymous reviewers for their constructive feedback.

### References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

### **Author Index**

Angluin, Dana 1 Antonopoulos, Timos 1 Ascari, Flavio 21 Baier, Christel 40 Balasubramanian, A. R. 61 Blondin, Michael 81 Boisseau, Guillaume 101 Boker, Udi 120, 140 Broadbent, Anne 161 Bruni, Roberto 21 Caltais, Georgiana 184 Castelnovo, Davide 205 Chistikov, Dmitry 225 Cimatti, Alessandro 244 Colcombet, Thomas 264 Esparza, Javier 81 Fervari, Raul 305 Finkbeiner, Bernd 325 Fisman, Dana 1 Funke, Florian 40 Gadducci, Fabio 205 Gay, Simon J. 347 Geatti, Luca 244 Gehnen, Christina 449 George, Nevin 1 Gigante, Nicola 244 Gori, Roberta 21 Guillou, Lucie 61 Haase, Christoph 225 Hainry, Emmanuel 368 Heim, Philippe 325 Hirschowitz, André 389 Hirschowitz, Tom 389 Hojjat, Hossein 184 Jaakkola, Reijo 409

Kapron, Bruce M. 368 Karvonen, Martti 161 Katoen, Joost-Pieter 449 Kesner, Delia 285 Lafont, Ambroise 389 Lehtinen, Karoliina 120, 140 Maggesi, Marco 389 Mansutti, Alessio 225, 305 Marion, Jean-Yves 368 McDermott, Dylan 428 Miculan, Marino 205 Montanari, Angelo 244 Morvan, Rémi 264 Mousavi, Mohammad Reza 184 Passing, Noemi 325 Péchoux, Romain 368 Peyrot, Loïc 285 Piedeleu, Robin 101 Piribauer, Jakob 40 Poças, Diogo 347 Rivas, Exequiel 428 Santo, José Espírito 285 Sickert, Salomon 140 Tonetta, Stefano 244 Tunç, Hünkar Can 184 Uustalu, Tarmo 428 van Gool, Sam 264 Vasconcelos, Vasco T. 347 Weil-Kennedy, Chana 61 Winkler, Tobias 449 Ziemek, Robin 40


*2.9.4 Damage*

Black cutworm has a broad has range and feeds on all crops and pasture plants. Newly emerged crop seedlings are attacked by the full-grown larvae migrated from summer and autumn weeds. Species of the *Agrotis* are the worst destroyers that they may attack on the whole fields of cereal crops. Early instars of larvae feed on the tender tissues of the foliage, but as they grow, they suppose their classic cutworm 'felling' activity [84].


**3. Result and discussion**

## **3.1 Nutritional composition**

**Table 1** shows the nutritional composition of dark chocolate-coated Chinese chestnut. Except for the moisture content, all compositions were measured using dry materials (**Table 1**). The prepared chocolate contained no extra ingredients when compared to commercial fruit and nut dark chocolate, which is made up of preservatives and other sweeteners. The dark chocolate-coated chinese chestnut is therefore highly fascinating and appears to be beneficial for human health, as proved by its overall high nutritional quality.

By using a glancing angle X-ray diffractometer with monochromatic Cu-K as the radiation source (45 kV and 20 mA), the XRD pattern of the prepared sample was recorded (**Figure 11**). As shown in **Figure 11**, the XRD measurements were made in the range of 2θ from 5° to 90°.

The sample's obtained diffraction pattern reveals its amorphous nature. Using Debye Scherrer's formula, the sample's crystallite size (Dhkl) was estimated-.

$$\mathbf{D}\_{h\mathbf{k}1} = \frac{\mathbf{0}.\mathbf{9}\lambda}{\mathcal{B}\_{hkl}{}^{\mathrm{Ca}}\left(\theta\_{hkl}\right)}$$

Here λ represents the X-ray wavelength, θhkl indicates the Bragg diffraction angle and βhkl represents the full width at half maximum (FWHM) of the major peaks in XRD pattern in radians.

The sample's crystallite size was determined to be 76.30 nm.