Events at MS Teams

GPUexplore is a tool that exploits the computational power of graphics processors to efficiently construct state spaces, and on-the-fly check safety and liveness properties. Its current main practical limitation, though, is related to its input language. The tool accepts networks of Labelled Transition Systems, which were initially useful to test whether state space could be …continue reading

What is the structure of a transition system that represent the behaviour of processes? We assumed that it was just an ordinary random graph, but got odd results when predicting the sizes of state spaces generated by lps2lts. Viewing state spaces as parallel non-communicating random state spaces gave far better results. This also helps in …continue reading

Mutual exclusion algorithms such as Peterson’s, make sure only a single thread can be present in the exclusive section at a given time. Similarly, a shared-exclusive lock also provides a shared section, in which any number of threads can be present, but only if no thread is present in the exclusive section. In this talk, …continue reading

Two optimizations for Zielonka’s recursive algorithm for solving parity games are investigated. The first optimization is partial re-decomposition, in which only the part of the graph containing vertices of SCCs which have 1 or more vertices removed will be re-decomposed. The second optimization is dynamic SCC maintenance, which builds an SCC tree for each SCC …continue reading

It is well known that Peterson’s algorithm for two processes is starvation free. In this talk I study the generalization of Peterson’s algorithm to N>2 processes using tournament trees. In particular, I will show how, contrary to the two processes version, this algorithm is not starvation free if we do not make any fairness assumptions. …continue reading