In various service-oriented applications such as distributed autonomous delivery, healthcare, tourism, transportation, and many others, where service agents need to perform serial and time-bounded tasks to achieve their goals, quality of service must constantly be assured. In addition to safety requirements, such agents also need to fulfill performance requirements in order to satisfy their quality of service. This paper proposes the novel quality-aware time window temporal logic (QTWTL) by extending the traditional time window temporal logic (TWTL) with two operators for counting and aggregation operations. We also propose offline runtime monitoring algorithms for the performance monitoring of QTWTL specifications. To analyze the feasibility and efficiency of our proposed approach, we generate a large number of traces using the New York City Taxi and Limousine Commission Trip Record data, formalize their performance requirements using QTWTL, and monitor them using the proposed algorithms. The obtained results show that the monitoring algorithm has a linear space and time complexity with respect to the number of traces monitored.

Motivated by the expressiveness of hyperproperties, Hyperproperties extend trace properties to express properties of several hyper-temporal logics, such as HyperLTL [20], sets of traces, and they are increasingly popular in specifying various HyperSTL [38], and HyperMTL [11], were recently proposed by extending security and performance-related properties in domains such the conventional temporal logics such as Linear Temporal as cyber-physical systems, smart grids, and automotive. This paper Logic (LTL) [41], Signal Temporal Logic (STL) [37], and Metric Temporal introduces HyperTWTL, which extends Time Window Temporal Logic (MTL) [33], respectively. Consequently, various model Logic (TWTL)-a domain-specific formal specification language for checking techniques have been proposed for verifying HyperLTL robotics, by allowing explicit and simultaneous quantification over [20, 22, 25, 27], HyperMTL [11, 30], HyperMITL [31], HyperSTL multiple execution traces. We propose two different semantics for [38] specifications employing alternating automata, model checking, HyperTWTL, synchronous and asynchronous, based on the alignment strategy synthesis, and several other methods [32]. of the timestamps in the traces. Consequently, we demonstrate Time bounded specifications are common in many applications, the application of HyperTWTL in formalizing important such as robotics.

We introduce a formal framework (called NCDC-ASP) for representing and reasoning about cardinal directions between extended spatial objects on a plane, using Answer Set Programming (ASP). NCDC-ASP preserves the meaning of cardinal directional relations as in Cardinal Directional Calculus (CDC), and provides solutions to all consistency checking problems in CDC under various conditions (i.e., for a complete/incomplete set of basic/disjunctive CDC constraints over connected/disconnected spatial objects). In particular, NCDC-ASP models a discretized version of the consistency checking problem in ASP, over a finite grid (rather than a plane), where we provide new lower bounds on the grid size to guarantee that it correctly characterizes solutions for the consistency checking in CDC. In addition, NCDC-ASP has the following two novelties important for applications. NCDC-ASP introduces default CDC constraints to represent and reason about background or commonsense knowledge that involves default qualitative directional relations (e.g., "the ice cream truck is by default to the north of the playground" or "the keyboard is normally placed in front of the monitor"). NCDC-ASP introduces inferred CDC constraints to allow inference of missing CDC relations and to provide them as explanations. We illustrate the uses and usefulness of NCDC-ASP with interesting scenarios from the real-world. We design and develop a variety of benchmark instances, and comprehensively evaluate NCDC-ASP from the perspectives of computational efficiency.

Automaton-based representations of task knowledge play an important role in control and planning for sequential decision-making problems. However, obtaining the high-level task knowledge required to build such automata is often difficult. Meanwhile, large-scale generative language models (GLMs) can automatically generate relevant task knowledge. However, the textual outputs from GLMs cannot be formally verified or used for sequential decision-making. We propose a novel algorithm named GLM2FSA, which constructs a finite state automaton (FSA) encoding high-level task knowledge from a brief natural-language description of the task goal. GLM2FSA first sends queries to a GLM to extract task knowledge in textual form, and then it builds an FSA to represent this text-based knowledge. The proposed algorithm thus fills the gap between natural-language task descriptions and automaton-based representations, and the constructed FSA can be formally verified against user-defined specifications. We accordingly propose a method to iteratively refine the queries to the GLM based on the outcomes, e.g., counter-examples, from verification. We demonstrate GLM2FSA's ability to build and refine automaton-based representations of everyday tasks (e.g., crossing a road), and also of tasks that require highly-specialized knowledge (e.g., executing secure multi-party computation).

