Marco Faella

I&C Journal 2026 Journal Article

Verifying Linear Temporal Properties on Polyhedral Systems: Decidability and Symbolic Algorithms

• Massimo Benerecetti
• Marco Faella
• Fabio Mogavero

We study the problem of model checking linear temporal logic formulae on finite trajectories generated by polyhedral differential inclusions, thus enriching the landscape of models where such specifications can be effectively verified. Each model in the class comprises a static and a dynamic component. The static component features a finite set of observables represented by (non-necessarily convex) polyhedra. The dynamic one is given by a convex polyhedron constraining the dynamics of the system, by specifying the possible slopes of the trajectories in each time instant. We devise an exact algorithm that computes a symbolic representation of the region of points that existentially satisfy a given formula φ, i. e. , the points from which there exists a trajectory satisfying φ.

ECAI Conference 2025 Conference Paper

Convex Optimization Yields Empirically Superior Best-Arm Identification

• Marco Faella
• Francesco Magliocca
• Luigi Sauro

We introduce a novel approach (COpt) to Fixed-Budget Best-Arm Identification (FBBAI) specifically designed for contexts where both the expected rewards and their variances are unknown a priori. Our methodology starts with the derivation of a general upper bound on the misidentification probability applicable to sub-Gaussian distributions. Based on this theoretical foundation, we develop an algorithm that iteratively solves a non-linear optimization problem over empirical estimators to determine the optimal allocation of the residual sampling budget among the arms. We conducted empirical validation across a range of synthetic distribution classes and a real-world scenario based on the MovieLens dataset. Experimental results demonstrate that COpt consistently achieves superior accuracy compared to established algorithms, including Sequential Halving, VBR, and Gap-EV. Execution time remains within the range of tens of milliseconds, making it suitable for a wide range of applications.

ECAI Conference 2024 Conference Paper

A Unified Automata-Theoretic Approach to LTL f Modulo Theories

• Marco Faella
• Gennaro Parlato

We present a novel automata-based approach to address linear temporal logic modulo theory (LTLfMT) as a specification language for data words. LTLfMT extends LTLf by replacing atomic propositions with quantifier-free multi-sorted first-order formulas interpreted over arbitrary theories. While standard LTLf is reduced to finite automata, we reduce LTLfMT to symbolic data-word automata (SDWAs), whose transitions are guarded by constraints from underlying theories. Both the satisfiability of LTLfMT and the emptiness of SDWAs are undecidable, but the latter can be reduced to a system of constrained Horn clauses, which are supported by efficient solvers and ongoing research efforts. We discuss multiple applications of our approach beyond satisfiability, including model checking and runtime monitoring. Finally, a set of empirical experiments shows that our approach to satisfiability works at least as well as a previous custom solution.

TIME Conference 2024 Conference Paper

Model Checking Linear Temporal Properties on Polyhedral Systems

• Massimo Benerecetti
• Marco Faella
• Fabio Mogavero

We study the problem of model checking linear temporal logic formulae on finite trajectories generated by polyhedral differential inclusions, thus enriching the landscape of models where such specifications can be effectively verified. Each model in the class comprises a static and a dynamic component. The static component features a finite set of observables represented by (non-necessarily convex) polyhedra. The dynamic one is given by a convex polyhedron constraining the dynamics of the system, by specifying the possible slopes of the trajectories in each time instant. We devise an exact algorithm that computes a symbolic representation of the region of points that existentially satisfy a given formula φ, i. e. , the points from which there exists a trajectory satisfying φ.

JAAMAS Journal 2024 Journal Article

On preferences and reward policies over rankings

• Marco Faella
• Luigi Sauro

Abstract We study the rational preferences of agents participating in a mechanism whose outcome is a ranking (i. e. , a weak order) among participants. We propose a set of self-interest axioms corresponding to different ways for participants to compare rankings. These axioms vary from minimal conditions that most participants can be expected to agree on, to more demanding requirements that apply to specific scenarios. Then, we analyze the theories that can be obtained by combining the previous axioms and characterize their mutual relationships, revealing a rich hierarchical structure. After this broad investigation on preferences over rankings, we consider the case where the mechanism can distribute a fixed monetary reward to the participants in a fair way (that is, depending only on the anonymized output ranking). We show that such mechanisms can induce specific classes of preferences by suitably choosing the assigned rewards, even in the absence of tie breaking.

