A three-valued model abstraction framework for PCTL* stochastic model checking

Abstract

Stochastic model checking can automatically verify and analyse the software-driven autonomous systems with stochastic behaviors, which is a formal verification technique based on system models. When coping with large-scale systems, it suffers from state space explosion problem very seriously. Model abstraction is a potential technique for mitigating this problem. At present, only a few properties specified by PCTL (Probabilistic Computation Tree Logic), such as probabilistic safety and probabilistic reachability, can be preserved in the practical model abstraction of stochastic model checking, which are the proper subset of PCTL* (Probabilistic Computation Tree Logic*) properties. For dealing with this, an effective and efficient three-valued model abstraction framework for full PCTL* stochastic model checking is proposed in this paper. We propose a new abstract model to preserve full PCTL* properties for nondeterministic and probabilistic system, which orthogonally integrates interval probability of transition and game for nondeterminism. A game-based three-valued PCTL* stochastic model checking algorithm is developed to verify abstract model, and a BPSO (binary particle swarm optimization) algorithm integrated with sample learning is designed to refine the indefinite result of three-valued PCTL* stochastic model checking abstract model. It is proved that full PCTL* properties are preserved when the result of three-valued stochastic model checking is definite, and the efficiency of this framework is demonstrated by some large cases.

1 Introduction

Software-driven autonomous systems are increasingly being used in a lot of domains, e.g., industry automation, transport, finance, medical surgery and so on (Ebert and Weyrich 2019; Shivakumar et al. 2020; Fremont et al. 2020).

They are becoming larger and more complex, some of which are accompanied with the stochastic behaviors (Clarke et al. 2018). The essential reasons for exhibiting stochastic behaviors can be classified as, among others: (a) the system itself contains randomness, e.g., probabilistic algorithms or randomized algorithms are included; (b) the running environment of system is open, dynamic and unmanageable, which may lead to random failures, e.g., message loss or failing to invoke some components; (c) the stochastic variables are artificially employed to capture system performance index for evaluation and analysis, e.g., reliability. As an automatic and formal verification technique, stochastic model checking (a.k.a. probabilistic model checking) (Clarke et al. 2018, 2009; Kwiatkowska et al. 2022; Baier and Katoen 2008) can be naturally applied to quantitatively analyse intelligent software-driven autonomous systems with stochastic behaviors. In practice, stochastic model checking has been exploited to analyze or guarantee the correctness of probabilistic program (Hark et al. 2020), system performance of mobile service robots (Lacerda et al. 2019), reliability of critical communication protocols (Oxford et al. 2020), resource control mechanisms in cloud computing (Evangelidis 2020), software adaptation of an unmanned undersea vehicle (Pfeffer et al. 2019), trustworthiness of deep learning systems (Kwiatkowska 2019), and so on. In the verification process, the autonomous systems are modelled as full probabilistic models, e.g., DTMCs (Discrete-time Markov Chains), PPNs (Probabilistic Petri Nets), or nondeterministic and probabilistic models, e.g., MDPs (Markov Decision Processes), NPPNs (Nondeterministic Probabilistic Petri Nets); and the requirement properties are specified by LTL (Linear Temporal Logic) with probability or PCTL (Probabilistic Computation Tree Logic) (Kwiatkowska et al. 2022).

The biggest obstacle is state space explosion in stochastic model checking the software-driven autonomous systems, especially the large-scale systems. This is rooted in the facts that: (a) the number of states grows double exponentially in the number of variables or components in a software-driven autonomous system; (b) stochastic model checking algorithm combines the classical model checking algorithm and linear equation solving or linear programming algorithms, which computes the probabilistic vector over states rather than bit-vector in classical model checking. Hence, how to fight state space explosion problem is a major challenge in the field of stochastic model checking software-driven autonomous systems. Clarke, Turing Award winner for founding the field of model checking, points out that it is an important direction in the future research of model checking at “Turing Lecture” (Clarke et al. 2009). In recent years, some techniques have been proposed for combating this problem, ranging from the multi-terminal binary decision diagram (MTBDD) (Kwiatkowska et al. 2017), abstraction (Dehnert 2018; Dams and Grumberg 2018), and bounded stochastic model checking algorithm (Hartmanns et al. 2018) to compositional reasoning (He et al. 2016; Ma et al. 2019a). However, it is still an open problem.

1.1 Problem statement of model abstraction for stochastic model checking

As an important means to tackle the state space explosion problem, abstraction (Clarke et al. 2003, 1994a) has been applied in the field of stochastic model checking. It performs stochastic model checking on the abstraction of one or more components in the concrete stochastic model checking. Concrete stochastic model checking is to decide whether $M \vDash {\Phi }$ holds, where $M$ is the stochastic system model, ${\Phi }$ is the quantitative requirement property specification, and $\vDash$ is the satisfaction relation. Abstraction for stochastic model checking can be denoted as: $M^{A} \vDash ^{A} {\Phi }^{A}$, where $M^{A}$ is the model abstraction of $M$, $\vDash ^{A}$ is the relation abstraction of $\vDash$ based on algorithm, ${\Phi }^{A}$ is the specification abstraction of ${\Phi }$. In fact, $M^{A}$ usually leads to $\vDash ^{A}$ and ${\Phi }^{A}$; $\vDash ^{A}$ also results in ${\Phi }^{A}$; ${\Phi }^{A}$ may also lead to $M^{A}$ and $\vDash ^{A}$. In the present research on abstraction for stochastic model checking, the abstraction refers to model abstraction by default; while relation abstraction (Alfaro and Roy 2007; Didier et al. 2010; Filieri et al. 2011; Huang et al. 2019; Younes 2005) and specification abstraction (Dehnert 2018; Dams and Grumberg 2018) are specifically identified, and the related works of them is less. This paper also focuses on model abstraction for stochastic model checking.

Informally, model abstraction for stochastic model checking is omitting details from concrete stochastic system model, which are not relevant for verifying properties under consideration(Liu et al. 2015). It concludes the value of $M \vDash {\Phi }$ from the result of $M^{A} \vDash {\Phi }$. Applying model abstraction in stochastic model checking faces the following four issues, which is named MA4SMC (model abstraction for stochastic model checking) problem: P1) how to construct abstract model, P2) how to verify the abstract model, P3) what quantitative properties can be preserved, P4) how to present the counterexample. Thereinto, the answer to P1) is the key for solving the MA4SMC problem. It has an important effect on the answers to P2), P3) and P4). The goal of model abstraction is to make the abstract model that has a small enough state space, yet contains abundant information of concrete model. In other words, perfect model abstraction technology should meet the following conditions: C1) the state space of abstract model $M^{A}$ is significantly less than the concrete model $M$; C2) the results of stochastic model checking $M^{A}$ is equivalent to the results of stochastic model checking $M$, i.e., $M^{A} \vDash {\Phi } \to M \vDash {\Phi }$, and $M^{A} { \nvDash }\;\Phi \to M{ \nvDash }\;\Phi$. That is to say, if $M^{A}$ satisfies ${\Phi }$, $M$ satisfies ${\Phi }$; and if $M^{A}$ doesnot satisfy ${\Phi }$, $M$ doesnot satisfy ${\Phi }$. However, abstraction process will cause information loss inevitably. There is a tradeoff in abstraction process between state space and information loss, and various model abstraction techniques choose the different tradeoffs.

The existing model abstraction techniques, discussed elaborately in Sect. 2, can be divided into two categories: (a) accurate abstraction, e.g., probabilistic bisimulation-based abstraction (Larsen and Skou 1991; Milner 1980, 1971; Park 1981; Buchholz 1994; Segala and Lynch 1995; Paige and Tarjan 1987; Huynh and Tian 1992; Hermanns and Katoen 2000; Derisavi 2007; Christian et al. 2013; Zhang et al. 2018; Baier and Hermanns 1997; Philippou et al. 2000; Ferrer et al. 2016; Hermanns and Turrini 2012; Jonsson and Larsen 1991; Clarke et al. 1994b; Baier et al. 2005a; Zhang 2008; Zhang and David 2016; Hashemi et al. 2013), symmetry reduction-based abstraction (Clarke et al. 1996; Emerson and Sistla 1996; Norris and Dill 1996; Miller et al. 2006; Donaldson and Miller 2006; Emerson and Wahl 2003, 2005a, b; Donaldson et al. 2009; Wahl et al. 2008; Kwiatkowska et al. 2006a; Kamaleson 2018; Christopher 2012) and partial order reduction-based abstraction (Gerth et al. 1995; Peled 1993, 1996; Peled et al. 1997; Valmari 1992; Baier et al. 2004, 2005b; D’Argenio and Niebert 2004; Ciesinski 2011; Fernandez-Diaz et al. 2012; Hansen et al. 2011; Kwiatkowska et al. 2011; Hansen and Wang 2011; Winterer et al. 2017); (b) approximate abstraction, e.g., probabilistic CEGAR (counterexample-guided abstraction-refinement) (Clarke et al. 2003; Hermanns et al. 2008; Hahn et al. 2010; Chadha and Viswanathan 2010; Ma et al. 2019b), error-guided abstraction (Ma et al. 2019b; Kwiatkowska et al. 2006b; Kattenbelt et al. 2010; Katoen and Sher 2017; Wachter and Zhang 2010; Winterer et al. 2020; Kwiatkowska et al. 2020), indefinite result-guided abstraction (Fecher et al. 2006; Katoen et al. 2012; Luisa et al. 2017). In accurate abstraction, the abstract model is the quotient of concrete model, verification algorithm and counterexample generation are the same with traditional stochastic model checking. The abstract model of exact abstraction is not small enough, but it preserves almost all the properties. The accurate abstraction is difficult to realize in practical application at technical level, as it cannot reduce state space obviously, and the system models need to have the corresponding special structure. In approximate abstraction, probabilistic CEGAR has a wide range of practical applications, but the preserved properties are too less, only probabilistic safety is preserved. Error-guided abstraction and indefinite result-guided abstraction are the potential model abstraction paradigms for stochastic model checking. The limitations of error-guided abstraction are: (1) the scope of preserved properties is too narrow, only probabilistic reachability, (2) the refinement algorithm is not efficient enough, and (3) counterexample generation is not included. Indefinite result-guided abstraction can preserve PCTL properties, but it isnot complete, which solves the MASMC problem partially, and the limitations of which are: (1) the verified system model is full probabilistic model, (2) the refinement is not involved for steering repartition of abstract model, and (3) counterexample generation is also not included.

1.2 Our contributions

For preserving more properties in model abstraction, we argue that error-guided abstraction and indefinite result-guided abstraction can be combined orthogonally to form an ideal abstraction framework, as they have the complementary advantages. Game can characterize the new nondeterminism occurred by abstraction, which can reduce the state space of abstract model. Indefinite result-guided abstraction can over-approximate and under-approximate the concrete system model at the same time, which can get the tight lower and upper bounds. This paper is dedicated to this direction.

In this paper, with a breakthrough in constructing and presenting abstract model, we propose a complete and efficient model abstraction framework, i.e., three-valued abstraction-refinement, for PCTL* (Probabilistic Computation Tree Logic*) stochastic model checking nondeterministic and probabilistic systems. As shown in Fig. 1, we mainly make the following contributions to solve the MA4SMC problem: (1) proposing a new abstract model which orthogonally integrates interval probability of transition and game for nondeterminism, i.e. LGIPPN (Game Interval PPN with Label), and combining sample learning and BPSO (binary particle swarm optimization) algorithm to refine the abstract model; (2) generalizing two-player ($verifier$ and $refuter$) stochastic game semantics (Liu et al. 2016; Shoham and Grumberg 2007) for three-valued PCTL* stochastic model checking the abstract model, and exploiting coloring process for strategy solving; (3) preserving the full PCTL* properties which is a proper superset of probabilistic safety, probabilistic reachability, and PCTL properties; (4) extending the evidence for refutation (Liu et al. 2016; Shoham and Grumberg 2007) to express the counterexample. This solution meets the conditions of perfect model abstraction well: (1) the state space of abstract model $M^{A}$ is significantly less than the concrete model $M$; C2) $M^{A} \vDash {\Phi } \to M \vDash {\Phi }$, $M^{A} { \nvDash }\; {\Phi } \to M{ \nvDash }\; {\Phi }$, except for the indefinite result. As far as we know, this is the first complete framework for three-valued abstraction-refinement in stochastic model checking, and it is also the first abstraction framework for preserving full PCTL*. In this framework, the concrete system model that we deal with is LNPPN (Nondeterministic Probabilistic Petri Net with Label) (Albanese et al. 2008; Liu et al. 2016; Bernemann et al. 2020) which is a high-level formal model for modelling autonomous systems with nondeterministic and probabilistic behaviors. The LNPPN model can be modelled from an existing autonomous system, or it is a design model by designer for developing the autonomous system. Note that this framework can also be used to abstract other nondeterministic and probabilistic systems models, such as MDP or probabilistic automaton.

Fig. 1

Three-valued abstraction-refinement for PCTL* stochastic mode checking

1.3 Outline of the paper

In the next section, we survey the related works of model abstraction techniques for stochastic model checking. We give the necessary preliminaries for LNPPN, PCTL* and stochastic model checking LNPPN in Sect. 3. In Sect. 4, we propose a novel abstract model for nondeterministic and probabilistic system, and describe how to construct the abstract models for LNPPN. Section 5 extends the game-based PCTL* stochastic model checking to verify abstract model, which transforms the three-valued PCTL* stochastic model checking into strategy solving of three-valued stochastic game. We propose the refinement algorithm for refining the abstract model, which integrates BPSO and sample learning in Sect. 6. The experimental results are presented in Sect. 7. We conclude the paper in Sect. 8.

2 Related works

There are some model abstraction techniques have been proposed for stochastic model checking. We classify them according to the methods of presenting and constructing abstract model, summarise their solutions to MA4SMC problem, and analyse the extent to which they satisfy the conditions of perfect abstraction.

2.1 Simulation relation-based model abstraction

• (1) Strong probabilistic bisimulation

  Strong probabilistic bisimulation (Larsen and Skou 1991), i.e., probabilistic bisimulation, is the quantitative extension of strong bisimulation (Milner 1980; Park 1981) on LTS (labelled transition system). It has been used for model abstraction for DTMC (discrete-time Markov chain), CTMC (discrete-time Markov chain) (Buchholz 1994) and MDP (Markov decision process) (Segala and Lynch 1995). Based on study (Paige and Tarjan 1987), Huynh et al. (1992) gave the first automatic constructing abstract model algorithm for DTMC. Hermanns et al. (2000) adopted compositional method to transform the strong probabilistic bisimulation of model into the strong probabilistic bisimulation of sub-model, and used it to quantitatively verify POTS (plain-old telephone system). Derisavi (2007) firstly presented a symbolic algorithm and its implementation for the construct abstract model of CTMC, which was optimal for generating the smallest possible abstract model. Christian et al. (2013) leveraged satisfiability solvers to extract the minimised system from the PRISM modelling language directly, which could generate coarser abstract model and no state space was generated. Song et al. (Zhang et al. 2018) introduced novel notions of strong probabilistic bisimulation relation for PA (probabilistic automaton), which could get the coarsest abstract model among the existing strong probabilistic bisimulation techniques. Strong probabilistic bisimulation-based abstraction solves the MA4SMC problem in the following way: W1) use the strong probabilistic bisimulation minimization to construct a smaller equivalent abstract model, and use the quotient model to present abstract model; W2) use existing stochastic model checking algorithm to verify abstract model; W3) preserve all the quantitative temporal logics; W4) use existing method to generate the counterexample. It meets condition C2) of perfect model abstraction well, and performs badly for condition C1). The limitation of it: the abstract model is so refined that the state space of it does not become smaller obviously, and the time to construct the abstract model may exceed the stochastic model checking time for concrete model.

• (2) Weak probabilistic bisimulation

  Compared with Strong probabilistic bisimulation, weak probabilistic bisimulation (Zhang et al. 2018; Baier and Hermanns 1997; Philippou et al. 2000) is a coarse simulation relation. It solves the MA4SMC problem in the following way: W1) use the weak probabilistic bisimulation minimization to construct a smaller stuttering equivalent abstract model, and use the quotient model to present abstract model; W2) use existing stochastic model checking algorithm to verify abstract model; W3) preserve all the quantitative temporal logics without next operator; W4) use existing method to generate the counterexample. Although some work (Baier and Hermanns 1997; Ferrer et al. 2016; Hermanns and Turrini 2012) manage to reduce the time complexity of constructing abstract model, it is still subject to the cost of a complex minimization algorithm.

