Original Publication Date: 1998-Mar-01
Included in the Prior Art Database: 2002-Jun-20
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.