Index
Algorithmic verification
model checking, Model checking
Bounded model checking
Branching temporal logic
CTL
CTL*
Büchi Automata
acceptance
basis for model checking
definition
emptiness check
product
from PTL formulae
Classical logic
first-order, First-order logic
intuition
propositional, Propositional logic
Clausal resolution
binary resolution
first-order logic
first-order substitution
hyperresolution
input resolution
linear resolution
logic programming
ordered resolution
refutation
resolution rule
set of support
temporal, Clausal temporal resolution
unit resolution
Clausal temporal resolution
implementation, TSPASS System
overview
step resolution, Step resolution
temporal resolution, Temporal resolution
CNF
first-order
propositional
Communication between programs
broadcast
channels
message-passing
multicast
shared variables
Computational complexity
model checking
validity
Concurrency
asynchronous execution
interleaving
synchronous execution
true concurrency
Concurrent MetateM System
basic invocation
beliefs
benefits and drawbacks
communication
concurrency
Concurrent MetateM System (continued)
content and context
deliberation
embedded Java
meta-level control
multi-agent systems
organizations
rule syntax
theory, Temporal execution, MetateM
CTL, Branching temporal logic, CTL
CTL*, Branching temporal logic, CTL*
Deduction
automation
DNF
propositional
Executable temporal logic, Temporal execution
Finite-State Automata
accepting finite strings
accepting infinite strings, Büchi ...
