FO-CTL 1.0

First-order Computation Tree Logic solver

Thierry Martinez, François Fages

Copyright (C) 2012 INRIA, Institut National de Recherche en
Informatique et en Automatique, France.


FO-CTL is a solver for FO-CTL(ℝlin), handling first-order CTL queries on
constraint transition systems (CTS).  CTS are a generalization of
labeled transition systems where states and transitions are described.


We welcome any feedbacks and comments: Thierry.Martinez@inria.fr


INSTALLATION

There is no official installation procedure at this time.

FO-CTL is a program written for SWI Prolog using the PPL library.

SWI Prolog can be downloaded here: http://www.swi-prolog.org/
PPL library can be downloaded here: http://bugseng.com/products/ppl/

PPL should be configured with the SWI Prolog interface:
./configure --enable-interfaces=swi_prolog

FO-CTL has been tested with PPL version 0.11.2.


USING FO-CTL

Typical use of FO-CTL consists in querying the solver for some FOCTL(ℝlin)
formulas.

$ swipl
?- ['/path/to/ppl/lib/ppl/ppl_swiprolog.pl'].
?- [foctl].
?- foctl(example1, X, A, ax(X = 5), C).
C = (A>=1/\X=4).

where example1 is a predicate which defines the transition constraint.

example1(X, X_, A, R) :-
   constraint_to_polyhedric_union(
      1 =< X /\ X =< 4 /\ X_ = X + 1 \/
      X = 4 /\ X_ = 3 /\ A < 1 \/
      X = 5 /\ X_ = 2,
      R
   ).


In the examples/ directory, there are some exports from Grégory Batt's
RoVerGeNe tool [1] of some large biological examples of transition
systems.  You can load and query them with the check_export/3 predicate.

On the simple two genes example:
| ?- check_export([X1, X2], 'examples/export_two_genes_square',
       ef(X1 = 3 /\ X2 = 1)).
| ?- check_export([X1, X2], 'examples/export_two_genes_square',
       (X1 = V1 /\ X2 = V2) /\ ag(X1 = V1 /\ X2 = V2)).

On the big examples:
| ?- check_export([X1, X2, X3, X4], 'examples/export10-400_100-6000',
      ag(X3 >= 4)).
| ?- check_export([X1, X2, X3, X4], 'examples/export10-400_100-6000',
      ef(ag(X3 >= 4))).
| ?- check_export([X1, X2, X3, X4], 'examples/export_low_4000-5050',
      X4 = 1 /\ af(ag(X3 =< 2))).
| ?- check_export([X1, X2, X3, X4], 'examples/export10-900_10-400_100-6000',
      ef(ag(X3 >= 4))).


[1] http://iasi.bu.edu/~batt/rovergene/rovergene.htm