Yuji KukimotoThe VIS Group. University of California, Berkeley.

Jae-Young JangThe VIS Group. University of Colorado, Boulder.

Mohammad AwedhThe VIS Group. University of Colorado, Boulder.

Nikhil JayakumarThe 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 paperE. M. Clarke, E. A. Emerson and A. P. Sistla,This syntax should be followed when VIS users create CTL filesAutomatic 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

and fairness constraint files for the commandsmodel_check,, and

approximate_model_checkread_fairness, respectively.

The syntax for CTL is:TRUE, FALSE, andvar-name=valueare CTL formulas,

wherevar-nameis the full hierarchical name of a

variable , andvalueis a legal value in the domain

of the variable.var-name1 == var-name2is the atomic

formula that is true ifvar-name1has the same value

asvar-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 + gis a CTL

formula whilef+gis not. The same is true forUin until formulas

andRin 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 meanings^{1}.* -- AND, + -- OR, ^ -- XOR, ! -- NOT, -> -- IMPLY, <-> -- EQUIVOperator Precedence for CTL:

High!An entire formula should be followed by a semicolon. All text from

AG, AF, AX, EG, EF, EX

*

+

^

<->

->

U

Low

>#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 themodel_checkandapproximate_model_checkcommands 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

commandsltl_model_checkandbounded_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!Low

G, F, X

*

+

^

<->

->

U, R

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 theltl_model_checkandbounded_model_checkcommands for

more details.

______________________________________________________

^{1}&& and || are also supported for AND and OR respectively