ABSTRACT. The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment $\square$LTL of the logic LTL(EB), the integration of the UNTIL-fragment of Pnueli's linear time temporal logic (LTL) and the logic of Event-B, in which the most commonly used liveness conditions can be expressed. For this fragment a sound set of derivation rules is developed, which is also complete under mild restrictions for Event-B machines.

ABSTRACT. Analogical proportions, i.e., relational assertions of the form "a is to b as c is to d" are fundamental for analogical reasoning, a cognitively motivated form of reasoning that has several important applications in AI, including problem solving and learning. This paper contributes to the logic characterization of analogical reasoning by establishing a link between two perspectives. Analogical proportions can either be viewed atomically as a quaternary relation or as the implicit relation induced by applying analogical comparison a:b to an element d in order to identify a suitable element c. For linking these views we tackle a general question: Given a quaternary relation between four elements a, b, c, d, how can it be decomposed into a representation a:b::c:d with "::" denoting a binary relation and ":" denoting a binary function---possibly under additional constraints on : and ::? In particular we show that for a whole class of analogical proportions such a decomposition is possible with ":" denoting the same function in all of the analogical proportions of the class.

ABSTRACT. Linear temporal logic (LTL) is used in system verificationto write formal specifications for reactive systems.However, some relevant properties,e.g. non-inference in information flow security,cannot be expressed in LTL.A class of such properties that has recentlyreceived ample attentionis known as hyperproperties.There are two major streams in the research regardingcapturing hyperproperties, namelyhyperlogics, which extend LTL with trace quantifiers (HyperLTL),and logics that employ team semantics,extending truth to sets of traces.In this article we explore the relation between asynchronousLTL under set-basedteam semantics (TeamLTL) and HyperLTL.In particular we consider the extensions of TeamLTL withthe Boolean disjunction and a fragment of the extension ofTeamLTL with the Boolean negation, where the negationcannot occur in the left-hand side of the Until-operator orwithin the Global-operator.We show that TeamLTL extended withthe Boolean disjunction is equi-expressive withthe positive Boolean closure of HyperLTL restricted toone universal quantifier,while the left-downward closed fragment ofTeamLTL extended with the Boolean negationis expressively equivalent withthe Boolean closure of HyperLTL restricted toone universal quantifier.

ABSTRACT. The Rescher quantifier and Härtig quantifier have been the subject of much theoretical inquiry, due to the ability of their respective languages to capture much of second-order logic. This paper deals with a hybrid of the two, which for clarity I have termed the Rescher-Härtig quantifier, the first-order language of which is expressively equivalent to that of the Rescher quantifier but contains language fragments with interesting properties. Specifically, the negationless fragment has the property of satisfiability of all sentences within a single model, yet the question of entailment in the language fragment has equal complexity to the question of entailment in the whole language. This can be demonstrated by embedding problems of entailment from the whole language into the language fragment. By additionally embedding the problem into propositional logic, in which entailment is known to be decidable, and reducing the first problem of entailment to the two embedded problems, we show that entailment in the whole language is no more complex than in the language fragment. The paper concludes with a discussion of the different notions of logical compactness and various open questions.

ABSTRACT. Service compositions à la Roman model consists of realizing a virtual service by orchestrating suitably a set of already available services, where all services are described procedurally as probabilistic transition systems. In this paper, we study a goal-oriented variant of the service composition à la Roman Model, where the goals specified allowed traces declaratively via Linear Temporal Logic on finite traces (LTLf). Specifically, we want to synthesize a controller to orchestrate the available services to maximize the probability of satisfaction of the LTLf specification and simultaneously minimize the utilization cost of the services. To do so, we combine techniques from service composition à la Roman Model, reactive synthesis, and bi-objective lexicographic optimization on MDPs. This framework has several interesting applications, including Smart Manufacturing and Digital Twins.

ABSTRACT. In the contexts of database querying and constraint satisfaction problems (CSPs), the hypertree decomposition method can be used query optimization and for faster CSP solving and for, whereby problem instances having a low hypertree width (i.e., a low degree of cyclicity) can be recognized and decomposed automatically, and efficiently evaluated. Queries and CSPs having bounded hypertree width are also highly parallelizable. The notion of Hypertree decomposition was introduced in 1999. This talk reviews - in form of questions and answers - the main relevant concepts and algorithms and surveys selected related work including applications and more recent results.