• (3) Strong probabilistic simulation

  Strong probabilistic simulation (Larsen and Skou 1991; Jonsson and Larsen 1991) can be seen as the quantitative extension of strong simulation (Milner 1971; Clarke et al. 1994b). Baier et al. (2005a) proved that equivalence of strong probabilistic simulation over DTMC or CTMC was in accordance with strong probabilistic bisimulation. For MDP, the quotient under strong probabilistic simulation is strict coarser than strong probabilistic bisimulation. Zhang et al. (2008, 2016) pursued the optimization of constructing abstract model based on strong probabilistic bisimulation, and Huang et al. (2019) generalized probabilistic simulation to probabilistic pushdown automata and finite-state systems. Strong probabilistic simulation-based abstraction solves the MA4SMC problem in the following way: W1) use the strong probabilistic simulation minimization to construct a smaller abstract model, and use the quotient model to present abstract model; W2) use existing stochastic model checking algorithm to verify abstract model; W3) preserve the truth value of quantitative safety temporal logics; W4) use existing method to generate the counterexample. It meets the perfect model abstraction C1) well, but for C2), it just preserves the truth value of quantitative safety temporal logics formula Φ, i.e., $M^{A} \vDash {\Phi } \to M \vDash {\Phi }$.

• (4) Weak probabilistic simulation

  Weak probabilistic simulation is the coarsest among all the simulation relations. At present, the related work about weak probabilistic simulation is less (Zhang 2008; Zhang and David 2016; Hashemi et al. 2013). It solves the MA4SMC problem in the following way: W1) use the weak probabilistic simulation minimization to construct a smaller abstract model, and use the quotient model to present abstract model; W2) use existing stochastic model checking algorithm to verify abstract model; W3) preserve the truth value of quantitative safety temporal logics without next operator; W4) use existing method to produce the counterexample. It meets the perfect model abstraction C1) well, but for C2), it just preserves the truth value of quantitative safety temporal logics without next operator.

2.2 Symmetry reduction-based model abstraction

Symmetry reduction (Clarke et al. 1996; Emerson and Sistla 1996; Norris and Dill 1996; Miller et al. 2006) exploits presence of replication within model to be verified. Donaldson et al. (2006) applied symmetry reduction (Emerson and Wahl 2003, 2005a) for non-probabilistic symbolic model checking in PRSIM with MDP or DTMC semantics, translated the SP (symmetric PRISM) program into the reduced form, and developed corresponding tool GRIP. Based on study (Donaldson and Miller 2006), Donaldson et al. (2009) presented a much richer language, which allowed specification of probabilistic systems in a way that guaranteed the applicability of the generic representative technique, together with an extended translation algorithm. Via dynamic symmetry reduction (Emerson and Wahl 2005b; Wahl et al. 2008), Kwiatkowska et al. (2006a) proposed an efficient algorithm for the construction of quotient models of DTMC, CTMC, MDP, which were built PRISM with MTBDD data structure. Kamaleson (2018) and Christopher (2012) applied symmetry reduction to stochastic model checking with explicit states, which could the automated detect component symmetries or arbitrary data in the probabilistic specification. Symmetry reduction-based abstraction uses quotient to present abstract model. The relation between it and concrete model is probabilistic bisimulation, but it needs less cost when constructing abstract model compared with probabilistic bisimulation-based abstraction.

2.3 Partial order reduction-based model abstraction

Partial order reduction methods (Gerth et al. 1995; Peled 1993; Peled et al. 1997; Valmari 1992) rely on expanding a state space only partially, exploring representatives of sets of executions of a system. Baier et al. (2004) firstly investigated partial order reduction for LTL without next operator model-checking MDP via a variant of Peled’s ample set method (Peled 1993, 1996). Argenio et al. (2004) enhanced ample set conditions of study (Baier et al. 2004) to make the abstraction preserve maximum and minimum probabilities of next-free LTL properties, which was implemented in LiQuor (Ciesinski 2011). Baier et al. (2005b) presented the partial order reduction criteria for verifying branching time properties formalized by PCTL. Fernandez et al. (2012) regarded the work of Baier et al. (2004, 2005b), D’Argenio and Niebert (2004) as the dynamic partial order reduction methods, the drawback of which was that they can hardly be combined with other techniques to tackle the state space explosion problem. It studied partial order reduction realized by a static analysis which injected the reduction criteria into the control flow graph. Different from partial order reduction via ample set, Hansen et al. (2011) and Kwiatkowska et al. (2011) firstly proposed a weak variant of the stubborn set (Hansen and Wang 2011) to reduce the state space of MDP, which would preserve the maximal probabilities of reaching bottom end components under far schedulers and realizability of unconditional fairness. This work is then extended in Winterer et al. (2017). Partial order reduction-based abstraction can be seen as the weak probabilistic bisimulation-based abstraction.

2.4 Probabilistic counterexample-guided model abstraction

CEGAR (counterexample-guided abstraction-refinement) (Clarke et al. 2003) has been en vogue for the automatic verification of very large systems in the past years. At present, there are two methods for applying CEGAR in stochastic model checking, i.e., probabilistic CEGAR (Hermanns et al. 2008; Chadha and Viswanathan 2010), which are based on over-approximation of concrete model. Hermanns et al. (2008) firstly applied CEGAR for stochastic model-checking probabilistic automaton, and developed the corresponding tool PASS (Hahn et al. 2010). It solves the MA4SMC problem in the following way: W1) use counterexample-guided refinement to construct abstract model, and use the abstract quotient automaton to present abstract model; W2) use existing stochastic model checking algorithm to verify abstract model; W3) preserve the truth value of reachability properties; W4) use existing method to produce the counterexample expressed by a finite Markov chain. It meets condition C1) of perfect model abstraction well, and performs badly for condition C2), for reachability property Φ, i.e., $M^{A} \vDash {\Phi } \to M \vDash {\Phi }$. Chadha et al. (2010) pointed out that DTMC could not serve as counterexample for the richer class of properties and argued that no formal statement characterizing process based on the refinement algorithm outlined in Hermanns et al. (2008). This was supplemented by Ma et al. (2019b), in which counterexample was represented with sub-graph. They can be seen as the second solution for MA4SMC problem in the following way: W1) use counterexample-guided refinement to construct abstract model, and use the another MDP or sub-graph to present abstract model; W2) use existing stochastic model checking algorithm to verify abstract model; W3) preserve the truth value of safety and liveness fragments of PCTL; W4) use existing method with heuristics to generate the counterexample expressed by a sub-MDP or sub-graph. It meets condition C1) of perfect model abstraction well, and does not perform well for condition C2), i.e., for safety and liveness fragments of PCTL formulae Φ, i.e., $M^{A} \vDash {\Phi } \to M \vDash {\Phi }$.

2.5 Error-guided model abstraction

Error-guided abstraction-refinement (game-based abstraction) proposed by Marta, Mark, et al. (Kwiatkowska et al. 2006b; Kattenbelt et al. 2010; Katoen and Sher 2017) is a new framework for model abstraction in stochastic model checking. Error-guided abstraction-refinement framework comprises an abstraction based on stochastic 2-player games, two refinement methods (strategy-based refinement, value-based refinement) and an efficient algorithm for an abstraction-refinement loop. Recent extensions to the PASS tool (Wachter and Zhang 2010) use this framework and demonstrate that it is faster and yields smaller abstractions. Winterer et al. (2020) extended and complemented the work (Katoen and Sher 2017) for strategy synthesis for POMDPs in robot planning. The solution of game-based abstraction to the MA4PMC problem is as follows: W1) use error-guided refinement to construct abstract model, and use stochastic game to present abstract model; W2) use existing stochastic game algorithm (Kwiatkowska et al. 2006b, 2020) to analyze abstract model; W3) allows lower and upper bounds to be computed for the values of reachability properties of the MDP; W4) do not involve the counterexample generation. It meets condition C1) of perfect model abstraction well, but the properties to be verified is limited to reachability properties.

2.6 Indefinite result-guided model abstraction

In recent years, indefinite result-guided abstraction-refinement (three-valued abstraction) (Fecher et al. 2006) is used in stochastic model checking, which is both over-approximation and under-approximation of concrete model. Fecher et al. (2006) considered three-valued abstraction for DTMC firstly. It solves the MA4SMC problem partially in the following way: W1) use abstract Markov chain to present abstract model, do not involve refinement method; W2) use a dedicated three-valued stochastic model checking to verify abstract model; W3) preserve PCTL of the DTMC, except for the indefinite results; W4) do not include the counterexample generation. Katoen et al. (2012) extended the work of Fecher et al. (2006) to CTMC, and laid down the theoretical underpinnings of three-valued abstraction for DTMC and CTMC. Luisa et al. (2017) extended the work of Fecher et al. (2006), Katoen et al. (2012) to Spatio-Temporal Logic for stochastic systems, and Belardinelli et al. (2019) generalized the three-valued abstraction to verify strategic properties in multi-agent systems with imperfect information. It solves the MA4SMC problem partially in the following way: W1) use interval Markov chain to present abstract model, do not involve refinement method; W2) use a dedicated three-valued stochastic model checking to verify abstract model; W3) preserve PCTL/CSL of the DTMC/CTMC, except for the indefinite results; W4) do not include the counterexample generation. The work of Katoen et al. (2012), Luisa et al. (2017), Belardinelli et al. (2019) meets condition C1) and C2) of perfect model abstraction well, but they are incomplete, and there is not yet an implementation to test this on practical examples.

3 Preliminaries

3.1 LNPPN

Petri net is a high-level formal method for modeling, analyzing, and verifying the complex systems. It was proposed by C. A. Petri in his dissertation “Communication with Automata” in 1962. Today, it has been widely used in all aspects of software or system engineering to ensure the quality. For modeling the complex system with stochastic behaviors, probability measurement theory is introduced in Petri net (Albanese et al. 2008; Liu et al. 2016; Bernemann et al. 2020), which is under the guidance of general net theory (Petri 1979). At present, there are 4 types of probabilistic Petri nets for modelling stochastic systems, as shown in Table 1. We consider the nondeterministic probabilistic system models, i.e., NPPN. PPN can be seen as the special case of NPPN without nondeterminism. LNPPN (Liu et al. 2016) is the NPPN with label functions.

Table 1 Petri nets with probability measurement theory

Definition 1

LNPPN (NPPN with Label). The LNPPN can be defined as a 7-tuple $M = \left( {S,\;T;\;F,\;f;\;C;\;AP,\;L} \right)$, where: (1) $T = \left( {Transition,{ }Prt} \right)$, $Transition$ denotes the transition act, $Prt \in \left[ {0,1} \right]$ denotes the success probability of the transition; $T$ is the act transition $\left( {AT} \right)$ with the probability equals 1, or the probabilistic act transition $\left( {AT,Prt} \right)$ with an act satisfying a certain probability distribution, or the pure probability transition $\left( {PT} \right)$ without any act. If $Prt = 0$, it means that the transition is invalid; (2) $S$ is the set of places,$S \cap T = \phi$, $S \cup T \ne \phi$, $F \subseteq S \times T \cup T \times S$, which is the flow relation of net, and $N = \left( {S,AT,F} \right)$ is the pure net, where $AT$ is the act transition with probability equals 1; (3) $f = f_{T} \cup f_{S} \cup f_{S \times T} \cup f_{T \times S}$, $f_{T} :T \to 2^{Transition \times Prt}$, $f_{S} = S \to \left[ {0,1} \right]$, $f_{S \times T} = S \times T \to \left[ {0,1} \right]$, $f_{T \times S} = T \times S \to \left[ {0,1} \right]$, and the value of $f_{S \times T}$ is determined by the nondeterminism of transitions, the value of $f_{T \times S}$ can be obtained from the probability value of $f_{T} \left( t \right)$, i.e., $\sigma_{Prt} \left( {f_{T} \left( t \right)} \right)$, the value of $f_{S}$ except initial place can be computed according to the value of $f_{S \times T}$ and $f_{T \times S}$; (4) $\forall t \in T$, $\exists s \in S,{ }f_{T \times S} = 1 - \sigma_{Prt} \left( {f_{T} \left( t \right)} \right)$.$f_{T \times S} \left( {t \times s} \right) = 0$, if $\sigma_{Prt} \left( {f_{T} \left( t \right)} \right) = 1$, which represents transition $\left( {t,s} \right)$ and place $s$ are invalid; (5) $C$ is the set of nondeterminism classes, and each nondeterminism class is a set comprised of $\left( {s,t_{i} } \right)$. If $\left\{ {\left( {s,t_{1} } \right),\left( {s,t_{1} } \right) \ldots \left( {s,t_{1} } \right)} \right\} \in C$, then $\mathop \sum \limits_{i = 1}^{n} f_{S \times T} \left( {s,t_{i} } \right) = 1$; (6) $AP$ is a set of atomic propositions; (7) $L:S \to 2^{AP}$ is the labeling function, which can express the requirements of users, i.e., the properties.

A LNPPN $M$ is finite, if $S$ and $T$ are finite. The size of $M$ is the number of places and transitions plus the number of pairs $\left( {s,t} \right)$ with $f_{S \times T} > 0$ and $\left( {t,s} \right)$ with $f_{T \times S} > 0$. A LNPPN model is measurable with probability (Liu et al. 2016).

Definition 2

Adversary (Policy, or Scheduler) of LNPPN. An adversary of a LNPPN model $M$ is a function $Adv:S^{ + } \to T$, such that $Adv\left( {s_{0} s_{1} s_{2} \ldots s_{n} } \right) \in C$ for all $s_{0} s_{1} s_{2} \ldots s_{n} \in S^{ + }$. The path ${\uppi } = s_{0} \to ^{{t_{1} }} s_{1} \to ^{{t_{2} }} \cdots \to ^{{t_{i} }} s_{i} \cdots$ is called a $Adv$-path if $t_{i} = Adv\left( {s_{0} \ldots s_{i - 1} } \right)$ for all $i > 0$.

3.2 PCTL* in release-PNF

Every PCTL* (Baier and Katoen 2008) formula can be transformed as a canonical form. Release-PNF (positive normal form) of PCTL* is a kind of canonical forms for PCTL*, which is described by a restriction that negation operator only occurs adjacent to atomic propositions. It can avoid the exponential blowup in transforming the PCTL* formulae into PNF.

Definition 3

Release-PNF of PCTL*. Let $AP$ be a set of atomic propositions, the release-PNF of PCTL* state formulae ${\Phi }$ are defined as follows: $\Phi :: = {\text{true}}\left| {{\text{false}}} \right|a\left| {\neg a} \right|\Phi \wedge \Phi \left| {\Phi \vee \Phi } \right|{\text{P}}_{{\sim p}} \left( \Psi \right)$, where $a \in AP$,${\Psi }$ is the path formula, $\sim \in \left\{ {\left\langle {, \le ,} \right\rangle , \ge } \right\}$, and $p \in \left[ {0,1} \right]$ is the rational bound; the release-PNF of PCTL* path formulae ${\Psi }$ are defined as follows: $\Psi :: = \Phi \left| {\Psi \wedge \Psi } \right|\Psi \vee \Psi \left| {{\text{X}}\Psi } \right|\Psi {\text{U}}\Psi |\Psi {\text{R}}\Psi$, where the temporal modality ${\text{R}}$ is dual to the until operator ${\text{U}}$. $\Psi _{0} {\text{R}}\Psi _{1}$ is “true” over a path, if ${\Psi }_{1}$ always holds, a requirement that is released no sooner than ${\Psi }_{0}$ becomes valid.

3.3 Stochastic model checking LNPPN

