Abstract: In the model checking, state spaces are either represented explicitly or symbolically. Although the latter has the potential to compact the representation of a system, efficiently distributing symbolic states or parallelizing computation can be hard. On the contrary, the explicit techniques allow to distribute a state space in a straightforward way. Still, the nature of algorithms that execute over a distributed state space might be inherently sequential. In this talk, algorithms for explicit state LTL model checking and the partial order reduction – explicit state space reduction technique – are examined in order to evaluate their potential for parallelizing their computation.

Jiri Simsa received his BSc. and Msc. in Computer Science from the Masaryk University. During his studies there he published several papers on distributed techniques for explicit state model checking. After finishing his master studies, he was awarded the Fulbright Science and Technology Award, an incentive to study at a university in the US. Currently, Jiri is pursuing a Ph.D. at the Carnegie Mellon University under the guidance of professors Randy Bryant and Garth Gibson. Appointments: dcm@cs.cmu.edu