Reference 1
References: Lecture 7, Computation Tree Logics Path Quantifier $A$: for every path. $E$: there exists a path. Linear-time operators $\boldsymbol{X}_p$: $p$ holds next time. $\boldsymbol{F}_p$: $p$ holds sometime in the future. $\boldsymbol{G}_p$: $p$ holds globally in the future. $p\boldsymbol{U}q$: $p$ holds until $q$ holds. Path Formulas and State Formulas More
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?