The descriptive powers of PPN, NPPN, SPN and PTPN are the same with low-lever formal model DTMC, MDP, CTMC (Continuous-time Markov Chain) and CTMDP (Continuous-time Markov Decision Process), respectively. State-of-the-art stochastic model checker, e.g., PRISM, PAT, can verify LNPPN, Markov process or probabilistic automaton, indiscriminately. Actually, PCTL* stochastic model checking NPPN is a very complex process, as shown in Fig. 2, because the PCTL* is a combination of PCTL and LTL with probability. The time complexity of it is proved to be double exponential in |${\Psi }$| and polynomial in the size of NPPN $M$ (Clarke et al. 2018; Liu et al. 2016), where ${\Psi }$ is the path formula in PCTL* ${\Phi }$. Liu et al. (2016) proposed a game (Shoham and Grumberg 2007)-based PCTL* stochastic model checking algorithm, which yielded a single exponential time complexity in |${\Psi }$| for PCTL* stochastic model checking LNPPN. They proved that this cannot be improved further, as the LTL with probability stochastic model checking LNPPN is PSPACE-completeness. Moreover, in reference Liu et al. (2016), the counterexample was generated by evidence of winning strategy of player refuter $refuter$. It is the first work to generate counterexamples for PCTL* stochastic model checking.

Fig. 2

PCTL* stochastic model checking

From the point of view of time complexity, abstraction for PCTL* stochastic model checking LNPPN is also very important and necessary. The model abstraction methods in Sect. 2 can also be used to LNPPN, if they don’t take the LNPPN as the concrete model, originally. It should be noted that there are currently no model abstraction methods to preserve full PCTL* properties for LNPPN.

4 Three-valued abstraction for LNPPN

In the fields of classical model checking, three-valued abstraction (Fecher et al. 2006; Shoham and Grumberg 2007) has been advocated as a better method for fighting state space explosion problem. It uses may and must transitions between abstract states to over- and under-approximate the concrete model. When lifting the three-valued abstraction to nondeterministic and probabilistic system model (i.e., LNPPN in this paper), it should be considered to handle the new nondeterminism and the probabilistic transition for over- and under-approximation in abstraction process.

5 Abstract model

We firstly present two kinds of extended LNPPN, which are used later for defining the abstract model of LNPPN.

Definition 4

Interval NPPN with Label (LINPPN). The interval LNPPN (LINPPN) can also be defined as a 7-tuple $M = \left( {S,\; T;\; F,\; f;\; C;\; AP,\;{ }L} \right)$, where: (1) $T = \left( {Transition,\left[ {Pt_{l} ,Pt_{u} } \right]} \right)$, $Transition$ denotes the transition act, $Pt_{l} ,Pt_{u} \in \left[ {0,1} \right]$ denotes the success probability interval of the transition, and $Pt_{l} \le Pt_{u}$; (2) $f = f_{T} \cup f_{S} \cup f_{S \times T} \cup f_{T \times S}$, $f_{T} :T \to 2^{{Transition \times \left[ {Pt_{l} ,Pt_{u} } \right]}}$, and $Pt_{l} ,Pt_{u} :T \to \left[ {0,1} \right]$ describe the lower and upper bounds for the success probabilities of $T$, $f_{S} = S \to \left[ {0,1} \right]$, $f_{S \times T} = S \times T \to \left[ {0,1} \right]$ describe the probabilities between places and transitions, the value of $f_{T \times S}$ can be obtained from the probability interval value of $f_{T} \left( t \right)$, i.e., [$\sigma_{{Pt_{l} }} \left( {f_{T} \left( t \right)} \right),\sigma_{{Pt_{u} }} \left( {f_{T} \left( t \right)} \right)$], the value of $f_{S}$ except initial place can be computed according to the value of $f_{S \times T}$ and $f_{T \times S}$; (3) $\forall t \in T$, $\exists s \in S,{ }f_{T \times S} = \left[ {1 - \sigma_{{Pt_{u} }} \left( {f_{T} \left( t \right)} \right), 1 - \sigma_{{Pt_{l} }} \left( {f_{T} \left( t \right)} \right)} \right]$.$f_{T \times S} \left( {t \times s} \right) = \left[ {0,0} \right]$, if the probability interval value of $f_{T} \left( t \right)$ is $\left[ {1,1} \right]$, which represents transition $\left( {t,s} \right)$ and place $s$ are invalid; (4) $C$ is the set of nondeterminism classes, and each nondeterminism class is a set comprised of $\left( {s,t_{i} } \right)$ and $\sum \sigma_{{Pt_{l} }} \left( {f_{T} \left( {t_{i} } \right)} \right) \le 1 \le \sum \sigma_{{Pt_{u} }} \left( {f_{T} \left( {t_{i} } \right)} \right)$. If $\left\{ {\left( {s,t_{1} } \right),\left( {s,t_{1} } \right) \ldots \left( {s,t_{1} } \right)} \right\} \in C$, then $\mathop \sum \limits_{i = 1}^{n} f_{S \times T} \left( {s,t_{i} } \right) = 1$; (5) the others are the same with LNPPN.

An INPPN can be regarded as the extension of NPPN in transition probability, which permits the probability value of transition is the interval. The standard and complete LNPPN is a special case of LINPPN with $Pt_{l} = Pt_{u}$.

Definition 5

Game Probabilistic Petri Net with Label (LGPPN). A Game Probabilistic Petri Net with Label (LGPPN) is a tuple $M = \left( {S,\;\left( {S_{0} ,\;S_{1} ,\;S_{p} } \right),\;T;\;F,\;f;\;AP,\;L} \right)$ where: (1) $\left( {S_{0} ,{ }S_{1} ,{ }S_{p} } \right)$ is a partition of $S$, and places in $S_{0} ,{ }S_{1}$ and $S_{p}$ are called ‘Player 0’, ‘Player 1’ and ‘Probabilistic’ places, respectively; (2) if place $s \in S_{0} \cup S_{1}$ ($s$ is called player place), $f_{S \times T} \left( {s,t} \right) \in \left[ {0,1} \right]$ for every $t \in T$, and if $s \in S_{p}$, $\mathop \sum \limits_{t \in T} f_{S \times T} \left( {s,t} \right) = 1$; (3) the others are the same with LNPPN.

On the one hand, a LGPPN can be seen as the turn-based stochastic 2-player game played on NPPN. On the other hand, we can say that LGPPN extends the LNPPN with another non-deterministic choice among the enabled transitions in place s occurred. Moreover, either the non-deterministic choice has been made for reaching place s, or the non-deterministic choice has to be made after the enabled transitions in place s having been occurred. The standard and complete LNPPN can be defined as $\left( {S,\;\left( {S_{0} ,\;\emptyset ,\;S_{p} } \right),\;T;\;F,\;f} \right)$ in LGPPN form, which substitutes the set of nondeterminism classes C with $\left( {S_{0} ,\emptyset ,{ }S_{p} } \right)$.

To contain more information in abstract model for both negative and affirmative results of three-valued PCTL* stochastic model checking, we extend both LGPPN and LINPPN orthogonally to present abstract model that is named LGIPPN. As defined in Definition 5, ‘Player 0’ making choices in $S_{0}$ corresponds to the new nondeterminism caused by abstraction, ‘Player 1’ making choices in $S_{1}$ corresponds to the original nondeterminism in LNPPN, lower bound and upper bound of the interval under- and over-approximate probabilistic transition, respectively.

Definition 6

Game Interval PPN with Label (LGIPPN). A LGIPPN can be defined as $M = \left( {S,\;\left( {S_{0} ,\;S_{1} ,\;S_{p} } \right),\;T;\;F,\;f;\;AP,\;L} \right)$ where: (1) $\left( {S_{0} ,{ }S_{1} ,{ }S_{p} } \right)$ is a partition of$S$, and places in $S_{0} ,{ }S_{1}$ and $S_{p}$ are called ‘Player 0’, ‘Player 1’ and ‘Probabilistic’ places, respectively; (2) $f = f_{T} \cup f_{S} \cup f_{S \times T} \cup f_{T \times S}$, $f_{T} :T \to 2^{{Transition \times \left[ {Pt_{l} ,Pt_{u} } \right]}}$, and $Pt_{l} ,Pt_{u} :T \to \left[ {0,1} \right]$ describe the lower and upper bounds for the success probabilities of $T$,$f_{S} = S \to \left[ {0,1} \right]$, $f_{S \times T} = S \times T \to \left[ {0,1} \right]$ describe the probabilities between places and transitions, the value of $f_{T \times S}$ can be obtained from the probability interval value of $f_{T} \left( t \right)$, i.e., [$\sigma_{{Pt_{l} }} \left( {f_{T} \left( t \right)} \right),\sigma_{{Pt_{u} }} \left( {f_{T} \left( t \right)} \right)$], the value of $f_{S}$ except initial place can be computed according to the value of $f_{S \times T}$ and $f_{T \times S}$; (3) $\forall t \in T$, $\exists s \in S,{ }f_{T \times S} = \left[ {1 - \sigma_{{Pt_{u} }} \left( {f_{T} \left( t \right)} \right), 1 - \sigma_{{Pt_{l} }} \left( {f_{T} \left( t \right)} \right)} \right]$.$f_{T \times S} \left( {t \times s} \right) = \left[ {0,0} \right]$, if the probability interval value of $f_{T} \left( t \right)$ is$\left[ {1,1} \right]$, which represents transition $\left( {t,s} \right)$ and place $s$ are invalid; (4) if place $s \in S_{0} \cup S_{1}$ ($s$ is called player place), $f_{S \times T} \left( {s,t} \right) \in \left\{ {0,1} \right\}$ for every$t \in T$, if$s \in S_{p}$, $\mathop \sum \limits_{t \in T} f_{S \times T} \left( {s,t} \right) = 1$, and for every$t_{i} \in s^{.}$, $\sum \sigma_{{Pt_{l} }} \left( {f_{T} \left( {t_{i} } \right)} \right) \le 1 \le \sum \sigma_{{Pt_{u} }} \left( {f_{T} \left( {t_{i} } \right)} \right)$ and $\sigma_{{Pt_{l} }} \left( {f_{T} \left( {t_{i} } \right)} \right) \le \sigma_{{Pt_{u} }} \left( {f_{T} \left( {t_{i} } \right)} \right)$; (5) $L:S \times AP \to \left\{ {true,\;?,\;flase} \right\}$ is a labeling function that assigns a truth value in $\left\{ {true,\;?,\;flase} \right\}$ to each pair of place in $S$ and proposition in $AP$; (6) the others are the same with LNPPN.

Note that we don’t consider the place without any outgoing transition, which can be implemented by augmenting a transition to itself with probability 1. $L\left( {s,a} \right) = ?$ means that the truth value of an atomic proposition $a$ is indefinite in the place s. Player 0, probability interval and the third value “?” are used to model explicitly a loss of information due to abstraction of place and probabilistic transition properties of the LNPPN, respectively. We call a LGIPPN model a LNPPN if $S_{1} = \emptyset$, $Pt_{l} = Pt_{u}$, and there is no proposition taking value $?$ in any place. The relationship among LNPPN, ILNPPN, GLPPN and LGIPPN is shown in Fig. 3.

Fig. 3

Relationship between LNPPN, LGPPN, LINPPN and LGIPPN

We formalize the notion of the 3-valued abstraction in Definition 7 on the level of interval LGIPPN, because: (1) the LNPPN is a special case of LGIPPN; (2) generally speaking, appropriate abstract model LGIPPN cannot be constructed at the first time, when abstraction is used after the first time, the concrete model is just LGIPPN which is constructed in abstract process at last time.

Definition 7

Three-valued abstraction of LGIPPN. Let $M = \left( {S,\;\left( {S_{0} ,\;S_{1} ,\;S_{p} } \right),\;T;\;F,\;f;\;AP,\;L} \right)$ be a concrete model and ${\mathcal{P}} = \left\{ {{\mathcal{P}}_{1} ,{\mathcal{P}}_{2} , \ldots ,{\mathcal{P}}_{n} } \right\} \subseteq 2^{S}$ a partition of$S$, i.e., ${\mathcal{P}}_{i} \ne \emptyset$, ${\mathcal{P}}_{i} \cap {\mathcal{P}}_{j} = \emptyset$, for $i \ne j$, $1 \le i,j \le n$, and $\cup_{i = 1}^{n} {\mathcal{P}}_{i} = S$. Then the three-valued abstract model $M^{A} = \left( {S^{A} ,\;\left( {S_{0}^{A} ,\;S_{1}^{A} ,\;S_{p}^{A} } \right),\;T^{A} ;\;F^{A} ,\;f^{A} ;\;AP,\;L^{A} } \right)$ of $M$ induced by ${\mathcal{P}}$ can be defined as:

• (1) $S^{A} = S_{0}^{A} \cup S_{1}^{A} \cup { }S_{p}^{A}$

• (2) $S_{0}^{A} = {\mathcal{P}}$; $S_{1}^{A}$ is composed of place s from $S$, whose next places reached by s^. are identical after lifting; $S_{p}^{A}$ is set of probabilistic transitions emanating from each element of $S_{1}^{A}$, in the same style as $M$.

