-
Self-Balancing Semi-Hierarchical PCNs for CBDCs
Authors:
Marco Benedetti,
Francesco De Sclavis,
Marco Favorito,
Giuseppe Galano,
Sara Giammusso,
Antonio Muci,
Matteo Nardelli
Abstract:
We introduce a family of PCNs (Payment Channel Networks) characterized by a semi-hierarchical topology and a custom set of channel rebalancing strategies. This family exhibits two interesting benefits, if used as a platform for large-scale, instant, retail payment systems, such as CBDCs: Technically, the solution offers state-of-the-art guarantees of fault-tolerance and integrity, while providing…
▽ More
We introduce a family of PCNs (Payment Channel Networks) characterized by a semi-hierarchical topology and a custom set of channel rebalancing strategies. This family exhibits two interesting benefits, if used as a platform for large-scale, instant, retail payment systems, such as CBDCs: Technically, the solution offers state-of-the-art guarantees of fault-tolerance and integrity, while providing a latency and throughput comparable to centralized systems; from a business perspective, the solution perfectly suits the 3-tier architecture of the current banking ecosystem (central banks / commercial banks / retail users), assigning a pivotal and peculiar role to the members of each tier. Furthermore, the cryptographic privacy of payments for retail users -- typical of PCNs such as the public Lightning Network -- is largely (possibly fully) retained. We study the system by simulating a scaled-down version of a hypothetical European CBDC, exploring the trade-offs among liquidity locked by market operators, payment success rate, throughput, latency, and load on the underpinning blockchain.
△ Less
Submitted 22 January, 2024;
originally announced January 2024.
-
Composition of Nondeterministic and Stochastic Services for LTLf Task Specifications
Authors:
Giuseppe De Giacomo,
Marco Favorito,
Luciana Silo
Abstract:
In this paper, we study the composition of services so as to obtain runs satisfying a task specification in Linear Temporal Logic on finite traces (LTLf). We study the problem in the case services are nondeterministic and the LTLf specification can be exactly met, and in the case services are stochastic, where we are interested in maximizing the probability of satisfaction of the LTLf specificatio…
▽ More
In this paper, we study the composition of services so as to obtain runs satisfying a task specification in Linear Temporal Logic on finite traces (LTLf). We study the problem in the case services are nondeterministic and the LTLf specification can be exactly met, and in the case services are stochastic, where we are interested in maximizing the probability of satisfaction of the LTLf specification and, simultaneously, minimizing the utilization cost of the services. To do so, we combine techniques from LTLf synthesis, service composition à la Roman Model, reactive synthesis, and bi-objective lexicographic optimization on MDPs. This framework has several interesting applications, including Smart Manufacturing and Digital Twins.
△ Less
Submitted 29 November, 2023;
originally announced November 2023.
-
Ontological Reasoning over Shy and Warded Datalog$+/-$ for Streaming-based Architectures (technical report)
Authors:
Teodoro Baldazzi,
Luigi Bellomarini,
Marco Favorito,
Emanuel Sallinger
Abstract:
Recent years witnessed a rising interest towards Datalog-based ontological reasoning systems, both in academia and industry. These systems adopt languages, often shared under the collective name of Datalog$+/-$, that extend Datalog with the essential feature of existential quantification, while introducing syntactic limitations to sustain reasoning decidability and achieve a good trade-off between…
▽ More
Recent years witnessed a rising interest towards Datalog-based ontological reasoning systems, both in academia and industry. These systems adopt languages, often shared under the collective name of Datalog$+/-$, that extend Datalog with the essential feature of existential quantification, while introducing syntactic limitations to sustain reasoning decidability and achieve a good trade-off between expressive power and computational complexity. From an implementation perspective, modern reasoners borrow the vast experience of the database community in develo** streaming-based data processing systems, such as volcano-iterator architectures, that sustain a limited memory footprint and good scalability. In this paper, we focus on two extremely promising, expressive, and tractable languages, namely, Shy and Warded Datalog$+/-$. We leverage their theoretical underpinnings to introduce novel reasoning techniques, technically, "chase variants", that are particularly fit for efficient reasoning in streaming-based architectures. We then implement them in Vadalog, our reference streaming-based engine, to efficiently solve ontological reasoning tasks over real-world settings.
△ Less
Submitted 20 November, 2023;
originally announced November 2023.
-
Exploiting Multiple Abstractions in Episodic RL via Reward Sha**
Authors:
Roberto Cipollone,
Giuseppe De Giacomo,
Marco Favorito,
Luca Iocchi,
Fabio Patrizi
Abstract:
One major limitation to the applicability of Reinforcement Learning (RL) to many practical domains is the large number of samples required to learn an optimal policy. To address this problem and improve learning efficiency, we consider a linear hierarchy of abstraction layers of the Markov Decision Process (MDP) underlying the target domain. Each layer is an MDP representing a coarser model of the…
▽ More
One major limitation to the applicability of Reinforcement Learning (RL) to many practical domains is the large number of samples required to learn an optimal policy. To address this problem and improve learning efficiency, we consider a linear hierarchy of abstraction layers of the Markov Decision Process (MDP) underlying the target domain. Each layer is an MDP representing a coarser model of the one immediately below in the hierarchy. In this work, we propose a novel form of Reward Sha** where the solution obtained at the abstract level is used to offer rewards to the more concrete MDP, in such a way that the abstract solution guides the learning in the more complex domain. In contrast with other works in Hierarchical RL, our technique has few requirements in the design of the abstract models and it is also tolerant to modeling errors, thus making the proposed approach practical. We formally analyze the relationship between the abstract models and the exploration heuristic induced in the lower-level domain. Moreover, we prove that the method guarantees optimal convergence and we demonstrate its effectiveness experimentally.
△ Less
Submitted 4 August, 2023; v1 submitted 28 February, 2023;
originally announced March 2023.
-
Forward LTLf Synthesis: DPLL At Work
Authors:
Marco Favorito
Abstract:
This paper proposes a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (\LTLf), that overcomes some limitations of previous approaches. Within such framework, we devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves in a truly depth-first fashion, possibly avoiding exhaustiv…
▽ More
This paper proposes a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (\LTLf), that overcomes some limitations of previous approaches. Within such framework, we devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves in a truly depth-first fashion, possibly avoiding exhaustive enumeration or costly compilations. We also propose a novel equivalence check for search nodes based on syntactic equivalence of state formulas. Since the resulting procedure is not guaranteed to terminate, we identify a stop** condition to abort execution and restart the search with state-equivalence checking based on Binary Decision Diagrams (BDD), which we show to be correct. The experimental results show that in many cases the proposed techniques outperform other state-of-the-art approaches. Our implementation Nike competed in the LTLf Realizability Track in the 2023 edition of SYNTCOMP, and won the competition.
△ Less
Submitted 19 June, 2023; v1 submitted 27 February, 2023;
originally announced February 2023.
-
Reinforcement Learning for Combining Search Methods in the Calibration of Economic ABMs
Authors:
Aldo Glielmo,
Marco Favorito,
Debmallya Chanda,
Domenico Delli Gatti
Abstract:
Calibrating agent-based models (ABMs) in economics and finance typically involves a derivative-free search in a very large parameter space. In this work, we benchmark a number of search methods in the calibration of a well-known macroeconomic ABM on real data, and further assess the performance of "mixed strategies" made by combining different methods. We find that methods based on random-forest s…
▽ More
Calibrating agent-based models (ABMs) in economics and finance typically involves a derivative-free search in a very large parameter space. In this work, we benchmark a number of search methods in the calibration of a well-known macroeconomic ABM on real data, and further assess the performance of "mixed strategies" made by combining different methods. We find that methods based on random-forest surrogates are particularly efficient, and that combining search methods generally increases performance since the biases of any single method are mitigated. Moving from these observations, we propose a reinforcement learning (RL) scheme to automatically select and combine search methods on-the-fly during a calibration run. The RL agent keeps exploiting a specific method only as long as this keeps performing well, but explores new strategies when the specific method reaches a performance plateau. The resulting RL search scheme outperforms any other method or method combination tested, and does not rely on any prior information or trial and error procedure.
△ Less
Submitted 7 December, 2023; v1 submitted 23 February, 2023;
originally announced February 2023.
-
A PoW-less Bitcoin with Certified Byzantine Consensus
Authors:
Marco Benedetti,
Francesco De Sclavis,
Marco Favorito,
Giuseppe Galano,
Sara Giammusso,
Antonio Muci,
Matteo Nardelli
Abstract:
Distributed Ledger Technologies (DLTs), when managed by a few trusted validators, require most but not all of the machinery available in public DLTs. In this work, we explore one possible way to profit from this state of affairs. We devise a combination of a modified Practical Byzantine Fault Tolerant (PBFT) protocol and a revised Flexible Round-Optimized Schnorr Threshold Signatures (FROST) schem…
▽ More
Distributed Ledger Technologies (DLTs), when managed by a few trusted validators, require most but not all of the machinery available in public DLTs. In this work, we explore one possible way to profit from this state of affairs. We devise a combination of a modified Practical Byzantine Fault Tolerant (PBFT) protocol and a revised Flexible Round-Optimized Schnorr Threshold Signatures (FROST) scheme, and then we inject the resulting proof-of-authority consensus algorithm into Bitcoin (chosen for the reliability, openness, and liveliness it brings in), replacing its PoW machinery. The combined protocol may operate as a modern, safe foundation for digital payment systems and Central Bank Digital Currencies (CBDC).
△ Less
Submitted 9 May, 2023; v1 submitted 14 July, 2022;
originally announced July 2022.
-
Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic: A Polynomial Reduction to Standard Planning
Authors:
Giuseppe De Giacomo,
Marco Favorito,
Francesco Fuggitti
Abstract:
We study temporally extended goals expressed in Pure-Past LTL (PPLTL). PPLTL is particularly interesting for expressing goals since it allows to express sophisticated tasks as in the Formal Methods literature, while the worst-case computational complexity of Planning in both deterministic and nondeterministic domains (FOND) remains the same as for classical reachability goals. However, while the t…
▽ More
We study temporally extended goals expressed in Pure-Past LTL (PPLTL). PPLTL is particularly interesting for expressing goals since it allows to express sophisticated tasks as in the Formal Methods literature, while the worst-case computational complexity of Planning in both deterministic and nondeterministic domains (FOND) remains the same as for classical reachability goals. However, while the theory of planning for PPLTL goals is well understood, practical tools have not been specifically investigated. In this paper, we make a significant leap forward in the construction of actual tools to handle PPLTL goals. We devise a technique to polynomially translate planning for PPLTL goals into standard planning. We show the formal correctness of the translation, its complexity, and its practical effectiveness through some comparative experiments. As a result, our translation enables state-of-the-art tools, such as FD or MyND, to handle PPLTL goals seamlessly, maintaining the impressive performances they have for classical reachability goals.
△ Less
Submitted 31 May, 2022; v1 submitted 21 April, 2022;
originally announced April 2022.
-
On the Relationship between Shy and Warded Datalog+/-
Authors:
Teodoro Baldazzi,
Luigi Bellomarini,
Marco Favorito,
Emanuel Sallinger
Abstract:
Datalog^E is the extension of Datalog with existential quantification. While its high expressive power, underpinned by a simple syntax and the support for full recursion, renders it particularly suitable for modern applications on knowledge graphs, query answering (QA) over such language is known to be undecidable in general. For this reason, different fragments have emerged, introducing syntactic…
▽ More
Datalog^E is the extension of Datalog with existential quantification. While its high expressive power, underpinned by a simple syntax and the support for full recursion, renders it particularly suitable for modern applications on knowledge graphs, query answering (QA) over such language is known to be undecidable in general. For this reason, different fragments have emerged, introducing syntactic limitations to Datalog^E that strike a balance between its expressive power and the computational complexity of QA, to achieve decidability. In this short paper, we focus on two promising tractable candidates, namely Shy and Warded Datalog+/-. Reacting to an explicit interest from the community, we shed light on the relationship between these fragments. Moreover, we carry out an experimental analysis of the systems implementing Shy and Warded, respectively DLV^E and Vadalog.
△ Less
Submitted 10 August, 2022; v1 submitted 13 February, 2022;
originally announced February 2022.
-
A Standard Grammar for Temporal Logics on Finite Traces
Authors:
Marco Favorito
Abstract:
The heterogeneity of tools that support temporal logic formulae poses several challenges in terms of interoperability. In particular, a standard syntax for temporal logic on finite traces, despite similar to the one for infinite traces, is currently missing. This document proposes a standard grammar for several temporal logic formalisms interpreted over finite traces, like Linear Temporal Logic (L…
▽ More
The heterogeneity of tools that support temporal logic formulae poses several challenges in terms of interoperability. In particular, a standard syntax for temporal logic on finite traces, despite similar to the one for infinite traces, is currently missing. This document proposes a standard grammar for several temporal logic formalisms interpreted over finite traces, like Linear Temporal Logic (LTLf), Linear Dynamic Logic (LDLf), Pure-Past Linear Temporal Logic (PLTLf) and Pure-Past Linear Dynamic Logic (PLDLf).
△ Less
Submitted 7 June, 2021; v1 submitted 25 December, 2020;
originally announced December 2020.
-
Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf restraining specifications
Authors:
Giuseppe De Giacomo,
Luca Iocchi,
Marco Favorito,
Fabio Patrizi
Abstract:
In this work we investigate on the concept of "restraining bolt", envisioned in Science Fiction. Specifically we introduce a novel problem in AI. We have two distinct sets of features extracted from the world, one by the agent and one by the authority imposing restraining specifications (the "restraining bolt"). The two sets are apparently unrelated since of interest to independent parties, howeve…
▽ More
In this work we investigate on the concept of "restraining bolt", envisioned in Science Fiction. Specifically we introduce a novel problem in AI. We have two distinct sets of features extracted from the world, one by the agent and one by the authority imposing restraining specifications (the "restraining bolt"). The two sets are apparently unrelated since of interest to independent parties, however they both account for (aspects of) the same world. We consider the case in which the agent is a reinforcement learning agent on the first set of features, while the restraining bolt is specified logically using linear time logic on finite traces LTLf/LDLf over the second set of features. We show formally, and illustrate with examples, that, under general circumstances, the agent can learn while sha** its goals to suitably conform (as much as possible) to the restraining bolt specifications.
△ Less
Submitted 11 November, 2019; v1 submitted 17 July, 2018;
originally announced July 2018.
