Introduction to Temporal Logic Propositional Checker by Hugh McGuire

Names

    "sat", "ver", "fsat", "fver": satisfy/verify propositional temporal formulas


Command-Syntax

    sat   [<options>]  [<file-name>]  [<options>]

    ver   [<options>]  [<file-name>]  [<options>]

    fsat  [<options>]  [<file-name>]  [<options>]

    fver  [<options>]  [<file-name>]  [<options>]


Description

    Each of the programs "sat" and "fsat" seeks a model that would satisfy
    a given formula of propositional linear temporal logic; each of the
    programs "ver" and "fver" seeks a model that would falsify a given
    formula.  The "f"-versions are tuned for formulas whose temporal
    operators refer only to the future.

    The formula to be handled is taken from the input "<file-name>"; if
    "<file-name>" is not specified, standard input is used.

    If a model is found, it is displayed via standard output.

    This output plus some additional information is also stored in a
    log-file.  The name of the log-file can be specified via the option
    "-l".  If such specification is not done, then a default name, chosen
    as follows, is used.  If the input-"<file-name>" is "<name>.tl", the
    default name of the log-file will be "<name>.log".  If the input-
    "<file-name>" is not of the form "<name>.tl", the default log-file
    will be "<file-name>.log".  If actually no input-"<file-name>" is
    given, then as the invoked program is "sat", "ver", "fsat", or "fver",
    the default log-file will be "sat.log", "ver.log", "fsat.log", or
    "fver.log", respectively.