Linear Temporal Logic (LTL) is one of the most popular temporal logics and comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free ω-automata, to star-free ω-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. Safety-LTL (resp., coSafety-LTL) is a fragment of LTL where only the tomorrow, the weak tomorrow and the until temporal modalities (resp., the tomorrow, the weak tomorrow and the release temporal modalities) are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called Safety-FO, and of its dual coSafety-FO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize Safety-LTL and coSafety-LTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in Safety-LTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of Safety-LTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, Safety-LTL (resp.

Montague semantics is a compositional method to translate the semantics of written language into first order logic. As a simple example one can understand the meaning of the sentence "(all) dogs eat snacks" as x, y.dogs(x) snacks(y) eats(x, y). However, when translating the meaning of the sentence "Every farmer who owns a donkey beats it", the variable representing the donkey cannot be bound by the existential quantifier coming from the determiner'a'. This issue was studied by Geach [4], using it as a counterexample to the scope of Montague semantics. Many have created systems that form semantic representations of donkey sentences, to name a few we have dynamic predicate logic [7], where the binding rules of quantifiers in first order logic are relaxed, discourse representation theory [11] where an collection of'discourse referents' keep track of individuals' mentions and are identified to keep track of references, as well as an approach using dependent type theory [18], exploiting dependent sums to differentiate between ambiguous readings of donkey sentences. However, none of the models mentioned above are type-logical grammars which poses the question whether it is possible to parse donkey sentences and form usable representations of them using type logical grammars? We propose to model donkey sentences using (an extension of) Lambek calculus, L. In the following section, we explain how a type-logical analysis of natural language works, and in sections 1.3,1.4,1.5 how to extend it to model more exotic linguistic phenomena, culminating in a parse of a donkey sentence. Then we introduce relational semantics and vector space semantics of the extended Lambek calculus in sections 3.1 and 3.3 respectively, demonstrating how donkey sentence is interpreted as a relation or as a linear map.

This work introduces efficient symbolic algorithms for quantitative reactive synthesis. We consider resource-constrained robotic manipulators that need to interact with a human to achieve a complex task expressed in linear temporal logic. Our framework generates reactive strategies that not only guarantee task completion but also seek cooperation with the human when possible. We model the interaction as a two-player game and consider regret-minimizing strategies to encourage cooperation. We use symbolic representation of the game to enable scalability. For synthesis, we first introduce value iteration algorithms for such games with min-max objectives. Then, we extend our method to the regret-minimizing objectives. Our benchmarks reveal that our symbolic framework not only significantly improves computation time (up to an order of magnitude) but also can scale up to much larger instances of manipulation problems with up to 2x number of objects and locations than the state of the art.

We present dPASP, a novel declarative probabilistic logic programming framework for differentiable neuro-symbolic reasoning. The framework allows for the specification of discrete probabilistic models with neural predicates, logic constraints and interval-valued probabilistic choices, thus supporting models that combine low-level perception (images, texts, etc), common-sense reasoning, and (vague) statistical knowledge. To support all such features, we discuss the several semantics for probabilistic logic programs that can express nondeterministic, contradictory, incomplete and/or statistical knowledge. We also discuss how gradient-based learning can be performed with neural predicates and probabilistic choices under selected semantics. We then describe an implemented package that supports inference and learning in the language, along with several example programs. The package requires minimal user knowledge of deep learning system's inner workings, while allowing end-to-end training of rather sophisticated models and loss functions.

Probabilistic model checking is a technique for formal automated reasoning about software or hardware systems that operate in the context of uncertainty or stochasticity. It builds upon ideas and techniques from a diverse range of fields, from logic, automata and graph theory, to optimisation, numerical methods and control. In recent years, probabilistic model checking has also been extended to integrate ideas from game theory, notably using models such as stochastic games and solution concepts such as equilibria, to formally verify the interaction of multiple rational agents with distinct objectives. This provides a means to reason flexibly about agents acting in either an adversarial or a collaborative fashion, and opens up opportunities to tackle new problems within, for example, artificial intelligence, robotics and autonomous systems. In this paper, we summarise some of the advances in this area, and highlight applications for which they have already been used. We discuss how the strengths of probabilistic model checking apply, or have the potential to apply, to the multi-agent setting and outline some of the key challenges required to make further progress in this field.

Cost-guided bottom-up search (BUS) algorithms use a cost function to guide the search to solve program synthesis tasks. In this paper, we show that current state-of-the-art cost-guided BUS algorithms suffer from a common problem: they can lose useful information given by the model and fail to perform the search in a best-first order according to a cost function. We introduce a novel best-first bottom-up search algorithm, which we call Bee Search, that does not suffer information loss and is able to perform cost-guided bottom-up synthesis in a best-first manner. Importantly, Bee Search performs best-first search with respect to the generation of programs, i.e., it does not even create in memory programs that are more expensive than the solution program. It attains best-first ordering with respect to generation by performing a search in an abstract space of program costs. We also introduce a new cost function that better uses the information provided by an existing cost model. Empirical results on string manipulation and bit-vector tasks show that Bee Search can outperform existing cost-guided BUS approaches when employing more complex domain-specific languages (DSLs); Bee Search and previous approaches perform equally well with simpler DSLs. Furthermore, our new cost function with Bee Search outperforms previous cost functions on string manipulation tasks.