# Probabilistic Rewriting

From Termination-Portal.org

Jump to navigationJump to search## General

As in the non-probabilistic setting, we use an adaption of the ARI format, so probabilistic TRSs (PTRSs) are represented as S-Expressions (see here, Sec. 3.1). The format of TRSs is explained here. To extend this format for PTRSs, rules are replaced by probabilistic rules that are defined as follows:

prule ::= ( prule term dist cost? ) cost ::= :cost number dist ::= ( ( term prob? )* ) prob ::= :prob number

The goal of the analysis is implicitly specified by the category.

## Probabilistic Termination

All probabilistic termination categories consider termination w.r.t. arbitrary start terms.

### PTRS Standard

- full rewriting

The tools can give the following answers:

MAYBE, AST, PAST, SAST

### PTRS Innermost

- innermost rewriting

The tools can give the following answers:

MAYBE, AST, PAST, SAST