Links to papers I have read

Recursive Markov Chains, Stochastic Grammars, and Monotone Systems of Nonlinear Equations

Analysis of RMCs offers a way to find the probability of a language that a stochastic grammar generates. The paper generalizes the method to an algorithm for a monotone system of nonlinear equations. Also, it shows that when the goal is just to find the probability of a language for a grammar, this is equivalent to extinction probability of a multitype branching process. It shows that both can be modeled by termination probabilities of 1-exit RMCs.

PReMo: an analyzer for Probabilistic Recursive Models

This paper has a few practical points. Basic (Jacobi) iteration can be optimized slightly with Gauss-Seidel iteration. Newton's method can avoid explicit inversion of a matrix when it is sparse.

A Logic for Reasoning about Time and Reliability

This paper introduces PCTL. A key idea may be that there are two types of formulas, state formulas and path formulas. The way to convert a path formula into a state formula is with probability. Path formulas themselves are essentially LTL rather than CTL. The paper gives algorithms to do model checking with the general case of an Until expression, and it also considers extreme time and probability cases separately. I wonder about the situation when an infinite path (thus with probability of 0) is the only one for which the expression does (or does not) hold.

Model checking probabilistic and stochastic extensions of the π calculus

The probabilistic extension of π calculus has two types of choice, probabilistic and nondeterministic, and has MDP semantics. The stochastic extension has CTMC semantics, and the choice represents a race condition. In case of parallel composition causing a race condition, there is a rate associated with the transition corresponding to matching input/output actions.

Probabilistic Temporal Logics via the Modal Mu-Calculus

This paper uses reactive probabilistic labeled transition systems (RPLTS) as the underlying model, and generalized probabilistic logic (GPL) as the language. RPLTSs use deterministic trees (d-trees) as "outcomes," resolving internal choices, but leaving the external choices. GPL has two types of formulae, called state formulae and fuzzy formulae. A state formula can be made from a fuzzy formula by asking for its probability.

Verification of multiprocess probabilistic protocols

The Science/Engineering Library has a hard copy of the Distributed Computing journal with the paper.

Model-Checking Algorithms for Continuous-Time Markov Chains

A paper on CSL and uniformization.