LITE: A little LITL Verifier

 Copyright (C) 1994,1991, 
 Shinji Kono (kono@csl.sony.co.jp)
   Sony Computer Science Laboratory, Inc.
   The University, Newcastle upton Tyne

 Everyone is permitted to copy and distribute verbatim copies
 of this license, but changing it is not allowed.  You can also
 use this wording to make the terms for other programs.

 send your comments to kono@csl.sony.co.jp

Files
    Makefile		Makefile for *.ql/*.pl, "make" is called from Prolog
    bdtstd.pl		Binary Tree Database of Temporal Logic Formula
    chop.pl		Chop normal form expander
    demoi		Install Script for X-Window Interface
    demoim		    "  with module
    diag.pl		Diagnosis and Execution
    display.pl		X-Window Interface (GM and InterViews)
    dvcomp.pl		Lazy expansion version of ITL tableau
    ex.pl		Built-in Examples
    exdev.pl		Expansion Loop
    init		Install Script 
    initm		Install Script with module
    kiss.pl		KISS2 format for UCB SIS
    lite.pl		Install Script 
    ndcomp.pl		ITL tableau expansion
    read.me		This file

0. Installation

    Edit Makefile and change
          PROLOG               your prolog path name, such as sicstus
          PROLOG_TYPE          SICSTUS, XSB, SBPROLOG, CPROLOG, CPROLOG15
    see cp.pl.c for portbaliity information.

    Run your Prolog. I use SICStus Prolog but Quintus Prolog or C-Prolog 
    will work.  In case of SBPROLOG, you also need SB_START_FILE.

    Then consult a file init. 

?-[init].

    It runs unix make and compile and load necessary Prolog programs.
    If you need a moduled version use ?-[initm].

    In case of SB-Prolog, type
	make
    by hand. This create file named "lite". Then start SB-Prolog like this.
        sbprolog lite
    or you can use load(lite). Then you need to initialize by
        ?- lite_start.

0.1 How to run

    Try numbered examples in ex.pl.

?-ex(2).

    It generates state machine. It also accepts an ITL formula.

?-ex( [](p) -> <> p ).

    Please be careful about funny Prolog operator grammar.
    Someday I will make a parser for Ben's notation. But not now...
    After the state machine expansion, there are two diagnosis predicates.

?-diag.

    This shows ``valid'' if it is a theorem, otherwise it shows you a counter
    example.

?-exe.

    This shows an execution of ITL formula, if it is possible. It is
    a counter example of negation of the original formula. ?-diag(N) or 
    ?-exe(N) shows at least N length examples.  
   	1: +p-q   means "at clock 1, p is true and q is false". 
    Please note exe(N)/diag(N) generate all possible state transition,
    but it only shows one possible state transition conditon for a
    state transition.

?-infinite. 
      Check satisfiability on infinite interval. Like exe, it shows
      possible accept states with a loop marked by *. To check infinite
      validity, use negation.

    In case of a large formula, you may want to make output tarse.

?-verbose(off). 
    generates one character per state transition condition.
     e   empty
     t   true
     f   false
     123. newly genrated state number
     .   transition to a registerd state
?-verbose(on).

?-ex. runs all examples in diag.pl. But it takes several hours.
      Some of the examples are quite large.
?-exex. runs all examples and save state machine in file ``ex''.

0.1. X-Window Interace

    If you want to run X-window version, you have to install InterViews
    interface for SICSTUS. It requires ispgm binary and library/gmlib.
    ?-[demoim].    % This loads and runs X-window interface.
    Type-in a formula. 
       ex(1) or demo(1) for the example number in ex.pl.
    Push verify buttom and execute buttom in order.
    Execute and Counter Example buttons show an example in a graphical way.
    Map button shows bitmap of the characteristic function.

0.1.1 Tcl/Tk Interface


0.2. KISS format interface

    To generate KISS2 format for SIS, try run

?-kiss.

    right after verification. To specify input variables and
    output variables assert this predicate:
	st_variables(In,Out).
    State machine description is also supported
    in this system. You can read a KISS2 format state machine.
    Only one state machine is accepted because of variable 
    declaration.

?- read_kiss(File,In,Out,Empty).

    reads KISS2 format. In and Out are list of variables in the order
    of the KISS2 file. If Out is [], output variales are omitted.
    If In or Out are uninstantiated variables, name 'i0' or 'o2'
    are used.  Empty is usually set to empty and it generates 
    empty condition for each state, for example:
	st(st0,empty,empty).
    To modify or to generate KISS format again, you have to
    verify it.
	?- ex(st(st0)).
    `st0' is the start state of automaton. The state machine can
    be used in arbitrary temporal logic expression. But if you 
    generate very non-deterministic modification, the output
    can be very large. For examle:
	 ?- ex(exists(i0,st(st0))).

?- read_kiss(File).
    =>  read_kiss(File,_,_,empty)
?- read_kiss(File,Empty).
    =>  read_kiss(File,_,_,Empty)

0.3
    dvcomp.pl contains lazy state transition clause generation and binary
    tree representation of ITL term.  Reconsult it after [init].  It 
    reduces memory usage drastically. To control lazy generation, use:
       ?-lazy(on).
       ?-lazy(off).
    kiss format generation is not supported for lazy generation.

1. Syntax of ITL Formula

Comma for conjunction, and semi-coron for disjunction as in Prolog.
& for chop operator. @ for strong next. next(P) for weak next. 
Postfix * means weak closure, that is, it allows 0 times execution.
To use existential quantifier, a form exists(R,f(R)) is used,
here R have to be Prolog variable.

Other definitions are found in chop.pl. If you want to see the expanding
results ( chop normal form, cannot be readable...) use ?-expand(X,Y).

    ~(P) 	=   not(P)
    P->Q 	=   (not(P);Q)
    P<->Q 	=   ((not(P);Q),(P; not(Q)))
    P=Q 	=   ((not(P);Q),(P; not(Q)))
    (P && Q) 	=   ((not(empty),P) & Q)               strong chop
    <>(Q) 	=   (true & Q)
    #(Q) 	=   not(true & not(Q))
    [](Q) 	=   not(true & not(Q))
    '[a]'(Q) 	=   not(true & not(Q) & true)
    fin(Q) 	=   (true & (empty,Q))
    halt(Q) 	=   [](empty=Q)
    keep(Q) 	=   not(true & not((empty ; Q)))
    more 	=   not(empty)
    skip 	=   @(empty)
    length(I)            expanded into series of strong next.
    less(I)              expanded into series of weak next.
    next(P) 	=   (empty; @(P))
    gets(A,B)	=   keep(@A<->B)
    stable(A) 	=   keep(@A<->A)

    infinite    =   (true&false)
    finite      =   ~infinite

    P proj Q  	=   Q is true using P as a clock period
    *P          =   P&P&..&P.. chop infinite closure 

    Q=>P 	=   exists(R,(Q = R,stable(R),fin(P = R)))
    P<=Q 	=   Q=>P
    +A  	=   (A & (empty;A) *)                  strong closure
    while(Cond,Do)	=   ((Cond->Do) , (~Cond->empty)) * 
    exists(P,Q) =   Exsistential Quantifier
    all(P,Q)   	=   not(exists(P,not(Q)))

    even(P) 	=   exists(Q,(Q, keep( @Q = ~Q),[](Q->P)))
    evenp(P) 	=   ((P,skip) & skip;empty,P)* & (empty;skip)
    phil(L,R)  	=   ([]((~L  =    ~R)) & @ (L, ~R,@ (L,R, @ (R,[]( ~L)))) )

For user define predicate use define/2. Ex.
	define(yeilds(A,B), not(not(A) & B)).


1.1 Finte State Automaton support

1.1.1 Output.

This version supports Finite State Automaton I/O. The output of
our verifier is finite automaton.

?-tgen.

generates automaton as Tokio Temporal Logic Programming Language.
KISS2 format output is also supported, see 0.2.

1.1.2 Input

It is possible to use automaton as a part of ITL formula.
Finite automaton is stored in Prolog clauses.

st(s0) starts Finite State Automaton (FSA) from s0 states.
This is a temporal logic term, so you can use this anywhere
in ITL formula, for example: st(s0) & not(st(s0)), <>(st(s0)).
FSA is defined as Prolog clauses in this way:

st_variables([q],[s]).   
%   st_varaibles(Input_variables,Output_variables)
%   This is important only for KISS format generation
	    
st(s0,((not(a);not(b)),q),s0). 
%    st(Current_State, Condition, Next_State)
st(s1,(not(c),q),s1).
st(s1, empty,empty).

Conditions can be non-deterministic. Actually it allows
arbitrary ITL formula, but if you use temporal condtions,
it is not a state machine any more. The automaton is
determinized during verfication, since generated state
machine is determinisc. Be careful, the output can be very large.

If a state machine contains no empty conditions, it is
not satisfiable in ITL, because our ITL only have finite
interval. But it may contains infinite clock periods. 

2. Basic Algorithm of the Verifier

This program uses classic tableau method. So hold your breath, it is
exponential to the number of the variables in the formula and  also
combinatorial to the nesting of temporal logic operator. I think it is
possible to reduce complexity for the nesting, but not for the
variables.

Major contribution (I think) is in the classification of ITL formula,
which is found in bdtstd.pl. I use binary decision tree (not diagram)
standard form among subterms in original formula. Since this program
always keep state machine deterministic, determinization of state
machine is done by outer-most loop.

The algorithm is quite simple. There are three stages. In the first
stage, an ITL formula is decomposed into three  parts: empty, now and
next. In the second stage, next parts is classifyed using subterm bdt
and stored into database.  In the third stage, decomposition is
repeatedly applied until no more new next parts are generated.

Since ITL assumes any interval is finite, no eventuality checking is
necessary.  Diagnosis algorithm is linear to the number of the state.

3. Wish lists

It is possible to reduce complexity in somehow.

4. Brief description of this program.

File exdev.pl contains main driver of tableau based interval temporal 
logic verifier. A developer deve(X) does tableau development.

deve(ITL) :-
	init,!,
	expand(ITL,ITL0),
	itlstd(ITL0,StdNext),
	check_state(StdNext,ITL0,_,S),!,
	deve0((S,ITL0)).

In init, formula databases are initialized. 
Usually ITL formula contains several macro definitions, expand(X,Y) 
expands these macros form X to Y.
The formula is translated into standard form in itlstd(X,Y), where X is original
formula and Y is binary decision tree standard form (not diagram).
The formula databases are maintained in check_state(Stdoriginal,NewFlag,No).
Std is the standard form. We need original formula here for display.
Whether Std is already in database or not is shown in NewFlag and when
database sequence number (i.e. state number) is returned in No.

deve0((S,ITL)) :-
        show_state(S,ITL),
	setof(Next,itldecomp(ITL,Next,S),
	    Nexts),!,
	deve1(Nexts).
deve0(_).

We are now in deve0(X) predicates. After displaying current states, it
gathers possible tableau expansion using setof predicates. Since not so
many formula is generated from one state, setof is not a bottle neck of
this program. The real bottle neck is total number of state/condition pair and
it's database looking up.  Setof predicates returns only new candidates and 
theses are stored in a list, in LIFO way.

deve1([]).
deve1([H|T]) :- deve0(H),deve1(T).

Here is a repetition part. 

itldecomp(ITL,(NextS,Next),From) :-
	itl(ITL,Next,Cond),
	%% showing
	itlshow(Next,NextS,Cond,From).

Actual tableau expansion is done by itl(ITL,Next,Cond). It generate
Sumof( Cond -> @(Next) ), where Cond is exclusive, that is, it generates
deterministic automaton. You can test itl predicates by hands, for example,
?-itl(p & q,Next,Cond).

itlshow(Next,S,Cond,From):-
	itlstd(Next,StdNext),
	check_state(StdNext,Next,New,S),
	assertz(state(From,Cond,S)),
	!,itlshow1(S,Cond,Next,New).

In itlshow, standard form conversion and database checking is performed.
Rest of parts are related to state database and displaying.

That's all. There are more stories about itlstd and itl predicates, but it is
better to look source code rather than vague English...