• (3) For $\forall t_{i}^{A}$ between $(s_{1}^{A} )_{m}$ and $\left( {s_{0}^{A} } \right)_{k}$, $\sigma_{{Pt_{l} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right) = {\text{inf}}_{{ \cdot \left( {t_{j} } \right) \in (s_{1}^{A} )_{m} }} \left( {\mathop \sum \limits_{{\left( {t_{j} } \right) \cdot \in \left( {s_{0}^{A} } \right)_{k} }} \sigma_{{Pt_{l} }} \left( {f_{T} \left( {t_{j} } \right)} \right)} \right)$ and $\sigma_{{Pt_{u} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right) = {\text{min}}\left\{ {1,{\text{ sup}}_{{ \cdot \left( {t_{j} } \right) \in (s_{1}^{A} )_{m} }} \left( {\mathop \sum \limits_{{\left( {t_{j} } \right) \cdot \in \left( {s_{0}^{A} } \right)_{k} }} \sigma_{{Pt_{u} }} \left( {f_{T} \left( {t_{j} } \right)} \right)} \right)} \right\}$

• (4) $T^{A}$ is the set of $t_{i}^{A}$

• (5) $F^{A}$ and $f^{A}$ can be got from $S^{A}$, $\left( {S_{0}^{A} ,{ }S_{1}^{A} ,{ }S_{p}^{A} { }} \right)$ and $T^{A}$ according to Definition 5.

• (6) $L^{A} \left( {(s_{0}^{A} )_{n} ,~a} \right) = \left\{ {\begin{array}{*{20}l} {~true,} \hfill & {if~L\left( {s,a} \right) = true~for~all~s \in (s_{0}^{A} )_{n} } \hfill \\ {false,~} \hfill & {if~L\left( {s,a} \right) = false~for~all~s \in (s_{0}^{A} )_{n} } \hfill \\ {?,} \hfill & {otherwise} \hfill \\ \end{array} } \right.$

• (7) Initial place of $M^{A}$ is $s_{init}^{A} = {\mathcal{P}}_{i}$, where initial place of $M$ $s_{init} \in {\mathcal{P}}_{i}$. Initial distribution of $M^{A}$ is $\mu_{0}^{A} \left( {(s_{0}^{A} )_{n} } \right) = \mathop \sum \limits_{{s \in (s_{0}^{A} )_{n} }} \mu_{0} \left( s \right)$.

Note that partition ${\mathcal{P}}$ is usually depending on where $M$ are used. In this paper, partition ${\mathcal{P}}$ is based on invisible variables (Clarke et al. 2002) which means that an abstract place (${\mathcal{P}}_{i}$) “agrees” on all the variables that are visible. Intuitively speaking, the Player 0 place is an element of the partition of places in concrete $M$. Player 0 selects a concrete place in the set ${\mathcal{P}}$ firstly, then Player 1 selects a probability distribution over the concrete $t_{i}$, which is a distribution over abstract places rather than concrete places.

Theorem 1

For any LGIPPN $M$ and partition ${\mathcal{P}}$, the three-valued abstract model $M^{A}$ constructed by Definition 7is also a LGIPPN.

Proof

It is obvious that $S^{A}$, $\left( {S_{0}^{A} ,{ }S_{1}^{A} ,{ }S_{p}^{A} } \right)$, $F^{A}$, $f^{A}$, $AP$ and $L^{A}$ are all in accordance with the definition of LGIPPN. To prove $M^{A}$ is a LGIPPN, it is just to prove: (1) $\sigma_{{Pt_{l} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right) \in \left[ {0,1} \right]$, $\sigma_{{Pt_{u} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right) \in \left[ {0,1} \right]$, and $\sigma_{{Pt_{l} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right) \le \sigma_{{Pt_{u} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right)$; (2) $\sum \sigma_{{Pt_{l} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right) \le 1 \le \sum \sigma_{{Pt_{u} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right)$. The former obligation (1) follows by easy derivation from (3) of Definition 7. We show that obligation (2) holds: $\sum \sigma_{{Pt_{l} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right)\mathop \sum \limits_{{\left( {t_{j} } \right) \cdot \in S_{0}^{A} }} \left( {\mathop \sum \limits_{{ \cdot \left( {t_{j} } \right) \in (S_{1}^{A} )_{m} , \left( {t_{j} } \right) \cdot \in \left( {S_{0}^{A} } \right)_{k} }} \sigma_{{Pt_{l} }} \left( {f_{T} \left( {t_{j} } \right)} \right)} \right) \le 1$; $\sum \sigma_{{Pt_{u} }} \left( {f_{{T^{A} }} \left( {t_{i}^{A} } \right)} \right) = \mathop \sum \limits_{{\left( {t_{j} } \right) \cdot \in S_{0}^{A} }} \left( {{\text{min}}\left\{ {1,{\text{ sup}}_{{ \cdot \left( {t_{j} } \right) \in (S_{1}^{A} )_{m} }} \left( {\mathop \sum \limits_{{\left( {t_{j} } \right) \cdot \in \left( {S_{0}^{A} } \right)_{k} }} \sigma_{{Pt_{u} }} \left( {f_{T} \left( {t_{j} } \right)} \right)} \right)} \right\}} \right) \ge \mathop \sum \limits_{{\left( {t_{j} } \right) \cdot \in S_{0}^{A} }} \left( {\mathop \sum \limits_{{ \cdot \left( {t_{j} } \right) \in (S_{1}^{A} )_{m} , \left( {t_{j} } \right) \cdot \in \left( {S_{0}^{A} } \right)_{k} }} \sigma_{{Pt_{u} }} \left( {f_{T} \left( {t_{j} } \right)} \right)} \right) \ge 1$. So, $M^{A}$ is a LGIPPN.□

5.1 Simulation relation on LGIPPN

To compare the behavior between LGIPPN model and its abstract model, we will discuss simulation relation on LGIPPN model. Simulation relations have been extensively studied both in classical model checking and stochastic model checking. The state-based simulation for probabilistic models (Jonsson and Larsen 1991) is a preorder on a state space. It requires that if state u simulates state v, u can mimic the stepwise behavior of v but may have more behavior that cannot be matched by u. This state-based simulation can be employed to distributions over places of LGIPPN model via weight function (Jonsson and Larsen 1991).

Definition 8

Distribution-based simulation. Let $S$, $S^{\prime }$ be the set of places in LGIPPN model, and $\mu \in distr\left( S \right)$, $\mu^{\prime } \in distr\left( {S^{\prime } } \right)$. For $R \subseteq S \times S^{\prime }$, $\mu^{\prime }$ simulates $\mu$ w.r.t. $R$, denoted $\mu R\mu^{\prime }$, if there exists a weight function $\Delta :S \times S^{\prime } \to \left[ {0,1} \right]$ such that for all $u \in S$, $v \in S^{\prime }$: (1) $\Delta \left( {u,v} \right) > 0 \Rightarrow uRv$, (2) $\mathop \sum \limits_{{s^{\prime } \in \;S^{\prime } }} \Delta \left( {u,s^{\prime } } \right) = \mu \left( u \right)$, (3)$\mathop \sum \limits_{s \in S} \Delta \left( {s,v} \right) = \mu^{\prime } \left( v \right)$

Distribution-based simulation can be computed by reducing them to a maximum-flow problem (Zhang et al. 2018). It plays an important role in defining simulation relation on LGIPPN model.

Definition 9

Probabilistic simulation. Let $M$, $M^{\prime }$ be LGIPPN models, $\mu_{0}$, $\mu_{0}^{^{\prime}}$ be the initial distributions. $R \subseteq S \times S^{\prime }$ is a probabilistic simulation relation for $\left( {M,M^{\prime } } \right)$, which holds that: (1) $\mu_{0} R\mu_{0}^{^{\prime}}$, (2) for $\forall \left( {s,s^{\prime } } \right) \in R$: (2–1) $L^{\prime } \left( {s^{\prime } ,a} \right) \ne ? \Rightarrow L^{\prime } \left( {s^{\prime } ,a} \right) = L\left( {s,a} \right)$, (2–2) $s\to ^{t} \mu$ implies $s^{\prime } \to ^{{t^{\prime } }} \mu^{\prime }$ such that $\mu R\mu^{\prime }$, where $t = \left( {Transition,\left[ {Pt_{l} ,Pt_{u} } \right]} \right)$, $t^{\prime } = \left( {Transition,\left[ {Pt_{l}^{^{\prime}} ,Pt_{u}^{^{\prime}} } \right]} \right)$

If there exists a probabilistic simulation relation for $\left( {M,M^{\prime } } \right)$, we say that LGIPPN model $M$ is simulated by $M^{\prime }$, denoted $M{ \preceq }M^{\prime }$.

Theorem 2

Given a LGIPPN model $M$, the LGIPPN model ${M}^{A}$ obtained by applying Definition 7 is such that $M\preccurlyeq {M}^{A}$.

Proof

In order to prove$M\preccurlyeq {M}^{A}$, we just show that $R=\{(s, {\mathcal{P}}_{i})|s\in {\mathcal{P}}_{i},{\mathcal{P}}_{i}\in \mathcal{P}\}$ is a probabilistic simulation in Definition 8. According to Definition 7-(7), ${\mu }_{0}^{A}\left({{(s}_{0}^{A})}_{n}\right)={\sum }_{s\in {{(s}_{0}^{A})}_{n}}{\mu }_{0}(s)$, it directly follows ${\mu }_{0}R{\mu }_{0}^{A}$ and fulfils condition (1) of Definition 8. It can also show that ${L}^{A}$ fulfills condition (2–1) of Definition 8 by the Definition 7-(6). Let$\left(s,{{(s}_{0}^{A})}_{n}\right)\in R$, $s\stackrel{t}{\to }\mu$ and${\mathcal{P}}_{i}\stackrel{{t}^{A}}{\to }{\mu }^{A}$, then we construct a weight function $\Delta$ and show it fulfills the condition (2–2) of Definition 8, i.e., the condition (1) (2) (3) of Definition 7. (1) for $v\in \mathcal{P}$ let${\mu }^{A}\left(v\right)={\sum }_{u\in v}\mu (u)$, and for $u\in S$ let$\Delta \left( {u,v} \right) = \left\{ {\begin{array}{*{20}l} {\mu \left( u \right)} \hfill & {if(u,v) \in R} \hfill \\ 0 \hfill & {otherwise} \hfill \\ \end{array} } \right.$, function ${\mu }^{A}$ is a probability distribution if $\mu$ is:$\sum _{{v \in {\mathcal{P}}}} \mu ^{A} \left( v \right) = \sum _{{v \in {\mathcal{P}},\;u \in v}} \mu (u) = \sum _{{u \in S}} \mu (u) = 1$. Then for$v\stackrel{{t}^{A}}{\to }{\mathcal{P}}_{i}$, ${\sigma }_{{Pt}_{l}}({f}_{T}({t}^{A}))\le {\mu }^{A}\left(v\right)\le {\sigma }_{{Pt}_{u}}({f}_{T}({t}^{A}))$ is hold according to Definition 6. Condition (1) of Definition 7 is fulfilled trivially, since $\Delta \left( {u,v} \right) = 0$ if $(u,v )\notin R$. (2) $\sum\limits_{{\rm{\mathcal{P}}_{i} \in {\text{ }}\rm{\mathcal{P}}}} \Delta \left( {u,\rm{\mathcal{P}}_{i} } \right) = \mu (u)$, condition (2) of Definition 7 is fulfilled. (3)$\sum _{{u \in S}} \Delta \left( {u,v} \right) = \sum _{{u \in v}} \Delta \left( {u,v} \right) = \sum _{{u \in v}} \mu (u) = \mu ^{A} \left( v \right)$, condition (3) of Definition 7 is fulfilled. So, $M\preccurlyeq {M}^{A}$.□

5.2 Preservation of PCTL*

When evaluating a PCTL* formula over the LGIPPN model, a place may no longer just satisfy or refuse the formula, i.e., “true” or “false”, but indefinitely satisfy or refuse it, i.e., value “?”. If a formula is evaluated to “true” or “false” in a place, we say that the result is definite. Otherwise, we say that it is indefinite. We generalize Kleene’s strong 3-valued propositional logic (Paoli and Prabaldi 2020) to interpret propositional operators on the LGIPPN model. Operator conjunction $\sqcap$ is defined as follows: the operation value is “true”, if both arguments of $\sqcap$ are “true”; the operation value is “false”, if either of arguments is “false”; and the operation value is “?” (i.e., the value is indefinite), otherwise. Operator negation $\neg$ maps “true” to “false”, “false” to “true”, and “?” to “?”. Operator disjunction $\bigsqcup$ can be derived from the operator $\sqcap$ with De Morgan’s laws.

Given a LGIPPN model $M = \left( {S,\;\left( {S_{0} ,\;S_{1} ,\;S_{p} } \right),\;T;\;F,\;f;\;AP,\;L} \right)$ a PCTL* state formula ${\Phi }$, the three-valued semantics of ${\Phi }$ in a place $s$, denoted as $\left[ {\left( {M,s} \right) \vDash _{3} {\Phi }} \right]$, can be defined inductively:

$$\left[ {\left( {M,s} \right) \vDash _{3} {\text{true}}} \right] = {\text{true}}$$

$$\left[ {\left( {M,s} \right) { \vDash }_{3} \;a} \right] = \left\{ {\begin{array}{*{20}l} {{\text{true}}} \hfill & {{\text{if}}\;a \in L\left( {\text{s}} \right)} \hfill \\ {{\text{false}}} \hfill & {{\text{if}}\;\neg \;a \in L\left( s \right)} \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$$

$$\left[ {\left( {M,s} \right) \vDash _{3} \neg \Phi } \right] = \left\{ {\begin{array}{*{20}l} {{\text{true}}} \hfill & {{\text{if}}~~s{ \nvDash }_{3} \Phi } \hfill \\ {{\text{false}}~} \hfill & {{\text{if}}~~s \vDash _{3} \Phi } \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$$

$$\left[ {\left( {M,s} \right) { \vDash }_{3}\; \Phi _{0} \wedge \Phi _{1} } \right] = \left\{ {\begin{array}{*{20}l} {{\text{true}}} \hfill & {{\text{if}}\;\left[ {\left( {M,s} \right)\;{ \vDash }_{3}\; \Phi _{0} } \right] = {\text{true}}\;{ \sqcap }\;\left[ {\left( {M,s} \right)\;{ \vDash }_{3}\; \Phi _{1} } \right] = {\text{true}}} \hfill \\ {{\text{false}}} \hfill & {{\text{if}}\;\left[ {\left( {M,s} \right)\;{ \vDash }_{3}\; \Phi _{0} } \right] = {\text{false}}\;{ \sqcup }\;\left[ {\left( {M,s} \right)\;{ \vDash }_{3}\; \Phi _{1} } \right] = {\text{false}}} \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$$

$$\left[ {\left( {M,\;s} \right){ \vDash }_{3} \;{\text{P}}_{{ \ge p}} \left( \Psi \right)} \right] = \left\{ {\begin{array}{*{20}l} {{\text{true}}} \hfill & {~{\text{if}}~~Prob_{{\inf }} \left( {s,\;\Psi ,\;{\text{true}}} \right) \ge p} \hfill \\ {{\text{false}}} \hfill & {{\text{if}}~~Prob_{{\sup }} \left( {s,\,\Psi ,\;{\text{false}}} \right) < p} \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$$

$$\left[ {\left( {M,s} \right) \vDash _{3} {\text{P}}_{ \le p} \left( {\Psi } \right)} \right] = \left\{ {\begin{array}{*{20}l} {{\text{true}}} \hfill & {{\text{if}}\; Prob_{{{\text{sup}}}} \left( {s,{\Psi },{\text{false}}} \right) \le p} \hfill \\ {{\text{false}}} \hfill & {{\text{if}}\; Prob_{{{\text{inf}}}} \left( {s,{\Psi },{\text{true}}} \right) > p} \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$$

where $Prob_{{{\text{inf}}}} \left( {s,{\Psi },{\text{true}}} \right)$ is the probability measure of path set such that $\pi \vDash {\Psi }$, i.e., $Prob\left( {s,\;\Psi } \right)$$\; = Pr_{s} \left( {\left\{ {\pi \in Path\left( s \right)\;|\pi \;{ \vDash }\;\Psi } \right\}} \right)$, $Path\left( s \right)$ is the path set which starts with place$s$. Case $\left[ {\left( {M,s} \right) \vDash _{3} {\Phi }_{0} \vee {\Phi }_{1} } \right]$ can be derived from $\left[ {\left( {M,s} \right) \vDash _{3} {\Phi }_{0} \wedge {\Phi }_{1} } \right]$ according to De Morgan’s laws. Cases $\left[ {\left( {M,s} \right) \vDash _{3} {\text{P}}_{ > p} \left( {\Psi } \right)} \right]$ and $\left[ {\left( {M,s} \right) \vDash _{3} {\text{P}}_{ < p} \left( {\Psi } \right)} \right]$ are similar to the cases $\left[ {\left( {M,s} \right) \vDash _{3} {\text{P}}_{ \ge p} \left( {\Psi } \right)} \right]$ and $\left[ {\left( {M,s} \right) \vDash _{3} {\text{P}}_{ \le p} \left( {\Psi } \right)} \right]$, respectively, but we exchange $\ge$ by $>$ and vice versa. For a path $\pi = s_{0} \to ^{{t_{0} }} s_{1} \to ^{{t_{1} }} s_{2} \to ^{{t_{2} }} s_{3} \ldots$ (abbr.$\pi = s_{0} s_{1} s_{2} s_{3} \ldots$, if it is not related to$t$), the three-valued semantics of a path formula ${\Psi }$ on$\pi$, denoted $\left[ {\left( {M,\pi } \right) \vDash _{3} {\Psi }} \right]$, is defined inductively as follows:

$$\left[ {\left( {M,\pi } \right) \vDash _{3} {\Phi }} \right] = \left\{ {\begin{array}{*{20}l} {\left[ {\left( {M,s_{0} } \right) \vDash _{3} {\Phi }} \right] } \hfill & {{\text{if}}\; \left| \pi \right| > 0} \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$$

$$\left[ {\left( {M,\pi } \right) \vDash _{3} {\text{X}}\Psi ~} \right] = \left\{ {\begin{array}{*{20}l} {\left[ {\left( {M,s_{1} } \right) \vDash _{3} \Psi } \right]~} \hfill & {~{\text{if}}~\left| \pi \right| > 1} \hfill \\ ? \hfill & {{\text{otherwise}}~} \hfill \\ \end{array} } \right.$$

$$\left[ {\left( {M,\pi } \right) \vDash _{3} \neg \Psi } \right] = \left\{ {\begin{array}{*{20}l} {{\text{true}}} \hfill & {{\text{if}}\; \pi { \nvDash }_{3} \Psi } \hfill \\ {{\text{false}}} \hfill & {{\text{if}}\; \pi \vDash _{3} \Psi } \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$$

$\left[ {\left( {M,\pi } \right)\;{ \vDash }_{3}\; \Psi _{0} \wedge \Psi _{1} } \right] = \left\{ {\begin{array}{*{20}l} {{\text{true}}} \hfill & {{\text{if}}\;\left[ {\left( {M,\pi } \right)\;{ \vDash }_{3}\; \Psi _{0} } \right] = {\text{true}}\;{ \sqcap }\;\left[ {\left( {M,\pi } \right)\;{ \vDash }_{3}\; \Psi _{1} } \right] = {\text{true}}} \hfill \\ {{\text{false}}} \hfill & {{\text{if}}\;\left[ {\left( {M,\pi } \right)\;{ \vDash }_{3}\; \Psi _{0} } \right] = {\text{false}}\;{ \sqcup }\;\left[ {\left( {M,\pi } \right)\;{ \vDash }_{3}\; \Psi _{1} } \right] = {\text{false}}} \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$ $\left[ {\left( {M,\pi } \right) \vDash _{3} \Psi _{0} {\text{U}}\Psi _{1} ~} \right] = \left\{ {\begin{array}{*{20}l} {{\text{true}}} \hfill & \begin{gathered} {\text{if}}~~\exists ~0 \le k < \left| \pi \right|:[\left( {\left[ {\left( {M,s_{k} } \right) \vDash _{3} \Psi _{1} } \right] = {\text{true}}} \right){ \sqcap } \hfill \\ (\forall j < k:\left[ {\left( {M,s_{j} } \right) \vDash _{3} \Psi _{0} } \right] = {\text{true}})] \hfill \\ \end{gathered} \hfill \\ {{\text{false}}} \hfill & \begin{gathered} {\text{if}}~(\forall ~0 \le k < \left| \pi \right|:\left( {[(\forall j < k:\left[ {\left( {M,s_{j} } \right) \vDash _{3} \Psi _{0} } \right] \ne {\text{false}}} \right) \hfill \\ \Rightarrow \left( {\left[ {\left( {M,s_{k} } \right) \vDash _{3} \Psi _{1} } \right] = {\text{false}}} \right)]){ \sqcap } \hfill \\ \left( {\left( {\forall 0 \le k < \left| \pi \right|:\left[ {\left( {M,s_{k} } \right) \vDash _{3} \Psi _{0} } \right] \ne {\text{false}}} \right) \Rightarrow \left| \pi \right| = \infty } \right) \hfill \\ \end{gathered} \hfill \\ ? \hfill & {{\text{otherwise}}} \hfill \\ \end{array} } \right.$ The other path operators can be derived from above cases.

If $\forall {s}_{0}\in {S}_{0}:\left[\left(M,{s}_{0}\right){\models }_{3}\Phi \right]=\mathrm{true}$, we can conclude that $\left[M{\models }_{3}\Phi \right]=\mathrm{true}$, i.e., $M{\models }_{3}\Phi$. If $\exists {s}_{0}\in {S}_{0}:\left[\left(M,{s}_{0}\right){\models }_{3}\Phi \right]=\mathrm{false}$, we can conclude that $\left[M{\models }_{3}\Phi \right]=\mathrm{false}$, i.e., $M{ \nvDash }_{3} {{\Phi }}$. $\left[M{\models }_{3}\Phi \right]=?$, otherwise. Formally, the three-valued semantics of PCTL* characters a preorder relation over a LGIPPN model that reflects the degree of completeness. Let $\lesssim$ denote an information ordering over the truth values, in which $?\lesssim \mathrm{true}$, $?\lesssim \mathrm{false}$, and $x\lesssim x$ ($x\in \{\mathrm{true},\mathrm{false},?\}$). The operators $comp$, $min$ and $max$ are monotonic on$\lesssim$, i.e., if ${x}_{1}\lesssim {x}_{2}$ and ${y}_{1}\lesssim {y}_{2}$, then $comp({x}_{1})\lesssim comp({x}_{2})$, $min({x}_{1})\lesssim min({x}_{2})$ and $max({x}_{1})\lesssim max({x}_{2})$. We can conclude that $[({M}^{A},{s}_{init}^{A} ){\models }_{3}\Phi ]\lesssim [(M,{s}_{init}){\models }_{3}\Phi ]$. Informally, if a LGIPPN model is more abstract with respect to $\preccurlyeq$, it has less definite properties that are either “true” or “false” with respect to $\lesssim$. Moreover, a formula of PCTL* is evaluated to “true” of “false” on an abstract LGIPPN model, then it has the same truth value on any refinement models. In other words, the result of three-valued PCTL* stochastic model-checking an abstract LGIPPN model agrees with the concrete model, if the results are definite. This is asserted in Theorem 3.

Theorem 3

Let $R\subseteq S\times {S}^{A}$ be a mixed probabilistic simulation relation from a LGIPPN model $M$ to a LGIPPN model ${M}^{A}$, i.e., $M\preccurlyeq {M}^{A}$. Then for all PCTL* formulas $\Phi$:$\left[{M}^{A}{\models }_{3}\Phi \right]\ne ? implies \left[{M}^{A}{\models }_{3}\Phi \right]=\left[M\models \Phi \right]$.

Proof

$\left[{M}^{A}{\models }_{3}\Phi \right]=[({M}^{A},{s}_{init}^{A} ){\models }_{3}\Phi ]$ and $\left[M\models\Phi \right]=[(M,{s}_{init}){\models }_{3}\Phi ]$, so, we can prove the following proposition for proving it. For every $(s,{ s}^{A})\in R$ and all PCTL* formulas $\Phi$: $\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}\Phi \right]\ne ?$ implies $\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}\Phi \right]=\left[\left(M,s\right)\models\Phi \right]$. It can be proved by the induction method: (1) $\Phi =\mathrm{true}$: $\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}\mathrm{true}\right]=\mathrm{true}=\left[\left(M,s\right)\models \mathrm{true}\right]$, since $s\preccurlyeq {s}^{A}$. (2) PCTL* formulae $\Phi$ is atomic proposition $a$: $\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}a\right]={L}^{A}\left({ s}^{A}, a\right)=L(s, a)=\left[\left(M,s\right)\models a\right]$. Induction hypothesis: suppose ${\Phi }^{\mathrm{^{\prime}}}$ represents all sub-formulas of $\Phi$, $\left[ {\left( {M^{A} ,~s^{A} } \right) \vDash _{3} \Phi ^{\prime } } \right] \ne ?$ implies that $\left[ {\left( {M^{A} ,~s^{A} } \right) \vDash _{3} \Phi ^{\prime } } \right] = \left[ {\left( {M,s} \right) \vDash \Phi ^{\prime } } \right]$. (3) $\Phi = \neg \Phi ^{\prime }$: $\left[ {\left( {M^{A} ,~s^{A} } \right) \vDash _{3} \neg \Phi ^{\prime } } \right] = \neg \left[ {\left( {M,~s^{A} } \right) \vDash _{3} \Phi ^{\prime } } \right] = \neg \left[ {\left( {M,s} \right) \vDash \Phi ^{\prime } } \right] = \left[ {\left( {M,s} \right) \vDash \neg \Phi ^{\prime } } \right]$. (4) $\Phi ={\Phi }_{0}^{^{\prime}}\wedge {\Phi }_{1}^{^{\prime}}$: $\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}{\Phi }_{0}^{^{\prime}}\wedge {\Phi }_{1}^{^{\prime}}\right]=\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}{\Phi }_{0}^{^{\prime}}\right]\sqcap \left[\left({M}^{A},{ s}^{A}\right){\models }_{3}{\Phi }_{1}^{^{\prime}}\right]=\left[\left(M,s\right)\models {\Phi }_{0}^{^{\prime}}\right]\wedge \left[\left(M,s\right)\models {\Phi }_{1}^{^{\prime}}\right]=\left[\left(M,s\right)\models {\Phi }_{0}^{^{\prime}}\wedge {\Phi }_{1}^{^{\prime}}\right]$. (5) $\Phi ={\mathrm{P}}_{\le p}(\Psi )$, where $\Psi = \Phi ^{\prime } /X\Psi ^{\prime } /\neg \Psi ^{\prime } /\Psi _{0} \; \wedge \;\Psi _{1} /\Psi _{0} \;{\text{U}}\;\Psi _{1}$: if $\left[\left({M}^{A},{s}^{A}\right){\models}_{3}\Phi \right] = {\text{true}}\Rightarrow {Prob}_{\text{sup}}\left(s,\Psi ,{\text{true}}\right)\le {Prob}_{\text{sup}}\left({s}^{A},\Psi ,{\text{true}}\right)\le p\Rightarrow \left[\left(M,s\right) \models \Phi \right]={\text{true}}$; if $\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}\Phi \right]=\mathrm{false}\Rightarrow {Prob}_{\mathrm{inf}}\left(s,\Psi ,\mathrm{true}\right)\ge {Prob}_{\mathrm{inf}}\left({ s}^{A},\Psi ,\mathrm{true}\right)>p\Rightarrow \left[\left(M,s\right)\models\Phi \right]=\mathrm{false}$. (6) $\Phi ={\mathrm{P}}_{\ge p}(\Psi )$, where $\Psi = \Phi ^{\prime } /X\Psi ^{\prime } /\neg \Psi ^{\prime } /\Psi _{0} \; \wedge \;\Psi _{1} /\Psi _{0} \;{\text{U}}\;\Psi _{1}$: if $\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}\Phi \right]=\mathrm{true}\Rightarrow {Prob}_{\mathrm{inf}}\left(s,\Psi ,\mathrm{true}\right)\ge {Prob}_{\mathrm{inf}}\left({ s}^{A},\Psi ,\mathrm{true}\right)\ge p\Rightarrow \left[\left(M,s\right)\models\Phi \right]=\mathrm{true}$; if $\left[\left({M}^{A},{ s}^{A}\right){\models }_{3}\Phi \right]=\mathrm{false}\Rightarrow {Prob}_{\mathrm{sup}}\left(s,\Psi ,\mathrm{true}\right)\le {Prob}_{\mathrm{sup}}\left({ s}^{A},\Psi ,\mathrm{true}\right)<p\Rightarrow \left[\left(M,s\right)\models\Phi \right]=\mathrm{false}$.□

The above theorem states that our abstraction framework can indeed be used as a solution to MA4SMC problem, which constructs three-valued abstract model according to Definition 7, and preserves the full PCTL* properties. Intuitively speaking, in this framework, the results of PCTL* stochastic model-checking an abstract model agree with PCTL* stochastic model-checking a concrete model, unless the result is indefinite.

6 Three-valued stochastic model checking

Given a three-valued abstract model (LGIPPN model ${M}^{A}$) and a PCTL* formula $\Phi$ in release-PNF, deciding whether ${M}^{A}{\models }_{3}\Phi$, i.e., $\left({M}^{A},{s}_{init}^{A}\right){\models }_{3}\Phi$, holds or not, is named the three-valued PCTL* stochastic model checking. Theoretically speaking, it can be reduced to two instances of the traditional PCTL* stochastic model checking, as the three-valued model checking to traditional model checking. In this section, we give a direct game-based three-valued PCTL* stochastic model checking algorithm.

6.1 Game semantics for three-valued stochastic model checking

The game-based operational semantics for PCTL* stochastic model checking is an intuitive and succinct approach for stochastic model checking, and it can provide the succinct evidences for corresponding results. In this section, we generate it to three-valued PCTL* stochastic model checking.

The game ${\mathrm{G}}_{{M}^{A}}^{\Phi }(player, board, rule)$ for a three-valued abstract model (LGIPPN model ${M}^{A}$) and a PCTL* formula $\Phi$ in release-PNF can be defined as in Liu et al. (2016). However, some move rules of the player and the winning criteria need to be changed. The differences are caused by the fact that LGIPPN model has the interval transitions. Since the transitions are considered only in configurations with sub-formulae of ${\mathrm{P}}_{\ge p}(\mathrm{X\Psi })$ or ${\mathrm{P}}_{\le p}(\mathrm{X\Psi })$, the new move rules for game consist of move rules in Liu et al. (2016), with exception that rule (6) are adapted as follows:

• (0) $p = 0$, the play finishes and player $verifier$ wins.

• (1) $Con_{i} = \left( {player,s,{\text{true}}/{\text{false}}/a/\neg a/{\text{P}}_{ \ge p} \left( {{\text{true}}/{\text{false}}/a/\neg a} \right),{\Omega }} \right)$, the play finishes.

• (2) $Con_{i} = \left( {verifier,s,{\Phi }_{0} \wedge {\Phi }_{1} ,{\Omega }} \right)$, player $refuter$ chooses ${\Phi }_{j}$,$j \in \left\{ {0,1} \right\}$, and $Con_{i + 1} = \left( {verifier,s,{\Phi }_{j} ,\left\{ {{\Phi }_{1 - j} } \right\} \cup {\Omega }} \right)$.

• (3) $Con_{i} = \left( {verifier,s,{\Phi }_{0} \vee {\Phi }_{1} ,{\Omega }} \right)$, player $verifier$ chooses ${\Phi }_{j}$,$j \in \left\{ {0,1} \right\}$, and $Con_{i + 1} = \left( {verifier,s,{\Phi }_{j} ,{\Omega }} \right)$.

• (4) $Con_{i} = \left( {refuter{ },s,{\Phi }_{0} \wedge {\Phi }_{1} ,{\Omega }} \right)$, player $refuter$ chooses${\Phi }_{j}$,$j \in \left\{ {0,1} \right\}$, and$Con_{i + 1} = \left( {refuter{ },s,{\Phi }_{j} ,{\Omega }} \right)$.

• (5) $Con_{i} = \left( {refuter{ },s,{\Phi }_{0} \vee {\Phi }_{1} ,{\Omega }} \right)$, player $verifier$ chooses${\Phi }_{j}$,$j \in \left\{ {0,1} \right\}$, and$Con_{i + 1} = \left( {refuter{ },s,{\Phi }_{j} ,\left\{ {{\Phi }_{1 - j} } \right\} \cup {\Omega }} \right)$.

• (6) $Con_{i} = \left( {verifier,s^{A} ,{\text{P}}_{{ \ge p}} \left( {{\text{X}}\Psi } \right),\Omega } \right)$: player $verifier$ chooses some transitions $t^{A}$ in the minimum nondeterministic class by an adversary, and $Con_{{i + 1}} = \left( {verifier,s^{{A\prime }} ,{\text{P}}_{{ \ge ps^{{A\prime }} }} \left( \Psi \right)} \right)$, where $s^{A} \to ^{{t^{A} }} s^{A} {^{\prime}}$, and where $\sum P_{l} \left( {s^{A} ,s^{\prime}} \right) \cdot ps^{\prime} \ge p$ where $P_{l} \left( {s^{A} ,s^{\prime}} \right)$ is the lower probability from the place $s^{A}$ to $s^{A} {^{\prime}}$ and $ps^{A} {^{\prime}}$ is the probability of $s^{A} {^{\prime}}$ satisfies ${\Psi }$; or player $refuter$ chooses some transitions $t^{A}$ in the maximum nondeterministic class by an adversary, and $Con_{i + 1} = \left( {refuter,s^{A} {^{\prime}},{\text{P}}_{{ < ps^{A^{\prime}} }} \left( {\Psi } \right)} \right)$, where $s^{A} \to ^{t} s^{A} {^{\prime}}$, and where $\sum P_{u} \left( {s^{A} ,s^{A} {^{\prime}}} \right) \cdot ps^{A} {^{\prime}} \ge p$ where $P_{u} \left( {s^{A} ,s^{A} {^{\prime}}} \right)$ is the upper probability from place $s^{A}$ to $s^{A} {^{\prime}}$ and $ps^{A} {^{\prime}}$ is the probability of $s^{A} {^{\prime}}$ satisfies ${\Psi }$.

• (7) $Con_{i} = \left( {verifier,s,{\text{P}}_{ \ge p} \left( {{\Psi }_{1} \wedge {\Psi }_{2} } \right),{\Omega }} \right)$, player $refuter$ chooses ${\Psi }_{j}$,$j \in \left\{ {0,1} \right\}$, and $Con_{i + 1} = (refuter,s,{\text{P}}_{ \ge pj} \left( {{\Psi }_{j} } \right)$), and $p0 + p1 - 1 < p$.

• (8) $Con_{i} = \left( {verifier,s,{\text{P}}_{ \ge p} \left( {{\Psi }_{0} \vee {\Psi }_{1} } \right),{\Omega }} \right)$, player $verifier$ chooses ${\Psi }_{j}$, and $Con_{i + 1} = \left( {verifier, s,{\text{P}}_{ \ge pj} \left( {{\Psi }_{j} } \right)} \right)$, and $p0 + p1 \ge p$.

• (9) $Con_{i} = \left( {verifier,s,{\text{P}}_{{ \ge p}} \left( {\Psi _{0} {\text{U}}\,\Psi _{1} } \right),\Omega } \right)$:$Con_{{i + 1}} = \left( {verifier,s,{\text{P}}_{{ \ge p}} \left( {\Psi _{1} \vee \left( {\Psi _{0} \wedge X\left( {\Psi _{0} {\text{U}}\;\Psi _{1} } \right)} \right)} \right)} \right)$.

• (10) $Con_{i} = \left( {verifier,s,P_{{ \ge p}} \left( {\Psi _{0} R\Psi _{1} } \right),\Omega } \right)$:$Con_{{i + 1}} = \left( {verifier,s,{\text{P}}_{{ \ge p}} \left( {\Psi _{1} \wedge \left( {\Psi _{0} \vee {\text{X}}\left( {\Psi _{0} {\text{R}}\Psi _{1} } \right)} \right)} \right)} \right)$.

• (11) $Con_{i} = (player,s,{\Phi },\{ {\text{P}}_{ \ge p} \left( {\Psi } \right)\} \cup {\Omega }):$ $Con_{i + 1} = \left( {player,s,{\Phi },{\Omega }} \right)$.

• (12) $Con_{i} = \left( {player,s,{\Phi },\left\{ {{\text{true}}/{\text{false}}/a/\neg a} \right\} \cup {\Omega }} \right):$ $Con_{i + 1} = \left( {player,s,{\Phi },{\Omega }} \right)$.

• (13) $Con_{i} = \left( {verifier,s,{\Phi }_{0} ,\left\{ {{\Phi }_{1} } \right\} \cup {\Omega }} \right)$, player $refuter$ chooses, and $Con_{i + 1} = \left( {verifier,s, {\Phi }_{1} , \left\{ {{\Phi }_{0} } \right\} \cup {\Omega }} \right)$.

• (14) $Con_{i} = \left( {refuter,s,{\Phi }_{0} ,\left\{ {{\Phi }_{1} } \right\} \cup {\Omega }} \right)$, player $verifier$ chooses, and $Con_{i + 1} = \left( {refuter, s, {\Phi }_{1} , \left\{ {{\Phi }_{0} } \right\} \cup {\Omega }} \right)$.

For $Con_{i} = \left( {verifier,s,{\text{P}}_{{ \le p}} \left( {{\text{X}}\Psi } \right),\Omega } \right)$, the move rule can be defined analogously. Intuitively speaking, each player can use both lower and upper bound of transition, and the players use lower bond of transition in order to win, while they use upper bound of transition in order to prevent the other player from wining. Therefore, the new winning criteria are:

• (1) The $verifier$ wins the play if and only if one of the following conditions holds: (a) the play ends with rule (0); (b) the play ends with rule (1), and the configuration is $(player,s,\mathrm{true}/{\mathrm{P}}_{\ge p}(\mathrm{true}),\Omega )$, or $(player,s,a/\neg a/{\mathrm{P}}_{\ge p}(a/\neg a),\Omega )$ and $a/\neg a\in L(s)$; (c) the play iterates infinitely with rule (10); (d) the rule (13) is used for second time.

• (2) The $refuter$ wins the play if and only if one of the following conditions holds: (a) the play ends with rule (0); (b) the play ends with rule 1), and the configuration is $(player,s,\mathrm{false}/{\mathrm{P}}_{\ge p}(\mathrm{false}),\Omega )$, or $(player,s,a/\neg a/{\mathrm{P}}_{\ge p}(a/\neg a),\Omega )$ and $a/\neg a\notin L(s)$; (c) the play infinitely with rule (9); (d) the rule (14) is used for second time.

• (3) Either $verifier$ or $refuter$ cannot win the play, and the play ends with a tie.

With the winning criteria in ${\mathrm{G}}_{{M}^{A}}^{\Phi }$, we can capture the operational semantics for three-valued PCTL* stochastic model checking.

Theorem 4

Let ${M}^{A}$ be a three-valued abstract model (LGIPPN), $\Phi$ a PCTL* formula $\Phi$ in release-PNF and ${s}^{A}\in {S}^{A}$. Then, for $\forall s$: $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}\Phi \right]=true$ if and only if $verifier$ has a winning strategy for game ${G}_{{M}^{A}}^{\Phi }$ with start configuration $(player,{s}^{A},\Phi ,\Omega )$; $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}\Phi \right]=false$ if and only if $refuter$ has a winning strategy for game ${G}_{{M}^{A}}^{\Phi }$ with start configuration $(player,{s}^{A},\Phi ,\Omega )$; $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}\Phi \right]=?$ if and only if either of the players has a winning strategy with start configuration $(player,{s}^{A},\Phi ,\Omega )$. In addition, it is independent of initial player which is $verifier$ or $refuter$.

Proof

The “if” part is obvious, it is sufficient to prove the “only if” part which can be done by constructing the winning strategy of player $verifier$ or $refuter$ for $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}\Phi \right]=\mathrm{true}$ or $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}\Phi \right]=\mathrm{false}$, as for $\left[\left({M}^{A},{s}^{A}\right)\models\Phi \right]=\mathrm{true}$ or $\left[\left({M}^{A},{s}^{A}\right)\models\Phi \right]=\mathrm{false}$ in game for stochastic model checking. So, we just show the result for the truth value “?”.

• (1) $\Phi =\mathrm{true}/\mathrm{false}/a/\neg a/{\mathrm{P}}_{\ge p}(\mathrm{true}/\mathrm{false}/a/\neg a)$: if $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}{\Phi }_{0}\wedge {\Phi }_{1}\right]=?$, every play ends with a tie, and either of them has a winning strategy.

• (2) $\Phi ={\Phi }_{0}\wedge {\Phi }_{1}$: if $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}{\Phi }_{0}\wedge {\Phi }_{1}\right]=?$, then, according to the denotational semantics, $\left[ {\left( {M^{A} ,s^{A} } \right)\;{ \vDash }_{3} \;\Phi _{j} } \right] = ?\;{\text{or}}\;{\text{false}}$ at least for one of $j\in \{\mathrm{0,1}\}$. So, by the induction hypothesis, whatever strategies $verifier$ (or $refuter$) chooses, $refuter$ (or $verifier$) can always choose to proceed to $(player,\;s^{A} ,\;\Phi _{j} ,\;\Omega )$ in which $verifier$ (or $refuter$) has no winning strategy.

