activity
20112022
most citedProperty-Directed Verification of Recurrent Neural Networks

5 citations · 9 across the 4 of their papers we have counts for

collaborators
Showing cs.LOShow all

6 papers · 1 filter

cs.LO20221 cited

On the Existential Fragments of Local First-Order Logics with Data

Benedikt Bollig, Arnaud Sangnier, Olivier Stietel

We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain which can be compared wrt. equality. As the satisfi…

cs.LO2020

Erratum to "Frequency Linear-time Temporal Logic"

Benedikt Bollig, Normann Decker, Martin Leucker

We correct our proof of a theorem stating that satisfiability of frequency linear-time temporal logic is undecidable [TASE 2012].

cs.LO2018

It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"

Benedikt Bollig, Marie Fortin, Paul Gastin

Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO…

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.