Filetype PDF | Posted on 28 Jan 2023 | 2 years ago
Authentication
digital resources
129x Filetype PDF File size 0.84 MB Source: hal.archives-ouvertes.fr
Automated generation of partial Markov chain from
high level descriptions
Pierre-Antoine Brameret, Antoine Rauzy, Jean-Marc J.-M. Roussel
To cite this version:
Pierre-Antoine Brameret, Antoine Rauzy, Jean-Marc J.-M. Roussel. Automated generation of partial
Markov chain from high level descriptions. Reliability Engineering and System Safety, 2015, 139,
pp.179-187. 10.1016/j.ress.2015.02.009. hal-01238630
HALId: hal-01238630
https://hal.science/hal-01238630
Submitted on 6 Dec 2015
HAL is a multi-disciplinary open access L’archive ouverte pluridisciplinaire HAL, est
archive for the deposit and dissemination of sci- destinée au dépôt et à la diffusion de documents
entific research documents, whether they are pub- scientifiques de niveau recherche, publiés ou non,
lished or not. The documents may come from émanant des établissements d’enseignement et de
teaching and research institutions in France or recherche français ou étrangers, des laboratoires
abroad, or from public or private research centers. publics ou privés.
Automated Generation of Partial Markov Chain from High Level Descriptions
a,∗ b a
P.-A. Brameret , A. Rauzy , J.-M. Roussel
a Lurpa, Ens Cachan, Univ Paris-Sud,
F-94235 Cachan, France
{pierre-antoine.brameret,jean-marc.roussel}@lurpa.ens-cachan.fr
b ´
Chaire Bleriot-Fabre, LGI
´
Ecole Centrale de Paris, Grande voie des vignes,
92295 Chˆatenay-Malabry cedex, France
Antoine.Rauzy@ecp.fr
Abstract
We propose an algorithm to generate partial Markov chains from high level implicit descriptions, namely AltaRica
models. This algorithm relies on two components. First, a variation on Dijkstra’s algorithm to compute shortest paths
in a graph. Second, the definition of a notion of distance to select which states must be kept and which can be safely
discarded.
The proposed method solves two problems at once. First, it avoids a manual construction of Markov chains, which
is both tedious and error prone. Second, up the price of acceptable approximations, it makes it possible to push back
dramatically the exponential blow-up of the size of the resulting chains.
Wereport experimental results that show the efficiency of the proposed approach.
Keywords: Model Based Safety Assessment, Markov chains, State space build, AltaRica
1. Introduction to explore the underlying state graph at a bounded depth,
MarkovchainsarepervasiveinProbabilisticSafetyAnal- i.e. to keep states (and transitions between these states)
yses. They make it possible to assess performance indica- that are at the shortest distance from the initial state. Our
tors for systems with complex control structures such as algorithm relies on two components:
cold spare units, or systems with limited number of re- ❼ An efficient way to explore the underlying graph in
sources. However, they suffer from the exponential blow- order to avoid revisiting states. To do so, we apply
up of the number of states and transitions. This drawback a variation of Dijkstra’s algorithm to determine on-
has two aspects. First, the manual construction of Markov the-fly shortest paths in a graph [6].
chains is both tedious and error prone. Second, assessment ❼ A suitable notion of distance which is basically the
of large Markov chains is very resource consuming. probability of the path and that is used as an indi-
A way to solve the first problem consists in generat- cator of relevance for states.
ing Markov chains from higher level descriptions, typically
Generalized Stochastic Petri Nets [1] or AltaRica models Thecombinationofthesetwocomponentsprovesextremely
[2]. These descriptions represent the state space in an efficient. We present here examples for which a partial
implicit way. To obtain the Markov chain, a space ex- chain, whose size is a tiny fraction of the complete chain,
ploration algorithm is used: starting from the initial state, makes it possible to approximate system unreliability with
states and transitions are progressively added to the result- a relative error less than 0.25%.
ing chain, until no more state or transition can be added. It is not possible to guarantee a priori the quality of the
However, only some of the many states of a very large approximation (to get a “probably approximately correct”
Markov chain are relevant to the calculation of reliability result according to Valiant’s scheme for approximation al-
indicators. The odds of reaching them is very low. There- gorithms [7]). However, we show that it is possible to
fore, they have almost no influence on the calculated quan- calculate a posteriori an upper bound of the probability of
tities and can be safely ignored. The same idea is behind discarded states. This bound provides the analyst with a
algorithms that consider failure sequences in turn, while means to assess the accuracy of the approximation.
keeping only probable enough sequences; see e.g. [3, 4, 5]. The method we propose in this paper is a contribu-
Whatweproposehereisrathertogeneratearelevantfrac- tion to so-called Model-Based Safety Analyses: it makes
tion of the whole Markov chain. Technically, the idea is Markov chains an effective tool to assess large high level
models. This tool is of paramount interest for systems
∗Corresponding author that show dependencies amongst failures, i.e. systems for
Preprint submitted to Reliability Engineering & System Safety April 28, 2015
❼ V = S ⊎ F is a set of variables, divided into two
disjoint subsets: the subset S of state variables and
the subset F of flow variables.
❼ E is a set of events.
❼ T is a set of transitions. A transition is a triple
he,G,Pi, denoted as e : G → P, where e ∈ E is an
event, G is a guard, i.e. a Boolean formula built over
V, and P is an instruction built over V, called the
action of the transition. The action modifies only
state variables.
❼ A is an assertion, i.e. an instruction built over V .
The assertion modifies only flow variables.
Figure 1: Overview of the AltaRica 3.0 project ❼ ι is the initial assignment of variables of V .
In a GTS, states of the system are represented by vari-
which combinatorial representations (such as Fault Trees) able assignments. A transition e : G → P is said fireable
are not suitable. in a given state σ if its guard G is satisfied in this state,
The remainder of this paper is organized as follows. i.e. if G(σ) = true. The firing of that transition trans-
Section 2 introduces the context of the present paper, forms the state σ into the state σ′ = A(P(σ)), i.e. σ′ is
and discusses related studies. Section 3 presents the al- obtained from σ by applying successively the action of the
gorithm. Section 4 discusses issues regarding the practical transition and the assertion.
implementation of the algorithm and the accuracy of the Guarded Transition Systems are implicit representa-
approximation. Finally, section 5 presents experimental tions of labeled Kripke structures, i.e. of graphs whose
results. nodes are labeled by variable assignments and whose edges
are labeled by events. The so-called reachability graph
2. Problem Statement Γ=hΣ,Θi of a GTS hV,E,T,A,ιi is the smallest Kripke
structure such that:
2.1. Context ❼ ι ∈ Σ.
Classical formalisms used in safety analyses, such as ❼ If σ ∈ Σ, e : G → P is a transition of T and
Fault Trees and Markov chains, are well mastered by an- G(σ) = true (the transition is fireable in σ), then
alysts. Moreover, they provide a good tradeoff between σ′ = A(P(σ)) ∈ Σ and e : σ → σ′ ∈ Θ.
the expressiveness of the modeling formalism and the effi-
ciency of assessment algorithms. They stand however at a If exponential distributions are associated with events
low level. As a consequence, there is a significant distance of E, the Kripke structure Γ = hΣ,Θi can be interpreted
between the specifications of the system under study and as a Continuous Time Homogeneous Markov Chain (for
the safety models of this system. This distance is both sake of brevity we shall just write Markov Chain in the
error prone and a source of inefficiency in the modeling remainder of the article). The reliability indicators (such
process. Not only are models difficult to share amongst as system unavailability) can be defined by associating a
stakeholders, but any change in the specifications may re- reward (a real number) with each state of the chain.
quire a tedious review of safety models. The reachability graph may be very large, even for
Hence the idea to describe systems with high level small GTS. Assume for instance we model a system made
modeling formalisms and to compile these high level de- of n independent, repairable components. Then, the num-
scriptions into lower level ones, typically Fault Trees and ber of variables of V is n, the number of transitions of T is
n
Markov chains, for which efficient assessment algorithms 2×n,butthe number of states of Σ is 2 and the number
n
exist. AltaRica 3.0 is such a high level formalism (see e.g. of transitions of Θ is n×2 . Even when the components of
[8]). the system are not fully independent, safety models tend
The semantics of AltaRica 3.0 is defined in terms of to show the same picture, i.e. a number of states which is
Guarded Transition Systems [9]. Prior to most of any as- exponential in the number of components (or the variables
sessment, including compilation into Markov chains, Al- in the GTS) and a number of transitions which is a small
taRica 3.0 models are flattened into Guarded Transition multiple of the number of states.
Systems as illustrated in Figure 1, which gives an overview The idea is thus to generate (still starting from the
of the AltaRica 3.0 project. initial state and applying the above principle) only a frac-
As defined in [8], a Guarded Transition System (GTS tion of the Kripke structure, keeping only states that are
for short) is a quintuple hV,E,T,A,ιi, where: relevant with respect to the calculation of reliability indi-
cators, and transitions between these states.
2
2.2. Related work the smaller chain uses matrix product involving the tran-
Several strategies have been proposed to overcome, or sition matrix of the bigger chain, so the method is not
at least to contain, the combinatorial explosion of the size scalable.
of Markov chains. Establishing a full review of the litera- Muntz et al. developed in [18] a method to bound
ture on this topic is quite difficult, because Markov chains steady-state performance indicators of a system using ap-
are pervasive in many areas of science. We review here a proximate aggregation in Markov chains. They build the
few ideas that are related to the proposed work, but our Markov chains from (simple) high level description, and
aim is not to provide a comprehensive review of related avoid the construction of the whole chain. The method we
research. develop in this paper is close to that one: we generate also
As already pointed out in the Introduction, methods a partial the Markov chain from a higher level modeling
have been developed to assess implicitly described Markov language. However, in contrast to Muntz et al., we do not
chains sequence by sequence (see e.g. [3, 4, 5]). The calcu- makeanyassumptionabouttheinputmodel. Themethod
lated quantity is obtained by summing-up individual val- proposed by Muntz et al. works only for models in which
ues obtained for sequences. Sequences with a too low prob- the number of possible failures in each state of the system
ability are discarded. This method is used by Bouissou and is known prior to the calculation of the chain and only one
Bon to assess so-called Boolean-Driven Markov Processes component can be repaired at a time.
[10]. Of course, generating a partial Markov chain induces Tothebest of our knowledge, the approach we propose
of course a higher memory consumption than considering in this paper is original. It can evaluate any performance
sequences in turn (if sequences are not saved), but sub- indicator of any system, while the full Markov chain is
sequent calculations are much easier. The partial chain never generated.
is actually generated independently of any specific target
indicator or mission time. It can then be used to calculate 3. Partial Construction of the Reachability Graph
any indicator defined in terms of rewards and transient
probabilities, steady state probabilities or sojourn times. The algorithm to build a partial reachability graph re-
Another approach has been proposed by Plateau et lies on two components: first, a variation of Dijkstra’s
al. for the assessment of Stochastic Automata Network shortest path algorithm, second the calculation of suitable
– SAN are another high level formalism to describe finite notion of distance, i.e. a relevance factor for states. In this
state automata –, see e.g. [11, 12]. The idea is to express section, we shall present them in turn.
the Markov chain in terms of a generalized tensor prod-
uct, using the modularity of SAN models. This approach 3.1. Variation on Dijkstra’s Shortest Path Algorithm
makes it possible to reduce the size of the chain, but it Let hV,E,T,A,ιi be a Guarded Transition System and
does not to reduce its number of states. Γ=hΣ,Θibeitsreachabilitygraph. Assumethatalength
Pribadi et al. introduced a method to reduce the size l(e : σ → τ), i.e. a positive real number, is associated with
of Markov chains while guaranteeing the exact assessment each transition of Θ (no matter what it means for now).
of the rewards [13]. This method seems efficient to reduce The distance from a state σ to any state τ of Σ is
the chain, but it relies on a strong ergodicity hypothesis. defined as usual as the minimum, over the paths from σ
This hypothesis is not always verified, in particular in the to τ, of the lengths of the paths. The length of a path is
case of non-repairable systems. the sum, over the transitions of the path, of the length of
Fourneau et al. proposed a theoretical framework to the transitions.
study state-space truncation, i.e. to estimate bounds on The Dijskra’s algorithm [6] calculates distances of all
the error made by applying such censoring (see e.g. [14, states from a source state. The basic idea is as follows. At
15]). These theoretical developments are of interest al- any time, there is a set C of candidates, i.e. of states that
though it seems difficult to apply them to our concrete have been reached but not treated yet. Initially C con-
problem because of the complexity of underlying algo- tains only the source state. The calculation is completed
rithms. when there are no more candidates. If C is not empty, the
Mercierdevelopedin[16]approximateboundstoquickly algorithm picks up the candidate σ that is at the shortest
calculate transient and steady-state probabilities. Unfor- distance from the source, removes it from C and then con-
tunately, the method uses the inversion of a matrix which siders in turn all of the successors of σ. Let τ be such a
is similar to the transition matrix, so the method is not successor. If τ is already treated, there is nothing to do. If
scalable. τ is not in C, then it is added to C and its distance to the
Carrasco proposed in [17] approximate bounds with source d(τ) is set to d(σ) + l(σ,τ), where l(σ,τ) denotes
error control to calculate transient rewards of a Markov the length of the edge (σ,τ). Finally, if τ already belongs
chain. This method is interesting because it uses a smaller to C, then its distance to the source is updated, i.e. is
Markov chain to approximate the bigger one, and is based replaced by d(σ) + l(σ,τ) if this value is smaller than the
on sequences. It is an optimized algorithm to calculate previous value of d(τ).
rewarded Markov chains. However, the algorithm to build This strategy ensures that each state is treated only
once and therefore the algorithm is linear in the number
3
no reviews yet
Please Login to review.
