Models of discrete concurrent systems often lead to huge and complex
state transition graphs that represent their dynamics.
Here, we are particularly interested in logical models of biological
regulatory networks. Given an initial condition, it is of real interest
to identify reachable attractors that denote the potential asymptotical
behaviours of the system. These attractors are described as terminal
strongly connected components, that are either single (stable) states or
sets of states (denoting cyclical behaviours).

Beyond attractor identification, we propose to assess the probability to
reach each of them from an initial condition or from any portion of the
state space, relying on the structure of the state transition graph.
First, we present a solution to the problem with an original algorithm
called FIREFRONT, based on the exhaustive exploration of the reachable
state space. Then, for the cases where FIREFRONT is not applicable, we
define a modified Monte Carlo simulation, termed AVATAR.