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.

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.

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.

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.

We study the complexity of the model-checking problem for parameterized discrete-timed systems with arbitrarily many anonymous and identical processes, with and without a distinguished "controller", and communicating via synchronous rendezvous. Our framework extends the seminal work from German and Sistla on untimed systems by adding discrete-time clocks to processes. For the case without a controller, we show that the systems can be efficiently simulated -- and vice versa -- by systems of untimed processes that communicate via rendezvous and symmetric broadcast, which we call "RB-systems". Symmetric broadcast is a novel communication primitive that allows all processes to synchronize at once; however, it does not distinguish between sending and receiving processes. We show that the parameterized model-checking problem for safety specifications is pspace-complete, and for liveness specifications it is decidable in exptime. The latter result is proved using automata theory, rational linear programming, and geometric reasoning for solving certain reachability questions in a new variant of vector addition systems called "vector rendezvous systems". We believe these proof techniques are of independent interest and will be useful in solving related problems. For the case with a controller, we show that the parameterized model-checking problems for RB-systems and systems with asymmetric broadcast as a primitive are inter-reducible. This allows us to prove that for discrete timed-networks with a controller the parameterized model-checking problem is undecidable for liveness specifications. Our work exploits the intimate connection between parameterized discrete-timed systems and systems of processes communicating via broadcast, providing a rare and surprising decidability result for liveness properties of parameterized timed-systems, as well as extend work from untimed systems to timed systems.

We study synthesis and verification of probabilistic models and specifications over finite traces. Probabilistic models are formalized in this work as Markov Chains and Markov Decisions Processes. Motivated by the recent attention given to, and importance of, finite-trace specifications in AI, we use linear-temporal logic on finite traces as a specification formalism for properties of traces with finite but unbounded time horizons. Since there is no bound on the time horizon, our Markov chains generate infinite traces, and we consider two possible semantics: “existential (resp. universal) prefix- semantics” which says that the finite-trace property holds on some (resp. every) finite prefix of the trace. For both types of semantics, we study two computational problems: the verification problem — “does a given Markov chain satisfy the specification with probability one?”; and the synthesis problem — “find a strategy (if there is one) that ensures the Markov decision process satisfies the specification with probability one”. We provide optimal algorithms that follow an automata-theoretic approach, and prove that the complexity of the synthesis problem is 2EXPTIME-complete for both semantics, and that for the verification problem it is PSPACE-complete for the universal-prefix semantics, but EXPSPACE-complete for the existential-prefix semantics.

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.

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.

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.

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

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 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 introduce Probabilistic Strategy Logic, an extension of Strategy Logic for stochastic systems. The logic has probabilistic terms that allow it to express many standard solution concepts, such as Nash equilibria in randomised strategies, as well as constraints on probabilities, such as independence. We study the model-checking problem for agents with perfect- and imperfect-recall. The former is undecidable, while the latter is decidable in space exponential in the system and triple-exponential in the formula. We identify a natural fragment of the logic, in which every temporal operator is immediately preceded by a probabilistic operator, and show that it is decidable in space exponential in the system and the formula, and double-exponential in the nesting depth of the probabilistic terms. Taking a fixed nesting depth, this gives a fragment that still captures many standard solution concepts, and is decidable in exponential space.

Parameterized model checking is the problem of deciding if a given formula holds irrespective of the number of participating processes. A standard approach for solving the parameterized model checking problem is to reduce it to model checking finitely many finite-state systems. This work considers the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases where model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Büchi word automaton), and establish tight bounds on the sizes of such automata.

A nondeterministic weighted finite automaton (WFA) maps an input word to a numerical value. Applications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. Many of these applications require the WFAs to be deterministic, or work substantially better when the WFAs are deterministic. Unlike NFAs, which can always bedeterminized, not all WFAs have an equivalent deterministic weighted automaton (DWFA). In \cite{Moh97}, Mohri describes a determinization construction for a subclass of WFA. He also describes a property of WFAs (the {\em twins property}), such that all WFAs that satisfy thetwins property are determinizable and the algorithm terminates on them. Unfortunately, many natural WFAs cannot be determinized. In this paper we study {\em approximated determinization\/} of WFAs. We describe an algorithm that, given a WFA $\A$ and an approximation factor $t \geq 1$, constructs a DWFA $\A'$ that{\em $t$-determinizes\/} $\A$. Formally, for all words $w \in \Sigma^*$, the value of $w$ in $\A'$ is at least its value in $\A$ and at most $t$times its value in $\A$. Our construction involves two new ideas:attributing states in the subset construction by both upper and lower residues, and collapsing attributed subsets whose residues can be tightened. The larger the approximation factor is, the more attributed subsets we can collapse. Thus, $t$-determinization is helpful not only for WFAs that cannot be determinized, but also in cases determinization is possible but results in automata that are too big to handle. In addition, $t$-determinization is useful for reasoning about the competitive ratio of on line algorithms. We also describe a property (the {\em $t$-twins property}) and use it in order to characterize $t$-determinizable WFAs. Finally, we describea polynomial algorithm for deciding whether a given WFA has the $t$-twins property.

We describe an automata-theoretic approach for the competitive analysis of online algorithms . Our approach is based on weighted automata , which assign to each input word a cost in R ≥0 . By relating the “unbounded look ahead” of optimal offline algorithms with nondeterminism, and relating the “no look ahead” of online algorithms with determinism, we are able to solve problems about the competitive ratio of online algorithms, and the memory they require, by reducing them to questions about determinization and approximated determinization of weighted automata.

We describe an automata-theoretic approach for the competitive analysis of online algorithms. Our approach is based on weighted automata, which assign to each input word a cost in IR≥0. By relating the “unbounded look ahead” of optimal offline algorithms with nondeterminism, and relating the “no look ahead” of online algorithms with determinism, we are able to solve problems about the competitive ratio of online algorithms, and the memory they require, by reducing them to questions about determinization and approximated determinization of weighted automata.