
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 discretestate models, Petri nets,
temporal logic, and Markov chains, we start with binary decision diagrams,
widely used for statespace 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 edgevalued decision diagrams, and use them to encode a state indexing
function or a distance function, and to real multiterminal decision diagrams,
edgevalued decision diagrams, Kronecker algebra, and matrix diagrams,
and use them to encode the transition rate matrix of a CTMC.
 