• (3) $\Phi ={\Phi }_{0}\vee {\Phi }_{1}$: if $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}{\Phi }_{0}\vee {\Phi }_{1}\right]=?$, according to the denotational semantics, $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}{\Phi }_{j}\right]=?$ at least for one of $j\in \{\mathrm{0,1}\}$, and $\left[ {\left( {M^{A} ,s^{A} } \right){ \vDash }_{3}\: \Phi _{j} } \right] = ?\;{\text{or}}\;{\text{false}}$ for the one $k \in \left\{ {{\text{0}},{\text{1}}} \right\}\;k \ne j$. So, by the induction hypothesis, whatever strategies $verifier$ (or $refuter$) chooses, $refuter$ (or $verifier$) can always choose to proceed to $(player,{s}^{A},{\Phi }_{j},\Omega )$ in which $verifier$ (or $refuter$) has no winning strategy.

• (4) $\Phi ={\mathrm{P}}_{\ge p}(\mathrm{X\Psi })$: if $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}{\mathrm{P}}_{\ge p}(\mathrm{X\Psi })\right]=?$, according to the denotational semantics, the value of ${Pr}_{{s}^{A}}\{\pi \in Path({s}^{A})|\pi \models \mathrm{X\Psi }\}\ge p$ is ? or false, i.e., the value of $\Pr _{{s^{A} }} \{ \pi \in Path\left( {s^{A} } \right)|\pi \vDash {\text{X}}\Psi \} \ge p$ is ? or false, where $P({s}^{A},{s}^{A}\mathrm{^{\prime}})$ is the lowest probability from the place ${s}^{A}$ to ${s}^{A}\mathrm{^{\prime}}$, ${s}^{A}\stackrel{{t}^{A}}{\to }{s}^{A}\mathrm{^{\prime}}$ and $ps^{{A\prime }}$ is the probability of ${s}^{A}\mathrm{^{\prime}}$ satisfying $\Psi$, and the value of $\Pr _{{s^{A} }} \left\{ {\pi \in Path\left( {s^{A} } \right)|\pi { \nvDash }X\Psi } \right\} > 1 - p$ is ? or false, i.e., the value of $\sum P\left( {s^{A} ,s^{{A''}} } \right) \cdot ps^{{A''}} > 1 - p$ is ? or false, where $P({s}^{A},{s}^{A}\mathrm{^{\prime}}\mathrm{^{\prime}})$ is the lowest probability from the place ${s}^{A}$ to ${s}^{A}\mathrm{^{\prime}}\mathrm{^{\prime}}$, $s^{A} \mathop \to \limits^{{t^{{A'}} }} s^{{A''}}$ and $ps^{{A''}}$ is the probability of ${s}^{A}\mathrm{^{\prime}}\mathrm{^{\prime}}$ satisfying $\neg\Psi$. So, by the induction hypothesis, whatever strategies $verifier$ (or $refuter$) chooses, $refuter$ (or $verifier$) can always choose to proceed to $(player,{s}^{A},{\mathrm{P}}_{\ge p}(\mathrm{X\Psi }),\Omega )$ in which $verifier$ (or $refuter$) has no winning strategy.

• (5) $\Phi ={\mathrm{P}}_{\ge p}({\Psi }_{0}\wedge {\Psi }_{1})$: if $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}{\mathrm{P}}_{\ge p}({\Psi }_{0}\wedge {\Psi }_{1})\right]=?$, according to the denotational semantics, the value of ${Pr}_{{s}^{A}}\{\pi \in Path({s}^{A})|\pi \models {\Psi }_{0}\wedge {\Psi }_{1}\}\ge p$ is ? under the lowest probability, and value of ${Pr}_{{s}^{A}}\{\pi \in Path({s}^{A})|\pi \models \mathrm{X\Psi }\}\ge p$ is true or ? under the upperest probability. So, by the induction hypothesis, whatever strategies $verifier$ (or $refuter$) chooses, $refuter$ (or $verifier$) can always choose to proceed to $(player,{s}^{A},{\mathrm{P}}_{\ge p}({\Psi }_{0}\wedge {\Psi }_{1}),\Omega )$ in which $verifier$ (or $refuter$) has no winning strategy.

• (6) $\Phi ={\mathrm{P}}_{\ge p}({\Psi }_{0}\vee {\Psi }_{1})$: if $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}{\mathrm{P}}_{\ge p}({\Psi }_{0}\vee {\Psi }_{1})\right]=?$, according to the denotational semantics, the value of ${Pr}_{{s}^{A}}\{\pi \in Path({s}^{A})|\pi \models {\Psi }_{0}\vee {\Psi }_{1}\}\ge p$ is ? under the lowest probability, and value of ${Pr}_{{s}^{A}}\{\pi \in Path({s}^{A})|\pi \models \mathrm{X\Psi }\}\ge p$ is true or ? under the upperest probability. So, by the induction hypothesis, whatever strategies $verifier$ (or $refuter$) chooses, $refuter$ (or $verifier$) can always choose to proceed to $(player,{s}^{A},{\mathrm{P}}_{\ge p}({\Psi }_{0}\vee {\Psi }_{1}),\Omega )$ in which $verifier$ (or $refuter$) has no winning strategy.

