H-0256 (H0801-006) January 6, 2008
Computer Science
IBM Research Report
Proposal for Extending Annex B of PSL with Local Variables,
Procedural Blocks, Past Expressions and
Clock Alignment Operators
Cindy Eisner, Dana Fisman*
IBM Research Division
Haifa Research Laboratory
Mt. Carmel 31905
Haifa, Israel
*also with Hebrew University
Research Division
Almaden - Austin - Beijing - Cambridge - Haifa - India - T. J. Watson - Tokyo - Zurich
Proposal for Extending Annex B of PSL with
Local Variables, Procedural Blocks,
Past Expressions and Clock Alignment Operators
Cindy Eisner1
1
and
Dana Fisman1,2
IBM Haifa Research Lab
2
Hebrew University
December 3, 2007
Abstract
In this document we extend Proposal A’ for augmenting the formal semantics of PSL with
local variables to all of PSL (issue 67). Proposal A’ provides semantics for PSL without truncated
words, abort and clock operators. In this proposal we augment the entire formal semantics of
PSL (including the above constructs) with local variables. In addition, we add semantics for
procedural blocks (issue 66), for built-in functions that refer to the past (issue 117) and for clock
alignment operators (issue 137).
This document presents the semantics gradually. First it presents the semantics of the base
logic, which is the set of FL formulas that (i) do not use the clock operator (ii) do not refer to
the past (i.e., do not use past built-in functions) and (iii) do not use local variables or procedural
blocks. Then it presents the semantics of the base logic extended with either the clock operator
or references to the past or local variables and procedural blocks. Last it presents the overall
semantics of linear formulas with no restrictions.
Annex B
(normative)
Formal Syntax and Semantics of IEEE Std 1850 Property Specification Language (PSL)
This appendix formally describes the syntax and semantics of the temporal layer.
B.1 Typed-text representation of symbols
Table 1 shows the mapping of various symbols used in this definition to the corresponding typed-text
PSL representation, in the different flavors.
NOTE −
For reasons of simplicity, the syntax given herein is more flexible than the one defined by the extended BNF
(given in Annex A). That is, some of the expressions which are legal here are not legal under the BNF
Grammar. Users should use the stricter syntax, as defined by the BNF grammar in Annex A.
Table 1: Typed-text symbols in the SystemVerilog, Verilog, VHDL, SystemC and GDL flavors
→
⇒
→
↔
¬
∧
∨
..
hi
SystemVerilog
|->
|=>
->
<->
!
&&
||
:
[ ]
Verilog
|->
|=>
->
<->
!
&&
||
:
[ ]
VHDL
|->
|=>
->
<->
not
and
or
to
( )
SystemC
|->
|=>
->
<->
!
&&
||
:
( )
GDL
|->
|=>
->
<->
!
&
|
..
( )
B.2 Syntax
The logic PSL is defined with respect to a non-empty finite set of atomic propositions AP , a finite
set of local variables LV with domain D, a given set of (unary and binary) operators OP over the
domain D and a given set of procedural blocks P B with local variables in LV as input parmeters.
We assume that t and f belong to D.
Definition 1 (Expressions and Boolean expressions)
The set E of expressions is defined as follows:
1. Every atomic proposition p ∈ AP is an expression in E.
2. Every local variable v ∈ LV is an expression in E.
3. If e is an expression and ◦ a unary operator in OP then ◦e is an expression in E.
4. If e1 , e2 are expressions and ⊗ a binary operator in OP then e1 ⊗ e2 is an expression in E.
5. If e is an expression, c a Boolean expression and n a non-negative integer then prev(e),
prev(e, n) and prev(e, n, c) are expressions in E.
6. If r is a sere and c a Boolean expression then ended(r) and ended(r, c) are (Boolean) expressions in E.
We refer to an expression whose domain is {t, f} as a Boolean expression and use B to denote the
set of Boolean expressions. We use B–lv to denote the set of Boolean expressions that do not use local
variables. We use B–pe to denote the set of Boolean expressions that do not use past expressions (that
is, prev(·), ended(·) and their derivatives as per Section B.4.0). We use B–lv,pe to denote the set of
Boolean expressions that do not use local variables or past expressions. We often refer to Boolean
expressions in B–lv,pe as basic Boolean expressions. Note that we have B ⊆ E, B–lv,pe ⊆ B–lv ⊆ B
and B–lv,pe ⊆ B–pe ⊆ B.
Definition 2 (Sequential Extended Regular Expressions (seres))
1. Every Boolean expression b ∈ B is a sere.
2. If b is a Boolean expression in B, e1 , . . . , en are expressions in E, and y1 , . . . , yn are local
variables in LV then the following is a sere:
b, y1 ←e1 , . . . , yn ←en
3. If r, r1 , and r2 are seres, c is a Boolean expression in B–lv , and z ∈ LV is a local variable
then the following are seres:
• {r}
• r1 ; r2
• r1 : r2
• r1 | r2
• r1 && r2
• [∗0]
• r[∗]
• r@c
• {var(z) r}
• {free(z) r}
Definition 3 (Formulas of the Foundation Language (FL formulas))
If ϕ and ψ are FL formulas, n a non-negative integer, r is a sere, a, c ∈ B–lv Boolean expressions
over AP, and z ∈ LV is a local variable then the following are FL formulas:
• (ϕ)
• ¬ϕ
• ϕ∧ψ
• r!
•r
•r→ϕ
• X![n] ϕ
•ϕUψ
• ϕ@c
• ϕ async abort a
• ϕ sync abort a
• (var(z) ϕ)
Definition 4 (Formulas of the Optional Branching Extension (OBE))
1. Every basic Boolean expression b ∈ B–lv,pe is an OBE formula.
2. If f , f1 , and f2 are OBE formulas, then so are the following:
(a) (f )
(b) ¬f
(c) f1 ∧ f2
(d) EXf
(e) E[f1 U f2 ]
(f ) EGf
Definition 5 (PSL Formulas)
1. Every FL formula is a PSL formula.
2. Every OBE formula is a PSL formula.
In Section B.4, we show additional operators which provide syntactic sugaring to the ones above.
B.3 Semantics
The semantics of PSL formulas are defined with respect to a model. A model is a quintuple
(S, S0 , R, AP , L), where S is a finite set of states, S0 ⊆ S is a set of initial states, R ⊆ S × S
is the transition relation, AP is a non-empty set of atomic propositions, and L is the valuation, a
function L : S −→ 2AP , mapping each state with a set of atomic propositions valid in that state.
A path π is a possibly empty finite (or infinite) sequence of states π = (π0 , π1 , π2 , · · · , πn ) (or
π = (π0 , π1 , π2 , · · ·)). A computation path π of a model M is a non-empty finite (or infinite) path
π such that π0 ∈ S0 and for every i < n, R(πi , πi+1 ) and for no s, R(πn , s) (or such that for
every i, R(πi , πi+1 )). Given a finite (or infinite) path π, we overload L, to denote the extension of
the valuation function L from states to paths as follows: L(π) = L(π0 )L(π1 ) . . . L(πn ) (or L(π) =
L(π0 )L(π1 ) . . . ). Thus we have a mapping from states in M to letters of 2AP , and from finite (or
infinite) paths in M to finite (or infinite) words over 2AP .
Let v be an empty/finite/infinite word over some alphabet. We denote the length of word v as
|v|. A finite non-empty word v = (`0 `1 `2 · · · `n ) has length n + 1, the (finite) empty word v = ² has
length 0, and an infinite word has length ∞. We use i, j, and k to denote non-negative integers.
We denote the ith letter of v by v i−1 (since counting of letters starts at zero). We denote by v i..
the suffix of v starting at v i . That is, for every i < |v|, v i.. = v i v i+1 · · · v n or v i.. = v i v i+1 · · ·. We
denote by v i..j the finite sequence of letters starting from v i and ending in v j . That is, for j ≥ i,
v i..j = v i v i+1 · · · v j and for j < i, v i..j = ². We use `ω to denote an infinite-length word, each letter
of which is `.
B.3.1 Semantics of FL formulas
This document presents the semantics of FL formulas gradually. First it presents the semantics of
the base logic, which is the set of FL formulas that (i) do not use the clock operator (ii) do not refer
to the past (i.e., do not use prev(·) or ended(·)) and (iii) do not use local variables or procedural
blocks. Then it presents the semantics of the base logic extended with either the clock operator or
references to the past or local variables and procedural blocks. Last it presents the overall semantics
of FL formulas.
B.3.1.1 Semantics of the Base Logic
In this section we provide semantics of FL formulas that (i) do not use the clock operator (ii) do
not refer to the past and (iii) do not use local variables or procedural blocks, which we refer to as
the base semantics.
Let AP be a set of atomic propositions and let Σ be the set of all possible assignments of the
b denote the alphabet Σ ∪ {>, ⊥}.
atomic propositions AP (i.e. Σ = 2AP ). Let Σ
b and σ to denote a letter in Σ.
b
In the sequel we use u, v, w to denote words over Σ
b
Given a letter σ in Σ we use σ to denote the dual of σ which is ⊥ if σ is >, is > if σ is ⊥ and is
σ otherwise. We use v to denote the obvious extension of the definition of dual to words.
B.3.1.1.0 Base Semantics of Expressions
The semantics of FL formulas is defined inductively, using as the base case the semantics of expressions. In the case of the base semantics, we neglect local variables, and the built-in functions
ended(·) and prev(·). Thus we have only basic Boolean expressions (B–lv,pe ) to consider. We view
b 7→ {t, f}. Thus, b(σ) denotes the value of
a basic Boolean expression b ∈ B–lv,pe as a mapping b : Σ
b
b under σ ∈ Σ.
Let σ ∈ Σ. When b is an atomic proposition, say b is p for some p ∈ AP , then p(σ) is equivalent
to p ∈ σ. We define true and false to be the basic Boolean expressions that map every σ ∈ Σ to t
and f, respectively. We assume that operators are closed under {t, f} and that they behave in the
usual manner over letters in the alphabet Σ, i.e. that for σ ∈ Σ, b, b1 , b2 ∈ B–lv,pe , a binary operator
⊗ and a unary operator ◦ we have b1 (σ) ⊗ b2 (σ) = (b1 ⊗ b2 )(σ) and ◦(b(σ)) = (◦b)(σ). In particular
we assume that Boolean disjunction, conjunction and negation behave in the usual manner.
Regarding the letters > and ⊥, we assume that any basic Boolean expression b is evaluated to t
on (>) and to f on (⊥). That is b(>) = t and b(⊥) = f for any basic Boolean expression b. Note
that in particular we have true(>) = false(>) = t and true(⊥) = false(⊥) = f.
B.3.1.1.1 Base Semantics of SEREs
The notation v |≡ r, where r is a base sere and v a finite word means that v models tightly r. The
semantics of base seres are defined as follows, where b denotes a basic Boolean expression in B–lv,pe ,
and r, r1 , and r2 denote base seres:
1. v |≡ {r} ⇐⇒ v |≡ r
2. v |≡ b ⇐⇒ |v| = 1 and b(v 0 )=t
3. v |≡ r1 ; r2 ⇐⇒ ∃v1 , v2 s.t. v = v1 v2 , v1 |≡ r1 , and v2 |≡ r2
4. v |≡ r1 : r2 ⇐⇒ ∃v1 , v2 , and σ s.t. v = v1 σv2 , v1 σ |≡ r1 , and σv2 |≡ r2
5. v |≡ r1 | r2 ⇐⇒ v |≡ r1 or v |≡ r2
6. v |≡ r1 && r2 ⇐⇒ v |≡ r1 and v |≡ r2
7. v |≡ [∗0] ⇐⇒ v = ²
8. v |≡ r[∗] ⇐⇒ either v |≡ [∗0] or ∃v1 , v2 s.t. v1 6= ², v = v1 v2 , v1 |≡ r and v2 |≡ r[∗]
B.3.1.1.2 Base Semantics of FL Formulas
b a be a basic Boolean expression in B–lv,pe ,
Let v be a possibly empty finite or infinite word over Σ,
r a base sere, ϕ, ψ FL formulas, and n a non-negative integer. The notations v |= ϕ means that v
models (or satisfies) ϕ.
1. v |= (ϕ) ⇐⇒ v |= ϕ
2. v |= ¬ϕ ⇐⇒ v |=
/ϕ
3. v |= ϕ ∧ ψ ⇐⇒ v |= ϕ and v |= ψ
4. v |= r! ⇐⇒ ∃j < |v| s.t. v 0..j |≡ r
5. v |= r ⇐⇒ ∀j < |v|, v 0..j >ω |= r!
6. v |= r → ϕ ⇐⇒ ∀j < |v| s.t. v 0..j |≡ r, v j.. |= ϕ
7. v |= X![n] ϕ ⇐⇒ |v| > n and v n.. |= ϕ
8. v |= ϕ U ψ ⇐⇒ ∃k < |v| s.t. v k.. |= ψ, and ∀j < k, v j.. |= ϕ
9. v |= ϕ async abort a ⇐⇒ either v |= ϕ or ∃j < |v| s.t. a(v j )=t and v 0..j−1 >ω |= ϕ
10. v |= ϕ sync abort a ⇐⇒ v |= ϕ async abort a
NOTES −
1. The semantics given here for the ltl operators and the abort operators is equivalent to the truncated
semantics given in [B1] which is interpreted over 2P rather than over 2P ∪ {>, ⊥}. Using |=• for the
semantics in [B1] the following proposition states the equivalence: Let w be a finite word over 2P , and
let ϕ be a formula of ltltrunc . Then, as shown in [B5], the three following equivalences hold:
−
w |=• ϕ ⇐⇒ w>ω |= ϕ
w |=• ϕ ⇐⇒ w |= ϕ
+
w |=• ϕ ⇐⇒ w⊥ω |= ϕ
+
2. Using |=• as in Note 1 above, we use holds strongly for |=• , holds for |=• , and holds weakly for
−
|=• . The remaining terminology of Section 4.4.6 is formally defined as follows:
−
• ϕ is pending on word w iff w |=• ϕ and w |=
/• ϕ
−
• ϕ fails on word w iff w |=
/• ϕ
3. There is a subtle difference between Boolean negation and formula negation. For instance, consider
the formula ¬b. If ¬ is Boolean negation, then ¬b holds on an empty path. If ¬ is formula negation,
then ¬b does not hold on an empty path. Rather than introduce distinct operators for Boolean and
formula negation, we instead adopt the convention that negation applied to a Boolean expression is
Boolean negation. This does not restrict expressivity, as formula negation of b can be expressed as
{¬b}!.
4. A justification of why the semantics of a weak sere (e.g., r) is the appropriate definition given the
semantics of a strong sere (e.g. r!) can be found in [B6].
B.3.1.1.3 Base Semantics With Respect to a Model
Let ϕ be an FL formula and M a model. The notation M |= ϕ means that for all π such that π is
computation path of M , L(π) |= ϕ.
B.3.1.2 Semantics with Clocks
In this section we provide semantics of the base logic augmented with the clock operator, which we
refer to as the clocked semantics. We use the same alphabet and notation as in the base semantics,
and in addition we define a clock tick as follows.
Let c be a basic Boolean expression in B–lv,pe . We say that finite word v is a clock tick of c,
denoted tickc (v), if |v| > 0 and c(v |v|−1 )=t and for every non-negative integer i < |v| − 1, c(v i )=f
(where c(·) refers to the base semantics of expressions). For an integer m > 0 we say that finite
word v is m clock ticks of c, denoted ticksc (v, m), if there exist m words v1 , v2 , . . . , vm such that
v = v1 v2 · · · vm and for every 1 ≤ i ≤ m we have tickc (vi ).
B.3.1.2.0 Clocked Semantics of Expressions
The clocked semantics of expressions are the same as the base semantics of expressions.
B.3.1.2.1 Clocked Semantics of SEREs
c
The notation v |≡ r, where r is a sere, c is a basic Boolean expression in B–lv,pe and v a finite word,
means that v models tightly r in the context of clock c. The semantics of clocked seres are defined
as follows, where b, c, and c1 denote basic Boolean expressions in B–lv,pe , and r, r1 , and r2 denote
clocked seres:
c
c
1. v |≡ {r} ⇐⇒ v |≡ r
c
2. v |≡ b ⇐⇒ tickc (v) and b(v |v|−1 )=t
c
c
c
3. v |≡ r1 ; r2 ⇐⇒ ∃v1 , v2 s.t. v = v1 v2 , v1 |≡ r1 , and v2 |≡ r2
c
c
c
4. v |≡ r1 : r2 ⇐⇒ ∃v1 , v2 , and σ s.t. v = v1 σv2 , v1 σ |≡ r1 , and σv2 |≡ r2
c
c
c
5. v |≡ r1 | r2 ⇐⇒ v |≡ r1 or v |≡ r2
c
c
c
6. v |≡ r1 && r2 ⇐⇒ v |≡ r1 and v |≡ r2
c
7. v |≡ [∗0] ⇐⇒ v = ²
c
c
c
c
8. v |≡ r[∗] ⇐⇒ either v |≡ [∗0] or ∃v1 , v2 s.t. v1 6= ², v = v1 v2 , v1 |≡ r and v2 |≡ r[∗]
c
c
9. v |≡ r@c1 ⇐⇒ v |≡1 r
B.3.1.2.2 Clocked Semantics of FL Formulas
The semantics of clocked formulas is defined with respect to possibly empty finite/infinite words
b and a basic Boolean expression c in B–lv,pe which serves as the clock context. Let v be a
over Σ
possibly empty finite or infinite word, a, c, c1 basic Boolean expressions in B–lv,pe , r a clocked sere,
c
ϕ, ψ clocked formulas, and n a non-negative integer. The notation v |= ϕ means that v models ϕ in
the context of clock c.
c
c
1. v |= (ϕ) ⇐⇒ v |= ϕ
c
c
2. v |= ¬ϕ ⇐⇒ v |=
/ϕ
c
c
c
3. v |= ϕ ∧ ψ ⇐⇒ v |= ϕ and v |= ψ
c
c
4. v |= r! ⇐⇒ ∃j < |v| s.t. v 0..j |≡ r
c
c
5. v |= r ⇐⇒ ∀j < |v|, v 0..j >ω |= r!
c
c
c
6. v |= r → ϕ ⇐⇒ ∀j < |v| s.t. v 0..j |≡ r, v j.. |= ϕ
c
c
7. v |= X![n] ϕ ⇐⇒ ∃j < |v| s.t. ticksc (v 0..j , n + 1) and v j.. |= ϕ
c
c
c
8. v |= ϕ U ψ ⇐⇒ ∃k < |v| s.t. c(v k )=t, v k.. |= ψ, and ∀j < k s.t. c(v j )=t, v j.. |= ϕ
c
c
9. v |= ϕ@c1 ⇐⇒ v |=1 ϕ
c
c
c
10. v |= ϕ async abort a ⇐⇒ either v |= ϕ or ∃j < |v| s.t. a(v j )=t and v 0..j−1 >ω |= ϕ
c
c
c
11. v |= ϕ sync abort a ⇐⇒ either v |= ϕ or ∃j < |v| s.t. (a ∧ c)(v j )=t and v 0..j−1 >ω |= ϕ
NOTES −
1. The clocked semantics for the ltl subset follows the clocks paper [B2], with the exception that strength
is applied at the sere level rather than at the propositional level.
2. The operator obtained by instantiating X![n] with zero can be seen as an alignment operator, whose
introduction is of both practical and theoretical importance [B7].
B.3.1.2.3 Clocked Semantics With Respect to a Model
Let ϕ be an FL formula and M a model. The notation M |= ϕ means that for all π such that π is
true
computation path of M , L(π) |= ϕ.
B.3.1.3 Semantics with Past
In this section we provide semantics of the base logic augmented with past expressions, which we
refer to as the past augmented semantics. We use the same alphabet and notation as in the base
logic. We use the definition of clock ticks as in the clocked semantics.
B.3.1.3.0 Past Augmented Semantics of Expressions
In the case of the past augmented semantics, we do not have local variables. Thus we have only
Boolean expressions over AP (B–lv ) to consider.
b to the domain
The semantics of Boolean expressions over AP maps non-empty words over Σ
{t, f}. The last letter of the word represents the present, while the remainder of the word (without
b respectively.
the last letter) represents the past. Let u and σ be a finite word and a letter over Σ,
The semantics of Boolean expressions over AP (that may refer to the past) overloads the notation
b(·) defined in the base semantics as follows (where b(σ) below refers to the base semantics of
expressions).
Let c be a basic Boolean expression in B–lv . We say that finite word v with past u is a past
clock tick of c, denoted past tickc (u · v), if |v| > 0 and c(uv 0 )=t and for every non-negative integer
0 < i < |v|, c(uv 0..i )=f (where c(·) refers to the base semantics of expressions). For an integer
m > 0 we say that finite word v with past u is m past clock ticks of c, denoted past ticksc (u · v, m),
if there exist m words v1 , v2 , . . . , vm such that v = v1 v2 · · · vm and for every 1 ≤ i ≤ m we have
past tickc (uv1 . . . vi−1 · vi ).
• If b ∈ B–lv,pe is a basic Boolean expression then b(uσ) = b(σ).
• If r is a sere and c ∈ B–lv is a Boolean expression then
½
t iff ∃u1 , u2 such that u = u1 u2 and u1 · u2 σ |≡ r
– ended(r, c)(uσ) =
ended(Rc (r))(uσ)
if c=true
otherwise
– ended(r)(uσ) = ended(r, true)(uσ)
• If b, c ∈ B–lv are Boolean expressions then
½
e(u0..i )
if ∃i < |u| such that past ticksc (u0..i−1 · ui..|u|−1 , n + 1)
– prev(b, n, c)(u) =
undefined otherwise.
– prev(b, n)(u) = prev(b, n, true)(u)
– prev(b)(u) = prev(b, 1, true)(u)
where Rc (·) is defined in Section B.5.
Note that prev(e, n, c)(u) (as well as its derivatives as given in Section B.4.0) is undefined when
u does not contain n + 1 letters on which c holds.
B.3.1.3.1 Past Augmented Semantics of SEREs
The notation u · v |≡ r, where r is a past augmented sere and u, v are finite words means that v
models tightly r given that the past is u. The semantics of past augmented seres are defined as
follows, where b denotes a Boolean expression in B–lv , and r, r1 , and r2 denote past augmented
seres:
1. u · v |≡ {r} ⇐⇒ u · v |≡ r
2. u · v |≡ b ⇐⇒ |v| = 1 and b(uv 0 )
3. u · v |≡ r1 ; r2 ⇐⇒ ∃v1 , v2 s.t. v = v1 v2 , u · v1 |≡ r1 , and uv1 · v2 |≡ r2
4. u · v |≡ r1 : r2 ⇐⇒ ∃v1 , v2 , and σ s.t. v = v1 σv2 , u · v1 σ |≡ r1 , and uv1 · σv2 |≡ r2
5. u · v |≡ r1 | r2 ⇐⇒ u · v |≡ r1 or u · v |≡ r2
6. u · v |≡ r1 && r2 ⇐⇒ u · v |≡ r1 and u · v |≡ r2
7. u · v |≡ [∗0] ⇐⇒ v = ²
8. u · v |≡ r[∗] ⇐⇒ either u · v |≡ [∗0] or ∃v1 , v2 s.t. v1 6= ², v = v1 v2 , u · v1 |≡ r and uv1 · v2 |≡ r[∗]
B.3.1.3.2 Past Augmented Semantics of FL Formulas
b a be a Boolean expression in B–lv , r a
Let v be a possibly empty finite or infinite word over Σ,
past augmented sere, ϕ, ψ past augmented formulas, and n a non-negative integer. The notation
u · v |= ϕ means that v models ϕ given that the past is u.
1. u · v |= (ϕ) ⇐⇒ u · v |= ϕ
2. u · v |= ¬ϕ ⇐⇒ u · v |=
/ϕ
3. u · v |= ϕ ∧ ψ ⇐⇒ u · v |= ϕ and u · v |= ψ
4. u · v |= r! ⇐⇒ ∃j < |v| s.t. u · v 0..j |≡ r
5. u · v |= r ⇐⇒ ∀j < |v|, u · v 0..j >ω |= r!
6. u · v |= r → ϕ ⇐⇒ ∀j < |v| s.t. u · v 0..j |≡ r, uv 0..j−1 · v j.. |= ϕ
7. u · v |= X![n] ϕ ⇐⇒ |v| > n and uv 0..n−1 · v n.. |= ϕ
8. u · v |= ϕ U ψ ⇐⇒ ∃k < |v| s.t. uv 0..k−1 · v k.. |= ψ, and ∀j < k, uv 0..j−1 · v j.. |= ϕ
9. u · v |= ϕ async abort a ⇐⇒ either u · v |= ϕ or ∃j < |v| s.t. a(uv 0..j )=t and u · v 0..j−1 >ω |= ϕ
10. u · v |= ϕ sync abort a ⇐⇒ u · v |= ϕ async abort a
B.3.1.3.3 Past Augmented Semantics With Respect to a Model
Let ϕ be a past augmented formula and M a model. The notation M |= ϕ means that for all π such
that π is computation path of M , ² · L(π) |= ϕ.
B.3.1.4 Semantics with Local Variables
In this section we provide semantics of the base logic augmented with local variables and procedural
blocks, which we refer to as the lva semantics.
Let AP be a set of atomic propositions and LV a set of local variables with finite domain D.
Let Σ be the set of all possible assignments of the atomic propositions AP (i.e. Σ = 2AP ) and Γ the
set of all possible valuations of the local variables LV (i.e. Γ = DLV ). Let Λ denote the alphabet
b Γ
b and Λ
b denote the alphabets Σ ∪ {>, ⊥}, Γ ∪ {>, ⊥} and Λ ∪ { , }, respectively,
Σ × Γ × Γ. Let Σ,
where , abbreviate (>, >, >) and (⊥, ⊥, ⊥), respectively.
b and u, v, w to denote words over Λ.
b We use
In the sequel we use u, v, w to denote words over Σ
b
b
σ and a to denote a letter in Σ and Λ, respectively.
b (or γ in Γ)
b we use σ (γ) to denote the dual of σ (γ) which is ⊥ if σ (γ)
Given a letter σ in Σ
b is similar, replacing
is >, is > if σ (γ) is ⊥ and is σ (γ) otherwise. The definition of a for a ∈ Λ
with and vice versa. We use v and v to denote the obvious extensions of the definition of dual to
words.
Let v = (σ0 , γ0 , γ00 )(σ1 , γ1 , γ10 ) · · · be a word over Λ. We use v|σ ,v|γ ,v|γ 0 to denote the word
obtained from v by leaving only the first, second or third component, respectively. That is v|σ =
σ0 σ1 · · ·, v|γ = γ0 γ1 · · · and v|γ 0 = γ00 γ10 · · ·. The intuitive roles of the components of a letter are as
follows. The first component of a letter a (i.e. a|σ ) holds the valuation of the atomic propositions at
the given cycle. The second component of a letter a (i.e. a|γ ) holds the current values of the local
variables at the given cycle (the pre-value). The third component of a letter a (i.e. a|γ 0 ) holds the
values of the local variables after the assignments have taken place (the post-value).
We say that v is good if for every i ∈ {0..|v| − 2} we have that either γi+1 ∈ {>, ⊥} or γi+1 = γi0 ,
that is, the pre-value of the local variables at letter i + 1 is the same as the post-value of letter i
(i.e. is the result of the assignments that took place on letter i).
B.3.1.4.0 LVA Semantics of Expressions
The semantics of FL formulas is defined inductively, using as the base case the semantics of expressions. In the case of the lva semantics, we do not have the built-in functions ended(·) and prev(·).
We view an expression e ∈ E over AP ∪LV as a mapping e : Σ×Γ∪{(>, >), (⊥, ⊥)} 7→ D where D is
the domain of variables in LV . Thus, e(σ, γ) denotes the value of expression e under σ ∈ Σ ∪ {>, ⊥}
b we use e(a) to abbreviate e(a|σ , a|γ ). We first
and γ ∈ Γ ∪ {>, ⊥}. For an extended letter a over Λ
discuss the case where a ∈ Λ (that is σ ∈ Σ and γ ∈ Γ), then address the cases where a ∈ { , }
(that is, (σ, γ) ∈ {(>, >), (⊥, ⊥)}).
Let σ ∈ Σ and γ ∈ Γ. When e is an atomic proposition, say e is p for some p ∈ AP , then p(σ, γ)
is equivalent to p ∈ σ. When e is a local variable, say e is z for some z ∈ LV , then z(σ, γ) is the
value given to z by γ. For an atomic proposition p, we abuse the notation by writing p(σ) rather
than p(σ, γ). For a local variable z, we abuse the notation by writing z(γ) rather than z(σ, γ).
We assume t and f are in D. We define true and false to be the Boolean expressions that map
every pair (σ, γ) where σ ∈ Σ and γ ∈ Γ to t and f, respectively.
We assume that operators are closed under D and that they behave in the usual manner,
i.e. that for σ ∈ Σ, γ ∈ Γ, e, e1 , e2 ∈ E, a binary operator ⊗ and a unary operator ◦ we have
e1 (σ, γ) ⊗ e2 (σ, γ) = (e1 ⊗ e2 )(σ, γ) and ◦(e(σ, γ)) = (◦e)(σ, γ). In particular we assume that
Boolean disjunction, conjunction and negation behave in the usual manner.
Regarding the letters > and ⊥, we assume any expression e is evaluated to t on (>, >) and to
f on (⊥, ⊥). That is e(>, >) = t and e(⊥, ⊥) = f for any expression e. Note that in particular
we have true(>, >) = false(>, >) = t and true(⊥, ⊥) = false(⊥, ⊥) = f, and furthermore, even
non-Boolean expressions are mapped to t and f from (>, >) and (⊥, ⊥), respectively.
B.3.1.4.1 LVA Semantics of SEREs
The notation v |≡Z r, where r is an lva sere, v a finite word and Z a set of local variables means
that v models tightly r under the set of controlled variables Z. The semantics of lva seres are
defined as follows, where b denotes a Boolean expression in B–pe , and r, r1 , and r2 denote lva seres,
b and γ ∈ Γ.
b
z a local variable, e, e1 , . . . , en expressions over LV ∪ AP , σ ∈ Σ
For a set of local variables Y = {y1 , . . . , yn } , we denote by ζ(Y) a sequence of assignments
y1 ←e1 , . . . , yn ←en to the variables in Y, and define the valuation [ζ(Y)](σ, γ) recursively as
follows. The base of the definition [z←e](σ, γ) is the valuation γ̃ such that z(γ̃) = e(σ, γ) and
for every local variable y ∈ LV \ {z} we have y(γ̃) = y(γ). In the step of the definition we have
[z←e, ζ(Y)](σ, γ) = [ζ(Y)](σ, γ̃) where γ̃ = [z←e](σ, γ).
Z
b and Z ⊆ LV . We say that γ1 agrees with γ2 relative to Z, denoted γ1 ∼
Let γ1 , γ2 ∈ Γ
γ2 , if for
every z ∈ Z we have z(γ1 ) = z(γ2 ).
1. v |≡Z {r} ⇐⇒ v |≡Z r
Z
2. v |≡Z b ⇐⇒ |v| = 1 and b(v0 )=t and v0|γ 0 ∼ v0|γ
Z ∪Y
3. v |≡Z b, ζ(Y) ⇐⇒ |v| = 1 and b(v0 )=t and v0|γ 0 ∼ [ζ(Y)](v0 )
4. v |≡Z r1 ; r2 ⇐⇒ ∃v1 , v2 such that v = v1 v2 , v1 |≡Z r1 , and v2 |≡Z r2
5. v |≡Z r1 : r2 ⇐⇒ ∃v1 , v2 , a, γ̃ such that v = v1 av2 , v1 ha|σ , a|γ , γ̃i |≡Z r1 and ha|σ , γ̃, a|γ 0 iv2 |≡Z r2
6. v |≡Z r1 | r2 ⇐⇒ v |≡Z r1 or v |≡Z r2
7. v |≡Z r1 && r2 ⇐⇒ v |≡Z r1 and v |≡Z r2
8. v |≡Z [∗0] ⇐⇒ v = ²
9. v |≡Z r[∗] ⇐⇒ either v = ² or ∃v1 , v2 such that v1 6= ², v = v1 v2 , v1 |≡Z r and v2 |≡Z r[∗]
10. v |≡Z {var(z) r} ⇐⇒ v |≡Z ∪ {z} r
11. v |≡Z {free(z) r} ⇐⇒ v |≡Z\{z} r
B.3.1.4.2 LVA Semantics of FL Formulas
b a a basic Boolean expression in B–lv,pe ,
Let w be a possibly empty finite or infinite word over Σ,
b be a valuation of the
r an lva sere, ϕ, ψ lva formulas, and n a non-negative integer. Let γ ∈ Γ
local variables and Z ⊆ LV a set of local variables. The notation hw, γi|=Z ϕ means that the word
w satisfies ϕ under the set of local variables Z with the current valuation of variables γ.
b γ an element of Γ
b and Z a set of local variables. We say that a word
Let w be a word over Σ,
b enhances hw, γi iff w is good, w|σ = w, and if wσ0 ∈
w over Λ
/ {>, ⊥} then w0|γ = γ.
1. hw, γi|=Z (ϕ) ⇐⇒ hw, γi|=Z ϕ
2. hw, γi|=Z ¬ϕ ⇐⇒ hw, γi |=
/Z ϕ
3. hw, γi|=Z ϕ ∧ ψ ⇐⇒ hw, γi|=Z ϕ and hw, γi|=Z ψ
4. hw, γi|=Z r! ⇐⇒ ∃w that enhances hw, γi and ∃j < |w| such that w0..j |≡Z r
5. hw, γi|=Z r ⇐⇒ ∀j < |w|, hw0..j >ω , γi|=Z r!
6. hw, γi|=Z r → ϕ ⇐⇒ ∀w that enhances hw, γi and ∀j < |w|: if w0..j |≡Z r then hwj.. , wj |γ 0 i|=Z ϕ
7. hw, γi|=Z X![n] ϕ ⇐⇒ |w| > n and hwn.. , γi|=Z ϕ
8. hw, γi|=Z ϕ U ψ ⇐⇒ ∃k < |w| such that hwk.. , γi|=Z ψ and ∀j < k, hwj.. , γi|=Z ϕ
9. hw, γi|=Z ϕ async abort a ⇐⇒ either hw, γi|=Z ϕ or ∃j < |w| s.t. a(wj )=t and hw0..j−1 >ω , γi|=Z ϕ
10. hw, γi|=Z ϕ sync abort a ⇐⇒ hw, γi|=Z ϕ async abort a
11. hw, γi|=Z (var(z) ϕ) ⇐⇒ hw, γi|=Z ∪ {z} ϕ
B.3.1.4.3 LVA Semantics With Respect to a Model
Let ϕ be an lva formula and M a model. The notation M |= ϕ means that for all π such that π is
computation path of M , L(π) |=∅ ϕ.
B.3.1.5 Semantics with Everything
In this section we provide semantics of FL formulas. We use the same alphabet and notation as in
the lva semantics, and in addition we define a clock tick as follows.
Let c be a Boolean expression in B–lv . We say that finite word v with past u is a clock tick of
c, denoted tickc (u · v), if |v| > 0 and c(uv0..|v|−1 )=t and for every non-negative integer i < |v| − 1,
c(uv0..i )=f. For an integer m > 0 we say that finite word v with past u is m clock ticks of c,
denoted ticksc (u · v, m), if there exist m words v1 , v2 , . . . , vm such that v = v1 v2 · · · vm and for
every 1 ≤ i ≤ m we have tickc (uv1 · · · vi−1 · vi ).
We say that finite word v with past u is a past clock tick of c, denoted past tickc (u · v), if |v| > 0
and c(uv0 )=t and for every non-negative integer 0 < i < |v|, c(uv0..i )=f (where c(·) refers to the
base semantics of expressions). For an integer m > 0 we say that finite word v with past u is m
past clock ticks of c, denoted past ticksc (u · v, m), if there exist m words v1 , v2 , . . . , vm such that
v = v1 v2 · · · vm and for every 1 ≤ i ≤ m we have past tickc (uv1 · · · vi−1 · vi ).
B.3.1.5.0 Semantics of Expressions
The semantics of expressions (that may refer to the past) over AP ∪ LV maps non-empty words over
b and a clock context to the domain D of local variables. Let u and a be a finite word and a letter
Λ
b respectively. Let c be a boolean expression in B–lv . The semantics of expression e under
over Λ,
clock context c, denoted ec (·), is defined as follows (where e(a) below refers to the lva semantics of
expressions).
• If e ∈ E is an expression without prev(·) or ended(·) then ec (ua) = e(a)
• If r is a sere and c, c1 are Boolean expressions then
c
– endedc (r, c1 )(ua)=t iff there exist u1 , u2 such that u = u1 u2 and u1 · u2 a |≡1 ∅ r
– endedc (r)(ua) = endedc (r, c)(ua)
• If e is an expression and c, c1 Boolean expressions then
½
ec1 (u0..i ) if ∃i < |u| such that past ticksc1 (u0..i−1 · ui..|u|−1 , n + 1)
– prevc (e, n, c1 )(u) =
undefined otherwise.
– prevc (e, n)(u) = prevc (e, n, c)(u)
– prevc (e)(u) = prevc (e, 1, c)(u)
Note that prev(e, n, c)(u) (as well as its derivatives as given in Section B.4.0) is undefined when
u does not contain n + 1 letters on which c holds.
B.3.1.5.1 Semantics of SEREs
b Z ⊆ LV a set of local variables and c a Boolean expression
Let r be a sere, u, v finite words over Λ,
c
in B–lv . The notation u · v |≡Z r means that v models tightly r under the set of controlled variables
Z and clock context c assuming the past is u. The semantics of seres are defined as follows, where
b denotes a Boolean expression in B, c, c1 denote Boolean expressions in B–lv , and r, r1 , and r2
denote seres.
For a set of local variables Y = {y1 , . . . , yn }, we denote by ζ(Y) a sequence of assignments
y1 ←e1 , . . . , yn ←en to the variables in Y, and define the valuation [ζ(Y)]c (ua) recursively as
follows. The base of the definition [z←e]c (ua) is the valuation γ̃ such that z(γ̃) = ec (ua) and for
every local variable y ∈ LV \ {z} we have y(γ̃) = y(a|γ ). In the step of the definition we have
[z←e, ζ(Y)]c (ua) = [ζ(Y)]c (uha|σ , γ̃, a|γ 0 i) where γ̃ = [z←e]c (ua).
Z
b and Z ⊆ LV . We say that γ1 agrees with γ2 relative to Z, denoted γ1 ∼
Let γ1 , γ2 ∈ Γ
γ2 , if for
every z ∈ Z we have z(γ1 ) = z(γ2 ).
c
c
1. u · v |≡Z {r} ⇐⇒ u · v |≡Z r
c
2. u · v |≡Z b ⇐⇒
Z
tickc (u · v) and bc (uv)=t and ∀i < |v| we have vi|γ 0 ∼ vi|γ
c
3. u · v |≡Z b, ζ(Y) ⇐⇒
tickc (u · v) and bc (uv)=t and ∀i < |v − 1| we have vi|γ 0 ∼vi|γ and v|v|−1|γ 0 ∼ [ζ(Y)]c (uv)
Z
Z ∪Y
c
4. u · v |≡Z r1 ; r2 ⇐⇒
c
c
∃v1 , v2 such that v = v1 v2 , u · v1 |≡Z r1 , and uv1 · v2 |≡Z r2
c
5. u · v |≡Z r1 : r2 ⇐⇒
c
c
∃v1 , v2 , a, γ̃ such that v = v1 av2 , u · v1 ha|σ , a|γ , γ̃i |≡Z r1 and uv1 · ha|σ , γ̃, a|γ 0 iv2 |≡Z r2
c
6. u · v |≡Z r1 | r2 ⇐⇒
c
c
u · v |≡Z r1 or u · v |≡Z r2
c
7. u · v |≡Z r1 && r2 ⇐⇒
c
c
u · v |≡Z r1 and u · v |≡Z r2
c
8. u · v |≡Z [∗0] ⇐⇒
v=²
c
9. u · v |≡Z r[∗] ⇐⇒
c
c
either v = ² or ∃v1 , v2 such that v1 6= ², v = v1 v2 , u · v1 |≡Z r and uv1 · v2 |≡Z r[∗]
c
c
10. u · v |≡Z r@c1 ⇐⇒ u · v |≡1 Z r
c
11. u · v |≡Z {var(z) r} ⇐⇒
c
u · v |≡Z ∪ {z} r
c
12. u · v |≡Z {free(z) r} ⇐⇒
c
u · v |≡Z\{z} r
B.3.1.5.2 Semantics of FL Formulas
b w a possibly empty finite or infinite word over Σ,
b ba
Let u be a possibly empty finite word over Λ,
Boolean expression in B, a, c, c1 Boolean expressions in B–lv , r a sere, ϕ, ψ FL formulas, and n a
c
b and Z ⊆ LV a set of local variables. The notation u · hw, γi|=
non-negative integer. Let γ ∈ Γ
Z ϕ
means that the word w satisfies ϕ under the set of local variables Z with the current valuation of
variables γ given the past is u and the clock context is c.
b γ an element of Γ
b and Z a set of local variables. We say that a word w over
Let w be a word over Σ,
b
/ {>, ⊥} then w0|γ = γ. We use hhw, γii to denote
Λ enhances hw, γi iff w is good, w|σ = w, and if wσ0 ∈
the word enhancing hw, γi such that for every j < |w| we have hhw, γiij |γ = hhw, γiij |γ 0 ∈ {γ, >, ⊥}.
c
c
1. u · hw, γi|=Z (ϕ) ⇐⇒ u · hw, γi|=Z ϕ
c
2. u · hw, γi|=Z ¬ϕ ⇐⇒
c
u · hw, γi |=
/Z ϕ
c
3. u · hw, γi|=Z ϕ ∧ ψ ⇐⇒
c
c
u · hw, γi|=Z ϕ and u · hw, γi|=Z ψ
c
4. u · hw, γi|=Z r! ⇐⇒
c
∃w that enhances hw, γi and ∃j < |w| such that u · w0..j |≡Z r
c
5. u · hw, γi|=Z r ⇐⇒
c
∀j < |w|, u · hw0..j >ω , γi|=Z r!
c
6. u · hw, γi|=Z r → ϕ ⇐⇒
c
c
∀w that enhances hw, γi and ∀j < |w|: if u · w0..j |≡Z r then uw0..j−1 · hwj.. , wj |γ 0 i|=Z ϕ
c
7. u · hw, γi|=Z X![n] ϕ ⇐⇒
c
∃j < |w| s.t. ticksc (u · hhw, γii0..j , n + 1) and uhhw, γii0..j−1 · hwj.. , γi|=Z ϕ
c
8. u · hw, γi|=Z ϕ U ψ ⇐⇒
c
∃k < |w| such that c(uhhw, γii0..k )=t and uhhw, γii0..k−1 · hwk.. , γi|=Z ψ and ∀j < k such that
c
c(uhhw, γii0..j )=t we have uhhw, γii0..j−1 · hwj.. , γi|=Z ϕ
c
9. u · hw, γi|=Z ϕ@c1 ⇐⇒
c1
u · hw, γi|=Z ϕ
c
10. u · hw, γi|=Z ϕ async abort a ⇐⇒
c
c
either u · hw, γi|=Z ϕ or ∃j < |w| s.t. ac (uhhw, γiij )=t and u · hw0..j−1 >ω , γi|=Z ϕ
c
11. u · hw, γi|=Z ϕ sync abort a ⇐⇒
c
c
either u · hw, γi|=Z ϕ or ∃j < |w| s.t. (a ∧ c)c (uhhw, γiij )=t and u · hw0..j−1 >ω , γi|=Z ϕ
c
12. u · hw, γi|=Z (var(z) ϕ) ⇐⇒
c
u · hw, γi|=Z ∪ {z} ϕ
B.3.1.5.3 Semantics With Respect to a Model
Let ϕ be an FL formula and M a model. The notation M |= ϕ means that for all π such that π is
true
computation path of M , and for all γ ∈ Γ we have ² · hL(π), γi |= ∅ ϕ.
B.3.2 Semantics of OBE formulas
The semantics of OBE formulas are defined over states in the model, rather than finite or infinite
words. Let f be an OBE formula, M = (S, S0 , R, P, L) a model and s ∈ S a state of the model. The
notation M, s |= f means that f holds in state s of model M . The notation M |= f is equivalent to
∀s ∈ S0 : M, s |= f . In other words, f is valid for every initial state of M .
The semantics of OBE formulas are defined inductively, using as the base case the semantics
of Boolean expressions over letters in 2P . The semantics of Boolean expression is assumed to be
given as a relation
⊆ 2P × B–lv,pe relating letters in 2P with Boolean expressions in B–lv,pe .
If (`, b) ∈
we say that the letter ` satisfies the Boolean expression b and denote it ` b. We
behaves in the usual manner. In particular, that for every
assume that the Boolean relation
letter ` ∈ 2P , atomic proposition p ∈ P and Boolean expressions b, b1 , b2 ∈ B–lv,pe (i) ` p iff p ∈ `,
(ii) ` ¬b iff ` / b, (iii) ` b1 ∧ b2 iff ` b1 and ` b2 , and (iv) ` true and ` / false.
The semantics of an OBE formula are those of standard CTL. The semantics are defined as
follows, where b denotes a Boolean expression and f , f1 , and f2 denote OBE formulas.
1. M, s |= b ⇐⇒ L(s)
b
2. M, s |= (f ) ⇐⇒ M, s |= f
3. M, s |= ¬f ⇐⇒ M, s 6|= f
4. M, s |= f1 ∧ f2 ⇐⇒ M, s |= f1 and M, s |= f2
5. M, s |= EX f ⇐⇒ there exists a computation path π of M such that |π| > 1, π0 = s, and
M, π1 |= f
6. M, s |= E[f1 U f2 ] ⇐⇒ there exists a computation path π of M such that π0 = s and there
exists k < |π| such that M, πk |= f2 and for every j such that j < k: M, πj |= f1
7. M, s |= EG f ⇐⇒ there exists a computation path π of M such that π0 = s and for every j
such that 0 ≤ j < |π|: M, πj |= f
B.4 Syntactic Sugaring
The remainder of the temporal layer is syntactic sugar. In other words, it does not add expressive
power, and every piece of syntactic sugar can be defined in terms of the basic operators presented
above. The syntactic sugar is defined below.
NOTE −
The definitions given here do not necessarily represent the most efficient implementation. In some cases,
there is an equivalent syntactic sugaring, or a direct implementation, that is more efficient.
B.4.1 Additional Boolean expressions
Let b ∈ B and e ∈ E. Then additional Boolean operators can be viewed as abbreviations of the basic
Boolean operators given in Definition 1, as follows:
def
• rose(b) = ¬prev(b) ∧ b
def
• rose(b, c) = ¬prev(b, c) ∧ b ∧ c
def
• f ell(b) = prev(b) ∧ ¬b
def
• f ell(b, c) = prev(b, c) ∧ ¬b ∧ c
def
• stable(e) = prev(e) = e
def
• stable(e, c) = prev(e, c) = e ∧ c
B.4.2 Additional SEREs
We regard a procedural block as mechanism for both calculating a set of expressions and assigning
them to a set of local variables which are given to the procedural block as inputs. Formally,
• f (z1 , . . . , zn ) where f is a procedural block and z1 , . . . , zn are a local variables is interpreted
as an abbreviation to the sequence of assignments z1 ←ef1 , . . . , zn ←efn where ef1 , . . . , efn are
expressions corresponding to intermediate calculations of f .
B.4.3 Additional SERE operators
Let i, j, k, and l be integer constants such that i ≥ 0, j ≥ i, k ≥ 1, l ≥ k. Then additional
SERE operators can be viewed as abbreviations of the basic SERE operators given in Definition 2,
as follows, where b denotes a boolean expression, and r denotes a SERE.
def
• r[+] = r; r[∗]
def
• r[∗0] = [∗0]
k times
def z }| {
• r[∗k] = r; r; ...; r
def
• r[∗i..j] = r[∗i] | ... | r[∗j]
def
• r[∗i..] = r[∗i]; r[∗]
def
• r[∗..i] = r[∗0] | ... | r[∗i]
def
• r[∗..] = r[∗0..]
def
• [+] = true[+]
def
• [∗] = true[∗]
def
• [∗i] = true[∗i]
def
• [∗i..j] = true[∗i..j]
def
• [∗i..] = true[∗i..]
def
• [∗..i] = true[∗..i]
def
• [∗..] = true[∗..]
def
• b[= i] = {¬b[∗]; b}[∗i]; ¬b[∗]
def
• b[= i..j] = b[= i] | ... | b[= j]
def
• b[= i..] = b[= i]; [∗]
def
• b[= ..i] = b[= 0] | ... | b[= i]
def
• b[= ..] = b[= 0..]
def
• b[→] = ¬b[∗]; b
def
• b[→ k] = {¬b[∗]; b}[∗k]
def
• b[→ k..l] = b[→ k] | ... | b[→ l]
def
• b[→ k..] = b[→ k] | {b[→ k]; [∗]; b}
def
• b[→ ..k] = b[→ 1] | ... | b[→ k]
def
• b[→ ..] = b[→ 1..]
def
• skip = {free(LV ) true}
def
• r1 & r2 = { {r1 ; skip[∗]} && r2 } | { r1 && {r2 ; skip[∗]} }
def
• r1 within r2 = {[∗]; r1 ; [∗]} && {r2 } Check it now that we have local variables free etc.
def
• {var(z←e) r} = {var(z) {{true, z ← e} : r} | {[∗0] && r}}
B.4.4 Additional FL operators
Let i, j, k and l are integers such that i ≥ 0, j ≥ i, k > 0 and l ≥ k. Then additional FL operators
can be viewed as abbreviations of the basic operators given in Definition 3, as follows, where b
denotes a boolean expression, r, r1 , and r2 denote SEREs, and ϕ, ϕ1 , and ϕ2 denote FL formulas.
def
• ϕ1 ∨ ϕ2 = ¬(¬ϕ1 ∧ ¬ϕ2 )
def
• ϕ1 → ϕ2 = ¬ϕ1 ∨ ϕ2
def
• ϕ1 ↔ ϕ2 = (ϕ1 → ϕ2 ) ∧ (ϕ2 → ϕ1 )
def
• X!ϕ = X![1] ϕ
def
• Xϕ = X[1] ϕ
def
• X[i]ϕ = ¬X![i] ¬ϕ
def
• Fϕ = true U ϕ
def
• Gϕ = ¬F¬ϕ
def
• ϕ1 W ϕ2 = (ϕ1 U ϕ2 ) ∨ Gϕ1
def
• always ϕ = G ϕ
def
• never ϕ = G ¬ϕ
def
• next! ϕ = X! ϕ
def
• next ϕ = X ϕ
def
• eventually! ϕ = Fϕ
def
• ϕ1 until! ϕ2 = ϕ1 U ϕ2
def
• ϕ1 until ϕ2 = ϕ1 W ϕ2
def
• ϕ1 until! ϕ2 = ϕ1 U (ϕ1 ∧ ϕ2 )
def
• ϕ1 until ϕ2 = ϕ1 W (ϕ1 ∧ ϕ2 )
def
• ϕ1 bef ore! ϕ2 = (¬ϕ2 ) U (ϕ1 ∧ ¬ϕ2 )
def
• ϕ1 bef ore ϕ2 = (¬ϕ2 ) W (ϕ1 ∧ ¬ϕ2 )
def
• ϕ1 bef ore! ϕ2 = (¬ϕ2 ) U ϕ1
def
• ϕ1 bef ore ϕ2 = (¬ϕ2 ) W ϕ1
def
• next![i] ϕ = X![i] ϕ
def
• next[i] ϕ = X[i] ϕ
def
• next a![i..j]ϕ = (X![i]ϕ) ∧ . . . ∧ (X![j]ϕ)
def
• next a[i..j]ϕ = (X[i]ϕ) ∧ . . . ∧ (X[j]ϕ)
def
• next e![i..j]ϕ = (X![i]ϕ) ∨ . . . ∨ (X![j]ϕ)
def
• next e[i..j]ϕ = (X[i]ϕ) ∨ . . . ∨ (X[j]ϕ)
def
• next event!(b)(ϕ) = (¬b) U b ∧ ϕ
def
• next event(b)(ϕ) = (¬b) W (b ∧ ϕ)
k−1 times
z
}|
{
• next event!(b)[k](ϕ) = next event!(b) (X! next event!(b)...(X! next event!(b)(ϕ))...)
def
k−1 times
z
}|
{
• next event(b)[k](ϕ) = next event(b) (Xnext event(b)...(Xnext event(b)(ϕ))...)
def
def
• next event a!(b)[k..l](ϕ) = next event!(b)[k](ϕ) ∧ ... ∧ next event!(b)[l](ϕ)
def
• next event a(b)[k..l](ϕ) = next event(b)[k](ϕ) ∧ ... ∧ next event(b)[l](ϕ)
def
• next event e!(b)[k..l](ϕ) = next event!(b)[k](ϕ) ∨ ... ∨ next event!(b)[l](ϕ)
def
• next event e(b)[k..l](ϕ) = next event(b)[k](ϕ) ∨ ... ∨ next event(b)[l](ϕ)
def
• r(ϕ) = r → ϕ
def
• r ⇒ ϕ = {r; true} → ϕ
def
• ϕ abort b = ϕ async abort b
B.4.5 Parameterized SEREs and Formulas
Let r be a sere, and l, m integers. Let S be a set of constants, integers or boolean values and p an
identifier. The left hand side of the following are seres, equivalent to the seres on the right hand
side.
def
• for p in S : | r =
| {r[p ← s]}.
s∈S
def
• for phl..mi in S : | r =
| ...
| {r[phl..mi ← hsl ..sm i]}
sl ∈S
def
• for p in S : && r =
&& {r[p ← s]}.
s∈S
def
• for phl..mi in S : && r =
def
• for p in S : & r =
sm ∈S
&& . . . && {r[phl..mi ← hsl ..sm i]}
sl ∈S
sm ∈S
& {r[p ← s]}.
s∈S
def
• for & phl..mi in S : & r =
& ...
sl ∈S
& {r[phl..mi ← hsl ..sm i]}
sm ∈S
Where r[p ← s] is the sere obtained from r by replacing every occurrence of p by s and r[phl..mi ←
hsl ..sm i] is the sere obtained from r by replacing every occurrence of pj with sj for all j such that
l ≤ j ≤ m.
Let ϕ be an FL formula, and l, m integers. Let S be a set of constants, integers or boolean
values and p an identifier. The left hand side of the following are FL formulas equivalent to the FL
formulas on the right hand side.
def
• for p in S : ∨ ϕ =
_
ϕ[p ← s]
s∈S
def
• for phl..mi in S : ∨ ϕ =
_
...
sl ∈S
def
• for p in S : ∧ ϕ =
^
_
ϕ[phl..mi ← hsl ..sm i]
sm ∈S
ϕ[p ← s]
s∈S
def
• for phl..mi in S : ∧ ϕ =
^
sl ∈S
...
^
ϕ[phl..mi ← hsl ..sm i]
sm ∈S
def
• forall p in S : ϕ = for p in S : ∧ ϕ
def
• forall phl..mi in S : ϕ = for phl..mi in S : ∧ ϕ
where ϕ[p ← s] is the formula obtained from ϕ by replacing every occurrence of p by s and
ϕ[phl..mi ← hsl ..sm i] is the formula obtained from ϕ by replacing every occurrence of pj with
sj for all j such that l ≤ j ≤ m.
B.4.6 Additional OBE operators
Let f, f1 , f2 denote OBE formulas. Then additional OBE operators can be derived from the basic
OBE operators given in Definition 4 as follows:
• f1 ∨ f2 = ¬(¬f1 ∧ ¬f2 )
• f1 → f2 = ¬f1 ∨ f2
• f1 ↔ f2 = (f1 → f2 ) ∧ (f2 → f1 )
• EFf = E[true U f ]
• AXf = ¬EX¬f
• A[f1 U f2 ] = ¬(E[¬f2 U (¬f1 ∧ ¬f2 )] ∨ EG¬f2 )
• AGf = ¬E[true U ¬f ]
• AFf = A[true U f ]
B.5 Rewriting rules for clocks
In Section B.3.1.2 we gave the semantics of clocked FL formulas directly. There is an equivalent
definition in terms of FL formulas without clocks, as follows: Starting from the outermost clock, use
the following rules to translate clocked SEREs into unclocked SEREs, and clocked FL formulas into
unclocked FL formulas.
The rewrite rules for SEREs are:
1. Rc ({r}) = Rc (r)
2. Rc (b) = ¬c[∗]; c ∧ b
3. Rc (b, ζ(Y)) = ¬c[∗]; c ∧ b, ζ(Y)
4. Rc (r1 ; r2 ) = Rc (r1 ) ; Rc (r2 )
5. Rc (r1 : r2 ) = {Rc (r1 )} : {Rc (r2 )}
6. Rc (r1 | r2 ) = {Rc (r1 )} | {Rc (r2 )}
7. Rc (r1 && r2 ) = {Rc (r1 )} && {Rc (r2 )}
8. Rc ([∗0]) = [∗0]
9. Rc (r[∗]) = {Rc (r)}[∗]
10. Rc (var(z) r) = {var(z) Rc (r)}
11. Rc (free(z) r) = {free(z) Rc (r)}
12. Rc (r@c1 ) = Rc1 (r)
The rewrite rules for FL formulas are:
1. F c ((ϕ)) = (F c (ϕ))
2. F c (¬ϕ) = ¬F c (ϕ)
3. F c (ϕ ∧ ψ) = (F c (ϕ) ∧ F c (ψ))
4. F c (r!) = Rc (r)!
5. F c (r) = Rc (r)
6. F c (r → ϕ) = Rc (r) → F c (ϕ)
7. F c (X!ϕ) = (¬c U (c ∧ X! (¬c U (c ∧ F c (ϕ)))))
8. F c (ϕ U ψ) = ((c → F c (ϕ)) U (c ∧ F c (ψ)))
9. F c (ϕ async abort b) = F c (ϕ) async abort b
10. F c (ϕ sync abort b) = F c (ϕ) sync abort (b ∧ c)
11. F c (var(z) ϕ) = var(z) F c (ϕ)
12. F c (ϕ@c1 ) = F c1 (ϕ)
Acknowledgments
We would like to thank Shoham Ben-David, John Havlicek, Erich Marschner, Johann Mårtensson,
Avigail Orni, Dmitry Pidan and Sitvanit Ruah for many interesting discussions on the subject of
local variables. Special thanks to Avigail Orni for important comments on an early version of the
lva semantics.
References
[B1] EFHLMV03 - Reasoning with temporal logic over truncated paths
[B2] EFHMV03- The definition of a temporal clock operator
[B5] EFHM06 - The >, ⊥ approach for truncated semantics
[B6] EFH05 – A topological characterization of weakness
[B7] Fis07 – On the characterization of until as a fixed point under clocked semantics