A Practical Introduction to PSL

B.2: Syntax

B.2 Syntax

The logic PSL is defined with respect to a non-empty set of atomic propositions P and a given set of boolean expressions B over P . We assume two designated boolean expression true and false belong to B.

Definition 1: (Sequential Extended Regular Expressions (SEREs))
  1. Every boolean expression b ? B is a SERE.

  2. If r, r 1 , and r 2 are SEREs, and c is a boolean expression, then the following are SEREs:

  • { r}

  • r 1 ; r 2

  • r 1 : r 2

  • r 1 r 2

  • r 1 && r 2

  • [*0]

  • r[ *]

  • r@c

Definition 2: (FL Formulas)
  1. If b is a boolean expression, then both b and b! are FL formulas.

  2. If ? and ? are FL formulas, r, r1, r2 are SEREs, and b a boolean expression, then the following are FL formulas:

  • ( ?)

  • ?

  • ? ? ?

  • r ? ?

  • r!

  • r

  • X! ?

  • [ ? U ?]

  • ? @ b

  • ? async_abort b

  • ? sync_abort b

Note

We define formal semantics for both strong and weak booleans[20]. However, strong booleans are not accessible to the user.

Definition 3: (OBE Formulas)
  1. Every boolean expression is an OBE formula

  2. If f, f 1, and f 2 are OBE formulas, then so are the following:

    1. ( f)

    2. f

UNLIMITED FREE
ACCESS
TO THE WORLD'S BEST IDEAS

SUBMIT
Already a GlobalSpec user? Log in.

This is embarrasing...

An error occurred while processing the form. Please try again in a few minutes.

Customize Your GlobalSpec Experience

Category: Color Meters and Appearance Instruments
Finish!
Privacy Policy

This is embarrasing...

An error occurred while processing the form. Please try again in a few minutes.