Syntax

1 Syntax

The key notion of ITL is an interval. An interval $σ$ is considered to be a (in)finite sequence of states $σ , σ ... 0 1$ , where a state $σ i$ is a mapping from the set of variables $V ar$ to the set of values $V al$ . The length $|σ |$ of an interval $σ0 ...σn$ is equal to $n$ (one less than the number of states in the interval (this has always been a convention in ITL), i.e., a one state interval has length 0).

The syntax of ITL is defined in Table 1 where
$z$ is an integer value,
$a$ is a static integer variable (doesn’t change within an interval),
$A$ is a state integer variable (can change within an interval),
$v$ a static or state integer variable,
$g$ is a integer function symbol,
$q$ is a static Boolean variable (doesn’t change within an interval),
$Q$ is a state Boolean variable (can change within an interval),
$h$ is a predicate symbol.

Table 1: Syntax of ITL

|----------------------------------------------------| |Expressions | | e ::= z|a|A |g (e1,...,en)|CA |finA | | Formulae | | f ::= true|q|Q| h(e1,...,en)|¬f|f1 ∧ f2|∀v o f | | skip|f ;f |f* | -------------------1--2-------------------------------

Front

November 14, 2011