Input Format

We use an adapted version of the format for Integer Programs (see for example here or here) from the Termination and Complexity Competition extended by costs and probabilities (see below).

Integer Programs (IPs)

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f))
(VAR x y)
(RULES
  f(x,y) -{0}> g(x,y)
  g(x,y) -> g(x-1,y+x) :|: x>0
  g(x,y) -> h(x,y)
  h(x,y) -{y}> h(x,y-1) :|: y>0
)

• The first line (GOAL COMPLEXITY) indicates that we would like to compute upper bounds on the runtime of the given IP.
• The second line (STARTTERM (FUNCTIONSYMBOLS f)) specifies that f is the start location of the IP.
• The third line (VAR x y) specifies that the variables used in the system are x and y.
• The fourth line (RULES ... indicates that we now state the general transitions of our system. It is ended by a closing parenthesis ) in the last line of the example code above.
• The remaining lines contain the transitions of the program in the form LHS -{COST}> RHS (:|: GUARD) or LHS -> RHS (:|: GUARD).
  • LHS is the start location of the transition including the variables to be updated here, e.g., f(x,y). Locations are arbitrary alpha-numerical strings.
  • COST is a non-negative polynomial that bounds the cost of the transition. This is optional. If omitted, the cost defaults to 1.
  • RHS specifies the guard and the update of a transition.
    • Updates are polynomial expressions. If the updates contain variables which are not given on the left-hand side, they are treated as non-deterministic (those variables can be restricted in the guard).
      • For example, g(x,y) -> g(x-1,y+x) means that from the start location g, x is set to x-1 and y is set to y+x.
      • For example, g(x,y) -> g(z,y) means that from the start location g, the IP chooses the transition to location g where the first variable x is updated non-deterministically and the second variable y stays the same.
  • GUARD is a conjunction (using the connective &&) of linear (in)equalities representing the guard of the transition, e.g., x > 0 or x > 0 && 2 * x + 3 * y = 0. This is optional. If omitted, GUARD defaults to true, e.g., g(x,y) -{0}> h(x,y).

Probabilistic Integer Programs (PIPs)

(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f))
(VAR x y)
(RULES
  f(x,y) -{0}> g(x,y)
  g(x,y) -> 0.5:g(x-1,y+x) :+: 0.5:g(x,y+x) :|: x>0
  g(x,y) -{0}> h(x,y)
  h(x,y) -> h(x,y-1) :|: y>0
)

• The first line (GOAL EXPECTEDCOMPLEXITY) indicates that we would like to compute upper bounds on the expected runtime of the given PIP. Alternatively, (GOAL COMPLEXITY) can be used to analyse an over-approximation, i.e., replacing all probabilities by non-deterministic choices, of the PIP.
• In contrast to IPs, the remaining lines contain the general transitions of the program in the form LHS -{COST}> RHS (:|: GUARD) or LHS -> RHS (:|: GUARD).
  • LHS again is the start location of the general transition.
  • Here, COST is a non-negative integer constant that bounds the cost of the general transition.
  • RHS specifies the distribution over transitions in the general transition.
    • Elements of the transition are given by p:target(up1,...,upn) and are separated by :+:. This means that the variable x1 is updated to up1,…, the variable xn is updated to upn, and the system transitions to location target with probability p.
    • Probabilities are rational numbers strictly greater than 0 which must add up to 1.
    • In case of a singleton general transition, the probability can be omitted and then defaults to 1, e.g., f(x,y) -{0}> g(x,y).
    • Updates are polynomial expressions. If the updates contain variables which are not given on the left-hand side, they are treated as non-deterministic (those variables can be restricted in the guard).
      • For example, g(x,y) -> 0.5:g(x-1,y+x) :+: 0.5:g(x,y+x) means that from the start location g, with probability 0.5 x is set to x-1 and y is set to y+x, and with the remaining probability 0.5 x is set to x and y is set to y+x.
      • For example, g(x,y) -> 1:g(z,y) means that from the start location g, the PIP chooses the transition to location g where the first variable x is updated non-deterministically and the second variable y stays the same.
    • Updates can also be distribution functions. In our semantics, the value drawn from this distribution is added to the current value of the variable.
      • For example, g(x,y) -> g(x,GEOMETRIC(0.5)) means that in the transition from the location g, the variable x stays the same whereas y is increased by a value drawn from a geometric distribution with parameter 0.5.
      • At the moment, we support the following discrete distributions. Here, parameters are integer polynomial expressions, i.e., they may depend on variables, whereas constants are non-negative integers or non-negative rationals. The user has to ensure that their values meet the stated constraints:
        • Bernoulli distribution with rational constant 0 < p < 1 via BERNOULLI(p).
        • Binomial distribution with rational constant 0 < p < 1 and a non-negative integer parameter n via BINOMIAL(n,p).
        • Geometric distribution with rational constant 0 < p < 1 via GEOMETRIC(p).
        • Hypergeometric distribution with non-negative integer constant N and non-negative integer parameters k,n via HYPERGEOMETRIC(N,k,n).
        • Uniform distribution with integer parameters a < b via UNIFORM(a,b).