AAAI Conference 2023 Conference Paper

Reachability Games Modulo Theories with a Bounded Safety Player

• Marco Faella
• Gennaro Parlato

Solving reachability games is a fundamental problem for the analysis, verification, and synthesis of reactive systems. We consider logical reachability games modulo theories (in short, GMTs), i.e., infinite-state games whose rules are defined by logical formulas over a multi-sorted first-order theory. Our games have an asymmetric constraint: the safety player has at most k possible moves from each game configuration, whereas the reachability player has no such limitation. Even though determining the winner of such a GMT is undecidable, it can be reduced to the well-studied problem of checking the satisfiability of a system of constrained Horn clauses (CHCs), for which many off-the-shelf solvers have been developed. Winning strategies for GMTs can also be computed by resorting to suitable CHC queries. We demonstrate that GMTs can model various relevant real-world games, and that our approach can effectively solve several problems from different domains, using Z3 as the backend CHC solver.

JAAMAS Journal 2020 Journal Article

Irrelevant matches in round-robin tournaments

• Marco Faella
• Luigi Sauro

Abstract We consider tournaments played by a set of players in order to establish a ranking among them. We introduce the notion of irrelevant match, as a match that does not influence the ultimate ranking of the involved parties. After discussing the basic properties of this notion, we seek out tournaments that have no irrelevant matches, focusing on the class of tournaments where each player challenges each other exactly once. We prove that tournaments with a static schedule and at least five players always include irrelevant matches. Conversely, dynamic schedules for an arbitrary number of players can be devised that avoid irrelevant matches, at least for one of the players involved in each match. Finally, we prove by computational means that there exist tournaments where all matches are relevant to both players, at least up to eight players.

ECAI Conference 2020 Conference Paper

Preferences over Rankings and How to Control Them Using Rewards

• Marco Faella
• Luigi Sauro

We study the rational preferences of agents participating in a mechanism whose outcome is a weak order among participants. We propose a set of self-interest axioms and characterize the mutual relationships between all subsets thereof. We then assume that the mechanism can assign monetary rewards to the agents, in a way that is consistent with the weak order. We show that the mechanism can induce specific classes of preferences by suitably choosing the assigned rewards, even in the absence of tie breaking.

ECAI Conference 2020 Conference Paper

Rapidly Finding the Best Arm Using Variance

• Marco Faella
• Alberto Finzi
• Luigi Sauro

We address the problem of identifying the best arm in a pure-exploration multi-armed bandit problem. In this setting, the agent repeatedly pulls arms in order to identify the one associated with the maximum expected reward. We focus on the fixed-budget version of the problem in which the agent tries to find the best arm given a fixed number of arm pulls. We propose a novel sequential elimination method exploiting the empirical variance of the arms. We detail and analyse the overall approach providing theoretical and empirical results. The experimental evaluation shows the advantage of our variance-based rejection method in heterogeneous test settings, considering both identification accuracy and execution time.

OVERLAY Workshop 2019 Workshop Paper

Preference Theories on Weak Orders

• Marco Faella
• Luigi Sauro

AAMAS Conference 2018 Conference Paper

Do all Tournaments Admit Irrelevant Matches?

• Marco Faella
• Luigi Sauro

We consider tournaments played by a set of agents in order to establish a ranking among them. We introduce the notion of irrelevant match, as a match that does not influence the ultimate ranking of the involved parties. After discussing the basic properties of this notion, we seek out tournaments that have no irrelevant matches, focusing on the class of tournaments where each agent challenges each other exactly once. We prove that tournaments with a static schedule and at least 5 agents always include irrelevant matches. Conversely, dynamic schedules can be devised in ways that avoid irrelevant matches, at least for one of the involved agents.

IJCAI Conference 2017 Conference Paper

A New Semantics for Overriding in Description Logics (Extended Abstract)

• Piero Bonatti
• Marco Faella
• Iliana M. Petrova
• Luigi Sauro

