# Finite probability

Propagate a probability distribution through an explicitly finite stochastic model with exact fractions.

## Definitions

- **DTMC**: A discrete-time Markov chain whose row probabilities determine the next-state distribution.
- **Stochastic matrix**: A nonnegative matrix with every row summing to one.
- **Absorbing state**: A state that transitions to itself with probability one.

## Acceptance procedure

1. Validate the initial distribution and each matrix row.
2. Multiply the row distribution by the transition matrix.
3. Repeat for the exact declared horizon.
4. Compare every trajectory row and the final rational distribution.

## Complexity

A dense n-state chain over h steps costs O(hn²) arithmetic operations, with fraction sizes growing over time.

## Common failure

A finite-horizon probability is not automatically an eventual-reachability answer.

## Extensions

Add absorbing-state equations, expected hitting time, and nondeterministic MDP choices.

## Instances

- KL-FCS-058: Success and failure after four steps — Final probability distribution: ["1/16", "15/32", "15/32"]
- KL-FCS-059: A reversible two-state distribution — Final probability distribution: ["2731/4096", "1365/4096"]
- KL-FCS-060: Progress through two transient states — Final probability distribution: ["1/256", "1/32", "247/256"]

## References

- https://www.prismmodelchecker.org/doc/whatsinprism.php