We study the common generalization of Markov decision processes (MDPs) with sets of transition probabilities, known as robust MDPs (RMDPs). A standard goal in RMDPs is to compute a policy that maximizes the expected return under an adversarial choice of the transition probabilities. If the uncertainty in the probabilities is independent between the states, known as s-rectangularity, such optimal robust policies can be computed efficiently using robust value iteration. However, there might still be multiple optimal robust policies, which, while equivalent with respect to the worst-case, reflect different expected returns under non-adversarial choices of the transition probabilities. Hence, we propose a refined policy selection criterion for RMDPs, drawing inspiration from the notions of dominance and best-effort in game theory. Instead of seeking a policy that only maximizes the worst-case expected return, we additionally require the policy to achieve a maximal expected return under different (i.e., not fully adversarial) transition probabilities. We call such a policy an optimal robust best-effort (ORBE) policy. We prove that ORBE policies always exist, characterize their structure, and present an algorithm to compute them with a manageable overhead over standard robust value iteration. ORBE policies offer a principled tie-breaker among optimal robust policies. Numerical experiments show the feasibility of our approach.

We investigate the problem of synthesizing strategies that guarantee the successful execution of a high-level nondeterministic agent program in Golog within a nondeterministic first-order basic action theory, considering the environment as adversarial. Our approach constructs a symbolic program graph that captures the control flow independently of the domain, enabling strategy synthesis through the cross product of the program graph with the domain model. We formally relate graph-based transitions to standard Golog semantics and provide a synthesis procedure that is sound though incomplete (in general, the problem is undecidable, given that we have a first-order representation of the state). We also extend the framework to handle the case where the environment's possible behaviors are specified by a Golog program.

We study stochastic planning problems in Markov Decision Processes (MDPs) with goals specified in Linear Temporal Logic (LTL). The state-of-the-art approach transforms LTL formulas into good-for-MDP (GFM) automata, which feature a restricted form of nondeterminism. These automata are then composed with the MDP, allowing the agent to resolve the nondeterminism during policy synthesis. A major factor affecting the scalability of this approach is the size of the generated automata. In this paper, we propose a novel GFM state-space reduction technique that significantly reduces the number of automata states. Our method employs a sophisticated chain of transformations, leveraging recent advances in good-for-games minimisation developed for adversarial settings. In addition to our theoretical contributions, we present empirical results demonstrating the practical effectiveness of our state-reduction technique. Furthermore, we introduce a direct construction method for formulas of the form GFφ, where φ is a co-safety formula. This construction is provably single-exponential in the worst case, in contrast to the general doubly-exponential complexity. Our experiments confirm the scalability advantages of this specialised construction.

Abstract Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak $$\omega $$ ω -automata (DWA). We show that syntactic obligations can be very efficiently converted to minimal DWA represented using multi-terminal binary decision diagrams (MTBDDs), and that synthesis of such specifications can be solved directly on the MTBDD representation on the fly. Our implementation in Spot shows substantial runtime improvements in translation and synthesis.

We study a model of Agentic AI, building on LTL synthesis originally studied in formal methods, that consists of autonomous agents with independent sequential decision-making capabilities. Specifically, we associate with each agent a goal expressed in LTL, and assumptions on the strategies employed by its peers and that the agent can exploit while synthesizing a strategy to realize its goal. While we can solve the synthesis problem under assumptions for each such agent we are not only interested in (1) synthesizing strategies for individual agents. Indeed, assumptions in turn are recursively defined through these strategy spaces. Importantly, we do not assume the ability to access or analyze an agent's internal strategy, as we make no assumptions about the nature of the decision makers, which may be, for example, ML-based. Instead, we focus on (2) characterizing the set of traces that are generated by strategies that realize the specification assigned to each agent. Using this characterization, we are able to (3) verify that the whole system, when in execution, satisfies a global objective, regardless of the strategies chosen by the agents from their allowed spaces. Moreover, by observing the evolution of the execution trace, we can (4) identify whether an agent makes a move that violates its specification and assign precise responsibility for the violation. Technically, we present automata-theoretic techniques to solve these problems, and show that each of them is 2EXPTIME-complete, matching the complexity of classical LTL synthesis.

Golog programs over Situation Calculus action theories were introduced as a specification of desired agent behavior, very much like temporally extended goals in planning, but with a focus on procedural aspects typical of programs. In the words of the original paper: "Golog allows the programmer to strike a compromise between the often computationally infeasible classical planning task, in which a plan must be deduced entirely from scratch, and detailed programming, in which every little step must be specified." In this paper, we study temporal synthesis with Golog programs as specifications over nondeterministic propositional action theories. We show that Golog has the same expressive power as linear dynamic logics on finite traces (LDLf), namely that of regular languages or monadic second-order logic (MSO) over finite traces, while exhibiting a markedly lower synthesis complexity: synthesis can be performed by constructing a polynomial-size program graph and taking its cross-product with the domain, whereas LDLf synthesis requires building a deterministic automaton of worst-case doubly exponential size. This advantage is confirmed experimentally.

Autonomous agents' goals typically change as they operate. Handling this is particularly challenging when the environment is nondetermnistic and the goals are temporally extended. In this paper, we assume that the agent operates in a fully observable nondeterministic (FOND) domain and uses Linear Temporal Logic over finite traces (LTLf) to represent goals. We use LTLf synthesis notions to formalize this problem of online agent goal management, handling goal adoption, goal dropping, and performing steps of the synthesized strategy, while ensuring that the agent's goals always remain realizable. We propose automata-based and formula progression-based methods to manage LTLf goals. We implement these methods and evaluate their effectiveness experimentally.

This paper presents a manifesto that articulates the conceptual foundations of Agentic Business Process Management (APM), an extension of Business Process Management (BPM) for governing autonomous agents executing processes in organizations. From a management perspective, APM represents a paradigm shift from the traditional view on business processes. This shift is driven by the realization of process awareness by agent-oriented abstractions: software and human agents act as primary functional entities that perceive, reason, and act within explicit process frames. Thus, APM moves away from automation-oriented BPM towards systems in which autonomy is constrained, aligned, and made operational through process aware agents. We introduce the core abstractions and architectural elements required to realize APM systems and elaborate on four key capabilities that agents in APM systems must support: framed autonomy , explainability , conversational actionability , and self-modification . These capabilities jointly ensure that agents’ goals are aligned with organizational goals and that agents behave in a framed yet proactive manner in pursuing those goals. We discuss the extent to which the capabilities can be realized and identify research challenges whose resolution requires further advances in BPM, AI, and multi-agent systems. The manifesto thus serves as a roadmap for bridging these communities and for guiding the development of APM systems in practice.

Abstract Inferring linear temporal logic over finite traces ($\text{LTL}_{\text{f}}$) formulas from a set of example traces, known as passive learning, presents significant challenges due to its combinatorial nature. In this paper, we introduce a novel approach to $\text{LTL}_{\text{f}}$ passive learning based on inductive logic programming (ILP), leveraging the inductive learning of answer set programs framework. Our ILP-based method effectively exploits the set of example traces to guide the learning process, and experimental results demonstrate that it o ffers a more efficient solution compared to traditional techniques based on propositional satisfiability.

We present a new formal framework for generalized planning (GP) based on the situation calculus extended with LTL constraints. The GP problem is specified by a first-order basic action theory whose models are the problem instances. This low-level theory is then abstracted into a high-level propositional nondeterministic basic action theory with a single model. A refinement mapping relates the two theories. LTL formulas are used to specify the temporally extended goals as well as assumed trace constraints. If all LTL trace constraints hold at the low level and the high-level model can simulate all the low-level models with respect to the mapping, we say that we have a temporally lifted abstraction. We prove that if we have such an abstraction and the agent has a strategy to achieve a LTL goal under some trace constraints at the abstract level, then there exists a refinement of the strategy to achieve the refinement of the goal at the concrete level. We use LTL synthesis to generate the strategy at the abstract level. We illustrate our approach by synthesizing a program that solves a data structure manipulation problem.

We study the problem of realizing strategies for an LTLf goal specification while ensuring that at least an LTLf backup specification is satisfied in case of unreliability of certain input variables. We formally define the problem and characterize its worst-case complexity as 2EXPTIME-complete, like standard LTLf synthesis. Then we devise three different solution techniques: one based on direct automata manipulation, which is 2EXPTIME, one disregarding unreliable input variables by adopting a belief construction, which is 3EXPTIME, and one leveraging second-order quantified LTLf (QLTLf), which is 2EXPTIME and allows for a direct encoding into monadic second-order logic, which in turn is worst-case nonelementary. We prove their correctness and evaluate them against each other empirically. Interestingly, theoretical worst-case bounds do not translate into observed performance; the MSO technique performs best, followed by belief construction and direct automata manipulation. As a byproduct of our study, we provide a general synthesis procedure for arbitrary QLTLf specifications.

Inspired by Joker strategies in games on graphs, we introduce and study the synthesis problem of minimal best-effort strategies for goals expressed in Linear Temporal Logic on Finite Traces (LTLf), assuming that the agent operates in a Fully Observable Nondeterministic (FOND) domain. Minimal best-effort strategies always exist and guarantee that, when a winning strategy does not exist: (i) the agent does its best to achieve its goal; (ii) it relies the least on the environment’s cooperation. We present a game-theoretic algorithm to synthesize minimal best-effort strategies and prove its correctness as well as its optimality (wrt computational complexity). We implemented the algorithm and performed an experimental analysis on scalable benchmarks. The empirical results show that the computation of minimal best-effort strategies is quite efficient: it only requires a small overhead compared to standard best-effort strategies.

We study a variant of LTLf synthesis that synthesizes adaptive strategies for achieving a multi-tier goal, consisting of multiple increasingly challenging LTLf objectives in nondeterministic planning domains. Adaptive strategies are strategies that at any point of their execution (i) enforce the satisfaction of as many objectives as possible in the multi-tier goal, and (ii) exploit possible cooperation from the environment to satisfy as many as possible of the remaining ones. This happens dynamically: if the environment cooperates (ii) and an objective becomes enforceable (i), then our strategies will enforce it. We provide a game-theoretic technique to compute adaptive strategies that is sound and complete. Notably, our technique is polynomial, in fact quadratic, in the number of objectives. In other words, it handles multi-tier goals with only a minor overhead compared to standard LTLf synthesis.

