Author name cluster

Massimo Benerecetti

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

18 papers

2 author rows

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 φ.

Details DOI

GandALF Workshop 2025 Workshop Paper

An Automaton-based Characterisation of First-Order Logic over Infinite Trees

Massimo Benerecetti
Dario Della Monica
Angelo Matteo
Fabio Mogavero
Gabriele Puppis

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-theoretic characterisation of FO interpreted over infinite trees. To this end, two different classes of hesitant tree automata are introduced and proved to capture precisely the expressive power of two branching time temporal logics, denoted polcCTLp and cCTL*[f], which are, respectively, a restricted version of counting CTL with past and counting CTL* over finite paths, both of which have been previously shown equivalent to FO over infinite trees. The two automata characterisations naturally lead to normal forms for the two temporal logics, and highlight the fact that FO can only express properties of the tree branches which are either safety or co-safety in nature.

PDF Details DOI

TIME Conference 2024 Conference Paper

Full Characterisation of Extended CTL

Massimo Benerecetti
Laura Bozzelli
Fabio Mogavero
Adriano Peron

The precise identification of the expressive power of logic languages used in formal methods for specifying and verifying run-time properties of critical systems is a fundamental task and characterisation theorems play a crucial role as model-theoretic tools in this regard. While a clear picture of the expressive power of linear-time temporal logics in terms of word automata and predicate logics has long been established, a complete mapping of the corresponding relationships for branching-time temporal logics has proven to be a more elusive task over the past four decades with few scattered results. Only recently, an automata-theoretic characterisation of both CTL* and its full-ω-regular extension ECTL* has been provided in terms of Symmetric Hesitant Tree Automata (HTA), with and without a suitable counter-freeness restriction on their linear behaviours. These two temporal logics also correspond to the bisimulation-invariant semantic fragments of Monadic Path Logic (MPL) and Monadic Chain Logic (MCL), respectively. Additionally, it has been proven that the counting extensions of CTL* and ECTL*, namely CCTL* and CECTL*, enjoy equivalent graded versions of the HTAs for the corresponding non-counting logics. However, while Moller and Rabinovich have proved CCTL* to be equivalent to full MPL, thus filling the gap for the standard branching-time logic, no similar result has been given for CECTL*. This work completes the picture, by proving the expressive equivalence of CECTL* and full MCL, by means of a composition theorem for the latter logic. This also indirectly establishes the equivalence between HTAs and their first-order extensions HFTAs, as originally introduced by Walukiewicz.

Details

TIME Conference 2024 Conference Paper

Model Checking Linear Temporal Properties on Polyhedral Systems

Massimo Benerecetti
Marco Faella
Fabio Mogavero

Details

I&C Journal 2024 Journal Article

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, namely small progress measures and quasi dominions. We show that the integration of the two notions can be highly beneficial and significantly speeds up convergence to the problem solution. Experiments show that the resulting algorithm performs orders of magnitude better than the asymptotically-best solution algorithm currently known, without sacrificing on the worst-case complexity.

Details DOI

I&C Journal 2023 Journal Article

Taming Strategy Logic: Non-Recurrent Fragments

Massimo Benerecetti
Fabio Mogavero
Adriano Peron

