Abstract:
SELENE is a recently proposed voting protocol that provides reasonable
protection against coercion. Both verifiability and security of Selene
are based on cryptographic machinery applied to the concept of tracking
numbers assigned to votes. In this paper, we make the first step towards
a formalization of selected features of the protocol by means of
formulae and models of multi-agent logics. The models define the space
of strategies for the voters, the election authority, and the potential
coercer. We express selected properties of the protocol using the
strategic logic ATLir, and conduct preliminary verification by model
checking. While ATLir allows for intuitive specification of requirements
like coercion-resistance, model checking of ATLir is notoriously hard.
We show that some of the complexity can be avoided by using a recent
approach of approximate model checking, based on fixpoint approximations.

Camille Coti, Sami Evangelista, Laure Petrucci: One-Sided Communications and Distributed State Compression for Distributed Model-Checking

Abstract:
Communications are often the bottleneck in distributed state space exploration. To overcome this problem and benefit from the distributed model-scheme, we propose to use one-sided communications. We thus revisit the state of the art distributed algorithm and adapt it to RDMA clusters with an implementation over the OpenSHMEM library. Experiments conducted on the Grid'5000 cluster show that this asynchronous approach reduces the significant communication costs induced by process synchronisation in two-sided communications.
To further improve distributed model checking, we propose a distributed implementation of the collapse compression technique used by explicit state model checkers to reduce memory usage. This adapatation makes use of lock-free distributed hash tables based on one-sided communication primitives. The experiments reveal that, for some models, this distributed implementation can altogether preserve the memory reduction provided by collapse compression and reduce execution times by allowing the exchanges of compressed states between processes.

Streszczenie:
Na bazie analizy głosowań jury w finale ostatniego konkursu Wieniawskiego powstała pewna metoda głosowania, która ma na celu ograniczyć manipulacje jurorów. Najpierw jurorzy głosują metodą Bordy, potem wyznaczana jest dla każdego uczestnika średnia punktacja jurorów. Następnie dla każdego jurora oblicza się odległość (według metryki "Manhattan" – ulicowej) jego punktacji od punktacji średniej i 20% (zaokrąglenia w dół) jurorów najbardziej odległych od średniej zostaje odrzuconych (ich nazwiska podaje się do wiadomości publicznej lub nie), a wynik się oblicza używając tylko punktacji pozostałych. Ta metoda ma dobre antymanipulacyjne własności, co potwierdzają rozważania teoretyczne i eksperymenty. W eksperymentach sprawdzono, jak manipulują respondenci używając różnych wariantów tej metody. Rozważania teoretyczne wskazują na wyższość tej metody w stosunku do metody polegającej na odrzucaniu skrajnych wyników. Problemem otwartym jest aksjomatyzacja. Powstaje pytanie, czy rzeczywiście zdarzają się kliki jurorów. Do odpowiedzi na to pytanie próbujemy wykorzystać teorię sieci.