Nonmonotonic inferences are not yet supported by Description Logic technology, although their potential usefulness is widely recognized. Lack of support to nonmonotonic reasoning is due to a number of issues related to expressiveness, computational complexity, and optimizations. This work contributes to the practical support of nonmonotonic reasoning in description logics by introducing a new semantics designed to address knowledge engineering needs. The formalism is validated through extensive comparison with the other nonmonotonic DLs, and systematic scalability tests.

I&C Journal 2017 Journal Article

Tracking smooth trajectories in linear hybrid systems

• Massimo Benerecetti
• Marco Faella

We analyze the properties of smooth trajectories subject to a constant differential inclusion which constrains the first derivative to belong to a given convex polyhedron. We present the first exact symbolic algorithm that computes the set of points from which there is a trajectory that reaches a given polyhedron while avoiding another (possibly non-convex) polyhedron. We prove that this set of points remains the same if the smoothness constraint is replaced by a weaker differentiability constraint, but not if it is replaced by almost everywhere differentiability. We discuss the connection with (Linear) Hybrid Automata and in particular the relationship with the classical algorithm for reachability analysis for Linear Hybrid Automata.

Highlights Conference 2016 Conference Abstract

Average Controllability Measures for One-player Games

• Marco Faella

In this talk, I will discuss several ways to measure the extent to which a player can exert control over a one-player stochastic game, relating them to the existing literature on the “skill vs chance” dichotomy. I will focus on measures that depend only on the rules of the games, and not on how people actually play them. After outlining a set of desirable properties, I will observe that two statistical measures of effect size, known as “percentage of standard deviation explained” and “percentage of absolute deviation explained”, satisfy them but give rise to two different orders between games. Finally, I will present numerical estimates of these measures for several well-known games and a sport. The reason for targeting average controllability, rather than minimum or maximum controllability, stems from the observation that the first may more accurately approximate the behavior of a population of players of various skill levels. After all, min, average, and max are the three canonical points in the spectrum of rationality, with bounded rationality à la Simon and actual human players arguably positioned somewhere between the second and the third point. This talk is based on a paper presented at AAMAS 2016.

AAMAS Conference 2016 Conference Paper

Average Controllability Measures for Solitaire Games

• Marco Faella

We discuss several ways to measure the extent to which a player can exert control over a one-player game, relating them to the existing literature on the “skill vs chance” dichotomy. We focus on measures that depend only on the rules of the games, and not on how people actually play them. After presenting a set of desirable properties, we show that two statistical measures of effect size satisfy them and we estimate the value of such measures on several wellknown games.

AAMAS Conference 2016 Conference Paper

Generalized Agent-mediated Procurement Auctions

• Piero A. Bonatti
• Marco Faella
• Clemente Galdi
• Luigi Sauro

Procurement auctions (where the auctioneer needs a service and bidders offer it at their own conditions) are an appealing method for on-line service selection. They can improve service features and cost by exploiting the competition between different service providers. Software agents, acting on behalf of human users and organizations, are essential in making such auctions practical and usable. Since conveying user preferences to the agents in a faithful and complete way is virtually impossible, we advocate an approximate approach, where only partial preferences are formalized, and users pick their choice from a short list of options selected by the agents by means of those partial preferences. Another peculiarity of our scenarios is that there may be no contracts with null utility for a given bidder. These features affect the classical, desirable properties of standard auction mechanisms. We prove some impossibility results concerning truthfulness and (a qualitative analogue of) revenue. Then, we investigate a novel auction mechanism that is almost truthful in the sense that any strategic deviation from truthfulness has limited impact on the auctioneer’s revenue.

CSL Conference 2016 Conference Paper

Hedging Bets in Markov Decision Processes

• Rajeev Alur
• Marco Faella
• Sampath Kannan
• Nimit Singhania