• (7) $\Phi = {\text{P}}_{{ \ge p}} (\Psi _{0} \;{\text{U}}\;\Psi _{1} )$: if $\left[\left({M}^{A},{s}^{A}\right){\models }_{3}{\mathrm{P}}_{\ge p}({\Psi }_{0}\mathrm{U}{\Psi }_{1})\right]=?$, according to the denotational semantics, the value of $Pr_{{s^{A} }} \{ \pi \in Path\;(s^{A} )|\pi { \vDash }\;\Psi _{0} \;{\text{U}}\;\Psi _{1} \} \ge p$ is ? under the lowest probability, and value of $Pr_{{s^{A} }} \{ \pi \in Path\;(s^{A} )|\pi { \vDash }\;{\text{X}}\;\Psi \} \ge p$ is true or ? under the upperest probability. So, by the induction hypothesis, whatever strategies $verifier$ (or $refuter$) chooses, $refuter$ (or $verifier$) can always choose to proceed to $(player,s^{A} ,{\text{P}}_{{ \ge p}} (\Psi _{0} {\text{U}}\;\Psi _{1} ),\Omega )$ in which $verifier$ (or $refuter$) has no winning strategy.

• (8) $\Phi = {\text{P}}_{{ \ge p}} (\Psi _{1} \;{\text{R}}\;\Psi _{2} )$: if $\left[ {\left( {M^{A} ,s^{A} } \right){ \vDash }_{3} \;{\text{P}}_{{ \ge p}} (\Psi _{0} \;{\text{R}}\;\Psi _{1} )} \right] = ?$, according to the denotational semantics, the value of $Pr_{{s^{A} }} \{ \pi \in Path\;(s^{A} )|\pi \;{ \vDash }\;\Psi _{0} \;{\text{R}}\;\Psi _{1} \} \ge p$ is ? under the lowest probability, and value of $Pr_{{s^{A} }} \{ \pi \in Path\;(s^{A} )|\pi \;{ \vDash }\;\Psi _{0} {\text{R}}\;\Psi _{1} \} \ge p$ is true or ? under the upperest probability. So, by the induction hypothesis, whatever strategies $verifier$ (or $refuter$) chooses, $refuter$ (or $verifier$) can always choose to proceed to $(player,s^{A} ,{\text{P}}_{{ \ge p}} (\Psi _{0} {\text{R}}\;\Psi _{1} ),\;\Omega )$ in which $verifier$ (or $refuter$) has no winning strategy.

The Theorem 4 states three-valued PCTL* stochastic model checking is equivalent to two-player stochastic game ${\mathrm{G}}_{{M}^{A}}^{\Phi }(player, board, rule)$. If the player $verifier$ has a winning strategy from the initial place ${s}_{init}^{A}$ of ${M}^{A}$, then ${M}^{A}$ satisfies $\Phi$, i.e., ${M}^{A}{\models }_{3}\Phi$, and the winning strategy can be served as the evidence for ${M}^{A}{\models }_{3}\Phi$. If the player $refuter$ has a winning strategy from the initial place ${s}_{init}^{A}$ of ${M}^{A}$, then ${M}^{A}$ does not satisfy $\Phi$, i.e., $M^{A} { \nvDash }_{3} \Phi$, and the winning strategy can be served as the evidence for $M^{A} { \nvDash }_{3} \Phi$, i.e., the counterexample. If either of them has the winning strategy, then the result is indefinite, which means the abstract model should be refined.

6.2 Strategy solving in three-valued stochastic game

A two-player game process ${G}_{{M}^{A}}^{\Phi }$ for three-valued PCTL* stochastic model checking can be presented by the game-graph $Gg(N,E, w)$. It can be constructed from initial configuration as the initial node in a BFS (breadth first search) or DFS (depth first search) manner, and owns the same characteristics (Liu et al. 2016): game-graph can be partitioned into some MSCCs (maximal strongly connected components), and every play never leaves a ${\mathrm{MSCC}}_{m}$ into a ${\mathrm{MSCC}}_{n}$ with $m<n$.

The game ${G}_{{M}^{A}}^{\Phi }$ for three-valued PCTL* stochastic model checking is a three-valued stochastic game, essentially. We implement a three-valued coloring method for strategy solving, which can alter the coloring process (Liu et al. 2016; Shoham and Grumberg 2007) of traditional PCTL* stochastic model checking game and CTL model checking game. It colors each node in the MSCCs of game-graph $Gg(N,E, w)$, and processes ${\mathrm{MSCC}}_{i}$ according to i bottom-up. Let ${\mathrm{MSCC}}_{i}$ be the smallest MSCC at present, i.e., the other ${\mathrm{MSCC}}_{m}$ with $m<i$ have all been colored, the three-valued coloring rules of a node in ${\mathrm{MSCC}}_{i}$ is as follows: for a node with a current $\Phi ^{\prime }$ of sub-formula $\Phi$, (1) if player $verifier$ can win for current $\Phi ^{\prime }$, the corresponding node is colored white; (2) if player $refuter$ can win for current $\Phi ^{\prime }$, the corresponding node is colored black; (3) if either of the players can win for current $\Phi ^{\prime }$, the corresponding node is colored gray.

