next up previous
Next:Hierarchical Names

VIS CTL and LTL Syntax


Yuji Kukimoto

The VIS Group. University of California, Berkeley.
Jae-Young Jang The VIS Group. University of Colorado, Boulder.
Mohammad Awedh The VIS Group. University of Colorado, Boulder.
Nikhil Jayakumar The VIS Group. University of Colorado, Boulder.

July 18, 2002

This document describes the CTL and LTL syntax used in VIS.

CTL (Computation Tree Logic) is a language used to describe properties of systems.
For the semantics of CTL, the reader should refer to the following paper
E. M. Clarke, E. A. Emerson and A. P. Sistla,
Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,
ACM Transactions on Programming Languages and Systems,
vol 8-2, pages 244-263, April, 1986
This syntax should be followed when VIS users create CTL files
and fairness constraint files for the commands model_check,
approximate_model_check
, and read_fairness, respectively.
The syntax for CTL is:
TRUE, FALSE, and var-name=value are CTL formulas,
where var-name is the full hierarchical name of a
variable , and value is a legal value in the domain
of the variable. var-name1 == var-name2 is the atomic
formula that is true if var-name1 has the same value
as var-name2. Currently it can be used only in the
Boolean domain. ( It cannot be used for variables of
enumerated types. ) var-name1[i:j] == var-name2[k:l]
can be used if the lengths of vectors are the same.
Vector variables, the syntax of hierarchical names, and
macro definition are described later in this document.
The following character set may be used for variable names and values:
	A-Z a-z 0-9 ^ ? | / [ ] + * $ < > ~ @ _ # % : " ' .
If f and g are CTL formulas, then so are the following:
	(f), f * g, f + g, f ^ g, !f, f -> g, f <-> g, AG f,
AF f, AX f, EG f, EF f, EX f, A(f U g) and E(f U g).
AX:n(f) is allowed as a shorthand for AX(AX(...AX(f)...)), where
n is the number of invocations of AX. EX:n(f) is defined similarly.

Binary operators must be surrounded by spaces, i.e. f + g is a CTL
formula while f+g is not. The same is true for U in until formulas
and R in release (used in LTL only) formulas. Once parentheses are
inserted, the spaces can be omitted, i.e. (f)+(g) is a valid formula.
Unary temporal operators and their arguments must be separated by
spaces unless parentheses are used.


The symbols have the following meanings1.
	* -- AND, + -- OR, ^ -- XOR, ! -- NOT, -> -- IMPLY, <-> -- EQUIV
Operator Precedence for CTL:

High
    	!

AG, AF, AX, EG, EF, EX

*

+

^

<->

->

U

Low
>
An entire formula should be followed by a semicolon. All text from # to
the end of a line is treated as a comment. The model checker (mc) package is
used to decide whether or not a given FSM satisfies a given CTL formula. See
the help files for the model_check and approximate_model_check commands for
more details.

LTL (Linear Time Logic) is a language used to describe properties of systems.
For the semantics of LTL, the reader should refer to the following publication.
E. M. Clarke, O. Grumberg and D. A. Peled,
Model Checking,
MIT Press,1999

This syntax should be followed when VIS users create LTL files for the
commands ltl_model_check and bounded_model_check.

The syntax for LTL:
The syntax for LTL is simillar to the syntax of CTL. All the operators
have the same meanings (except for the R - 'release'operator which is only
available as an LTL operator in VIS). The main difference between LTL and
CTL formulas is the absence of E (existential) and A (universal) operators
in LTL formulas which reflects the linear-time paradigm.

The character set for LTL is the same as the character set for CTL


If f and g are LTL formulas, then so are the following:
	(f), f * g, f + g, f ^ g, !f, f -> g, f <-> g,
G f, F f, X f, f U g and f R g.
X:n(f) is allowed as a shorthand for X(X(...X(f)...)), where n is the
number of invocations of X.
Operator Precedence for LTL:
High
    	!

G, F, X

*

+

^

<->

->

U, R
Low

Just as in CTL, an entire formula should be followed by a semicolon.
All text from # to the end of a line is treated as a comment. The LTL
model checker (ltl) Bounded model checker (bmc) packages are used to
decide whether or not a given FSM satisfies a given LTL formula. See the
help files for the ltl_model_check and bounded_model_check commands for
more details.

______________________________________________________
1 && and || are also supported for AND and OR respectively



next
up
previous

Next: Hierarchical Names
Jayakumar Nikhil 2002-07-18