Abstract There has been a massive interest in utilizing Linear Temporal Logic on finite traces ( $$\textsc {ltl}_f$$ L T L f ) as a specification language in the last decade, particularly in reactive synthesis. This highlights the need for a unified and efficient framework to fulfil the increasing demand for easy-to-use implementations of synthesis (and reasoning) algorithms for $$\textsc {ltl}_f$$ L T L f . To that end, we introduce , an open-source compositional symbolic synthesis framework that integrates efficient data structures and techniques focused on $$\textsc {ltl}_f$$ L T L f specifications. supports both explicit-DFA and symbolic-DFA construction from $$\textsc {ltl}_f$$ L T L f formulas, essential DFA manipulations, and offers an extensible framework for reactive synthesis of $$\textsc {ltl}_f$$ L T L f specifications, accommodating more complex synthesis scenarios. We demonstrate this feasibility by supporting $$\textsc {ltl}_f$$ L T L f synthesis as well as $$\textsc {ltl}_f$$ L T L f synthesis with ltl environment specifications expressed in various forms. is highly efficient and versatile, providing user-friendly C++ interfaces and extensive benchmarks that cater to a diverse audience, including computer scientists, practitioners, students, and the reactive synthesis research community.

We study planning for temporally extended goals expressed in Pure-Past Linear Temporal Logic ( ppltl ) in the context of deterministic (i.e., classical) and fully observable nondeterministic (FOND) domains. ppltl is the variant of Linear-time Temporal Logic on finite traces ( ltl f ) that refers to the past rather than the future. Although ppltl is as expressive as ltl f , we show that it is computationally much more effective for planning. In particular, we show that checking the validity of a plan for a ppltl formula is Markovian. This is achieved by introducing a linear number of additional propositional variables that capture the validity of the entire formula in a modular fashion. The solution encoding introduces only a linear number of new fluents proportional to the size of the ppltl goal and does not require any additional spurious action. We implement our solution technique in a system called Plan4Past , which can be used alongside state-of-the-art classical and FOND planners. Our empirical analysis demonstrates the practical effectiveness of Plan4Past in both classical and FOND problems, showing that the resulting planner performs overall better than other planning approaches for ltl f goals.

In recent decades, manufacturing practices have undergone a significant transformation, with the integration of computers and automation playing a central role. Concurrently, there has been a growing interest in utilizing intelligent techniques to effectively manage manufacturing processes. These processes entail the seamless integration of various activities across the supply chain. Given the diverse range of actors in a supply chain, each one with distinct characteristics such as cost, quality, and probability of failure, task assignment becomes a crucial challenge. In such a complex scenario, manual decision-making becomes impractical, necessitating the adoption of automated techniques to effectively address these challenges in a resilient and adaptive manner. This article proposes a service-oriented approach to model each manufacturing actor within the supply chain. Furthermore, it categorizes automated synthesis approaches for smart manufacturing on the basis ofi)the characteristics of each actor, which are retrieved by their Industrial API, andii)the goal(s) of the manufacturing process. Finally, the article evaluates three distinct approaches that implement automated synthesis techniques for composing services and generating operational plans.

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

Recently, Pure-Past Temporal Logic (PPLTL) has proven highly effective in specifying temporally extended goals in deterministic planning domains. In this paper, we show its effectiveness also for fully observable nondeterministic (FOND) planning, both for strong and strong-cyclic plans. We present a notably simple encoding of FOND planning for PPLTL goals into standard FOND planning for final-state goals. The encoding only introduces few fluents (at most linear in the PPLTL goal) without adding any spurious action and allows planners to lazily build the relevant part of the deterministic automaton for the goal formula on-the-fly during the search. We formally prove its correctness, implement it in a tool called Plan4Past, and experimentally show its practical effectiveness.

Distributed Ledger Technologies (DLTs), when managed by a few trusted validators, require most but not all of the machinery available in public DLTs. To profit from this s tate of affairs, we inject a PoA (Proof-of-Authority) protocol into Bitcoin, replacing its PoW. Our PoA consensus algorithm-built on top of PBFT and FROST-exhibits Byzantine Fault Tolerance and Confidentiality of the network configuration an d of th e quorum of signers. As such, it may become a modern and safe foundation for payment systems used in stablecoins, sidechains, and CBDCs.

Synthesis techniques for temporal logic specifications are typically based on exploiting symbolic techniques, as done in model checking. These symbolic techniques typically use backward fixpoint computation. Planning, which can be seen as a specific form of synthesis, is a witness of the success of forward search approaches. In this paper, we develop a forward-search approach to full-fledged Linear Temporal Logic on finite traces (LTLf) synthesis. We show how to compute the Deterministic Finite Automaton (DFA) of an LTLf formula on-the-fly, while performing an adversarial forward search towards the final states, by considering the DFA as a sort of AND-OR graph. Our approach is characterized by branching on suitable propositional formulas, instead of individual evaluations, hence radically reducing the branching factor of the search space. Specifically, we take advantage of techniques developed for knowledge compilation, such as Sentential Decision Diagrams (SDDs), to implement the approach efficiently.

In this demonstration, we introduce a system that facilitates trading agent competitions. Competitions mirror a Walrasian Exchange Economy. Each agent is endowed with a set of digital assets and preferences over them. Agents then trade these assets with each other to increase their respective utilities. They negotiate one-on-one to arrive at an optimal trade, and if successful, settle their transaction trustlessly on an emulated permissionless blockchain. This system is a precursor to a trading platform for digital assets and crypto-tokens in which agents trade on behalf of their users.

In this work we have investigated the concept of “restraining bolt”, inspired by Science Fiction. We have two distinct sets of features extracted from the world, one by the agent and one by the authority imposing some restraining specifications on the behaviour of the agent (the “restraining bolt”). The two sets of features and, hence the model of the world attainable from them, are apparently unrelated since of interest to independent parties. However they both account for (aspects of) the same world. We have considered the case in which the agent is a reinforcement learning agent on a set of low-level (subsymbolic) features, while the restraining bolt is specified logically using linear time logic on finite traces f/f over a set of high-level symbolic features. We show formally, and illustrate with examples, that, under general circumstances, the agent can learn while shaping its goals to suitably conform (as much as possible) to the restraining bolt specifications.1

In Markov Decision Processes (MDPs), rewards are assigned according to a function of the last state and action. This is often limiting, when the considered domain is not naturally Markovian, but becomes so after careful engineering of extended state space. The extended states record information from the past that is sufficient to assign rewards by looking just at the last state and action. Non-Markovian Reward Decision Processes (NRMDPs) extend MDPs by allowing for non-Markovian rewards, which depend on the history of states and actions. Non-Markovian rewards can be specified in temporal logics on finite traces such as LTLf/LDLf, with the great advantage of a higher abstraction and succinctness; they can then be automatically compiled into an MDP with an extended state space. We contribute to the techniques to handle temporal rewards and to the solutions to engineer them. We first present an approach to compiling temporal rewards which merges the formula automata into a single transducer, sometimes saving up to an exponential number of states. We then define monitoring rewards, which add a further level of abstraction to temporal rewards by adopting the four-valued conditions of runtime monitoring; we argue that our compilation technique allows for an efficient handling of monitoring rewards. Finally, we discuss application to reinforcement learning.