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

## No comments:

Post a Comment