FOCTL(ℝ_{lin})
Firstorder Computation Tree Logic solver on linear arithmetic over the reals
Thierry Martinez,
François Fages
FOCTL(ℝ_{lin}) is a solver for full
FirstOrder Computation Tree Logic with linear arithmetic over the reals in constrained transition systems (CTS).
CTS are transition systems where both states and transitions
are described with constraints.
We welcome any feedbacks and comments:
Thierry.Martinez@inria.fr
Online service
Syntax

Constants

Integer or floatingpoint values.

Variables


x, y, A, foo, etc. and their prime versions in the transition constraint: x', y', A', foo', etc.

Arithmetic operators


+, , *

Comparison relations

=, <, >, <=, >=, \=

Logical constants

true, false

Logical connectives

/\, \/, =>, <=>, not(...), exists(x, ...), forall(x, ...)

Temporal modalities

EX(...), EF(...), EG(...), EU(..., ...), EW(..., ...), AX(...), AF(...), AG(...), AU(..., ...), AW(..., ...)
Download
The current version is 1.1. FOCTL is written in Prolog (foctl.pl) and requires
SWIProlog
with PPL bindings
(see README for more details).
History
 20120426 1.1
 Widening, fixedpoint arithmetic
 20120128 1.0
 Initial version