We study two logics, LTLf+ and PPLTL+, to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli’s LTL safety-progress hierarchy, and thus have the same expressive power as LTL. However, they also retain a crucial characteristic of reactive synthesis for the base logics: the game arena for strategy extraction can be derived from deterministic finite automata (DFA). Consequently, these logics circumvent the notorious difficulties associated with determinizing infinite trace automata, typical of LTL synthesis. We present optimal DFA-based technique for solving reactive synthesis for LTLf+ and PPLTL+. Additionally, we adapt these algorithms to optimally solve satisfiability and model-checking for these two logics.

The temporal logics LTLf+ and PPLTL+ have recently been introduced to express objectives over infinite traces. These logics are appealing because they match the expressive power of LTL on infinite traces while enabling efficient DFA-based techniques, which have been crucial to the scalability of reactive synthesis and adversarial planning in LTLf and PPLTL over finite traces. In this paper, we demonstrate that these logics are also highly effective in the context of MDPs. Introducing a technique tailored for probabilistic systems, we leverage the benefits of efficient DFA-based methods and compositionality. This approach is simpler than its nonprobabilistic counterparts in reactive synthesis and adversarial planning, as it accommodates a controlled form of nondeterminism ("good for MDPs") in the automata when transitioning from finite to infinite traces. Notably, by exploiting compositionality, our solution is both implementation-friendly and well-suited for straightforward symbolic implementations.

Responsibility is one of the key notions in machine ethics and in the area of autonomous systems. It is a multi-faceted notion involving counterfactual reasoning about actions and strategies. In this paper, we study different variants of responsibility for LTLf outcomes based on strategic reasoning. We show a connection with notions in reactive synthesis, including the synthesis of winning, dominant, and best-effort strategies. This connection provides a strong computational grounding of responsibility, allowing us to characterize the worst-case computa- tional complexity and devise sound, complete, and optimal algorithms for anticipating and attributing responsibility.

Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLf+ and PPLTL+, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach. We implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.

We investigate LTL synthesis under structured assumptions about the environment. In our setting, the environment is viewed by the protagonist as a collection of peer agents acting together in a shared world. In contrast to the symmetrical frameworks typically studied in multi-agent systems, we take a strikingly asymmetric first-person perspective in which the protagonist ascribes a specification to each of its peer agents and the world, capturing its understanding of their possible strategies. We show that in this setting, LTL synthesis has the same computational complexity as standard LTL synthesis, i.e., 2EXPTIME-complete. We establish this via a sophisticated, yet fully implementable, argument that builds on the notion of traces compatible with strategies: we use the fact that if the basic specification of the world and of each agent is given in LTL then the sets of traces compatible with the strategies describing the behaviors of the agents are omega-regular. This enables the use of word-automata rather than the more complicated tree-automata.

ltl_f reactive synthesis under environment specifications, which concerns the automated generation of strategies enforcing logical specifications, has emerged as a powerful technique for developing autonomous AI systems. It shares many similarities with Fully Observable Nondeterministic (fond) planning. In particular, nondeterministic domains can be expressed as ltl_f environment specifications. However, this is not needed since nondeterministic domains can be transformed into deterministic finite-state automata (dfa) to be used directly in the synthesis process. In this paper, we present a practical symbolic technique for translating domains expressed in Planning Domain Definition Language (pddl) into dfas. The technique allows for the integration of the planning domain, reduced to dfa in a symbolic form, into current symbolic ltl_f synthesis tools. We implemented our technique in a new tool, pddl2dfa, and applied it to solve fond planning by using state-of-the-art reactive synthesis techniques in a tool called syft4fond. Our empirical results confirm the effectiveness of our approach.

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 this paper, we study ltl f synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time.

Devising a strategy to make a system mimic behaviors from another system is a problem that naturally arises in many areas of Computer Science. In this work, we interpret this problem in the context of intelligent agents, from the perspective of LTLf, a formalism commonly used in AI for expressing finite-trace properties. Our model consists of two separated dynamic domains, D_A and D_B, and an LTLf specification that formalizes the notion of mimicking by mapping properties on behaviors (traces) of D_A into properties on behaviors of D_B. The goal is to synthesize a strategy that step-by-step maps every behavior of D_A into a behavior of D_B so that the specification is met. We consider several forms of mapping specifications, ranging from simple ones to full LTLf, and for each, we study synthesis algorithms and computational properties.

We present a general framework for abstracting agent behavior in multi-agent synchronous games in the situation calculus, which provides a first-order representation of the state and allows us to model how plays depend on the data and objects involved. We represent such games as action theories of a special form called situation calculus synchronous game structures (SCSGSs), in which we have a single action "tick" whose effects depend on the combination of moves selected by the players. In our framework, one specifies both an abstract SCSGS and a concrete SCSGS, as well as a refinement mapping that specifies how each abstract move is implemented by a Golog program defined over the concrete SCSGS. We define notions of sound and complete abstraction with respect to a mapping over such SCSGS. To express strategic properties on the abstract and concrete games we adopt a first-order variant of alternating-time mu-calculus mu-ATL-FO. We show that we can exploit abstraction in verifying mu-ATL-FO properties of SCSGSs under the assumption that agents can always execute abstract moves to completion even if not fully controlling their outcomes.

We present Pure-Past Action Masking (PPAM), a lightweight approach to action masking for safe reinforcement learning. In PPAM, actions are disallowed (“masked”) according to specifications expressed in Pure-Past Linear Temporal Logic (PPLTL). PPAM can enforce non-Markovian constraints, i.e., constraints based on the history of the system, rather than just the current state of the (possibly hidden) MDP. The features used in the safety constraint need not be the same as those used by the learning agent, allowing a clear separation of concerns between the safety constraints and reward specifications of the (learning) agent. We prove formally that an agent trained with PPAM can learn any optimal policy that satisfies the safety constraints, and that they are as expressive as shields, another approach to enforce non-Markovian constraints in RL. Finally, we provide empirical results showing how PPAM can guarantee constraint satisfaction in practice.

In this paper, we introduce Shielded FOND planning (S-FOND), which is the problem of computing a strategy to reach a final-state goal while preserving a safety specification called shield. In particular, we characterize shields as Pure-Past Linear Temporal Logic formulas that must hold in every prefix of a state trace induced by a solution strategy, thus capturing the whole safety fragment of Linear Temporal Logic formulas over finite traces. We propose three solution encodings for handling S-FOND problems: the first, which is our baseline, simply views a shield as a temporally extended goal; the second, instead, blocks the execution of further actions when the shield gets violated, and the third prevents the execution of actions that could violate the shield by using the notion of regression. We formally prove the correctness of each encoding and experimentally prove their effectiveness over a set of benchmark shields.

This paper introduces a novel algorithm for Reinforcement Learning (RL) in Regular Decision Processes (RDPs), a model of non-Markovian decision processes where dynamics and rewards depend on regular properties of the history. Our algorithm is inspired by Monte Carlo tree search (MCTS), yet it is improved with state merging capabilities. Performing merges allows us to evolve the tree model into a graph over time, as we periodically perform similarity tests borrowed from automata learning theory to learn states that are equivalent to one another. This results in improved efficiency and scalability over standard MCTS. We present empirical results that demonstrate orders of magnitude performance improvement over the state-of-the-art RL algorithms for RDPs.

Abstract With the growing use of temporal logics in areas ranging from robot planning to runtime verification, it is critical that users have a clear understanding of what a specification means. Toward this end, we have been developing a catalog of semantic errors and a suite of test instruments targeting various user-groups. The catalog is of interest to educators, to logic designers, to formula authors, and to tool builders, e.g., to identify mistakes. The test instruments are suitable for classroom teaching or self-study. This paper reports on five sets of survey data collected over a three-year span. We study misconceptions about finite-trace $$\textsc {ltl}_{f}$$ L T L f in three ltl-aware audiences, and misconceptions about standard ltl in novices. We find several mistakes, even among experts. In addition, the data supports several categories of errors in both $$\textsc {ltl}_{f}$$ L T L f and ltl that have not been identified in prior work. These findings, based on data from actual users, offer insights into what specific ways temporal logics are tricky and provide a groundwork for future interventions.

Classical planning problems are defined using some specification language, such as PDDL. The domain expert defines action schemas, objects, the initial state, and the goal. One key aspect of PDDL is that the set of objects cannot be modified during plan execution. While this is fine in many domains, sometimes it makes modeling more complicated. This may impact the performance of planners, and it requires the domain expert to bound the number of required objects beforehand, which can be a challenge. We introduce an extension to the classical planning formalism, where action effects can create and remove objects. This problem is semi-decidable, but it becomes decidable if we can bound the number of objects in any given state, even though the state space is still infinite. On the practical side, we extend the Powerlifted planning system to support this PDDL extension. Our results show that this extension improves the performance of Powerlifted while supporting more natural PDDL models.

To help it achieve its goal, an agent exploits assumptions it has about the behavior of its environment. The common view in planning and reactive synthesis is that such assumptions are sets of traces. This trace-centric view has the advantage of having well-understood specification formalisms, such as linear-time temporal logic. An alternative view, that we have promoted as being conceptually superior, is strategy-centric: assumptions are non-empty sets of environment strategies. In this work we relate these views and show that the strategy-centric view is a refinement of the trace-centric view. We thus address the following fundamental question: when should a set of traces be considered an assumption that the agent has about the environment's behavior? Our answer is in terms of coverability: every trace in the set should be consistent with some environment strategy that enforces it. We call such sets ``proper environment specifications''. Typical examples are given by (the traces consistent with a given) planning domain, and fairness constraints, but not arbitrary trace constraints. We provide an algorithm that, given a specification in linear-time temporal logic (LTL) decides whether or not it is a proper environment specification. Furthermore, we show that every set of traces has a ``proper environment core'', which excludes traces that the agent can ignore when devising its plan. We provide an algorithm for computing a representation of the core of an LTL formula, and prove that the core of an LTL-definable property is itself LTL-definable.

