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
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
Probabilistic Temporal Logics via the Modal
- 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
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.