The classical model of Markov decision processes with costs or rewards, while widely used to formalize optimal decision making, cannot capture scenarios where there are multiple objectives for the agent during the system evolution, but only one of these objectives gets actualized upon termination. We introduce the model of Markov decision processes with alternative objectives (MDPAO) for formalizing optimization in such scenarios. To compute the strategy to optimize the expected cost/reward upon termination, we need to figure out how to balance the values of the alternative objectives. This requires analysis of the underlying infinite-state process that tracks the accumulated values of all the objectives. While the decidability of the problem of computing the exact optimal strategy for the general model remains open, we present the following results. First, for a Markov chain with alternative objectives, the optimal expected cost/reward can be computed in polynomial-time. Second, for a single-state process with two actions and multiple objectives we show how to compute the optimal decision strategy. Third, for a process with only two alternative objectives, we present a reduction to the minimum expected accumulated reward problem for one-counter MDPs, and this leads to decidability for this case under some technical restrictions. Finally, we show that optimal cost/reward can be approximated up to a constant additive factor for the general problem.

TCS Journal 2014 Journal Article

Automata-theoretic decision of timed games

• Marco Faella
• Salvatore La Torre
• Aniello Murano

The solution of games is a key decision problem in the context of verification of open systems and program synthesis. Given a game graph and a specification, we wish to determine if there exists a strategy of the protagonist that allows to select only behaviors fulfilling the specification. In this paper, we consider timed games, where the game graph is a timed automaton and the specification is given by formulas of the temporal logics Ltl and Ctl. We present an automata-theoretic approach to solve the addressed games, extending to the timed framework a successful approach to solve discrete games. The main idea of this approach is to translate the timed automaton A, modeling the game graph, into a tree automaton A T accepting all trees that correspond to a strategy of the protagonist. Then, given an automaton corresponding to the specification, we intersect it with the tree automaton A T and check for the nonemptiness of the resulting automaton. Our approach yields a decision algorithm running in exponential time for Ctl and in double exponential time for Ltl. The obtained algorithms are optimal in the sense that their computational complexity matches the known lower bounds.

TCS Journal 2014 Journal Article

Preface to the special issue on GandALF 2012

• Marco Faella
• Aniello Murano

MFCS Conference 2013 Conference Paper

Auctions for Partial Heterogeneous Preferences

• Piero A. Bonatti
• Marco Faella
• Clemente Galdi
• Luigi Sauro

Abstract Online privacy provides fresh motivations to generalized auctions where: (i) preferences over bids may be partial, because of lack of knowledge and formalization difficulties; (ii) the preferences of auctioneers and bidders may be heterogeneous and unrelated. We tackle these generalized scenarios by introducing a few natural generalizations of second-price auctions, and by investigating which of their classical properties are preserved under which conditions.

TCS Journal 2013 Journal Article

Automatic synthesis of switching controllers for linear hybrid systems: Safety control

• Massimo Benerecetti
• Marco Faella
• Stefano Minopoli

In this paper we study the problem of automatically generating switching controllers for the class of Linear Hybrid Automata, with respect to safety objectives. While the same problem has been already considered in the literature, no sound and complete solution has been provided so far. We identify and solve inaccuracies contained in previous characterizations of the problem, providing a sound and complete symbolic fixpoint procedure to compute the set of states from which a controller can keep the system in a given set of desired states. While the overall procedure may not terminate, we prove the termination of each iteration, thus paving the way to an effective implementation. The techniques needed to effectively and efficiently implement the proposed solution procedure, based on polyhedral abstractions of the state space, are thoroughly illustrated and discussed. Finally, some supporting and promising experimental results, based on the implementation of the proposed techniques on top of the tool PHAVer, are presented.

Highlights Conference 2013 Conference Abstract

Best-effort control for Markov decision processes

• Laurent Doyen
• Marco Faella

The premise of this talk is that in order to obtain realistic decision plans for Markov Decision Processes (or other decision-theoretic models) it is useful to consider solution concepts that are as discriminating as possible, by exploiting as much as possible the information provided in the model. Hence, we propose novel solution concepts for MDPs, obtained by lexicographically composing different risk attitudes, ranging from absolutely risk-averse, or pessimistic, to risk-seeking, or optimistic, in an order that depends on the application domain.

TCS Journal 2012 Journal Article

Quantitatively fair scheduling

• Alessandro Bianco
• Marco Faella
• Fabio Mogavero
• Aniello Murano

