Package jline.api.mc

Class Ctmc_passage_taboo

java.lang.Object
jline.api.mc.Ctmc_passage_taboo
public final class Ctmc_passage_taboo extends Object
First passage into a TARGET state set B under a TABOO state set C: the passage is completed by entering B and is lost for good by entering C first. F is the DEFECTIVE distribution 
     F(t) = Pr{ B is entered by time t, and C is not entered before B }
          = atom + alpha (-S)^-1 (I - exp(St)) sB,
and f its density alpha exp(St) sB. F tends to the reach probability rather than to one. In temporal-logic terms this is the time-bounded until Pr{ not C U<=t B }.

The chain is cut into four parts: B and C, made absorbing; the states N that can reach neither, also absorbing, since they can only hold the passage up forever; and the transient states K, on which S = Q(K,K) is nonsingular by construction. A state in both B and C counts as B.

The ultimate probabilities come from the exit-probability matrix X of the stochastic complement onto B, C and N (Ctmc_stochcomp), so they are one linear solve and need no time grid.

A null pi0 starts from the conditional stationary law on the complement of B, as in Ctmc_passage_ph. An empty or null tset computes only the probabilities. A +Inf entry of tset returns the reach probability and a negative one returns zero. Indices are 0-based here and 1-based in the MATLAB reference. With an empty taboo set, F equals the CDF of Ctmc_passage_time.

Reference: C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, "Model-checking algorithms for continuous-time Markov chains", IEEE TSE 29(6), 2003.

  • Method Details

    • ctmc_passage_taboo

      public static CtmcPassageTaboo ctmc_passage_taboo(Matrix Q, Matrix pi0, int[] target, int[] taboo, double[] tset)

    • ctmc_passage_taboo

      public static CtmcPassageTaboo ctmc_passage_taboo(Matrix Q, Matrix pi0, int[] target, int[] taboo, double[] tset, String method, String ltiMethod)
      Parameters:
      Q - generator, rows summing to zero
      pi0 - initial distribution over the state space, or null
      target - 0-based target state indices B, not empty
      taboo - 0-based taboo state indices C, or null/empty
      tset - time grid, or null/empty to compute only the probabilities
      method - "expm" (default) or "lt"
      ltiMethod - inverter of the "lt" method