Seminars

Exploiting Model Structure to Encode Transition Relations and Transition Rate Matrices PDF
Gianfranco Ciardo - Department of Computer Science and Engineering, Bourns College of Engineering, University of California at Riverside

05/14/2012 – 2pm, GHC 8102.

Abstract

High-level formalisms (such as Petri nets, pseudo-code, or interacting finite-state machines) can compactly describe enormous "flat models". Fortunately, the structure of the state for such models can be exploited to achieve compact encodings for both the state space and the transition relation (in case of logic analysis) or the transition rate matrix (in case of Markov analysis).

BDDs and extension have been used for logic analysis, while Kronecker operators have been initially proposed for Markov analysis, although decision-diagram approaches are now being increasingly adopted. We present a unified view of the two approaches, and show how the best of both worlds can be obtained by merging their key advantages, namely the compactness and generality of decision diagrams and the effectiveness of Kronecker operators at modeling semi-independent behavior.

We then survey algorithms to manage Markov models whose transition rate matrix is structurally encoded, discuss their main advantages and overheads, and present a few new results on exact and approximate solutions.

Biography

Gianfranco Ciardo is a Professor in the Department of Computer Science and Engineering at the University of California, Riverside. Previously, he has been on the faculty at the College of William and Mary, Williamsburg, Virginia, a Visiting Professor at the University of Torino, Italy, and at the Technical University of Berlin, Germany, and has held research positions at HP Labs (Palo Alto, California), ICASE (NASA Langley
Research Center, Hampton, Virginia), Software Productivity Consortium (Herndon, Virginia), and CSELT (Torino, Italy).

He received a Laurea from the University of Torino, Italy, and a PhD from Duke University.  He has been on the editorial board of IEEE Transactions on Software Engineering and is on the editorial board of Transactions on Petri Nets and Other Models of Concurrency. He was keynote speaker at PNPM'01, ATPN'04, EPEW/WS-FM'05, and PDMC 2009. He is interested in algorithms and tools for logic and stochastic analysis of discrete-state models, symbolic model checking, performance and reliability evaluation of complex hardware/software systems, Petri nets, and Markov models.