FO-CTL(ℝ_lin)

First-order Computation Tree Logic solver on linear arithmetic over the reals

FO-CTL(ℝ_lin) is a solver for full First-Order 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 floating-point 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. FO-CTL is written in Prolog (foctl.pl) and requires SWI-Prolog with PPL bindings (see README for more details).

Browse distribution: distrib/1.1
Sources + examples: [tar.gz]

History

2012-04-26 1.1: Widening, fixed-point arithmetic
2012-01-28 1.0: Initial version