About Me

Friday, August 22, 2008

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

0 comments: