Seminar: Facets for partial order methods

Post date: 02-Jul-2012 08:28:03

Upcoming Seminar

Facets for partial order methods

July 2nd, 18.30

Aula C, Palazzo delle Scienze - Cagliari

Tobias Heindel

CEA Saclay Nano-INNOV, Institut CARNOT CEA LIST, DILS/LMEASI

Abstract. Persistent sets are a cornerstone of "classical" Partial Order Reduction: they are typically used in deadlock detection to reduce the explored state space of a concurrent system; however, they need to be combined with additional methods (such as sleep sets) to avoid state space explosion. One seemingly trivial but crucial fact is that any persistent singleton, which contains one transition that will remain enabled no matter what happens, is in fact "inessential" in a certain technical sense as described in Goubault's work on geometric models of concurrency -- inspired by (directed) algebraic topology.

The simple idea is to eliminate all of these "pesistent" transitions "directly" to avoid the state space explosion. In fact, we can render models of asynchronous concurrent systems more compact by "quotienting out" all persistent singletons. The talk illustrates the crucial ideas of persistent singletons and describes the quotient construction for the case of occurrence nets where it yields very intuitive results. Finally, the compression potential of this quotient construction is illustrated by a comparison with Haar's facet abstraction.