Options

    -@		Display copyright/warranty-information; do no processing.

    -l <file-name2>
		(`Log')  Use "<file-name2>" (instead of the default) as
		the log-file-name.

    -t		(`Terse')  Send all reports --- except error-messages and
		the final result ("SATISFIABLE", "NOT SATISFIABLE", "VALID",
		or "FALSIFIABLE") --- only to the log-file, not to standard
		output.

    -v		(`Verbose')  Standard output gets what the log-file gets.

    -c          (`Checking')  Provide information enabling the user to check
		the model.  The Terse option is set.

    -C		(`Checking')  Enable more thorough checking by displaying
		the entire graph --- even if there's no model.  The Terse
		option is set.

    -s          (`Singleton')  Seek a model that has only one repeated state.
		If such can't be found, seek any model.

    -S          (`Singleton')  Seek a model that has only one repeated state
		and a shortest possible path to the repeated state.  If a
		model with only one repeated state can't be found, seek any
		model.

    -u		(`(Not) Unbarring')  [available only for "sat" and "ver"]
		Save time by not executing "unbar_edges()" (see the paper).
		Satisfying (or for "ver", falsifying) models that are found
		will still be correct; but complete correctness is lost
		because some models may not be found, i.e. non-satisfiability
		or validity may be reported in some cases when they do not
		hold.

    -n		(`Numbering')  Number the printed model's states.



Syntax of Formulas

    Ignored:	    whitespace (blank, tab, newline, formfeed),
			"\,", \bigl, \bigr

    Comment:	    "#", ";", or "%" to end of line.


    Delimiters:	    parentheses or brackets, i.e. "(" and ")" or "[" and "]".
		    (Not braces, i.e. "{" and "}", and not newlines.)

    Proposition:    lower-case alphabetic character followed by any
		    combination of lower-case alphabetic characters,
		    digits, or the underscore "_".  (Length-limit: 8.)


    False	    F, FALSE, \false
    True	    T, TRUE, \true
    Negation	    ~, !, NOT, \lnot, \neg
    Disjunction	    \/, |, OR, \lor, \vee
    Conjunction	    /\, &, AND, \land, \wedge  (but not "^")
    Implication	    -->, IMPLIES, \rightarrow
    Equivalence	    <-->, EQUIV, \leftrightarrow
    N-ary exclusive disjunction
 		    *, ?, NXOR  (not "^" here either)
			(The value of "p_1 * p_2 * ... * p_n" is "TRUE"
			if and only if exactly one "p_i" has the value
			`true'.  Same as binary exclusive disjunction
			when n is 2.  Re attempting to use for true
			binary exclusive disjunction, note that as with
			conjunctions and (regular) disjunctions, trees
			of n-ary exclusive disjunctions are flattened:
			e.g. "(p_1 * p_2) * p_3" becomes "p_1 * p_2 * p_3".)

    Next	    O (`circle'), \X (`neXt'), (), \bigcirc
    Next (postfix)  '  (only following a proposition)
    Henceforth	    [], \G (`Generally'), \Box
    Eventually	    <>, \F (`Future'), \Diamond
    Until	    U, \U
    Awaiting(/unless)   W (`aWaiting'), \W

    Previous	    Y (`Yesterday'), \Y, (-)
    Has-always-been     H (`Heretofore'/`Hitherto'), [-], \H
    Once	    P (`Previously'), <->, \P
    Since	    S, \S
    Back-to	    B, \B

    Weak Previous   WY (`Weak Yesterday'), (~), \WY

    First	    first, FIRST, \first

    Strict ...	    SG, \SG, \widehat{\G}
		    SF, \SF, \widehat{\F}
		    SU, \SU, \widehat{\U}
		    SW, \SW, \widehat{\W}

		    SH, \SH, \widehat{\H}
		    SP, \SP, \widehat{\P}
		    SS, \SS, \widehat{\S}
		    SB, \SB, \widehat{\B}

    Entailment	    ==>, EN, \Rightarrow
    Congruence	    <==>, CONG, \Leftrightarrow


    Precedences of binary operators:
		    Temporal operators have stronger precedence than
		    non-temporal operators, e.g. "p /\ q U r" is parsed
		    as "p /\ (q U r)".  Otherwise, precedences are as
		    usual; e.g. "/\" has stronger precedence than "\/".
		    (Unary operators including negation have strongest
		    precedence, e.g. "~ p U q" is parsed as "(~p) U q"
		    rather than "~(p U q)".)

    Associativity of binary operators:
		    Right-associativity is used.  For example, "p W q W r"
		    is parsed as "p W (q W r)".




Suggestions

    Use the C preprocessor to define repeated subformulas.  ANSI C even
    provides for creation of tokens, so it's possible to have
    `parameterized' propositions (e.g. "p0", "p1"), perhaps
    corresponding to different processes of a concurrent system.  But
    remember that the C preprocessor sees the capital letters used here
    in operators (e.g.  "O", "U") as (parts of) identifiers.  So use
    (`macro'-) names that begin with "_" to facilitate catching
    (typographical) errors.  Otherwise, suppose you have
    "#define name replacement" and then "Oname"; the C preprocessor
    won't replace "name" here, seeing the token "Oname" instead of what
    to "sat" would be two tokens, "O" and "name".  Then, running "sat"
    may produce undesirable results.  If you have
    "#define _name replacement" and "O_name", the C preprocessor
    still may not replace "_name" but the error will nonetheless be
    caught --- when you execute "sat".



Examples

    1.  Suppose the file "example1.tl" contains:

	    OO[]p

    Then a session using "fsat" may proceed as follows:

	    prompt>  fsat example1.tl

	    SATISFIABLE:
	    
	    
	    Initial states:
	    {}
	    {}
	    
	    Repeat:
	    { p}


	    prompt>

    This model involves no commitments to "p" (nor to "~p") during the
    first two states, but then a state with "p" true should be repeated
    henceforth.

    The program "fsat" may also be run as follows --- more tersely:

	    prompt>  fsat -t example1.tl

	    SATISFIABLE


	    prompt>

    During both the former and the latter executions, the model is stored
    in the file "example1.log".


    2.  Suppose the file "example2.tl" contains:
    
	    (p U q) U r  -->  (p \/ q) U r

    Then one may use "fver" as follows:

	    prompt>  fver example2.tl
	    
	    VALID


	    prompt>


    3.  Suppose the file "example3.tl" contains:

	    []([p --> Oq] /\ [q --> Or] /\ [r --> Op])  /\  [](p * q * r)

    Then one may use "fsat" as follows:

	    prompt>  fsat example3.tl

	    SATISFIABLE:

	    Repeat:
	    { p, ~q, ~r}
	    {~p,  q, ~r}
	    {~p, ~q,  r}


	    prompt>

    This model involves forever repeating --- in the specified order ---
    three states of which the first has "p" true and "q" and "r" false, the
    second has only "q" true, and the third has only "r" true.


    4.  Suppose the file "example4.tl" contains:

	    ~p /\ O[](p /\ YOq)

    Then one may use "sat" as follows:

	    prompt>  sat example4.tl

	    SATISFIABLE:

	    Initial states:
	    {~p    }   (Also "first".)

	    Repeat:
	    { p,  q}


	    prompt>

    
    5.  Suppose the file "example5.tl" contains:

	    []<>p /\ []<>q

    Then one may use "fsat" as follows:

	    prompt>  fsat example5.tl
	    
	    SATISFIABLE:
	    
	    Repeat:
	    {}
	    {     q}
	    { p    }
	    { p,  q}
	    

	    prompt>  fsat -s example5.tl
	    
	    SATISFIABLE:
	    
	    Initial states:
	    {}
	    {     q}
	    { p    }
	    
	    Repeat:
	    { p,  q}


	    prompt> fsat -S example5.tl
	    
	    SATISFIABLE:
	    
	    Repeat:
	    { p,  q}


	    prompt>


    6.  Suppose the file "example6.tl" contains:

	    p U q

    Then one may use "fsat" as follows:

	    prompt>  fsat -c example6.tl

	    Table of formulas, with consistent satisfaction-replacements-sets:
	    (The main formula's index is 4.)

	    0.  F  :
		    (no consistent satisfaction-replacements-sets)

	    1.  p  :
		    set #1:  {1}

	    2.  q  :
		    set #1:  {2}

	    3.  O(p U q)  :
		    set #1:  {3}

	    4.  p U q  :
		    set #1:  {2}
		    set #2:  {1, 3}


	    SATISFIABLE:

	    Initial states:
	    { p    }
		Formulas satisfied:  {1, 3, 4}

	    {     q}
		Formulas satisfied:  {2, 4}

	    Repeat:
	    {}
		Formulas satisfied:  {}


	    prompt>

    The table indicates that the main formula (#4) "p U q" may be satisfied
    either by satisfying formula #2, which is "q", or by satisfying both
    #1, which is "p", and #3, which is "O(p U q)".  In the result, the
    latter alternative is used to satisfy the main formula in the first
    state: formula #4 is satisfied because formulas #1 and #3 are
    satisfied.  In the next state, formula #4 is satisfied because formula
    #2 is satisfied there.  In the last state, which is supposed to be
    repeated forever, no formulas need to be satisfied.



`Diagnostics'

    The programs "sat" and "fsat" exit with status-value 0, indicating
    success, when able to satisfy the given formula, or 1, indicating
    failure, otherwise.  The programs "ver" and "fver" exit with status-
    value 0 when able to verify the given formula, or 1 otherwise.


See Also

    Manna - Z. and Pnueli - A.:
	*The Temporal Logic of Reactive and Concurrent Systems:
	Specification*, 1991.

    Kesten - Y., Manna - Z., McGuire - H., and Pnueli - A.:
	"A Decision Algorithm for Full Propositional Temporal Logic", in
	*5th International Conference on Computer Aided Verification
	(CAV) '93*, 1993, pp. 97--109.  Springer-Verlag, Berlin.


Authors

    Hugh McGuire (of Stanford University), Rivi Sherman (of ???), and
    Amir Pnueli (of Stanford University and the Weizmann Institute of
    Science).  Edward Chang (of Stanford University) discovered the
    usefulness of the C preprocessor.  Zohar Manna supervised.


Copyright (c) 1994 The Board of Trustees of the Leland Stanford Junior
University (STANFORD).  All Rights Reserved.  See also the copyright/
warranty-information via the option "-@".


This document was last updated 1994:March:04.