We color all the nodes of the game-graph $Gg(N,E, w)$ according to the coloring rules. If the initial node is colored white, player $verifier$ wins the game, and all the white nodes compose the winning strategy of $verifier$. This means ${M}^{A}{\models }_{3}\Phi$ according to Theorem 4, and $M\models\Phi$ according to Theorem 3. If the initial node is colored black, player $refuter$ wins the game, and all the black nodes compose the winning strategy of $refuter$. This means $M^{A} { \nvDash }_{3} \Phi$ according to Theorem 4, and $M{ \nvDash }\Phi$ according to Theorem 3. If the initial node is colored gray, either of players wins the game. This means the result of three-valued PCTL* stochastic model checking ${M}^{A}$ is indefinite, according to Theorem 4; and the result of PCTL* stochastic model checking $M$ is also indefinite, according to Theorem 3. The gray nodes need to be refined, which is presented in Sect. 6.

Strategy solving algorithm for three-valued PCTL* stochastic model checking game can be summarized into three steps: (1) construct the game-graph $Gg(N,E, w)$ for ${M}^{A}$ and $\Phi$; (2) find the MSCCs and sort them bottom-up, (3) three-valued color the nodes of game-graph with the MSCCs’ order, according to the three-valued coloring rules; (4) determine the color of the initial node and return the corresponding winning strategy in DFS manner. It is the combination of searching MSCCs with order algorithm and three-valued coloring process, and the complexity of which is PSPACE. It can be proved similarly with stochastic model checking game (Liu et al. 2016; Kwiatkowska et al. 2021; Shoham and Grumberg 2007).

The winning strategy of $verifier$ or $refuter$ is the evidence whether PCTL* $\Phi$ is satisfied or not, respectively. An evidence of $refuter$, i.e., the black nodes of the three-valued colored game-graph, can be served as a kind of counterexample. It should be noted that the ideal counterexample(Abraham et al. 2014) just contains the smallest set of necessary nodes from the winning strategy of $refuter$.

7 Refinement

If the three-valued stochastic model checking returns an indefinite result, i.e., “?”, it means the abstract place is so coarse that we can say nothing from it and have to refine the abstract place. Roughly, refining an invalid abstract place is to split it into the smaller abstract places until the three-valued stochastic model checking result is definite on it. We can exploit information of the colored three-valued game-graph in refinement process.

7.1 Identifying and analyzing failure nodes

Definition 10

Failure node. A node in colored three-valued game-graph is the failure node, if it is colored gray, and none of its sons was colored gray when it is colored.

Intuitively speaking, a failure node is responsible for the loss of information in abstraction. Thus, it should be refined. If the initial node is colored gray, a failure node can be found by the identifying failure nodes algorithm. For each node, it is colored gray and is not a failure node, the coloring algorithm is adapted to remember that a son was colored gray when n is colored, denoted as go(n). Identifying failure nodes algorithm in Fig. 4 can identify the failure node from go(n), which starts from the initial node.

Fig. 4

Identifying failure nodes algorithm

Theorem 5

The identifying failure nodes algorithm can terminate.

Proof

If the current node n is not a failure node, the algorithm continues to identify at go(n). According to Definition 10 (failure node), there is a node that was colored gray before n. Thus, each recursive call is applied on the node colored gray earlier. So, the number of recursive calls is not bigger than the run time of the coloring algorithm that is finite.□

Failure nodes identifying (FNIdentify) algorithm is a DFS-like greedy algorithm. It proceeds from node to node of colored three-valued game-graph recursively, until it finds a failure node. Moreover, the failure node fulfils Theorem 6.

Identifying failure nodes algorithm is a recursive algorithm, which needs a recursive stack, so its space complexity is $\mathcal{O}(|S|)$. It takes time complexity $\mathcal{O}(|S|)$ to find the adjacent points of each node in the adjacency matrix. To get the whole matrix, the total time complexity is $\mathcal{O}({|S|}^{2})$, where $|S|$ is the number of nodes.

Theorem 6

A failure node returned by Identifying failure nodes algorithm is one of the following: (1) the terminal node $(verifier,{s}^{A}, a/{P}_{\ge p}(a))$ colored gray, where $a\in AP$; (2) the node in form of $(verifier,{s}^{A},{P}_{\ge p}(X\Psi ),\Omega )$ colored gray, where $\sum P (s^{A} ,s^{{A\prime }} ) \cdot {\text{ps}}^{{{\text{A}}\prime }} > 1 - {\text{p}}$, $P(s^{A} ,s^{{A\prime }} )$ is the upper probability from the place ${s}^{A}$ to $s^{{A\prime }}$, $s^{A} \mathop \to \limits^{{t^{A} }} s^{{A\prime }}$ and $ps^{{A\prime }}$ is the probability of $s^{{A\prime }}$ satisfying $\neg \Psi$.

Proof

According to coloring algorithm, $\Phi$ is ${\Phi }_{0}\wedge {\Phi }_{1}$, ${\Phi }_{0}\vee {\Phi }_{1}$, ${\mathrm{P}}_{\ge p}({\Psi }_{0}\wedge {\Psi }_{1})$, or ${\mathrm{P}}_{\ge p}({\Psi }_{0}\vee {\Psi }_{1})$, the node of which is colored gray only if it has at least one son that is colored gray. Thus, these nodes do not satisfy Definition 10 (failure node). For ${\text{P}}_{{ \ge p}} (\Psi _{1} {\text{U}}\;\Psi _{2} )$ or ${\mathrm{P}}_{\ge p}({\Psi }_{1}\;\mathrm{R}{\Psi }_{2})$, the node of which is colored gray depends on the witness of operator $\wedge$, $\vee$ or $\mathrm{X}$, so, it also does not satisfy Definition (failure node). If the node is a terminal node, it has to be $(verifier,{s}^{A}, a/{\mathrm{P}}_{\ge p}(a))$, since $(verifier,{s}^{A}, \mathrm{true}/\mathrm{false}/{\mathrm{P}}_{\ge p}(\mathrm{true})/{\mathrm{P}}_{\ge p}(\mathrm{false}))$ is colored by black or white, definitely. If the node is the form of $(verifier,{s}^{A},{\mathrm{P}}_{\ge p}(\mathrm{X\Psi }),\Omega )$, the value of $\sum P (s^{A} ,s^{{A\prime }} ) \cdot ps^{{A\prime }} > 1 - {\text{p}}$ has to be true, where $P({s}^{A},{s}^{A}\mathrm{^{\prime}})$ is the upper probability from the place ${s}^{A}$ to ${s}^{A}\mathrm{^{\prime}}$, ${s}^{A}\stackrel{{t}^{A}}{\to }{s}^{A}\mathrm{^{\prime}}$ and $ps^{{A\prime }}$ is the probability of $s^{{A\prime }}$ satisfying $\neg\Psi$. Otherwise, it will be colored by black.□

7.2 Refining failure nodes

For returning the definite result of three-valued stochastic model checking, it is enough to refine the failure node not all the indefinite nodes. The type of failure node in Theorem 6 provides the criteria for the refinement.

• (1) The failure node is a terminal node $(verifier,{s}^{A}, a/{\mathrm{P}}_{\ge p}(a))$. The reason for its gray color is the fact that one or some concrete places abstracted by ${s}^{A}$ are labeled $a$, meanwhile one or some concrete places abstracted by ${s}^{A}$ are labeled $\neg a$. In order to avoid the indefinite result returned at ${s}^{A}$, ${s}^{A}$ is refined by two abstract places ${s}^{A1}$ and ${s}^{A2}$, where the concrete place set ${FP}_{t}$ abstracted by ${s}^{A1}$ are labeled $a$ and the concrete place set ${FP}_{f}$ abstracted by ${s}^{A2}$ are labeled $\neg a$.

• (2) The failure node is the form of $(verifier,{s}^{A},{\mathrm{P}}_{\ge p}(\mathrm{X\Psi }),\Omega )$, where $\sum P (s^{A} ,s^{{A\prime }} ) \cdot ps^{{A\prime }} > 1 - {\text{p}}$, $P({s}^{A},{s}^{A}\mathrm{^{\prime}})$ is the upper probability from the place ${s}^{A}$ to ${s}^{A}\mathrm{^{\prime}}$, ${s}^{A}\stackrel{{t}^{A}}{\to }{s}^{A}\mathrm{^{\prime}}$ and $ps^{{A\prime }}$ is the probability of ${s}^{A}\mathrm{^{\prime}}$ satisfying $\neg\Psi$. In order to avoid the indefinite result returned at ${s}^{A}$, ${s}^{A}$ is refined by two abstract places ${s}^{A1}$ and ${s}^{A2}$, where the concrete place set ${FP}_{t}$ abstracted by ${s}^{A1}$ refute ${\mathrm{P}}_{\ge p}(\mathrm{X\Psi })$ definitely and the concrete place set ${FP}_{f}$ abstracted by ${s}^{A2}={s}^{A}\backslash {s}^{A1}$.

From the above analysis, it can be seen that the key for refining failure nodes is to split the abstract places in a way that eliminates the failure cause. Actually, a place is a family of valuations for all variables in V. We use$s^{A} _{{ \to v}}$ to denote the valuation of a place ${s}^{A}$ for the variable$v$. Given an abstract place in the failure node, they cannot be distinguished in the abstract model with the visible variables. Formally, $\forall v\in {V}_{{S}^{A}}$, $s^{{A1}} _{{ \to v}} = s^{{A2}} _{{ \to v}}$, but ${s}^{A1}$ and ${s}^{A2}$ should be distinguished in the refinement model. This is a state separation problem (SSP), and the minimal state separation problem (MSSP) is the NP-hard problem (Clarke et al. 2002). Moreover, the place at a failure node may abstract many concrete places, especially for large concrete model, which makes time complexity of refining is high. For dealing with this, we take the approximate solution of SSP as a tradeoff between the precision and time complexity. We infer the separation set on sample place set selected by sample learning (He et al. 2016, 2010; Clarke et al. 2002), instead of the entire concrete place set abstracted by the failure node, then, we use BPSO (binary particle swarm optimization) algorithm to solve the separation set for refinement.

7.2.1 Formalizing refinement as the MSSP

The place ${s}^{A}$ at a failure node is denoted as a vector of length $n$ with $s^{A} \left[ i \right] = s^{A} _{{ \to v}}$, where $v$ is the $i$ th invisible variable in ${V}_{N}$. ${s}^{A}$ cannot be separated by any present visible variable, so, we only consider its invisible variables. For simplicity, we use ${p}_{j}$ to denote a pair of places in ${FP}_{t}\times {FP}_{f}$, i.e., ${FP}_{t}\times {FP}_{f}=\{{p}_{1},{p}_{2},\dots ,{p}_{m}\}$, $1\le j\le m$. Assume $p_{j} = < (s)^{{p_{j} }} ,(s^{\prime } )^{{p_{j} }} >$, ${p}_{j}$ can be separated by certain variable in the separation set $\Lambda$, i.e., $\exists {v}_{i}\in\Lambda$, $(s)^{{p_{j} }} \left[ i \right] \ne (s^{\prime } )^{{p_{j} }} [i]$, where ${(s)}^{{p}_{j}}=<{(s)}^{{p}_{j}}\left[1\right],{(s)}^{{p}_{j}}\left[2\right],\dots ,{(s)}^{{p}_{j}}[n]>$ and $({{s}^{^{\prime}})}^{{p}_{j}}=<({{s}^{^{\prime}})}^{{p}_{j}}\left[1\right], ({{s}^{^{\prime}})}^{{p}_{j}}\left[2\right], \dots , ({{s}^{^{\prime}})}^{{p}_{j}}[n]>$. If ${v}_{i}\in\Lambda$, we define the decision variable ${x}_{i}=1$, else ${x}_{i}=0$, which is equivalent to $\sum_{i=1}^{n}({(s)}^{{p}_{j}}\left[i\right]\oplus {{(s}^{^{\prime}})}^{{p}_{j}}\left[i\right])\bullet {x}_{i}$, where $\oplus$ is the exclusive or operator, ${x}_{i}$ is the decision variable of ${v}_{i}$. Let $A={\{{a}_{ij}\}}_{m\times n}$ be a coefficient matrix where ${a}_{ij}={(s)}^{{p}_{j}}\left[i\right]\oplus {{(s}^{^{\prime}})}^{{p}_{j}}\left[i\right]$, $1\le i\le n, 1\le j\le m$. ${a}_{ij}=1$ iff the state pair ${p}_{j}$ is separated by the variable ${v}_{i}$. The refinement is the MSSP with $n$ invisible variables and $m$ state pairs: $min\sum_{i=1}^{n}{x}_{i}$, where $\sum_{i=1}^{n}{a}_{ij}{x}_{i}\ge 1, j=1,\dots ,m; {x}_{i}=\left\{\mathrm{0,1}\right\}, i=1,\dots ,n.$

7.2.2 Sample learning

We adopt sample learning (Clarke et al. 2002) algorithm to get the smaller place set ${S}_{{FP}_{t}}$ and ${S}_{{FP}_{f}}$ from ${S}_{{FP}_{t}}$ and ${S}_{{FP}_{f}}$, respectively, where ${S}_{{FP}_{t}}\subseteq {FP}_{t}$ and ${S}_{{FP}_{f}}\subseteq {FP}_{f}$. Then, the minimal separation set is computed on ${S}_{{FP}_{t}}$ and ${S}_{{FP}_{f}}$, which equals to be computed on ${FP}_{t}$ and ${FP}_{f}$. In the process of selecting the sample, places that contain more information will be selected, instead of random selecting places.

The iterative sample learning algorithm is shown in Fig. 5. MAXSAM denotes the maximal number of samples picked in the iteration. At each iteration, MAXSAM samples are selected from ${FP}_{t}\times {FP}_{f}$ which cannot be separated by the present separation set. Then separation set is computed, and ${FP}_{t}\times {FP}_{f}$ is updated, until ${FP}_{t}\times {FP}_{f}=\mathrm{\varnothing }$.

Fig. 5

Sample learning algorithm

According to the formula $\sum_{i=1}^{n}({s)}^{{p}_{j}}\left[i\right]\oplus {{(s}^{^{\prime}})}^{{p}_{j}}\left[i\right])\bullet {x}_{i}$, if $\sum_{i=1}^{n}{a}_{ij}{x}_{i}\ge 1$, i.e., ${A}_{j}{x}_{i}\ge 1$, the place pair ${p}_{j}$ can be separated. The effective approach of checking the validity of samples is based on $\sum_{i=1}^{n}{a}_{ij}{x}_{i}\ge 1$. This is easy to be performed and can always be accomplished in a constant time. Note that the order of selecting the sample is also important. In each iteration process, if there are not place pairs separated by the existing separation set, it will be selected, as can be separated by less variables in a greater probability as a sample. The sample learning algorithm is a recursive process, and its time complexity is $\mathcal{O}\left(\left|{FP}_{t}\times {FP}_{f}\right|*MAXSAM\right).$

7.2.3 BPSO algorithm

PSO (Particle swarm optimization) algorithm (Kennedy and Eberhart 1995; Wang et al. 2020) is a kind of EA (evolutionary algorithm), which originally was put forward by Eberhart and Kennedy in 1995. PSO algorithm is modified in binary form to obtain the invisible variables which should be visible in the refined model.

• (1) Objective function

The MSSP problem that we are solving is a constraint optimization problem, which can be described as: $min\sum_{i=1}^{n}{x}_{i}$, where $\sum_{i=1}^{n}{a}_{ij}{x}_{i}\ge 1,\; j=1,\dots ,m;\;{x}_{i}=\left\{\mathrm{0,1}\right\},\; i=1,\dots ,n.$

The particle in PSO algorithm has a strong ability to search generally at the first time, then it has to convergence. We adopt a non-stationary multi-stage assignment penalty to gain more accurate results and improve the convergence. The penalty factor is modified dynamically, according to the constraint function. Then, the optimization problem turns into:

$${\text{Minimize}}\mathop \sum \limits_{i = 1}^{n} x_{i} + h\left( k \right)\mathop \sum \limits_{j = 1}^{m} f\left( {\mathop \sum \limits_{i = 1}^{n} a_{ij} x_{i} \ge 1} \right)$$

(1)