Abstract Goal Recognitionis the task of discerning the intended goal that an agent aims to achieve, given a set of goal hypotheses, a domain model, and a sequence of observations (i.e., a sample of the plan executed in the environment). Existing approaches assume that goal hypotheses comprise a single conjunctive formula over a single final state and that the environment dynamics are deterministic, preventing the recognition of temporally extended goals in more complex settings. In this paper, we expand goal recognition totemporally extended goalsinFully Observable Non-Deterministic(fond) planning domain models, focusing on goals on finite traces expressed inLinear Temporal Logic(ltl $$_f$$ f ) andPure-Past Linear Temporal Logic(ppltl). We develop the first approach capable of recognizing goals in such settings and evaluate it using differentltl $$_f$$ f andppltlgoals over sixfondplanning domain models. Empirical results show that our approach is accurate in recognizing temporally extended goals in different recognition settings.

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.

We study the synthesis under environment specifications problem for LTL/LTLf which, in particular, generalizes FOND (strong) planning with these temporal goals. We consider the case where the agent cannot enforce its goal --- for which the argument for using best-effort strategies has been made --- and study the intermediate ground, between enforcing and best-effort strategies, of dominant strategies. Intuitively, such strategies achieve the goal against any environment for which it is achievable. We show that dominant strategies may exist when enforcing ones do not, while still sharing with the latter many desirable properties such as being interchangeable with each other, and being monotone with respect to tightening of environment specifications. We give necessary and sufficient conditions for the existence of dominant strategies, and show that deciding if they exist is 2EXPTIME-complete --- the same as for enforcing strategies. Finally, we give a uniform, optimal, game-theoretic algorithm for simultaneously solving the three synthesis problems of enforcing, dominant, and best-effort strategies.

Every automaton can be decomposed into a cascade of basic prime automata. This is the Prime Decomposition Theorem by Krohn and Rhodes. Guided by this theory, we propose automata cascades as a structured, modular, way to describe automata as complex systems made of many components, each implementing a specific functionality. Any automaton can serve as a component; using specific components allows for a fine-grained control of the expressivity of the resulting class of automata; using prime automata as components implies specific expressivity guarantees. Moreover, specifying automata as cascades allows for describing the sample complexity of automata in terms of their components. We show that the sample complexity is linear in the number of components and the maximum complexity of a single component, modulo logarithmic factors. This opens to the possibility of learning automata representing large dynamical systems consisting of many parts interacting with each other. It is in sharp contrast with the established understanding of the sample complexity of automata, described in terms of the overall number of states and input letters, which implies that it is only possible to learn automata where the number of states is linear in the amount of data available. Instead our results show that one can learn automata with a number of states that is exponential in the amount of data available.

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.

We study best-effort strategies (aka plans) in fully observable nondeterministic domains (FOND) for goals expressed in Linear Temporal Logic on Finite Traces (LTLf). The notion of best-effort strategy has been introduced to also deal with the scenario when no agent strategy exists that fulfills the goal against every possible nondeterministic environment reaction. Such strategies fulfill the goal if possible, and do their best to do so otherwise. We present a game-theoretic technique for synthesizing best-effort strategies that exploit the specificity of nondeterministic planning domains. We formally show its correctness and demonstrate its effectiveness experimentally, exhibiting a much greater scalability with respect to a direct best-effort synthesis approach based on re-expressing the planning domain as generic environment specifications.

We develop a general framework for abstracting the behavior of an agent that operates in a nondeterministic domain, i.e., where the agent does not control the outcome of the nondeterministic actions, based on the nondeterministic situation calculus and the ConGolog programming language. We assume that we have both an abstract and a concrete nondeterministic basic action theory, and a refinement mapping which specifies how abstract actions, decomposed into agent actions and environment reactions, are implemented by concrete ConGolog programs. This new setting supports strategic reasoning and strategy synthesis, by allowing us to quantify separately on agent actions and environment reactions. We show that if the agent has a (strong FOND) plan/strategy to achieve a goal/complete a task at the abstract level, and it can always execute the nondeterministic abstract actions to completion at the concrete level, then there exist a refinement of it that is a (strong FOND) plan/strategy to achieve the refinement of the goal/task at the concrete level.

A critical challenge in neuro-symbolic (NeSy) approaches is to handle the symbol grounding problem without direct supervision. That is mapping high-dimensional raw data into an interpretation over a finite set of abstract concepts with a known meaning, without using labels. In this work, we ground symbols into sequences of images by exploiting symbolic logical knowledge in the form of Linear Temporal Logic over finite traces (LTLf) formulas, and sequence-level labels expressing if a sequence of images is compliant or not with the given formula. Our approach is based on translating the LTLf formula into an equivalent deterministic finite automaton (DFA) and interpreting the latter in fuzzy logic. Experiments show that our system outperforms recurrent neural networks in sequence classification and can reach high image classification accuracy without being trained with any single-image label.

We study reactive systems with Borel goals operating in a possibly non-Markovian stochastic environment. Moreover, the specific environment is not known, only its support is, i.e., at each step one knows which transitions are possible and which are impossible, but the probability distribution amongst the possible transitions is unknown. We consider system strategies that are maximal in the dominance order, i.e., no other strategy achieves the goal with at least the same probability in all environments, and with a higher probability in some environment. We call such strategies "stochastic best-effort". We prove the very general result that stochastic best-effort strategies exist for any Borel goal. We do this by providing local characterizations in terms of a three-valued abstraction of the probability of achieving the goal at a history. The correctness of the characterization is shown using a version of the Lebesgue Density Theorem from geometric measure theory. On the more practical side, we consider goals given in linear temporal logic. We establish the computational complexity of synthesizing a stochastic best-effort strategy, and show that it is not harder than synthesizing an optimal strategy in a domain with fixed known probabilities.

Devising a strategy to make a system mimic behaviors from another system is a problem that naturally arises in many areas of Computer Science. In this work, we interpret this problem in the context of intelligent agents, from the perspective of ltlf , a formalism commonly used in AI for expressing finite-trace properties. Our model consists of two separated dynamic domains, DA and DB, and an LTLf specification that formalizes the notion of mimicking by mapping properties on behaviors (traces) of DA into properties on behaviors of DB. The goal is to synthesize a strategy that step-by-step maps every behavior of DA into a behavior of DB so that the specification is met. We consider several forms of mapping specifications, ranging from simple ones to full LTLf , and for each, we study synthesis algorithms and computational properties.

In this paper, we study synthesis of maximally permissive strategies for Linear Temporal Logic on finite traces (LTLf) specifications. That is, instead of computing a single strategy (aka plan, or policy), we aim at computing the entire set of strategies at once and then choosing among them while in execution, without committing to a single one beforehand. Maximally permissive strategies have been introduced and investigated for safety properties, especially in the context of Discrete Event Control Theory. However, the available results for safety properties do not apply to reachability properties (eventually reach a given state of affair) nor to LTLf properties in general. In this paper, we show that maximally permissive strategies do exist also for reachability and general LTLf properties, and can in fact be computed with minimal overhead wrt the computation of a single strategy using state-of-the-art tools.

``Strong-cyclic policies" were introduced to formalize trial-and-error strategies and are known to work in Markovian stochastic domains, i.e., they guarantee that the goal is reached with probability 1. We introduce ``best-effort" policies for (not necessarily Markovian) stochastic domains. These generalize strong-cyclic policies by taking advantage of stochasticity even if the goal cannot be reached with probability 1. We compare such policies with optimal policies, i.e., policies that maximize the probability that the goal is achieved, and show that optimal policies are best-effort, but that the converse is false in general. With this framework at hand, we revisit the foundational problem of what it means to plan in nondeterministic domains when the nondeterminism has a stochastic nature. We show that one can view a nondeterministic planning domain as a representation of infinitely many stochastic domains with the same support but different probabilities, and that for temporally extended goals expressed in LTL/LTLf a finite-state best-effort policy in one of these domains is best-effort in each of the domains. In particular, this gives an approach for finding such policies that reduces to solving finite-state MDPs with LTL/LTLf goals. All this shows that ``best-effort" policies are robust to changes in the probabilities, as long as the support is unchanged.

We address the problem of model checking first-order dynamic systems where new objects can be injected in the active domain during execution. Notable examples are systems induced by a first-order action theory, e.g., expressed in the Situation Calculus. Recent results have shown that, under the state-boundedness assumption, such systems, in spite of having a first-order representation of the state, admit decidable model checking for full first-order mu-calculus. However, interestingly, model checking remains undecidable in the case of first-order LTL (LTL-FO). In this paper, we show that in LTL-FOp, which is the fragment of LTL-FO in which quantification is over objects that persist along traces, model checking state-bounded systems becomes decidable over finite and infinite traces. We then employ this result to show how to handle monitoring of LTL-FOp properties against a trace stemming from an unknown state-bounded dynamic system, simultaneously considering the finite trace up to the current point, and all its possibly infinite future continuations.

