Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

PRE-CTL

IP.com Disclosure Number: IPCOM000008535D
Original Publication Date: 1998-Mar-01
Included in the Prior Art Database: 2002-Jun-20
Document File: 9 page(s) / 391K

Publishing Venue

Motorola

Related People

Richard Raimi: AUTHOR

Abstract

PRE-CTL is a set of abbreviations of CTL formulae. CTL is a well known temporal logic, which has been in the public domain a number of years, However, it is difftcult to write CTL specifi- cations, and PRECTL greatly eases that task. Each PRE-CTL abbreviation is called a "modality." Each PRE-CTL modality (except as noted) can be preceded by either an A or E, which are CTL path quantifiers. 'A' means the modality should hold along all paths (sequences of states), 'E' along some paths. PRE-CTL modalities can be mixed with CTL modalities, in formulae. PRECTL modalities can be nested inside one another, or inside CTL fomulae. The CTL logic is built from 6 special sym- bols, A and E, explained above, and the 4 temporal operators, F, G, U and X, meaning, respectively, "eventually," "always, " "until" and "next time." CTL also includes Boolean connectives, and propo- sitional formulae. The vast literature on CTL can be consulted for more formal definitions.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 16% of the total text.

Page 1 of 9

0 M

MOTOROLA Technical Developments

PRE-CTL

by Richard Raimi

  PRE-CTL is a set of abbreviations of CTL formulae. CTL is a well known temporal logic, which has been in the public domain a number of years, However, it is difftcult to write CTL specifi- cations, and PRECTL greatly eases that task. Each PRE-CTL abbreviation is called a "modality." Each PRE-CTL modality (except as noted) can be preceded by either an A or E, which are CTL path

quantifiers. 'A' means the modality should hold along all paths (sequences of states), 'E' along some paths. PRE-CTL modalities can be mixed with CTL modalities, in formulae. PRECTL modalities can be nested inside one another, or inside CTL fomulae. The CTL logic is built from 6 special sym- bols, A and E, explained above, and the 4 temporal operators, F, G, U and X, meaning, respectively, "eventually," "always, " "until" and "next time." CTL also includes Boolean connectives, and propo- sitional formulae. The vast literature on CTL can be consulted for more formal definitions.

  Below, m and n are integers, p,q,r,u,v, w, arbitrary CTL formulae. Each PRE-CTL modality will be numbered. Its usage (correct syntax) will be given. Its expansion into CTL will also be given. When dots appear in the argument list, it means an indeterminate number of arguments is permitted. The following symbols are used for Boolean con- nectives: '!' for negation, 'I' for disjunction, '&' for conjunction, and '->' for implication. As is common usage, a -> b has the same truth value as !a 1 b.

The following defines the PRE-CTL language:

Clock-phases n

  Clock-phases(n) is a keyword. Its argument, 'n', will be given by the user, and it indicates how many clock phases are in a clock period. This infor- mation is used when expanding various PRE-CTL modalities having the optional CLK argument. Othenvise, a default value for CLK will be assumed.

1. U-seq p, q

Usage: A [P U-seq 41, E [P U-seq ql

Expansion: A [p U-seq ql expands to: !q & A[p U q]

E [p U-seq q] expands to: !q & E[p U s]

2. U-weak p, q

Usage: A [p U-weak 41, E [p U-weak sl

Expansion: A [p U-weak q] expands to:

! E[ !q U (!p & !q) ]

E [p U-weak q] expands to:

EGP I E[P U sl

3. Same-time p, q

Usage: A Same-time(p, q), E Sameetime(p, q)

Expansion: A Same-time(p, q) expands to:

A[ (!P & !q) U (P & @I

E Same-time(p, q) expands to:

EL (!P & !q) U (P & 411

4. Same-time-seq p, q

Usage: A Same-time-seq (p, q).

E Same-time-seq (p, q)

Expansion: A Same-time-seq(p,q) expands to:

!p & !q & A[ (!p & !q) U (p & q)]

E Same-time-seq(p,q) expands to:

!p & !q & E[ (!p & !q) U (p & q)]

5. Before p, q

Usage: A [p Before q], E [p Before q]

0 Motorola, 1°C. 1998 2 March 199X

[This page contains 14 pictures or other non-text objects]

Page 2 of 9

0 M

MOTOROLA Technical Developments

Expansion: A [p Before q] expands to: !q & EX(!p & !q & EX(!p & !q &

A[!q U (p & !q & AF q)] WP U ql))))l)

E [p Before q] expands to:

E[!q U (p & !q & EF q)]

E[p Before(0,3) q] expands to:

E[!q U ( p & !q & ( (E[!q U...