3 papers
cs.LO2017
Communicating Finite-State Machines and Two-Variable Logic
Benedikt Bollig, Marie Fortin, Paul Gastin
Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they ar…
cs.LO2015
An Automata-Theoretic Approach to the Verification of Distributed Algorithms
C. Aiswarya, Benedikt Bollig, Paul Gastin
We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes coop…
cs.LO2011
An optimal construction of Hanf sentences
Benedikt Bollig, Dietrich Kuske
We give the first elementary construction of equivalent formulas in Hanf normal form. The triply exponential upper bound is complemented by a matching lower bound.