arXiv subjects

Marco Faella

Publications and source records attributed to Marco Faella.

15 recordsLinked to original sources

arXiv2025

Verifying Tree-Manipulating Programs via CHCs

Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, foundational approach to verifying such programs. Central to our approach is the knitted-tree encoding, modeling each program execution as a tree structure capturing input, output, and intermediate states. Leveraging the compositional nature of knitted-trees, we encode these structures as constrained Horn clauses (CHCs), reducing verification to CHC satisfiability task. To illustrate our approach, we focus on memory safety and show how it naturally leads to simple, modular invariants.

cs.PL↗

arXiv2024

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses

Verifying programs that manipulate tree data structures often requires complex, ad-hoc proofs that are hard to generalize and automate. This paper introduces an automatic technique for analyzing such programs. Our approach combines automata and logics to tackle the challenges posed by diverse tree data structures uniformly. At the core of our methodology is the knitted-tree encoding, which maps a program execution into a tree data structure encapsulating input, output, and intermediate configurations, within a single structure. By leveraging the compositional properties of knitted-trees, we characterize them using constrained Horn clauses (CHCs). This encoding reduces verification to solving CHC satisfiability, benefiting from ongoing advancements in CHC solvers. While we focus on the memory safety problem for illustration, our technique applies broadly to various verification tasks involving tree data structures.

cs.PL↗

arXiv2024

A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)

We present a novel automata-based approach to address linear temporal logic modulo theory (LTL-MT) as a specification language for data words. LTL-MT extends LTL_f by replacing atomic propositions with quantifier-free multi-sorted first-order formulas interpreted over arbitrary theories. While standard LTL_f is reduced to finite automata, we reduce LTL-MT to symbolic data-word automata (SDWAs), whose transitions are guarded by constraints from underlying theories. Both the satisfiability of LTL-MT 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.

cs.LO↗

arXiv2020

From Quasi-Dominions to Progress Measures

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 that, while progress measure based techniques typically focus on one of the two players, little information is gathered on the other player during the solution process. Adding quasi dominions provides additional information on this player that can be leveraged to greatly accelerate convergence to a progress measure. To accommodate quasi dominions, however, non trivial refinements of the approach are necessary. In particular, we need to introduce a novel notion of measure and a new method to prove correctness of the resulting solution technique.

cs.LO↗

arXiv2016

TrueReview: A Platform for Post-Publication Peer Review

In post-publication peer review, scientific contributions are first published in open-access forums, such as arXiv or other digital libraries, and are subsequently reviewed and possibly ranked and/or evaluated. Compared to the classical process of scientific publishing, in which review precedes publication, post-publication peer review leads to faster dissemination of ideas, and publicly-available reviews. The chief concern in post-publication reviewing consists in eliciting high-quality, insightful reviews from participants. We describe the mathematical foundations and structure of TrueReview, an open-source tool we propose to build in support of post-publication review. In TrueReview, the motivation to review is provided via an incentive system that promotes reviews and evaluations that are both truthful (they turn out to be correct in the long run) and informative (they provide significant new information). TrueReview organizes papers in venues, allowing different scientific communities to set their own submission and review policies. These venues can be manually set-up, or they can correspond to categories in well-known repositories such as arXiv. The review incentives can be used to form a reviewer ranking that can be prominently displayed alongside papers in the various disciplines, thus offering a concrete benefit to reviewers. The paper evaluations, in turn, reward the authors of the most significant papers, both via an explicit paper ranking, and via increased visibility in search.

cs.DL↗

arXiv2016

Incentives for Truthful Evaluations

We consider crowdsourcing problems where the users are asked to provide evaluations for items; the user evaluations are then used directly, or aggregated into a consensus value. Lacking an incentive scheme, users have no motive in making effort in completing the evaluations, providing inaccurate answers instead. We propose incentive schemes that are truthful and cheap: truthful as the optimal user behavior consists in providing accurate evaluations, and cheap because the truthfulness is achieved with little overhead cost. We consider both discrete evaluation tasks, where an evaluation can be done either correctly, or incorrectly, with no degrees of approximation in between, and quantitative evaluation tasks, where evaluations are real numbers, and the error is measured as distance from the correct value. For both types of tasks, we propose hierarchical incentive schemes that can be effected with a small amount of additional evaluations, and that scale to arbitrarily large crowd sizes: they have the property that the strength of the incentive does not weaken with increasing hierarchy depth. Interestingly, we show that for these schemes to work, the only requisite is that workers know their place in the hierarchy in advance.

cs.GT↗

arXiv2014

Partial Preferences for Mediated Bargaining

In this work we generalize standard Decision Theory by assuming that two outcomes can also be incomparable. Two motivating scenarios show how incomparability may be helpful to represent those situations where, due to lack of information, the decision maker would like to maintain different options alive and defer the final decision. In particular, a new axiomatization is given which turns out to be a weakening of the classical set of axioms used in Decision Theory. Preliminary results show how preferences involving complex distributions are related to judgments on single alternatives.

cs.GT↗

arXiv2014

Defeasible Inclusions in Low-Complexity DLs

