activity
20072026
most citedStrategy Logic with Imperfect Information

35 citations · 102 across the 24 of their papers we have counts for

collaborators

27 papers

cs.AI2026

FONDANT: Strong and Best-Effort Planning via Antichains

Benjamin Aminof, Tuan Khai Nguyen, Sasha Rubin

A classical solution concept in fully observable nondeterministic (FOND) planning, is the strong policy (aka winning strategy in the closely related area of reactive synthesis), i.…

cs.LO2026

Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems

Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin

Traditional model-checking techniques typically verify distributed algorithms only for a fixed number of finite-state processes. Parameterized model checking generalizes this to an…

cs.LO2024

LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces

Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin +1

We introduce LTLf+ and PPLTL+, two logics to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+…

cs.LO2023

Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems

Benjamin Aminof, Sasha Rubin, Francesco Spegni +1

We study the complexity of the model-checking problem for parameterized discrete-timed systems with arbitrarily many anonymous and identical processes, with and without a distingui…

cs.LO2023

LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties

Benjamin Aminof, Giuseppe De Giacomo, Antonio Di Stasio +3

In this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks…

cs.AI2021★ 1 cited

Sufficient reasons for classifier decisions in the presence of constraints

Niku Gorji, Sasha Rubin

Recent work has unveiled a theory for reasoning about the decisions made by binary classifiers: a classifier describes a Boolean function, and the reasons behind an instance being…