Strategy Logic ( Image 1 for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends Image 2 with first-order quantifiers over the agent strategies and encompasses other formalisms, such as Image 3 and Image 4. The model-checking problem for Image 1 and several of its fragments has been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal Image 1, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these two logics, and for the corresponding fragments of Image 3 and Image 4, is in Image 5 and Image 6, respectively.

Details DOI

TIME Conference 2022 Conference Paper

Taming Strategy Logic: Non-Recurrent Fragments

Massimo Benerecetti
Fabio Mogavero
Adriano Peron

Strategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments have been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these logics, and for the corresponding fragments of ATL* and CTL*, is ExpSpace and PSpace-Complete, respectively.

Details

I&C Journal 2020 Journal Article

Robust worst cases for parity games algorithms

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 theoretical exponential worst-case complexity and the negative reputation as a poorly effective algorithm in practice, it has been shown to rank among the best techniques for solving such games. Also, it proved to be resistant to a lower bound attack, even more than the strategy improvements approaches, but finally Friedmann provided a family of games on which the algorithm requires exponential time. An easy analysis of this family shows that a simple memoization technique can help the algorithm solve the family in polynomial time. The same result can also be achieved by exploiting an approach based on the dominion-decomposition techniques proposed in the literature. These observations raise the question whether a suitable combination of dynamic programming and game-decomposition techniques can improve on the exponential worst case of the original algorithm. In this paper we answer this question negatively, by providing a robustly exponential worst case, showing that no possible intertwining of the above mentioned techniques can help mitigating the exponential nature of the divide et impera approaches. The resulting worst case is even more robust than that, since it serves as a lower bound for progress measures based algorithms as well, such as Small Progress Measure and its quasi-polynomial variant recently proposed by Jurdziński and Lazic.

Details DOI

AAAI Conference 2019 Conference Paper

Satisfiability in Strategy Logic Can Be Easier than Model Checking

Erman Acar
Massimo Benerecetti
Fabio Mogavero

In the design of complex systems, model-checking and satisfiability arise as two prominent decision problems. While model-checking requires the designed system to be provided in advance, satisfiability allows to check if such a system even exists. With very few exceptions, the second problem turns out to be harder than the first one from a complexity-theoretic standpoint. In this paper, we investigate the connection between the two problems for a non-trivial fragment of Strategy Logic (SL, for short). SL extends LTL with first-order quantifications over strategies, thus allowing to explicitly reason about the strategic abilities of agents in a multi-agent system. Satisfiability for the full logic is known to be highly undecidable, while model-checking is non-elementary. The SL fragment we consider is obtained by preventing strategic quantifications within the scope of temporal operators. The resulting logic is quite powerful, still allowing to express important game-theoretic properties of multi-agent systems, such as existence of Nash and immune equilibria, as well as to formalize the rational synthesis problem. We show that satisfiability for such a fragment is PSPACE-COMPLETE, while its model-checking complexity is 2EXPTIME-HARD. The result is obtained by means of an elegant encoding of the problem into the satisfiability of conjunctive-binding first-order logic, a recently discovered decidable fragment of first-order logic.

PDF Details

I&C Journal 2018 Journal Article

A delayed promotion policy for parity games

Massimo Benerecetti
Daniele Dell'Erba
Fabio Mogavero

Parity games are two-player infinite-duration games on graphs that play a crucial role in various fields of theoretical computer science. Finding efficient algorithms to solve these games in practice is widely acknowledged as a core problem in formal verification, as it leads to efficient solutions of the model-checking and satisfiability problems of expressive temporal logics, e. g. , the modal μ Calculus. Their solution can be reduced to the problem of identifying sets of positions of the game, called dominions, in each of which a player can force a win by remaining in the set forever. Recently, a novel technique to compute dominions, called priority promotion, has been proposed, which is based on the notions of quasi dominion, a relaxed form of dominion, and dominion space. The underlying framework is general enough to accommodate different instantiations of the solution procedure, whose correctness is ensured by the nature of the space itself. In this paper we propose a new such instantiation, called delayed promotion, that tries to reduce the possible exponential behaviors exhibited by the original method in the worst case. The resulting procedure often outperforms both the state-of-the-art solvers and the original priority promotion approach.

Details DOI

GandALF Workshop 2017 Workshop Paper

Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games

Massimo Benerecetti
Dell
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 theoretical worst-case complexity and the negative reputation as a poorly effective algorithm in practice, it has been shown to rank among the best techniques for the solution of such games. Also, it proved to be resistant to a lower bound attack, even more than the strategy improvements approaches, and only recently a family of games on which the algorithm requires exponential time has been provided by Friedmann. An easy analysis of this family shows that a simple memoization technique can help the algorithm solve the family in polynomial time. The same result can also be achieved by exploiting an approach based on the dominion-decomposition techniques proposed in the literature. These observations raise the question whether a suitable combination of dynamic programming and game-decomposition techniques can improve on the exponential worst case of the original algorithm. In this paper we answer this question negatively, by providing a robustly exponential worst case, showing that no intertwining of the above mentioned techniques can help mitigating the exponential nature of the divide et impera approaches.

PDF Details DOI

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.

Details DOI

GandALF Workshop 2016 Workshop Paper

A Delayed Promotion Policy for Parity Games

Massimo Benerecetti
Dell
Fabio Mogavero

Parity games are two-player infinite-duration games on graphs that play a crucial role in various fields of theoretical computer science. Finding efficient algorithms to solve these games in practice is widely acknowledged as a core problem in formal verification, as it leads to efficient solutions of the model-checking and satisfiability problems of expressive temporal logics, e. g. , the modal muCalculus. Their solution can be reduced to the problem of identifying sets of positions of the game, called dominions, in each of which a player can force a win by remaining in the set forever. Recently, a novel technique to compute dominions, called priority promotion, has been proposed, which is based on the notions of quasi dominion, a relaxed form of dominion, and dominion space. The underlying framework is general enough to accommodate different instantiations of the solution procedure, whose correctness is ensured by the nature of the space itself. In this paper we propose a new such instantiation, called delayed promotion, that tries to reduce the possible exponential behaviours exhibited by the original method in the worst case. The resulting procedure not only often outperforms the original priority promotion approach, but so far no exponential worst case is known.

PDF Details DOI

TCS Journal 2016 Journal Article

Timed recursive state machines: Expressiveness and complexity

Massimo Benerecetti
Adriano Peron

The paper proposes a temporal extension of Recursive State Machines (RSMs), called Timed RSMs (TRSMs), which consists of an indexed collection of Timed Automata, called components. Each component can invoke other components in a potentially recursive manner. Besides being able to model procedure calls and recursion, TRSMs are equipped with the ability to suspend the evolution of time within a component when another component is invoked and to recover it when control is given back at return time. This mechanism is realized by storing clock valuations into an implicit stack at invocation time and restoring them upon return. Indeed, TRSMs can be related to an extension of Pushdown Timed Automata, called EPTAs, where an additional stack, coupled with the standard control stack, is used to store temporal valuations of clocks. The expressiveness and computational properties of the resulting model are analyzed, showing that it can be used to recognize timed languages exhibiting context-free properties not only in the untimed “control” part, but also in the associated temporal dimension. The reachability problem for both TRSMs and EPTAs is investigated, showing that the problem is undecidable in the general case. However, the problem becomes decidable for two meaningful subclasses, called I-TRSM and L-TRSM, obtained by suitably constraining the set of clocks to reset at invocation time and to restore at return time. The considered subclasses are compared with the corresponding EPTAs subclasses through bisimulation of their timed LTSs. The complexity of the reachability problem for L-TRSM and I-TRSM is proved to be EXPTIME-complete and PSPACE-complete, respectively. Moreover, we prove that such classes strictly enhance the expressive power of Timed Automata and of Pushdown Timed Automata, forming a proper hierarchy.

Details DOI

Highlights Conference 2015 Conference Abstract

Solving Parity Games via Priority Promotion

Massimo Benerecetti

The main contribution of the paper is a new family of algorithms for solving parity games, based on the notions of region and priority promotion. A region R for a given player is a set of vertices from each of which the player can enforce a winning play that never leaves the region, unless either the opponent can escape from R or the only choice for player itself is to exit from R (i. e. no edge from a vertex of remains in R). Therefore, a region is essentially a weaker form of winning region. Regions can be ordered by assigning to each of them a priority corresponding to the "best" priority the opponent can obtain along a play exiting from that region. An important property of regions is that, under suitable and easy to check assumptions, a higher priority region R1 and a lower priority region R2, with priorities p1 and p2, respectively, of the same parity, can be merged into a single region of the higher priority p1. We call this merging operation a priority promotion for R2. The underlying idea of the approach is then to iteratively enlarge regions by performing suitable sequences of promotions, until a closed -region, namely a region where player can force the game to remain, is obtained. When that happens, a winning region for has been found. Experimental results, comparing the new algorithms with the state of the art solvers, also show that all three algorithms perform very well in practice, most often significantly better than existing ones, on both random games and benchmark families proposed in the literature.

Details

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.

Details DOI

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.

PDF Details DOI

TIME Conference 2010 Conference Paper

Analysis of Timed Recursive State Machines

Massimo Benerecetti
Stefano Minopoli
Adriano Peron

The paper proposes a temporal extension of Recursive State Machines (RSMs), called Timed RSMs (TRSMs). A TRSM is an indexed collection of Timed Automata allowed to invoke other Timed Automata (procedural calls). The classes of TRSMs are related to an extension of Pushdown Timed Automata, called EPTAs, where an additional stack, coupled with the standard control stack, is used to store temporal valuations of clocks. A number of subclasses of TRSMs and EPTAs are considered and compared through bisimulation of their timed LTSs. It is shown that EPTAs and TRSMs can be used to recognize classes of timed languages exhibiting context-free properties not only in the untimed “control” part, but also in the associated temporal dimension. The reachability problem for both TRSMs and EPTAs is investigated, showing that the problem is undecidable in the general case, but decidable for meaningful subclasses. The complexity is stated for a TRSMs subclass.

Details