Title: Theory / Unimportant / CS / Softw / MightL
Tags: FromInstruction computer_to_instruction hasNotNewEffectReturnsMeaning
On every note of this deck, unless a note says otherwise:
Page: http://depinf-pc5.ulb.ac.be/~mightyl/#syntax

Instruction: G I phi
Effect: phi must hold at all positions that occur after a duration in I from now

Instruction: F I phi
Effect: phi must hold at some positions that occur after a duration in I from now

Instruction: phi1 U I phi2
Effect: formula phi1 must hold in all positions until phi2 holds, and that this position where phi2 holds must occur after a duration in I from now.

Instruction: X I phi
Effect: Formula phi must hold in the next position, which occurs after a duration in I from now.
Assuming: Pointwise semantic

Instruction: \(\phi_1 \parallel \phi_2\)
Effect: Some \(\phi_j\) holds
Assuming: Pointwise semantic

Instruction: phi_1 && phi_2
Effect: Both phi_i holds
Assuming: Pointwise semantic

Instruction: ! phi
Effect: phi does not holds
Assuming: Pointwise semantic

Instruction: phi1->phi2
Effect: if phi1 holds, then phi2 holds

Instruction: infty
Effect: the infinity bound