CompSys705

Verification up to now has been implementation verification. Now into the design or property verification.

Static logics stay fixed over time. Dynamic logic is temporal and is dependent on time, modal logic.

Proposition

Statement that is true or false. Formula: a statement built from symbols.

Propositional logic

A set of propositions and a set of connectives. Every proposition is a formula.

Predicate

Verb and its complement.

Predicate logic

Made of predicate symbols, constant symbols, variables, function symbols and connectives. Atom is the simplest predicate formula.

Logic based verification. Kripke structure = < Q, q, Atomic Propositions, ->, L>. Labeling function assigns outputs to states. Transition relation is total to imply no dead locking states. A path is such that a state is related to another state.

Computational tree logic

A tree that starts from a state and keeps building as paths continue to be taken. Basically a graph unrolled in time.

Linear temporal logics

Going up a tree

Branching time logics

Going down the tree.

Temporal operators

X: next time, F: future, G: global, U: until.

Path quantifiers

E: existential, A: universal.

Every term must be preceded by a path quantifier to be considered CTL.

Composed and transmitted from my iPod Touch