Manufacturing is transitioning from a mass production model to a service model in which facilities `bid' for previously unseen products. To decide whether to bid for a previously unseen product, a facility must be able to synthesize, on the fly, a process plan controller that delegates abstract manufacturing tasks in a supplied process recipe to the available manufacturing resources. First-order representations of the state are commonly considered in reasoning about action in AI. Here we show that we can leverage the wide literature on the Situation Calculus automatically synthesize such controllers. We identify two important decidable cases---finite domains and bounded action theories---for which we provide practical synthesis techniques.

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.

Our work aims at developing reinforcement learning algorithms that do not rely on the Markov assumption. We consider the class of Non-Markov Decision Processes where histories can be abstracted into a finite set of states while preserving the dynamics. We call it a Markov abstraction since it induces a Markov Decision Process over a set of states that encode the non-Markov dynamics. This phenomenon underlies the recently introduced Regular Decision Processes (as well as POMDPs where only a finite number of belief states is reachable). In all such kinds of decision process, an agent that uses a Markov abstraction can rely on the Markov property to achieve optimal behaviour. We show that Markov abstractions can be learned during reinforcement learning. Our approach combines automata learning and classic reinforcement learning. For these two tasks, standard algorithms can be employed. We show that our approach has PAC guarantees when the employed algorithms have PAC guarantees, and we also provide an experimental evaluation.

Abstract Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTL $$_f$$ f (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTL $$_f$$ f agent goal and a GR(1) environment specification. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.

The assessment of behavioral rules with respect to a given dataset is key in several research areas, including declarative process mining, association rule mining, and specification mining. An assessment is required to check how well a set of discovered rules describes the input data, and to determine to what extent data complies with predefined rules. Particularly in declarative process mining, Support and Confidence are used most often, yet they are reportedly unable to provide a sufficiently rich feedback to users and cause rules representing coincidental behavior to be deemed as representative for the event logs. In addition, these measures are designed to work on a predefined set of rules, thus lacking generality and extensibility. In this paper, we address this research gap by developing a measurement framework for temporal rules based on (LTLpf). The framework is suitable for any temporal rules expressed in a reactive form and for custom measures based on the probabilistic interpretation of such rules. We show that our framework can seamlessly adapt well-known measures of the association rule mining field to declarative process mining. Also, we test our software prototype implementing the framework on synthetic and real-world data, and investigate the properties characterizing those measures in the context of process analysis.

Runtime monitoring is a central operational decision support task in business process management. It helps process executors to check on-the-fly whether a running process instance satisfies business constraints of interest, providing an immediate feedback when deviations occur. We study runtime monitoring of properties expressed in ltl f , a variant of the classical ltl (Linear-time Temporal Logic) that is interpreted over finite traces, and in its extension ldl f , a powerful logic obtained by combining ltl f with regular expressions. We show that ldl f is able to declaratively express, in the logic itself, not only the constraints to be monitored, but also the de facto standard rv -LTL monitors. On the one hand, this enables us to directly employ the standard characterization of ldl f based on finite-state automata to monitor constraints in a fine-grained way. On the other hand, it provides the basis for declaratively expressing sophisticated metaconstraints that predicate on the monitoring state of other constraints, and to check them by relying on standard logical services instead of ad hoc algorithms. We then report on how this approach has been effectively implemented using Java to manipulate ldl f formulae and their corresponding monitors, and the RuM rule mining suite as underlying infrastructure.

We study best-effort synthesis under environment assumptions specified in LTL, and show that this problem has exactly the same computational complexity of standard LTL synthesis: 2EXPTIME-complete. We provide optimal algorithms for computing best-effort strategies, both in the case of LTL over infinite traces and LTL over finite traces (i.e., LTLf). The latter are particularly well suited for implementation.

The use of virtual collections of data is often essential in several data and knowledge management tasks. In the literature, the standard way to define virtual data collections is via views, i.e., virtual relations defined using queries. In data and knowledge bases, the notion of views is a staple of data access, data integration and exchange, query optimization, and data privacy. In this work, we study views in Ontology-Based Data Access (OBDA) systems. OBDA is a powerful paradigm for accessing data through an ontology, i.e., a conceptual specification of the domain of interest written using logical axioms. Intuitively, users of an OBDA system interact with the data only through the ontology's conceptual lens. We present a novel framework to express natural and sophisticated forms of views in OBDA systems and introduce fundamental reasoning tasks for these views. We study the computational complexity of these tasks and present classes of views for which these tasks are tractable or at least decidable.

Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTLf (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTLf agent goal and a GR(1) assumption. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.

Temporal logics over finite traces, such as LTLf and its extension LDLf, have been adopted in several areas, including Business Process Management (BPM), to check properties of processes whose executions have an unbounded, but finite, length. These logics express properties of single traces in isolation, however, especially in BPM it is also of interest to express properties over the entire log, i.e., properties that relate multiple traces of the log at once. In the case of infinite-traces, HyperLTL has been proposed to express these ``hyper'' properties. In this paper, motivated by BPM, we introduce HyperLDLf, a logic that extends LDLf with the hyper features of HyperLTL. We provide a sound, complete and computationally optimal technique, based on DFAs manipulation, for the model checking problem in the relevant case where the set of traces (i.e., the log) is a regular language. We illustrate how this form of model checking can be used for verifying log of business processes and for advanced forms of process mining.

Recently regular decision processes have been proposed as a well-behaved form of non-Markov decision process. Regular decision processes are characterised by a transition function and a reward function that depend on the whole history, though regularly (as in regular languages). In practice both the transition and the reward functions can be seen as finite transducers. We study reinforcement learning in regular decision processes. Our main contribution is to show that a near-optimal policy can be PAC-learned in polynomial time in a set of parameters that describe the underlying decision process. We argue that the identified set of parameters is minimal and it reasonably captures the difficulty of a regular decision process.

We formally introduce and solve the synthesis problem for LTL goals in the case of multiple, even contradicting, assumptions about the environment. Our solution concept is based on ``best-effort strategies'' which are agent plans that, for each of the environment specifications individually, achieve the agent goal against a maximal set of environments satisfying that specification. By means of a novel automata theoretic characterization we demonstrate that this best-effort synthesis for multiple environments is 2ExpTime-complete, i.e., no harder than plain LTL synthesis. We study an important case in which the environment specifications are increasingly indeterminate, and show that as in the case of a single environment, best-effort strategies always exist for this setting. Moreover, we show that in this setting the set of solutions are exactly the strategies formed as follows: amongst the best-effort agent strategies for ɸ under the environment specification E1, find those that do a best-effort for ɸ under (the more indeterminate) environment specification E2, and amongst those find those that do a best-effort for ɸ under the environment specification E3, etc.

We study the impact of the need for the agent to obligatorily instruct the action stop in her strategies. More specifically we consider synthesis (i.e., planning) for LTLf goals under LTL environment specifications in the case the agent must mandatorily stop at a certain point. We show that this obligation makes it impossible to exploit the liveness part of the LTL environment specifications to achieve her goal, effectively reducing the environment specifications to their safety part only. This has a deep impact on the efficiency of solving the synthesis, which can sidestep handling Buchi determinization associated to LTL synthesis, in favor of finite-state automata manipulation as in LTLf synthesis. Next, we add to the agent goal, expressed in LTLf, a safety goal, expressed in LTL. Safety goals must hold forever, even when the agent stops, since the environment can still continue its evolution. Hence the agent, before stopping, must ensure that her safety goal will be maintained even after she stops. To do synthesis in this case, we devise an effective approach that mixes a synthesis technique based on finite-state automata (as in the case of LTLf goals) and model-checking of nondeterministic Buchi automata. In this way, again, we sidestep Buchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.

The standard situation calculus assumes that atomic actions are deterministic. But many domains involve nondeterministic actions, with problems such as fully observable nondeterministic (FOND) planning and high-level program execution requiring solutions. Various approaches have been proposed to accommodate nondeterminism on top of the standard situation calculus language, for instance by introducing nondeterministic programs as in Golog and ConGolog. But a key problem in these approaches is that they don’t clearly distinguish between choices that can be made by the agent and choices that are made by the environment, i.e., angelic vs. devilish nondeterminism. In this paper, we propose a simple extension to the standard situation calculus that accommodates nondeterministic actions and preserves Reiter’s solution to the frame problem and answering projection queries through regression. We also provide a formalization of FOND planning and show how ConGolog high-level program execution in nondeterministic domains can be defined.

Trace Alignment is a prominent problem in Declarative Process Mining, which consists in identifying a minimal set of modifications that a log trace (produced by a system under execution) requires in order to be made compliant with a temporal specification. In its simplest form, log traces are sequences of events from a finite alphabet and specifications are written in DECLARE, a strict sublanguage of linear-time temporal logic over finite traces (LTLf ). The best approach for trace alignment has been developed in AI, using cost-optimal planning, and handles the whole LTLf . In this paper, we study the timed version of trace alignment, where events are paired with timestamps and specifications are provided in metric temporal logic over finite traces (MTLf ), essentially a superlanguage of LTLf . Due to the infiniteness of timestamps, this variant is substantially more challenging than the basic version, as the structures involved in the search are (uncountably) infinite-state, and calls for a more sophisticated machinery based on alternating (timed) automata, as opposed to the standard finite-state automata sufficient for the untimed version. The main contribution of the paper is a provably correct, effective technique for Timed Trace Alignment that takes advantage of results on MTLf decidability as well as on reachability for well-structured transition systems.

In this paper we study instance-level update in DL-LiteA , a well-known description logic that influenced the OWL 2 QL standard. Instance-level update regards insertions and deletions in the ABox of an ontology. In particular we focus on formula-based approaches to instance-level update. We show that DL-LiteA , which is well-known for enjoying first-order rewritability of query answering, enjoys a first-order rewritability property also for instance-level update. That is, every update can be reformulated into a set of insertion and deletion instructions computable through a non-recursive Datalog program with negation. Such a program is readily translatable into a first-order query over the ABox considered as a database, and hence into SQL. By exploiting this result, we implement an update component for DL-LiteA-based systems and perform some experiments showing that the approach works in practice.

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 synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLƒ goals on finite traces, environment assumptions need to be expressed over infinite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to finite-trace LTLƒ goals under infinite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLƒ and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTLƒ synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLƒ synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis.

The assessment of behavioral rules with respect to a given dataset is key in several research areas, including declarative process mining, association rule mining, and specification mining. The assessment is required to check how well a set of discovered rules describes the input data, as well as to determine to what extent data complies with predefined rules. In declarative process mining, in particular, some measures have been taken from association rule mining and adapted to support the assessment of temporal rules on event logs. Among them, support and confidence are used most often, yet they are reportedly unable to provide a sufficiently rich feedback to users and often cause spurious rules to be discovered from logs. In addition, these measures are designed to work on a predefined set of rules, thus lacking generality and extensibility. In this paper, we address this research gap by developing a general measurement framework for temporal rules based on Linear-time Temporal Logic with Past on Finite Traces (LTLpf). The framework is independent from the rule-specification language of choice and allows users to define new measures. We show that our framework can seamlessly adapt well-known measures of the association rule mining field to declarative process mining. Also, we test our software prototype implementing the framework on synthetic and real-world data, and investigate the properties characterizing those measures in the context of process analysis.

We consider an agent that operates with two models of the environment: one that captures expected behaviors and one that captures additional exceptional behaviors. We study the problem of synthesizing agent strategies that enforce a goal against environments operating as expected while also making a best effort against exceptional environment behaviors. We formalize these concepts in the context of linear-temporal logic, and give an algorithm for solving this problem. We also show that there is no trade-off between enforcing the goal under the expected environment specification and making a best-effort for it under the exceptional one.

We review PLTLf and PLDLf, the pure-past versions of the well-known logics on finite traces LTLf and LDLf, respectively. PLTLf and PLDLf are logics about the past, and so scan the trace backwards from the end towards the beginning. Because of this, we can exploit a foundational result on reverse languages to get an exponential improvement, over LTLf /LDLf , for computing the corresponding DFA. This exponential improvement is reflected in several forms of sequential decision making involving temporal specifications, such as planning and decision problems in non-deterministic and non-Markovian domains. Interestingly, PLTLf (resp., PLDLf ) has the same expressive power as LTLf (resp., LDLf ), but transforming a PLTLf (resp., PLDLf ) formula into its equivalent LTLf (resp.,LDLf) is quite expensive. Hence, to take advantage of the exponential improvement, properties of interest must be directly expressed in PLTLf /PLDLf .

We look at program synthesis where the aim is to automatically synthesize a controller that operates on data structures and from which a concrete program can be easily derived. We do not aim at a fully-automatic process or tool that produces a program meeting a given specification of the program’s behaviour. Rather, we aim at the design of a clear and well-founded approach for supporting programmers at the design and implementation phases. Concretely, we first show that a program synthesis task can be modeled as a generalized planning problem. This is done at an abstraction level where the involved data structures are seen as black-boxes that can be interfaced with actions and observations, the first corresponding to the operations and the second to the queries provided by the data structure. The abstraction level is high enough to capture intuitive and common assumptions as well as general and simple strategies used by programmers, and yet it contains sufficient structure to support the automated generation of concrete solutions (in the form of controllers). From such controllers and the use of standard data structures, an actual program in a general language like C++ or Python can be easily obtained. Then, we discuss how the resulting generalized planning problem can be reduced to an LTL synthesis problem, thus making available any LTL synthesis engine for obtaining the controllers. We illustrate the effectiveness of the approach on a series of examples.

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.

Nondeterministic strategies are strategies (or protocols, or plans) that, given a history in a game, assign a set of possible actions, all of which are winning. An important problem is that of refining such strategies. For instance, given a nondeterministic strategy that allows only safe executions, refine it to, additionally, eventually reach a desired state of affairs. We show that strategic problems involving strategy refinement can be solved elegantly in the framework of Strategy Logic (SL), a very expressive logic to reason about strategic abilities. Specifically, we introduce an extension of SL with nondeterministic strategies and an operator expressing strategy refinement. We show that model checking this logic can be done at no additional computational cost with respect to standard SL, and can be used to solve a variety of problems such as synthesis of maximally permissive strategies or refinement of Nash equilibria.

In synthesis, assumption are constraints on the environments that rule out certain environment behaviors. A key observation is that even if we consider system with LTLf goals on finite traces, assumptions need to be expressed considering infinite traces, using LTL on infinite traces, since the decision to stop the trace is controlled by the agent. To solve synthesis of LTLf goals under LTL assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both are 2EXPTIME-complete), the algorithms available for LTL synthesis are much harder in practice than those for LTLf synthesis. Recently, it has been shown that in basic forms of fairness and stability assumptions we can avoid such a detour to LTL and keep the simplicity of LTLf synthesis. In this paper, we generalize these results and show how to effectively handle any kind of LTL assumptions. Specifically, we devise a two-stage technique for solving LTLf under general LTL assumptions and show empirically that this technique performs much better than standard LTL synthesis.

There has recently been increasing interest in using reactive synthesis techniques to automate the production of manufacturing process plans. Previous work has assumed that the set of manufacturing resources is known and fixed in advance. In this paper, we consider the more general problem of whether a controller can be synthesized given sufficient resources. In the unbounded setting, only the types of available manufacturing resources are given, and we want to know whether it is possible to manufacture a product using only resources of those type(s), and, if so, how many resources of each type are needed. We model manufacturing processes and facilities as transducers (automata with output), and show that the unbounded orchestration problem is decidable and the (Pareto) optimal set of resources necessary to manufacture a product is computable for uni-transducers. However, for multitransducers, the problem is undecidable.

In this paper, we investigate non-Markovian Nondeterministic Fully Observable Planning Domains (NMFONDs), variants of Nondeterministic Fully Observable Planning Domains (FONDs) where the next state is determined by the full history leading to the current state. In particular, we introduce TFONDs which are NMFONDs where conditions on the history are succinctly and declaratively specified using the linear-time temporal logic on finite traces LTLf and its extension LDLf. We provide algorithms for planning in TFONDs for general LTLf/LDLf goals, and establish tight complexity bounds w.r.t. the domain representation and the goal, separately. We also show that TFONDs are able to capture all NMFONDs in which the dependency on the history is "finite state". Finally, we show that TFONDs also capture Partially Observable Nondeterministic Planning Domains (PONDs), but without referring to unobservable variables.

We introduce and study Regular Decision Processes (RDPs), a new, compact, factored model for domains with non-Markovian dynamics and rewards. In RDPs, transition and reward functions are specified using formulas in linear dynamic logic over finite traces, a language with the expressive power of regular expressions. This allows specifying complex dependence on the past using intuitive and compact formulas, and provides a model that generalizes MDPs and k-order MDPs. RDPs can also approximate POMDPs without having to postulate the existence of hidden variables, and, in principle, can be learned from observations only.

In Markov Decision Processes (MDPs), the reward obtained in a state is Markovian, i.e., depends on the last state and action. This dependency makes it difficult to reward more interesting long-term behaviors, such as always closing a door after it has been opened, or providing coffee only following a request. Extending MDPs to handle non-Markovian reward functions was the subject of two previous lines of work. Both use LTL variants to specify the reward function and then compile the new model back into a Markovian model. Building on recent progress in temporal logics over finite traces, we adopt LDLf for specifying non-Markovian rewards and provide an elegant automata construction for building a Markovian model, which extends that of previous work and offers strong minimality and compositionality guarantees.

In this paper, we model manufacturing processes and facilities as transducers (automata with output). The problem of whether a given manufacturing process can be realized by a given set of manufacturing resources can then be stated as an orchestration problem for transducers. We first consider the conceptually simpler case of uni-transducers (transducers with a single input and a single output port), and show that synthesizing orchestrations for uni-transducers is EXPTIME-complete. Surprisingly, the complexity remains the same for the more expressive multi-transducer case, where transducers have multiple input and output ports and the orchestration is in charge of dynamically connecting ports during execution.

We develop a general framework for abstracting online behavior of an agent that may acquire new knowledge during execution (e.g., by sensing), in the situation calculus and ConGolog. We assume that we have both a high-level action theory and a low-level one that represent the agent's behavior at different levels of detail. In this setting, we define ability to perform a task/achieve a goal, and then show that under some reasonable assumptions, if the agent has a strategy by which she is able to achieve a goal at the high level, then we can refine it into a low-level strategy to do so.

We study planning for LTLf and LDLf temporally extended goals in nondeterministic fully observable domains (FOND). We consider both strong and strong cyclic plans, and develop foundational automata-based techniques to deal with both cases. Using these techniques we provide the computational characterization of both problems, separating the complexity in the size of the domain specification from that in the size of the formula. Specifically we establish them to be EXPTIME-complete and 2EXPTIME-complete, respectively, for both problems. In doing so, we also show 2EXPTIME-hardness for strong cyclic plans, which was open.

One major task in business process management is that of aligning real process execution traces to a process model by (minimally) introducing and eliminating steps. Here, we look at declarative process specifications expressed in Linear Temporal Logic on finite traces (LTLf). We provide a sound and complete technique to synthesize the alignment instructions relying on finite automata theoretic manipulations. Such a technique can be effectively implemented by using planning technology. Notably, the resulting planning-based alignment system significantly outperforms all current state-of-the-art ad-hoc alignment systems. We report an in-depth experimental study that supports this claim.

We study the characterization and computation of general policies for families of problems that share a structure characterized by a common reduction into a single abstract problem. Policies mu that solve the abstract problem P have been shown to solve all problems Q that reduce to P provided that mu terminates in Q. In this work, we shed light on why this termination condition is needed and how it can be removed. The key observation is that the abstract problem P captures the common structure among the concrete problems Q that is local (Markovian) but misses common structure that is global. We show how such global structure can be captured by means of trajectory constraints that in many cases can be expressed as LTL formulas, thus reducing generalized planning to LTL synthesis. Moreover, for a broad class of problems that involve integer variables that can be increased or decreased, trajectory constraints can be compiled away, reducing generalized planning to fully observable non-deterministic planning.

We address verification of high-level programs over situation calculus action theories that have an infinite object domain, but bounded fluent extensions in each situation. We show that verification of mu-calculus temporal properties against ConGolog programs over such bounded theories is decidable in general. To do this, we reformulate the transition semantics of ConGolog to keep the bindings of “pick variables” into a separate variable environment whose size is naturally bounded by the number of variables. We also show that for situation-determined ConGolog programs, we can compile away the program into the action theory itself without loss of generality. This can also be done for arbitrary programs, but only to check certain properties, such as if a situation is the result of a program execution, not for mu-calculus verification.

We present a situation calculus-based account of multi-players synchronous games in the style of general game playing. Such games can be represented as action theories of a special form, situation calculus synchronous game structures (SCSGSs), in which we have a single action tick whose effects depend on the combination of moves selected by the players. Then one can express properties of the game, e.g., winning conditions, playability, weak and strong winnability, etc. in a first-order alternating-time μ-calculus. We discuss verification in this framework considering computational effectiveness. We also show that SCSGSs can be considered as a first-order variant of the Game Description Language (GDL) that supports infinite domains and possibly non-terminating games. We do so by giving a translation of GDL specifications into SCSGSs and showing its correctness. Finally, we show how a player's possible moves can be specified in a Golog-like programming language.

This is an extended abstract about what is hot in the field of Knowledge Representation and Reasoning.

In this talk, we survey recent results on situation calculus bounded action theories. These are action theories with the constraints that the size of the extension of fluents in every situation must be bounded, though such an extension changes from situation to situation. Such action theories give rise to infinite transition systems that can be faithfully abstracted into finite ones, making verification decidable.

In this paper we study when an LTL formula on finite traces (LTLf formula) is insensitive to infiniteness, that is, it can be correctly handled as a formula on infinite traces under the assumption that at a certain point the infinite trace starts repeating an end event forever, trivializing all other propositions to false. This intuition has been put forward and (wrongly) assumed to hold in general in the literature. We define a necessary and sufficient condition to characterize whether an LTLf formula is insensitive to infiniteness, which can be automatically checked by any LTL reasoner. Then, we show that typical LTLf specification patterns used in process and service modeling in CS, as well as trajectory constraints in Planning and transition-based LTLf specifications of action domains in KR, are indeed very often insensitive to infiniteness. This may help to explain why the assumption of interpreting LTL on finite and on infinite traces has been (wrongly) blurred. Possibly because of this blurring, virtually all literature detours to Buechi automata for constructing the NFA that accepts the traces satisfying an LTLf formula. As a further contribution, we give a simple direct algorithm for computing such NFA.

We look at agents reasoning about actions from a first-person perspective. The agent has a representation of world as situation calculus action theory. It can perform sensing actions to acquire information. The agent acts “online”, i.e., it performs an action only if it is certain that the action can be executed, and collects sensing results from the actual world. When the agent reasons about its future actions, it indeed considers that it is acting online; however only possible sensing values are available. The kind of reasoning about actions we consider for the agent is verifying a first-order (FO) variant (without quantification across situations) of linear time temporal logic (LTL) . We mainly focus on bounded action theories, where the number of facts that are true in any situation is bounded. The main results of this paper are: (i) possible sensing values can be based on consistency if the initial situation description is FO; (ii) for bounded action theories, progression over histories that include sensing results is always FO; (iii) for bounded theories, verifying our FO LTL against online executions with sensing is decidable.

In this work we survey the research on foundations of data-aware (business) processes that has been carried out in the database theory community. We show that this community has indeed developed over the years a multi-faceted culture of merging data and processes. We argue that it is this community that should lay the foundations to solve, at least from the point of view of formal analysis, the dichotomy between data and processes still persisting in business process management.

Data-centric dynamic systems are systems where both the process controlling the dynamics and the manipulation of data are equally central. We study verification of (first-order) mu-calculus variants over relational data-centric dynamic systems, where data are maintained in a relational database, and the process is described in terms of atomic actions that evolve the database. Action execution may involve calls to external services, thus inserting fresh data into the system. As a result such systems are infinite-state. We show that verification is undecidable in general, and we isolate notable cases where decidability is achieved. Specifically we start by considering service calls that return values deterministically (depending only on passed parameters). We show that in a mu-calculus variant that preserves knowledge of objects appeared along a run we get decidability under the assumption that the fresh data introduced along a run are bounded, though they might not be bounded in the overall system. In fact we tie such a result to a notion related to weak acyclicity studied in data exchange. Then, we move to nondeterministic services and we investigate decidability under the assumption that knowledge of objects is preserved only if they are continuously present. We show that if infinitely many values occur in a run but do not accumulate in the same state, then we get again decidability. We give syntactic conditions to avoid this accumulation through the novel notion of "generate-recall acyclicity", which ensures that every service call activation generates new values that cannot be accumulated indefinitely.

Description logic Knowledge and Action Bases (KAB) are a mechanism for providing both a semantically rich representation of the information on the domain of interest in terms of a description logic knowledge base and actions to change such information over time, possibly introducing new objects. We resort to a variant of DL-Lite where the unique name assumption is not enforced and where equality between objects may be asserted and inferred. Actions are specified as sets of conditional effects, where conditions are based on epistemic queries over the knowledge base (TBox and ABox), and effects are expressed in terms of new ABoxes. In this setting, we address verification of temporal properties expressed in a variant of first-order mu-calculus with quantification across states. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of weak acyclicity in data exchange.

Ontology-based data access (OBDA) is a novel paradigm for accessing large data repositories through an ontology, that is a formal description of a domain of interest. Supporting the management of OBDA applications poses new challenges, as it requires to provide effective tools for (i) allowing both expert and non-expert users to analyze the OBDA specification, (ii) collaboratively documenting the ontology, (iii) exploiting OBDA services, such as query answering and automated reasoning over ontologies, e.g., to support data quality check, and (iv) tuning the OBDA application towards optimized performances. To fulfill these challenges, we have built a novel system, called MASTRO STUDIO, based on a tool for automated reasoning over ontologies, enhanced with a suite of tools and optimization facilities for managing OBDA applications. To show the effectiveness of MASTRO STUDIO, we demonstrate its usage in one OBDA application developed in collaboration with the Italian Ministry of Economy and Finance.

In this paper we introduce the notion of mapping-based knowledge base (MKB) to formalize the situation where both the extensional and the intensional level of the ontology are determined by suitable mappings to a set of (relational) data sources. This allows for making the intensional level of the ontology as dynamic as traditionally the extensional level is. To do so, we resort to the meta-modeling capabilities of higher-order Description Logics, which allow us to see concepts and roles as individuals, and vice versa. The challenge in this setting is to design tractable query answering algorithms. Besides the definition of MKBs, our main result is that answering instance queries posed to MKBs expressed in Hi(DL-LiteR) can be done efficiently. In particular, we define a query rewriting technique that produces first-order (SQL) queries to be posed to the data sources.

An artifact-centric service is a stateful service that holistically represents both the data and the process in terms of a (dynamic) artifact. An artifact is constituted by a data component, holding all the data of interest for the service, and a lifecycle, which specifies the process that the service enacts. In this paper, we study artifact-centric services whose data component is a full-fledged relational database, queried through (first-order) conjunctive queries, and the lifecycle component is specified as sets of condition-action rules, where actions are tasks invocations, again based on conjunctive queries. Notably, the database can evolve in an unbounded way due to new values (unknown at verification time) inserted by tasks. The main result of the paper is that verification in this setting is decidable under a reasonable restriction on the form of tasks, called weak acyclicity, which we borrow from the recent literature on data exchange. In particular, we develop a sound, complete and terminating verification procedure for sophisticated temporal properties expressed in a first-order variant of μ-calculus.

Schema mappings establish a correspondence between data stored in two databases, called source and target respectively. Query processing under schema mappings has been investigated extensively in the two cases where each target atom is mapped to a query over the source (called GAV, global-as-view), and where each source atom is mapped to a query over the target (called LAV, local-as-view). The general case, called GLAV, in which queries over the source are mapped to queries over the target, has attracted a lot of attention recently, especially for data exchange. However, query processing for GLAV mappings has been considered only for the basic service of query answering, and mainly in the context of conjunctive queries (CQs) in relational databases. In this paper we study query processing for GLAV mappings in a wider sense, considering not only query answering, but also query rewriting, perfectness (the property of a rewriting to compute exactly the certain answers), and query containment relative to a mapping. We deal both with the relational case, and with graph databases, where the basic querying mechanism is that of regular path queries. Query answering in GLAV can be smoothly reduced to a combination of the LAV and GAV cases, and for CQs this reduction can be exploited also for the remaining query processing tasks. In contrast, as we show, GLAV query processing for graph databases is non-trivial and requires new insights and techniques. We obtain upper bounds for answering, rewriting, and perfectness, and show decidability of relative containment.

We investigate an extension of Description Logics (DL) with higher-order capabilities, based on Henkin-style semantics. Our study starts from the observation that the various possibilities of adding higher-order con- structs to a DL form a spectrum of increasing expres- sive power, including domain metamodeling, i.e., using concepts and roles as predicate arguments. We argue that higher-order features of this type are sufficiently rich and powerful for the modeling requirements aris- ing in many relevant situations, and therefore we carry out an investigation of the computational complexity of satisfiability and conjunctive query answering in DLs extended with such higher-order features. In particular, we show that adding domain metamodeling capabilities to SHIQ (the core of OWL 2) has no impact on the complexity of the various reasoning tasks. This is also true for DL-LiteR (the core of OWL 2 QL) under suit- able restrictions on the queries.

A schema mapping is a formal specification of the relationship holding between the databases conforming to two given schemas, called source and target, respectively. While in the general case a schema mapping is specified in terms of assertions relating two queries in some given language, various simplified forms of mappings, in particular LAV and GAV, have been considered, based on desirable properties that these forms enjoy. Recent works propose methods for transforming schema mappings to logically equivalent ones of a simplified form. In many cases, this transformation is impossible, and one might be interested in finding simplifications based on a weaker notion, namely logical implication, rather than equivalence. More precisely, given a schema mapping M, find a simplified (LAV, or GAV) schema mapping M' such that M' logically implies M. In this paper we formally introduce this problem, and study it in a variety of cases, providing techniques and complexity bounds. The various cases we consider depend on three parameters: the simplified form to achieve (LAV, or GAV), the type of schema mapping considered (sound, or exact), and the query language used in the schema mapping specification (conjunctive queries and variants over relational databases, or regular path queries and variants over graph databases). Notably, this is the first work on comparing schema mappings for graph databases.

This work develops an approach to efficient reasoning in first-order knowledge bases with incomplete information. We build on Levesque's proper knowledge bases approach, which supports limited incomplete knowledge in the form of a possibly infinite set of positive or negative ground facts. We propose a generalization which allows these facts to involve unknown individuals, as in the work on labeled null values in databases. Dealing with such unknown individuals has been shown to be a key feature in the database literature on data integration and data exchange. In this way, we obtain one of the most expressive first-order open-world settings for which reasoning can still be done efficiently by evaluation, as in relational databases. We show the soundness of the reasoning procedure and its completeness for queries in a certain normal form.

We give a formal definition of generalized planning that is independent of any representation formalism. We assume that our generalized plans must work on a set of deterministic environments, which are essentially unrelated to each other. We prove that generalized planning for a finite set of environments is always decidable and EXPSPACE-complete. Our proof is constructive and gives us a sound, complete and complexity-wise optimal technique. We also consider infinite sets of environments, and show that generalized planning for the infinite "one-dimensional problems," known in the literature to be recursively enumerable when restricted to finite-state plans, is EXPSPACE-decidable without sequence functions, and solvable by generalized planning for finite sets.

Classical planning has been notably successful in synthesizing finite plans to achieve states where propositional goals hold. In the last few years, classical planning has also been extended to incorporate temporally extended goals, expressed in temporal logics such as LTL, to impose restrictions on the state sequences generated by finite plans. In this work, we take the next step and consider the computation of infinite plans for achieving arbitrary LTL goals. We show that infinite plans can also be obtained efficiently by calling a classical planner once over a classical planning encoding that represents and extends the composition of the planning domain and the Büchi automaton representing the goal. This compilation scheme has been implemented and a number of experiments are reported.

The study of node-selection query languages for (finite) trees has been a major topic in the recent research on query lan- guages for Web documents. On one hand, there has been an extensive study of XPath and its various extensions. On the other hand, query languages based on classical logics, such as first-order logic (FO) or monadic second-order logic (MSO), have been considered. Results in this area typically relate an Xpath-based language to a classical logic. What has yet to emerge is an XPath-related language that is expressive as MSO, and at the same time enjoys the computational proper- ties of XPath, which are linear query evaluation and exponen- tial query-containment test. In this paper we propose μXPath, which is the alternation-free fragment of XPath extended with fixpoint operators. Using two-way alternating automata, we show that this language does combine desired expressiveness and computational properties, placing it as an attractive can- didate as the definite query language for trees.

In this paper, we review a series of agent behavior synthesis problems under full observability and nondeterminism (partial controllability), ranging from conditional planning, to recently introduced agent planning programs, and to sophisticated forms of agent behavior compositions, and show that all of them can be solved by model checking two-player game structures. These structures are akin to transition systems/Kripke structures, usually adopted in model checking, except that they distinguish (and hence allow to separately quantify) between the actions/moves of two antagonistic players. We show that using them we can implement solvers for several agent behavior synthesis problems.

A Description Logic (DL) ontology is constituted by two components, a TBox that expresses general knowledge about the concepts and their relationships, and an ABox that describes the properties of individuals that are instances of concepts. We address the problem of how to deal with changes to a DL ontology, when these changes affect only the ABox, i.e. when the TBox is considered invariant. We consider two basic changes, namely instance-level update and instance-level erasure, roughly corresponding to the addition and the deletion of a set of facts involving individuals. We characterize the semantics of instance-level update and erasure on the basis of the approaches proposed by Winslett and by Katsuno and Mendelzon. Interestingly, DLs are typically not closed with respect to instance-level update and erasure, in the sense that the set of models corresponding to the application of any of these operations to a knowledge base in a DL L may not be expressible by ABoxes in L⁠. In particular, we show that this is true for DL-LiteF⁠, a tractable DL that is oriented towards data-intensive applications. To deal with this problem, we first introduce DL-LiteFS⁠, a DL that minimally extends DL-LiteF and is closed with respect to instance-level update, and present a polynomial algorithm for computing instance-level update in this logic. Then, we provide a principled notion of best approximation with respect to a fixed language L of instance-level update and erasure, and exploit the algorithm for instance-level update for DL-LiteFS to get polynomial algorithms for approximated instance-level update and erasure for DL-LiteF⁠. These results confirm the nice computational properties of DL-LiteF for data intensive applications, even where information about instances is not only read, but also written.

Query containment and query answering are two important computational tasks in databases. While query answering amounts to computing the result of a query over a database, query containment is the problem of checking whether, for every database, the result of one query is a subset of the result of another query. In this article, we deal with unions of conjunctive queries, and we address query containment and query answering under description logic constraints. Every such constraint is essentially an inclusion dependency between concepts and relations, and their expressive power is due to the possibility of using complex expressions in the specification of the dependencies, for example, intersection and difference of relations, special forms of quantification, regular expressions over binary relations. These types of constraints capture a great variety of data models, including the relational, the entity-relationship, and the object-oriented model, all extended with various forms of constraints. They also capture the basic features of the ontology languages used in the context of the Semantic Web. We present the following results on both query containment and query answering. We provide a method for query containment under description logic constraints, thus showing that the problem is decidable, and analyze its computational complexity. We prove that query containment is undecidable in the case where we allow inequalities in the right-hand-side query, even for very simple constraints and queries. We show that query answering under description logic constraints can be reduced to query containment, and illustrate how such a reduction provides upper-bound results with respect to both combined and data complexity.

Pervasive computing environments are nowadays more and more used as a supporting tool for cooperative workflows, e.g., in emergency management. A typical problem in these scenarios is the synthesis of workflows in presence of sets of services (hosted on mobile devices) with constrained behaviors, just before the collaborating team is dropped off in the operation field. In this paper, we propose a technique able to automatically synthesize distributed orchestrators, each one coordinating a service and synchronizing with the other orchestrators, given a target generic workflow to be carried out and a set of behaviorally-constrained services.

Data exchange and virtual data integration have been the subject of several investigations in the recent literature. At the same time, the notion of peer data management has emerged as a powerful abstraction of many forms of flexible and dynamic data-centere ddistributed systems. Although research on the above issues has progressed considerably in the last years, a clear understanding on how to combine data exchange and data integration in peer data management is still missing. This is the subject of the present paper. We start our investigation by first proposing a novel framework for peer data exchange, showing that it is a generalization of the classical data exchange setting. We also present algorithms for all the relevant data exchange tasks, and show that they can all be done in polynomial time with respect to data complexity. Based on the motivation that typical mappings and integrity constraints found in data integration are not captured by peer data exchange, we extend the framework to incorporate these features. One of the main difficulties is that the constraints of this new class are not amenable to materialization. We address this issue by resorting to a suitable combination of virtual and materialized data exchange, showing that the resulting framework is a generalization of both classical data exchange and classical data integration, and that the new setting incorporates the most expressive types of mapping and constraints considered in the two contexts. Finally, we present algorithms for all the relevant data management tasks also in the new setting, and show that, again, their data complexity is polynomial.

The promise of Web services is to enable the composition of new distributed applications/solutions: when no available service can satisfy a client request, (parts of) available services can be composed and orchestrated in order to satisfy such a request. Service composition involves two different issues: the synthesis, in order to synthesize, either manually or automatically, a specification of how coordinating the component services to fulfill the client request, and the orchestration, i.e., how executing the previous obtained specification by suitably supervising and monitoring both the control flow and the data flow among the involved services. In this work, we address the automatic composition synthesis when the behavior of the available services is non-deterministic, and hence is not fully controllable by the orchestrator. The service behavior is modeled by the possible conversations the service can have with its clients. The presence of nondeterministic conversations stems naturally when modeling services in which the result of each interaction with its client on the state of the service can not be foreseen

This paper addresses the issue of automatic service composition. We first develop a framework in which the exported behavior of a service is described in terms of a so-called execution tree, that is an abstraction for its possible executions. We then study the case in which such exported behavior (i.e. the execution tree of the service) can be represented by a finite state machine (i.e. finite state transition system). In this specific setting, we devise sound, complete and terminating techniques both to check for the existence of a composition, and to return a composition, if one exists. We also analyze the computational complexity of the proposed algorithms. Finally, we present an open source prototype tool, called [Formula: see text] (E-Service Composer), that implements our composition technique. To the best of our knowledge, our work is the first attempt to provide a provably correct technique for the automatic synthesis of service composition, in a framework where the behavior of services is explicitly specified.

In this paper we study automatic composition synthesis of e-Services, based on automated reasoning. We represent the behavior of an e-Service in terms of a deterministic transition syst (or a finite state machine), in which for each action the role of the e-Service, either as initiator or as servant, is highlighted. In this setting we present an algorithm based on satisfiability in a variant of Propositional Dynamic Logic that solves the automatic composition probl. Specifically, given (i) a possibly incomplete specification of the sequences of actions that a client would like to realize, and (ii) a set of available e-Services, our technique synthesizes a composite e-Service that (i) uses only the available e-Services and (ii) interacts with the client "in accordance" to the given specification. We also study the computational complexity of the proposed algorithm.

In peer-to-peer data integration, each peer exports data in terms of its own schema, and data interoperation is achieved by means of mappings among the peer schemas. Peers are autonomous systems and mappings are dynamically created and changed. One of the challenges in these systems is answering queries posed to one peer taking into account the mappings. Obviously, query answering strongly depends on the semantics of the overall system. In this paper, we compare the commonly adopted approach of interpreting peerto-peer systems using a first-order semantics, with an alternative approach based on epistemic logic. We consider several central properties of peer-to-peer systems: modularity, generality, and decidability. We argue that the approach based on epistemic logic is superior with respect to all the above properties. In particular, we show that, in systems in which peers have decidable schemas and conjunctive mappings, but are arbitrarily interconnected, the first-order approach may lead to undecidability of query answering, while the epistemic approach always preserves decidability. This is a fundamental property, since the actual interconnections among peers are not under the control of any actor in the system. 1.

Query containment is the problem of checking whether for all databases the answer to a query is a subset of the answer to a second query. In several data management tasks, such as data integration, mobile computing, etc., the data of interest are only accessible through a given set of views. In this case, containment of queries should be determined relative to the set of views, as already noted in the literature. Such a form of containment, which we call view-based query containment, is the subject of this paper. The problem comes in various forms, depending on whether each of the two queries is expressed over the base alphabet or the alphabet of the view names. We present a thorough analysis of view-based query containment, by discussing all possible combinations from a semantic point of view, and by showing their mutual relationships. In particular, for the two settings of conjunctive queries and two-way regular path queries, we provide both techniques and complexity bounds for the different variants of the problem. Finally, we study the relationship between view-based query containment and view-based query rewriting.

Class-based languages express knowledge in terms of objects and classes, and have inspired a huge number of formalisms in computer science. Description logics forma family of both class-based and logic-based knowledge representation languages which allow for modeling an application domain in terms of objects, classes and relationships between classes, and for reasoning about them. This paper presents an overview of the research carried out in the last years in description logics, with the main goal of illustrating how these logics provide the foundations for class-based knowledge representation formalisms.

If the only information we have on a certain database is through a set of views, the question arises of whether this is sufficient to answer completely a given query. We say that the set of views is lossless with respect to the query, if, no matter what the database is, we can answer the query by solely relying on the content of the views. The question of losslessness has various applications, for example in query optimization, mobile computing, data warehousing, and data integration. We study this problem in a context where the database is semistructured, and both the query and the views are expressed as regular path queries. The form of recursion present in this class prevents us from applying known results to our case.We first address the problem of checking losslessness in the case where the views are materialized. The fact that we have the view extensions available makes this case solvable by extending known techniques. We then study a more complex version of the problem, namely the one where we abstract from the specific view extension. More precisely, we address the problem of checking whether, for every database, the answer to the query over such a database can be obtained by relying only on the view extensions. We show that the problem is solvable by utilizing, via automata-theoretic techniques, the known connection between view-based query answering and constraint satisfaction. We also investigate the computational complexity of both versions of the problem.

Information integration is one of the most important aspects of a Data Warehouse. When data passes from the sources of the application-oriented operational environment to the Data Warehouse, possible inconsistencies and redundancies should be resolved, so that the warehouse is able to provide an integrated and reconciled view of data of the organization. We describe a novel approach to data integration in Data Warehousing. Our approach is based on a conceptual representation of the Data Warehouse application domain, and follows the so-called local-as-view paradigm: both source and Data Warehouse relations are defined as views over the conceptual model. We propose a technique for declaratively specifying suitable reconciliation correspondences to be used in order to solve conflicts among data in different sources. The main goal of the method is to support the design of mediators that materialize the data in the Data Warehouse relations. Starting from the specification of one such relation as a query over the conceptual model, a rewriting algorithm reformulates the query in terms of both the source relations and the reconciliation correspondences, thus obtaining a correct specification of how to load the data in the materialized view.

When it comes to building controllers for robots or agents, high level programming languages like Golog and ConGolog offer a useful compromise between planning-based approaches and low-level robot programming. However, two serious problems typically emerge in practical implementations of these languages: how to evaluate test in a program efficiently enough in an open-world setting, and how to make appropiate nondeterministic choices while avoiding full lookahead. Recent proposals in the literature suggest that one could tackle the first problem by exploiting sensing information, and tackle the second by specifying the amount of lookahead allowed explicitly in the program. In this paper, we combine these two ideas and demonstrate their power by presenting an interpreter, written in Prolog, for a variant of Golog that is suitable for efficiently operating in open-world setting by exploiting sensing and bounded lookahead.

Query answering using views amounts to computing the answer to a query having information only on the extension of a set of views. This problem is relevant in several fields, such as information integration, data warehousing, query optimization, mobile computing, and maintaining physical data independence. We address query answering using views in a context where queries and views are regular path queries, i.e., regular expressions that denote the pairs of objects in the database connected by a matching path. Regular path queries are the basic query mechanism when the database is conceived as a graph, such as in semistructured data and data on the Web. We study algorithms for answering regular path queries using views under different assumptions, namely, closed and open domain, and sound, complete, and exact information on view extensions. We characterize data, expression, and combined complexity of the problem, showing that the proposed algorithms are essentially optimal. Our results are the first to exhibit decidability in cases where the language for expressing the query and the views allows for recursion.

View-based query processing requires answering a query posed to a database only on the basis of the information on a set of views, which are again queries over the same database. This problem is relevant in many aspects of database management, and has been addressed by means of two basic approaches: query rewriting and query answering. In the former approach, one tries to compute a rewriting of the query in terms of the views, whereas in the latter, one aims at directly answering the query based on the view extensions. We study view based query processing for the case of regular-path queries, which are the basic querying mechanisms for the emergent field of semistructured data. Based on recent results, we first show that a rewriting is in general a co-NP function wrt to the size of view extensions. Hence, the problem arises of characterizing which instances of the problem admit a rewriting that is PTIME. A second contribution of the work is to establish a tight connection between view based query answering and constraint satisfaction problems, which allows us to show that the above characterization is going to be difficult. As a third contribution, we present two methods for computing PTIME rewritings of specific forms. The first method, which is based on the established connection with constraint satisfaction problems, gives us rewritings expressed in Datalog with a fixed number of variables. The second method, based on automata-theoretic techniques, gives us rewritings that are formulated as unions of conjunctive regular-path queries with a fixed number of variables.

View-based query processing is the problem of computing the answer to a query based on a set of materialized views, rather than on the raw data in the database. The problem comes in two different forms, called query rewriting and query answering, respectively. In the first form, we are given a query and a set of view definitions, and the goal is to reformulate the query into an expression that refers only to the views. In the second form, besides the query and the view definitions, we are also given the extensions of the views and a tuple, and the goal is to check whether the knowledge on the view extensions logically implies that the tuple satisfies the query. In this paper we address the problem of view-based query processing in the context of semistructured data, in particular for the case of regular-path queries extended with the inverse operator. Several authors point out that the inverse operator is one of the fundamental extensions for making regular-path queries useful in real settings. We present a novel technique based on the use of two-way finite-state automata. Our approach demonstrates the power of this kind of automata in dealing with the inverse operator, allowing us to show that both query rewriting and query answering with the inverse operator has the same computational complexity as for the case of standard regular-path queries. 1.

Recent work on semi-structured da.ta ha.s revitalized the interest in pa.th qu.eries, i.e., queries that ask for ah pairs of objects in the database that are connected by a, path conforming to a certain specification, in particular to a regular expression.Also, in semi-structured data., as well as in data.integration, da.ta.wa.rehousing, and query optimization, the problem of query rewriting using views is receiving much attention: Given a. query and a collection of views, generate a new query which uses the views and provides the answer to the original one.In this paper we address the problem of query rewriting using views in the context of semi-structured data.We present a method for computing the rewriting of a regular expression i? in terms of other regular expressions.The method computes the exact rewriting (the one that defines the same regular language as E) if it exists, or the rewriting that defines the maximal language contained in the one defined by E, otherwise.We present a complexity analysis of both the problem+and the method, showing that the latter is essentially optimal.Finally, we illustrate how to exploit the method to rewrite regular path queries using views in semistructured data.The complexity results established for the rewriting of regular expressions apply also to the case of regu1a.rpath queries.

Recent proposals to improve the quality of interaction with the World Wide Web suggest considering the Web as a huge semistructured database, so that retrieving information can be supported by the task of database querying. Under this view, it is important to represent the form of both the network, and the documents placed in the nodes of the network. However, the current proposals do not pay sufficient attention to represent document structures and reasoning about them. In this paper, we address these problems by providing a framework where Document Type Definitions (DTDs) expressed in the eXtensible Markup Language (XML) are formalized in an expressive Description Logic equipped with sound and complete inference algorithms. We provide methods for verifying conformance of a document to a DTD in a polynomial time, and structural equivalence of DTDs in worst case deterministic exponential time, improving known algorithms for this problem which were double exponential. We also deal with parametric versions of conformance and structural equivalence, and investigate other forms of reasoning on DTDs. Finally, we show how to take advantage of the reasoning capabilities of our formalism in order to perform several optimization steps in answering queries posed to a document base. Key words: Knowledge representation, automated reasoning, description logics, XML, SGML.

E Franconi, G De Giacomo, IR Horrocks, DL McGuinness, W Nutt, PF Patel-Schneider, CA Welty; Conferences. Report on the 1998 International Workshop on Descriptio

We describe an approach to reasoning agents which is based on a formal theory of actions and is actually implemented on a mobile robot working in an office environment. From an epistemiological viewpoint, our proposal is originated by the correspondence between Dynamic Logics and Description Logics, Specifically, we consider an epistemic extension of Description Logics to provide a new theoretical framework for the representation of dynamic systems, where the agent's reasoning is based on its knowledge about the world. In this setting, we obtain a weaker notion of logical inference, thus simplifying the reasoning task. From a practical viewpoint, we use a general purpose knowledge representation system based on Description Logics and its associated reasoning tools, in order to plan the actions of the mobile robot 'Tino', starting from the knowledge about the environment and the action specification. In addition, we exploit the robot's capabilities in order to integrate the execution of the plan with reactive behaviours, thus enabling the agent to accomplish its tasks in the real world.

Information integration is one of the core problems in cooperative information systems. The authors argue that two critical factors for the design and maintenance of applications requiring information integration are conceptual modeling of the domain, and reasoning support over the conceptual representation. In particular they present a general architecture for information integration that explicitly includes a conceptual representation of the application. They illustrate how the architecture can express several integration settings and existing systems. They provide various arguments in favor of the conceptual level in the architecture and of automated reasoning over the conceptual representation. Finally, they present a specific proposal of an integration system which realizes the general architecture and is equipped with decidable reasoning procedures.

Query containment under constraints is the problem of checking whether for every database satisfying a given set of constraints, the result of one query is a subset of the result of another query, Recent research points out that this is a central problem in severa database applications, and we address it within A setting where constraints are specified in the form of special inclusion dependencies over complex expressions, built by using intersection and difference of relations, special forms of quantification, regular expressions over binary relations, and cardinality constraints.These types of constraints capture a great variety of data models, including the relational, the entity-relational, and the object-oriented model,We study the problem of checking whether q is contained in q' with respect to the constraints specified in a schema S, where q and q' are nonrecursive Datalog programs whose atoms are complex expressions.We present the following results on query containment.For the case where q does not contain regular expressions, we provide a method for deciding query containment, and analyze its computational complexity.We do the same for the case where neither S nor q, q' contain number restrictions.To the best of our knowledge, this yields the first decidability result on containment of conjunctive queries with regular expressions.Finally, we Provo that the problem is undecidable for the case where we admit inequalities in q', , 1 Introduction

Most modern formalisms used in Databases and Artificial Intelligence for describing an application domain are based on the notions of class (or concept) and relationship among classes. One interesting feature of such formalisms is the possibility of defining a class, i.e., providing a set of properties that precisely characterize the instances of the class. Many recent articles point out that there are several ways of assigning a meaning to a class definition containing some sort of recursion. In this paper, we argue that, instead of choosing a single style of semantics, we achieve better results by adopting a formalism that allows for different semantics to coexist. We demonstrate the feasibility of our argument, by presenting a knowledge representation formalism, the description logic muALCQ, with the above characteristics. In addition to the constructs for conjunction, disjunction, negation, quantifiers, and qualified number restrictions, muALCQ includes special fixpoint constructs to express (suitably interpreted) recursive definitions. These constructs enable the usual frame-based descriptions to be combined with definitions of recursive data structures such as directed acyclic graphs, lists, streams, etc. We establish several properties of muALCQ, including the decidability and the computational complexity of reasoning, by formulating a correspondence with a particular modal logic of programs called the modal mu-calculus.

We present a conceptual data model, called SDM, which is able to represent the relationships between elementary and statistical data at a conceptual level. SDM borrows elements from research both in object oriented databases and in knowledge representation. In addition it has suitable mechanisms to form classes of individuals by classifying the instances of a target class according to some specified criteria. Notably, the class resulting from such a statistical aggregation can then be treated exactly as a class of elementary data. This ability fulfils the often perceived necessity, in modeling real domains, of treating statistical aggregates and elementary data in an homogeneous way.