We consider finite graphs whose edges are labeled with elements, called colors, taken from a fixed finite alphabet. We study the problem of determining whether there is an infinite path where either (i) all colors occur with a fixed asymptotic frequency, or (ii) there is a constant that bounds the difference between the occurrences of any two colors for all prefixes of the path. These properties can be viewed as quantitative refinements of the classical notion of fair path in a concurrent system, whose simplest form checks whether all colors occur infinitely often. Our notions provide stronger criteria, particularly suitable for scheduling applications based on a coarse-grained model of the jobs involved. In particular, they enforce a given set of priorities among the jobs involved in the system. We show that both problems we address are solvable in polynomial time, by reducing them to the feasibility of a linear program. We also consider two-player games played on finite colored graphs where the goal is one of the above frequency-related properties. For all the goals, we show that the problem of checking whether there exists a winning strategy is Co-NP-complete.

AAAI Conference 2011 Conference Paper

Adding Default Attributes to EL++

• Piero Bonatti
• Marco Faella
• Luigi Sauro

The research on low-complexity nonmonotonic description logics recently identified a fragment of EL⊥, supporting defeasible inheritance with overriding, where reasoning can be carried out in polynomial time. We contribute to that framework by supporting more axiom schemata and all the concepts of EL++ without increasing asymptotic complexity.

GandALF Workshop 2011 Workshop Paper

Towards Efficient Exact Synthesis for Linear Hybrid Systems

• Massimo Benerecetti
• Marco Faella
• Stefano Minopoli

We study the problem of automatically computing the controllable region of a Linear Hybrid Automaton, with respect to a safety objective. We describe the techniques that are needed to effectively and efficiently implement a recently-proposed solution procedure, based on polyhedral abstractions of the state space. Supporting experimental results are presented, based on an implementation of the proposed techniques on top of the tool PHAVer.

IJCAI Conference 2009 Conference Paper

• Piero A. Bonatti
• Marco Faella
• Luigi Sauro

We analyze the complexity of reasoning with circumscribed low-complexity DLs such as DL-lite and the EL family, under suitable restrictions on the use of abnormality predicates. We prove that in circumscribed DL-liteR complexity drops from NExpNP to the second level of the polynomial hierarchy. In EL, reasoning remains ExpTime-hard, in general. However, by restricting the possible occurrences of existential restrictions, we obtain membership in Σp 2 and Πp 2 for an extension of EL.

MFCS Conference 2009 Conference Paper

Admissible Strategies in Infinite Games over Graphs

• Marco Faella

Abstract We consider games played on finite graphs, whose objective is to obtain a trace belonging to a given set of accepting traces. We focus on the states from which Player 1 cannot force a win. We compare several criteria for establishing what is the preferable behavior of Player 1 from those states, eventually settling on the notion of admissible strategy. As the main result, we provide a characterization of the goals admitting positional admissible strategies. In addition, we derive a simple algorithm for computing such strategies for various common goals, and we prove the equivalence between the existence of positional winning strategies and the existence of positional subgame perfect strategies.

MFCS Conference 2009 Conference Paper

Balanced Paths in Colored Graphs

• Alessandro Bianco
• Marco Faella
• Fabio Mogavero
• Aniello Murano

Abstract We consider finite graphs whose edges are labeled with elements, called colors, taken from a fixed finite alphabet. We study the problem of determining whether there is an infinite path where either (i) all colors occur with the same asymptotic frequency, or (ii) there is a constant which bounds the difference between the occurrences of any two colors for all prefixes of the path. These two notions can be viewed as refinements of the classical notion of fair path, whose simplest form checks whether all colors occur infinitely often. Our notions provide stronger criteria, particularly suitable for scheduling applications based on a coarse-grained model of the jobs involved. We show that both problems are solvable in polynomial time, by reducing them to the feasibility of a linear program.

TCS Journal 2005 Journal Article

Model checking discounted temporal properties

• Luca de Alfaro
• Marco Faella
• Thomas A. Henzinger
• Rupak Majumdar
• Mariëlle Stoelinga

Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic CTL which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0, 1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators ⋄ and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path. We interpret the resulting logic DCTL over transition systems, Markov chains, and Markov decision processes. We present two semantics for DCTL: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the μ -calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for DCTL, and we provide model-checking algorithms for both semantics.