benchmark_formulae.txt

### BENCHMARK FORMULAE

# states from which all outgoing paths eventually reach a "checkpoint" state
AF (!{x}: (AX (~{x} & AF {x})))

# states from which all outgoing paths eventually reach a "checkpoint" state that lies on at least two different cycles
AF (!{x}: ((AX (~{x} & AF {x})) & (EF (!{y}: EX ~AF {y}))))

# steady states, in case there are at least two of them
!{x}: 3{y}: ((@{x}: ~{y} & AX {x}) & (@{y}: AX {y}))

# existence of "fork" states in the system (states where system decides which terminal steady state to visit)
3{x}: 3{y}: ((@{x}: ~{y} & AX {x}) & (@{y}: AX {y}) & EF ({x} & (!{z}: AX {z})) & EF ({y} & (!{z}: AX {z})) & AX (EF ({x} & (!{z}: AX {z})) ^ EF ({y} & (!{z}: AX {z}))))


### OTHER USEFUL FORMULAE

# attractor states
!{x}: (AG EF {x})

# steady states
!{x}: (AX {x})

# attractor states which are always visited repeatedly
!{x}: (AX (~{x} & AF {x}))

# states of non-trivial cycle attractors
AG (!{x}: (AX (~{x} & AF {x})))

# existence of at least two attractors
3{x}: (3{y}: (@{x}: (AG~{y}) & (AG EF {x})) & (@{y}: AG EF {y}))


## EXPERIMENTAL FORMULAE EMPLOYING UNIVERSAL QUANTIFIER

# existence of a state weakly reachable from every state
3{x}: V{y}: (@{y}: EF {x})

# existence of a state strongly reachable from every state (cant use AF because of cycles on the path)
3{x}: V{y}: (@{y}: AG EF {x})