Some of the applications of OWL and RDF (e.g. biomedical knowledge representation and semantic policy formulation) call for extensions of these languages with nonmonotonic constructs such as inheritance with overriding. Nonmonotonic description logics have been studied for many years, however no practical such knowledge representation languages exist, due to a combination of semantic difficulties and high computational complexity. Independently, low-complexity description logics such as DL-lite and EL have been introduced and incorporated in the OWL standard. Therefore, it is interesting to see whether the syntactic restrictions characterizing DL-lite and EL bring computational benefits to their nonmonotonic versions, too. In this paper we extensively investigate the computational complexity of Circumscription when knowledge bases are formulated in DL-lite_R, EL, and fragments thereof. We identify fragments whose complexity ranges from P to the second level of the polynomial hierarchy, as well as fragments whose complexity raises to PSPACE and beyond.

cs.LO↗

arXiv2012

Proceedings Third International Symposium on Games, Automata, Logics and Formal Verification

This volume contains the proceedings of the Third International Symposium on Games, Automata, Logic and Formal Verification (GandALF), held in Naples (Italy) from September 6th to 8th, 2012. GandALF was founded by a number of Italian computer scientists interested in mathematical logic, automata theory, game theory, and their applications to the specification, design, and verification of complex systems. Its aim is to provide a forum where people from different areas, and possibly with different backgrounds, can fruitfully interact. Even though the idea of the symposium emerged within the Italian research community, the event has a truly international nature, as witnessed by the composition of the conference committees and the programme.

cs.LO↗

arXiv2011

Towards Efficient Exact Synthesis for Linear Hybrid Systems

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.

cs.LO↗

arXiv2011

Automatic Synthesis of Switching Controllers for Linear Hybrid Automata

In this paper we study the problem of automatically generating switching controllers for the class of Linear Hybrid Automata, with respect to safety objectives. We identify and solve inaccuracies contained in previous characterizations of the problem, providing a sound and complete symbolic fixpoint procedure, based on polyhedral abstractions of the state space. We also prove the termination of each iteration of the procedure. Some promising experimental results are presented, based on an implementation of the fixpoint procedure on top of the tool PHAVer.

cs.LO↗

arXiv2010

Quantitative Fairness Games

We consider two-player games played on finite colored graphs where the goal is the construction of an infinite path with one of the following frequency-related properties: (i) all colors occur with the same asymptotic frequency, (ii) there is a constant that bounds the difference between the occurrences of any two colors for all prefixes of the path, or (iii) all colors occur with a fixed asymptotic frequency. 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. In particular, the first two properties enforce equal treatment of all the jobs involved in the system, while the third one represents a way to assign a given priority to each job. For all the above goals, we show that the problem of checking whether there exists a winning strategy is CoNP-complete.

cs.GT↗

arXiv2009

Some Models and Tools for Open Systems

In computer science, there is a distinction between closed systems, whose behavior is totally determined in advance, and open systems, that are systems maintaining a constant interaction with an unspecified environment. Closed systems are naturally modeled by transitions systems. Open systems have been modeled in various ways, including process algebras, I/O automata, ``modules'', and interfaces. Games provide a uniform setting in which all these models can be cast and compared. In this paper, we discuss the features and costs related to the game-based approach to open systems, referring to some of the existing models. Finally, we describe a new model of interface, called sociable interface, which is geared towards easier specification, improved reusability of models, and efficient symbolic implementation.

cs.LO↗

arXiv2009

Qualitative Logics and Equivalences for Probabilistic Systems

We investigate logics and equivalence relations that capture the qualitative behavior of Markov Decision Processes (MDPs). We present Qualitative Randomized CTL (QRCTL): formulas of this logic can express the fact that certain temporal properties hold over all paths, or with probability 0 or 1, but they do not distinguish among intermediate probability values. We present a symbolic, polynomial time model-checking algorithm for QRCTL on MDPs. The logic QRCTL induces an equivalence relation over states of an MDP that we call qualitative equivalence: informally, two states are qualitatively equivalent if the sets of formulas that hold with probability 0 or 1 at the two states are the same. We show that for finite alternating MDPs, where nondeterministic and probabilistic choices occur in different states, qualitative equivalence coincides with alternating bisimulation, and can thus be computed via efficient partition-refinement algorithms. On the other hand, in non-alternating MDPs the equivalence relations cannot be computed via partition-refinement algorithms, but rather, they require non-local computation. Finally, we consider QRCTL*, that extends QRCTL with nested temporal operators in the same manner in which CTL* extends CTL. We show that QRCTL and QRCTL* induce the same qualitative equivalence on alternating MDPs, while on non-alternating MDPs, the equivalence arising from QRCTL* can be strictly finer. We also provide a full characterization of the relation between qualitative equivalence, bisimulation, and alternating bisimulation, according to whether the MDPs are finite, and to whether their transition relations are finitely-branching.

cs.LO↗

arXiv2008

Best-Effort Strategies for Losing States

We consider games played on finite graphs, whose goal is to obtain a trace belonging to a given set of winning traces. We focus on those states from which Player 1 cannot force a win. We explore and compare several criteria for establishing what is the preferable behavior of Player 1 from those states. Along the way, we prove several results of theoretical and practical interest, such as a characterization of admissible strategies, which also provides a simple algorithm for computing such strategies for various common goals, and the equivalence between the existence of positional winning strategies and the existence of positional subgame perfect strategies.

cs.GT↗