59 citations · 138 across the 23 of their papers we have counts for
18 papers · 1 filter
Deciding the Common Fragment of CTL with Past and LTL
Massimo Benerecetti, Dario Della Monica, Angelo Matteo +2
A central goal of language theory is to compare formalisms by understanding their relative expressive power. One challenging question in this direction is the problem of determinin…
Common Foundations for Recursive Shape Languages
Shqiponja Ahmetaj, Iovka Boneva, Jan Hidders +9
As schema languages for RDF data become more mature, we are seeing efforts to extend them with recursive semantics, applying diverse ideas from logic programming and description lo…
Automaton-based Characterisations of First Order Logic over Infinite Trees
Massimo Benerecetti, Dario Della Monica, Angelo Matteo +2
We study the expressive power of First-Order Logic (\FO) over (unordered) infinite trees, with the aim of identifying robust characterisations in terms of branching-time specificat…
An Automaton-based Characterisation of First-Order Logic over Infinite Trees
Massimo Benerecetti, Dario Della Monica, Angelo Matteo +2
In this paper, we study First Order Logic (FO) over (unordered) infinite trees and its connection with branching-time temporal logics. More specifically, we provide an automata-the…
Automata-Theoretic Characterisations of Branching-Time Temporal Logics
Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero +1
Characterisations theorems serve as important tools in model theory and can be used to assess and compare the expressive power of temporal languages used for the specification and…
Alternating (In)Dependence-Friendly Logic
Dylan Bellier, Massimo Benerecetti, Dario Della Monica +1
Hintikka and Sandu originally proposed Independence Friendly Logic (IF) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantic…
Quantifying over Trees in Monadic Second-Order Logic
Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero +1
Monadic Second-Order Logic (MSO) extends First-Order Logic (FO) with variables ranging over sets and quantifications over those variables. We introduce and study Monadic Tree Logic…
Good-for-Game QPTL: An Alternating Hodges Semantics
Dylan Bellier, Massimo Benerecetti, Dario Della Monica +1
An extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the fut…
SHACL Satisfiability and Containment (Extended Paper)
Paolo Pareti, George Konstantinidis, Fabio Mogavero +1
The Shapes Constraint Language (SHACL) is a recent W3C recommendation language for validating RDF data. Specifically, SHACL documents are collections of constraints that enforce pa…
From Quasi-Dominions to Progress Measures
Massimo Benerecetti, Daniele Dell'Erba, Marco Faella +1
We revisit the approaches to the solution of parity games based on progress measures and show how the notion of quasi dominions can be integrated with those approaches. The idea is…
Solving Mean-Payoff Games via Quasi Dominions
Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero
We propose a novel algorithm for the solution of mean-payoff games that merges together two seemingly unrelated concepts introduced in the context of parity games, small progress m…
Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games
Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero
The McNaughton-Zielonka divide et impera algorithm is the simplest and most flexible approach available in the literature for determining the winner in a parity game. Despite its t…
Reasoning about Strategies: on the Satisfiability Problem
Fabio Mogavero, Aniello Murano, Giuseppe Perelli +1
Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-…
Cycle Detection in Computation Tree Logic
Gaëlle Fontaine, Fabio Mogavero, Aniello Murano +2
Temporal logic is a very powerful formalism deeply investigated and used in formal system design and verification. Its application usually reduces to solving specific decision prob…
On the Remarkable Features of Binding Forms
Fabio Mogavero, Giuseppe Perelli
Hilbert's Entscheidungsproblem has given rise to a broad and productive line of research in mathematical logic, where the classification process of decidable classes of first-order…
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
Petr Čermák, Alessio Lomuscio, Fabio Mogavero +1
We introduce MCMAS-SLK, a BDD-based model checker for the verification of systems against specifications expressed in a novel, epistemic variant of strategy logic. We give syntax a…
A Decidable Fragment of Strategy Logic
Fabio Mogavero, Aniello Murano, Giuseppe Perelli +1
Strategy Logic (SL, for short) has been recently introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects,…
Reasoning About Strategies: On the Model-Checking Problem
Fabio Mogavero, Aniello Murano, Giuseppe Perelli +1
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the syste…