where $h(k)$ is a penalty factor, the value of which is $\mathrm{sup}(\sqrt{k})$, k is the current iteration, $f(\bullet )$ is a penalty function which has a strong influence on the performance of the algorithm. A simple and efficient penalty function is employed as follows: $f\left( x \right) = \left\{ {\begin{array}{*{20}l} {0,} \hfill & {if\;x\;is\;true} \hfill \\ {BIGVALUE,} \hfill & {otherwise} \hfill \\ \end{array} } \right.$.

• (2) Probabilistic initialization of particles

We use a n-bit vector $\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\rightharpoonup}$}}{{xx}}$ as a particle, i.e., $\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\rightharpoonup}$}}{{xx}} = \left( {v_{1} ,v_{2} , \ldots ,v_{n} } \right)$, where n is the number of invisible variables. If the value of the $i$ th bit is 1, the variable ${v}_{i}$ is selected into the separation set. The number of populations is Pop-size. We generate particles randomly in order to get wide guidance particles. The initialization process of particles is shown in Fig. 6.

• (3) Velocity and position evolution

Fig. 6

Initializing a particle

The update formulae of velocity and position in the classical PSO algorithm is not suitable for discrete constraint optimization problem, we need to reconstruct the formulae. We adopt the method proposed in Nguyen et al. (2021) with some modifications to update the velocity and position of a particle, which is named as BPSO (binary particle swarm optimization algorithm).

Two vectors for each particle are introduced as ${\overrightarrow{V}}_{i}^{0}$ and ${\overrightarrow{V}}_{i}^{1}$.${\overrightarrow{V}}_{i}^{0}$ is the probability of the bits of the $i$ th particle to change to zero, while ${\overrightarrow{V}}_{i}^{1}$ is the probability that bits of the $i$ th particle to change to one. Since the inertia term is used in the process of update equation, these velocities are not complementing. Then, we give the definition of the probability of change in the $j$ th bit of the $i$ th particle:

$$V_{{ij}}^{c} = \left\{ {\begin{array}{*{20}c} {V_{{ij}}^{1} \;if\;xx_{{ij}} = 0} \\ {V_{{ij}}^{0} \;if\;xx_{{ij}} = 1} \\ \end{array} } \right.$$

(2)

Assume that the $j$ th bit of the $i$ th best particle is one. The velocity of particle is calculated in this way. The $j$ th bit of the $i$ th particle is guided to its best position. The velocity of change to one (${\overrightarrow{V}}_{ij}^{1}$) for that particle increase and the velocity of change to zero (${\overrightarrow{V}}_{ij}^{0}$) is decreased. We get the following rules: (1) $If\;p_{{ibest}}^{j} = 1\;then\;d_{{ij,1}}^{1} = c_{1} r_{1} \;and\;d_{{ij,1}}^{0} = - c_{1} r_{1}$, (2) $If\; {p}_{ibest}^{j}=0\; then\; {d}_{ij, 1}^{0}={c}_{1}{r}_{1}\; and\; {d}_{ij, 1}^{1}=-{c}_{1}{r}_{1}$, (3) $If\; {p}_{gbest}^{j}=1\; then\; {d}_{ij, 2}^{1}={c}_{2}{r}_{2}\; and\; {d}_{ij, 2}^{0}=-{c}_{2}{r}_{2}$, (4) $If\; {p}_{gbest}^{j}=0\; then\; {d}_{ij, 2}^{0}={c}_{2}{r}_{2}\; and\; {d}_{ij, 2}^{1}=-{c}_{2}{r}_{2}$, where ${d}_{ij}^{1}$, ${d}_{ij}^{0}$ are two temporary values, ${r}_{1}$ and $r_{2}$. are two random variable in the range of (0,1) which are updated at each iteration, $c_{1}$ and $c_{2}$ are two fixed constants which are determined by user. Then: $V_{ij}^{1} \left( {t + 1} \right) = wV_{ij}^{1} \left( t \right) + d_{{ij,{ }1}}^{1} + d_{{ij,{ }2}}^{1}$, $V_{ij}^{0} \left( {t + 1} \right) = wV_{ij}^{0} \left( t \right) + d_{{ij,{ }1}}^{0} + d_{{ij,{ }2}}^{0}$, where $w$ is the inertia term.

Due to the velocities of the particles must be restricted within the range between 0 and 1 (Nguyen et al. 2017) the normalization function used here is a sigmoid function: $vel_{ij}^{^{\prime}} = sig\left( {vel_{ij} } \right) = \frac{1}{{1 + e^{{ - vel_{ij} }} }}$. So, the new position of the particle is obtained with the below equation:

$$xx_{{ij}} \left( {t + 1} \right) = \left\{ {\begin{array}{*{20}c} {\overline{{xx}} _{{ij}} \left( t \right),~~~if~r_{{ij}} < Vel_{{ij}}^{{\text{'}}} } \\ {xx_{{ij}} \left( t \right),~~~otherwise} \\ \end{array} } \right.$$

(3)

where $\overline{xx}_{ij}$ is the 2’s complement of $xx_{ij}$. i.e., if $xx_{ij} = 0$, then $\overline{xx}_{ij} = 1$; if ${ }xx_{ij} = 1$, then $\overline{xx}_{ij} = 0$.${ }r_{ij}$ is a uniform random number between 0 and 1. The value is proportional to the number of place pairs it separated. The BPSO algorithm shown in Fig. 7.

Fig. 7

BPSO algorithm

The time complexity of BPSO algorithm is linear with the number of iterations m and dimension n, its time complexity is ${\mathcal{O}}\left( {m*n} \right)$.

7.3 Incremental refinement

We refine the abstract model via splitting its places belong to failure node. There is no reason to split places for which the three-valued stochastic model checking results are definite. Although, the refinement process is decided locally, it has a global effect, since the refinement leads to the change of whole abstract model. The results of game-based three-valued stochastic model checking provide the valuable information for avoiding unnecessary refinement. At the end of the ith iteration of three-valued abstraction-refinement, the nodes that were colored gray are remembered. During the construction of a new refined three-valued game-graph in the (i + 1)th iteration, we prune the game-graph according to the remembered information. As a result of this, only the places of gray nodes are refined. The iterative abstraction-refinement process give rise to an incremental three-valued abstraction-based stochastic model checking framework. Moreover, the termination of the abstraction-refinement is given by the following theorem.

Theorem 7

For a finite concrete LNPPN model, the iterative three-valued abstraction-refinement process can guarantee to terminate with a definite result.

Proof

The refinement is done by means of splitting the indefinite places, which leads to a refined abstract LGIPPN model. So, every place $s_{r}^{A}$ in the refined model has some corresponding super-place $s_{s}^{A}$ in the less refined model, in the sense that the set of concrete places that $s_{r}^{A}$ abstracts is a subset of those abstracted by $s_{s}^{A}$. Moreover, there is at least one abstract place is splited in the refinement, which ensures that at least one of the refined places abstracts strictly fewer concrete places than its super-place. Thus, the number of concrete places is the bound of iterations of abstraction-refinement. Therefore, the abstraction-refinement process is guaranteed to terminate if the place space is finite, and when there are not the indefinite places which leads to the indefinite result.□

The termination of the three-valued abstraction-refinement process means the three-valued abstraction-based PCTL* stochastic model checking returns a definite result.

8 Case study

8.1 Experiments

Based on our open-source model checker PAT(Liu et al. 2011; Liu 2019), we implement three-valued abstraction-refinement framework in a prototype tool TVAR (three-valued abstraction-refinement), as shown in Fig. 8. It is developed in Java language with explicit-state data structures (sparse matrices, bit-sets, etc.). A symbolic (MTBDD-based) implementation of TVAR with implicit-state data structures (MTBDD), is being developed to offer more scalability on models with regularity. It will be released as the open-source software at PAT website (http://pat.comp.nus.edu.sg).

Fig. 8

Prototype tool TVAR

In order to demonstrate the feasibility and efficiency of three-valued abstraction-refinement framework in this paper, we compare it with the current approximate abstraction techniques of stochastic model checking (game-based abstraction and probabilistic CEGAR). The cases are the popular protocol algorithms in software-driven autonomous systems, and belong to the PRISM Benchmark Suite. All experiments are run on a PC with CPU Intel Core i7-3632QM (2.20 GHz) and RAM 8.00 GB.

The first case is the IPv4 Zeroconf protocol, which is a dynamic IP addresses configuration protocol for some software-driven autonomous systems connecting the network(Ejaz et al. 2019). It is a distributed "plug-and-play" manner for IP address configuration, which is automatically executed when an autonomous system is connected to the network. The process of IP addresses configuration is as follows: (1) When an autonomous system is being connected to the network, it firstly chooses a random IP address from the 65,024 available addresses (from 169.254.1.0 to 169.254.254.255) which are allocated by the Internet Assigned Number Authority for the purpose of such link-local networks. (2) Then the autonomous system will send messages to the other autonomous systems that have been connected to the network, and ask whether any of them are currently using the chosen IP address. (3) If no reply is received by the system, even after such messages were resent three more times, it starts to use the chosen IP address, and sends two more messages to claim that the IP address is occupied. (4) If the chosen IP address is being used, which will be replied by the corresponding system, the configuration process will return to 1) and the new system will choose another random IP address. Note that it sends the message repeatedly to avoid the message loss in the network. This IP address configuration process is both probabilistic and timed. Probability is used to characterize the random in initial selection of an IP address, or the message loss. Whereas, timing aspect is used to define the time periods that elapse between repeated retransmissions of the same message. In this case, the model to be verified is Zeroconf network configuration protocol for configured hosts K and IP addresses J, the property to be verified is minimum probability that the host configures successfully.

The second case is the IEEE 802.11 WLAN (Wireless Local Area Networks) protocol for network composed with the autonomous systems, which is used for a limited geographical area, e.g., stations, homes, offices, campuses(Chi and Chen 2019). The international standard IEEE 802.11 is developed for the interoperability of heterogeneous communication devices of autonomous systems in WLAN. It is part of the IEEE 802 technical standards, and specifies the set of MAC (Media Access Control) and PHY (Physical Layer) protocols for implementing wireless devices communication of autonomous systems. It is not the same as wired devices, the stations of a WLAN cannot employ medium access control schemes, e.g., CSMA/CD (Carrier Sense Multiple Access with Collision Detection), to prevent simultaneous transmission on the channel, as they are unable to listen to their own transmission. IEEE 802.11 standard describes a CSMA/CA (Carrier Sense Multiple Access with Collision Avoidance) mechanism, which uses a randomized exponential backoff rule to minimize the likelihood of transmission collision. In this case, the model to be verified is IEEE 802.11 WLAN protocols with a backoff counter maximum of bc and a maximum packet send time of 500 μs, and the property to be analyzed is the minimum probability that a station’s backoff counter reaches bc.

The third case is the IEEE 802.3 CSMA/CD (Carrier Sense, Multiple Access with Collision Detection) protocol for autonomous systems network, which is also part of the IEEE 802 technical standards (Dey et al. 2020). It is designed for networks with a single channel and specifies the behaviors of stations with the aim of minimizing simultaneous use of the channel (data collision). The basic structure of the protocol is as follows: (1) When a station tries to send data, it will listen to the medium; (2) If the medium was free (no one transmitting), the station starts to send its data; (3) If the medium is busy, the station waits a random amount of time and then repeats this process. In this case, the model to be verified is IEEE 802.3 CSMA/CD protocols with a backoff counter maximum of bc and a maximum packet send time of 500 μs, the property to be analyzed is minimum probability that a station’s backoff counter reaches bc.

The experimental results are shown in Tables 2 and 3. The “actual value” columns in Tables 2 and 3 are the exact probability value obtained by monolithic stochastic model checking tool PRISM. The model statistics are shown in Tables 4 and 5. We will compare them further and analyse the reasons for them in the next section.

Table 2 Minimum probability that the new host eventually succeeds in selecting a fresh IP address

Table 3 Minimum probability that a station’s backoff counter reaches bc

Table 4 Model statistics (places, transitions)

Table 5 Model statistics (places, transitions)

8.2 Analysis

The experimental results are very encouraging. In 14 cases of Tables 2 and 3, three-valued abstraction of this paper and game-based abstraction successfully generate tighter results than Probabilistic CEGAR. The three-valued abstraction framework gets the tightest results of them. The upper bounds produced by our framework is in coincidence with the actual value, and yields the exact values in some cases (for instance, IPv4 Zeroconf protocol with parameters J = 32, K = 4; J = 32, K = 5; and J = 64, K = 4). The reasons for this are that in three-valued abstraction and game-based abstraction, the additional nondeterministic behaviors of player 1 place are kept, and the transitions are equipped with interval in three-valued abstraction. In order to present the significance of our framework on the lower bound and upper bound, we make the statistical tests, as shown in Figs. 9 and 10. It can be seen that LNPPN, LGPPN and LGIPPN get very similar results in solving their upper bound probability for IPv4 Zeroconf protocol. The results of LGPPN and LGIPPN are better than LNPPN in solving the lower bound probability. For WLAN and CSMA protocols, the compactness of the solutions by LGIPPN, LGPPN and LNPPN decreases in turn. The reasons for which are the nondeterminism modeled by LGPPN can be closer to the real probability value than LNPPN as an abstract model, and LGIPPN introduces a third kind of nondeterministic interval value, which preserves more information of transition probability and can simultaneously approximate the upper bound and lower bound.

Fig. 9

Comparison of lower bound

Fig. 10

Comparison of upper bound

The state space of abstract model LGIPPN in our framework is significantly reduced, compared with LNPPN and LGPPN. The state space of concrete model for 14 cases is shown in Fig. 11, and the state space of abstract model is compared in Fig. 12. The abscissa represents 14 cases, and the ordinate represents the size of state space in bytes. Figure 12 shows that the abstract state space of our framework is smaller than probabilistic CEGAR or game-based abstraction, and the state space of probabilistic CEGAR and game-based abstraction are almost the same. This is because: (1) the places and transitions of abstract model is constructed by nearly the same method in all abstraction techniques, but in three-valued abstraction, the transitions are equipped by interval; (2) the dependent relation of variables is very strong, or the domain of some a variable is too big. It hides all logical relation which is defined on these variables. When some invisible variables are made visible in the refinement, the corresponding predicates variables are added, which may also lead to search more place space. It can be concluded that different transition methods have great influence on the state space.

Fig. 11

State space of concrete model

Fig. 12

State space of abstract model

We also compare the time efficiency of our framework with others. As shown in Fig. 13, we compare our framework with probabilistic CEGAR (LNPPN), game-base abstraction (LGPPN), and our framework without sample learning + BPSO. The run time (in seconds) contains the time spent on all stages, including abstract model construction, model checking abstract model and refinement. The run time of three-valued abstraction in this paper is distinctly less than probabilistic CEGAR and game-based abstraction, because the refinement in it is accelerated by sample learning and BPSO algorithm. When our framework integrates the sample learning + BPSO, it takes obvious less time, which makes the advantage of time consumption more apparent. BPSO has a trade-off between the solution precision and cost, which gives a suboptimal but sufficiently good set separation and makes refinement iterations less. It plays an important role to reduce the running time of LGIPPN. Moreover, the bigger of concrete model, the more preponderance of three-valued abstraction emerges. But, if the three-valued abstraction do not use the sample learning and BPSO algorithm for refining, it will be the worst among the abstraction techniques. Because refining the transitions with interval and places of player 1 in iteration is very time-consuming. The run time of probabilistic CEGAR is less than game-based abstraction, because refining the places of player 1 in iteration is very time-consuming.

Fig. 13

Run time

9 Conclusion

In this paper, we focus on approximate model abstraction techniques for dealing with state space explosion problem in stochastic model checking. We propose the first three-valued abstraction-refinement framework for stochastic model checking, which is also the first abstraction framework for preserving full PCTL* properties. We present a good balance between the state space and preserved properties of abstract model. The key components of the framework are a new abstract model which orthogonally integrates interval probability of transition and game for nondeterminism, and the refinement process which combines sample learning and BPSO algorithm. Some popular protocols in software-drived autonomous systems are used to demonstrate the efficiency of the framework, which are the best among the current approximate model abstraction techniques. This framework takes LNPPN as the concrete model, but it is applicable to other formal system models as well, such as probabilistic automaton and MDP. However, this framework can just abstract the autonomous system with discrete time stochastic behaviors, and just can be applied at the level of system model. In the future work, we will (1) generalize the three-valued abstraction framework to software-driven autonomous system in continuous time style or hybrid system, (2) generate models from the runtime autonomous system by L* or reinforcement learning algorithms(Zhang et al. 2020), and (3) develop the symbolic (MTBDD-based) implementation of this abstraction framework to offer improved scalability on models exhibiting regularity.