LTL Specifications

Specifications in Attestor are written as logical formulas in linear temporal logic for a set of atomic propositions which is specialized for analyzing pointer programs. A specification is passed to Attestor via the command-line option --model-checking (link).

The syntax of formulas accepted by Attestor is given by the context-free grammar below:

<ltlform> ::= <stateform> 
		| "X" <ltlform>                        # the formula holds in the next state
                | "G" <ltlform>                        # the formula globally holds
                | "F" <ltlform>                        # the formula eventually holds
		| <term>
		| "(" <ltlform> "U" <ltlform> ")"      # the left formula holds until eventually the right formula holds
		| "(" <ltlform> "R" <ltlform> ")"      # the right formula holds until the left formula becomes true
                | "(" <ltlform> "->" <ltlform> ")"     # the left formula implies the right formula
	
<stateform> ::= "!" <ltlform>                          # negation 
		| "(" <ltlform> "&" <ltlform> ")"      # conjunction
		| "(" <ltlform> "|" <ltlform> ")"      # disjunction

<term> ::= "true"
	        | "false"	
		| <atomicprop>

Furthermore, supported atomic propositions <atomicprop> are given by the following context-free grammar

<atomicprop> ::= "{" "L(" <NT> ")" "}"
	    | "{" "visited" "}"
	    | "{" "visited(" <variable> ")" "}"
	    | "{" "identicNeighbours" "}"
	    | "{" "isReachable(" <variable> "," <variable> ")" "}"
	    | "{" "terminated" "}"
	    | "{" <variable> " == " <variable> "}"
	    | "{" <variable> " != " <variable> "}"

where <variable> is a Java program variable, i.e. built from lower- and upper-case letters, numbers, "_" and "$", <selectorList> is a []-enclosed comma-separated list of fields and <var> is a variable, possibly followed a sequence of fields and <NT> is the identifier of a nonterminal defined in the input graph grammar.

Let us go through the atomic propositions in more detail.

L( <NT> )

The heap consists exactly of a shape contained in the language of nonterminal <NT> only.

visited

On all paths through the state space, all nodes in an initial heap are eventually accessed by some variable. This atomic proposition triggers the generation of markings. The atomic proposition visited is assigned to a state, whenever there is some variable that is attached to the marked node.

visited( <variable> )

On all paths through the state space, all nodes in an initial heap are eventually accessed by variable <variable>. This atomic proposition triggers the generation of markings. The atomic proposition visited(<variable>) is assigned to a state, whenever variable <variable> is attached to the marked node.

identicNeighbours

On all paths through the state space, the neighbourhood of all nodes in an initial heap, i.e. its direct successors and predecessors, is the same as in the initial heap. This atomic proposition triggers the generation of markings. The atomic proposition identicNeighbours is assigned to a state, whenever the neighbourhood of the marked node coincides with the neighbourhood of the node in the initial heap.

isReachable( <variable> , <variable> )

The second variable is reachable from the first variable by following arbitrary selectors in the heap.

terminated

Program execution has terminated in the current state.

<variable> == <variable>

The two supplied variables are attached to the same node in the current state.

<variable> != <variable>

The two supplied variables are not attached to the same node in the current state.