| |
| Decision Diagrams for Logic and Stochastic Modeling |
Gianfranco Ciardo
(Univ. of California at Riverside, USA)
|
| Duration: 180 minutes |
ABSTRACT:
We provide an introduction to decision diagrams and their applications to
verification and stochastic modeling, showing how structured representations
can reduce the memory and time required to analyize a system.
After covering some background notions on discrete-state models, Petri nets,
temporal logic, and Markov chains, we start with binary decision diagrams,
widely used for state-space generation and temporal logic model checking.
Their extension to multiway nodes (MDDs) is shown to be a natural match
to a Kronecker algebra encoding of the transition relation. We then move to
integer edge-valued decision diagrams, and use them to encode a state indexing
function or a distance function, and to real multiterminal decision diagrams,
edge-valued decision diagrams, Kronecker algebra, and matrix diagrams,
and use them to encode the transition rate matrix of a CTMC.
| |