Tutorial T3
Decision Diagrams for Logic and Stochastic Modeling
Gianfranco Ciardo
(Univ. of California at Riverside, USA)
Duration: 180 minutes
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.
Web Maintenance Person.