Title: Asynchronous Announcements
Abstract: We propose a logic of asynchronous announcements, where truthful announcements are publicly sent but individually received by agents. Additional to epistemic modalities, the logic therefore contains two types of dynamic modalities, for sending messages and for receiving messages. There are various results to report. For example, we show that on multi-agent epistemic models, each formula in asynchronous announcement logic is equivalent to a formula in epistemic logic.
Title: How to Save Democracy, or, Towards Model Checking of E-Voting Protocols in Alternating-time Temporal Logic
Abstract: Properties of receipt-freeness, coercion resistance, and voter verifiability refer to the existence (or nonexistence) of an appropriate strategy for the voter, the coercer, or both. One can try to specify such properties by formulae of a suitable strategic logic, such as Alternating-time Temporal Logic (ATL). However, automated verification of strategic properties in scenarios with partial observability is notoriously hard, and novel techniques are needed to overcome the complexity. I will start with an overview of the relevant properties, show how they can be specified in ATL, and present some novel results for model checking ATL with partial observability that we have obtained in the Polish-Luxembourgish project VoteVerif.