Probabilistic Rewriting
From Termination-Portal.org
Jump to navigationJump to searchGeneral
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
