Probabilistic Rewriting

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