Lutz Schröder

Merlin Humml, Lutz Schröder

Epistemic logics typically talk about knowledge of individual agents or groups of explicitly listed agents. Often, however, one wishes to express knowledge of groups of agents specified by a given property, as in `it is common knowledge among economists'. We introduce such a logic of common knowledge, which we term abstract-group epistemic logic (AGEL). That is, AGEL features a common knowledge operator for groups of agents given by concepts in a separate agent logic that we keep generic, with one possible agent logic being ALC. We show that AGEL is EXPTIME-complete, with the lower bound established by reduction from standard group epistemic logic, and the upper bound by a satisfiability-preserving embedding into the full $μ$-calculus. Further main results include a finite model property (not enjoyed by the full $μ$-calculus) and a complete axiomatization.

Merlin Humml, Lutz Schröder, Dirk Pattinson

Alternating-time temporal logic (ATL) and its extensions, including the alternating-time $μ$-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of the logic are path quantifiers specifying that some coalition of agents has a joint strategy to enforce a given goal. This basic setup has been extended to let some of the agents (revocably) commit to using certain named strategies, as in ATL with explicit strategies (ATLES). In the present work, we extend ATLES with fixpoint operators and strategy disjunction, arriving at the alternating-time $μ$-calculus with disjunctive explicit strategies (AMCDES), which allows for a more flexible formulation of temporal properties (e.g. fairness) and, through strategy disjunction, a form of controlled nondeterminism in commitments. Our main result is an ExpTime upper bound for satisfiability checking (which is thus ExpTime-complete). We also prove upper bounds QP (quasipolynomial time) and NP $\cap$ coNP for model checking under fixed interpretations of explicit strategies, and NP under open interpretation. Our key technical tool is a treatment of the AMCDES within the generic framework of coalgebraic logic, which in particular reduces the analysis of most reasoning tasks to the treatment of a very simple one-step logic featuring only propositional operators and next-step operators without nesting; we give a new model construction principle for this one-step logic that relies on a set-valued variant of first-order resolution.

Henning Urbat, Lutz Schröder

We propose a generic categorical framework for learning unknown formal languages of various types (e.g. finite or infinite words, weighted and nominal languages). Our approach is parametric in a monad T that represents the given type of languages and their recognizing algebraic structures. Using the concept of anautomata presentation of T-algebras, we demonstrate that the task of learning a T-recognizable language can be reduced to learning an abstract form of algebraic automaton whose transitions are modeled by a functor. For the important case of adjoint automata, we devise a learning algorithm generalizing Angluin's L*. The algorithm is phrased in terms of categorically described extension steps; we provide for a termination and complexity analysis based on a dedicated notion of finiteness. Our framework applies to structures like omega-regular languages that were not within the scope of existing categorical accounts of automata learning. In addition, it yields new learning algorithms for several types of languages for which no such algorithms were previously known at all, including sorted languages, nominal languages with name binding, and cost functions.

Merlin Göttlinger, Lutz Schröder

The Aristotelian trichotomy distinguishes three aspects of argumentation: Logos, Ethos, and Pathos. Even rich argumentation representations like the Argument Interchange Format (AIF) are only concerned with capturing the Logos aspect. Inference Anchoring Theory (IAT) adds the possibility to represent ethical requirements on the illocutionary force edges linking locutions to illocutions, thereby allowing to capture some aspects of ethos. With the recent extensions AIF+ and Social Argument Interchange Format (S-AIF), which embed dialogue and speakers into the AIF argumentation representation, the basis for representing all three aspects identified by Aristotle was formed. In the present work, we develop the Trichotomic Argument Interchange Format (T-AIF), building on the idea from S-AIF of adding the speakers to the argumentation graph. We capture Logos in the usual known from AIF+, Ethos in form of weighted edges between actors representing trust, and Pathos via weighted edges from actors to illocutions representing their level of commitment to the propositions. This extended structured argumentation representation opens up new possibilities of defining semantic properties on this rich graph in order to characterize and profile the reasoning patterns of the participating actors.

Thilo Breitsprecher, Mihai Codescu, Constantin Jucovschi et al.

The engineering design process follows a series of standardized stages of development, which have many aspects in common with software engineering. Among these stages, the principle solution can be regarded as an analogue of the design specification, fixing as it does the way the final product works. It is usually constructed as an abstract sketch (hand-drawn or constructed with a CAD system) where the functional parts of the product are identified, and geometric and topological constraints are formulated. Here, we outline a semantic approach where the principle solution is annotated with ontological assertions, thus making the intended requirements explicit and available for further machine processing; this includes the automated detection of design errors in the final CAD model, making additional use of a background ontology of engineering knowledge. We embed this approach into a document-oriented design workflow, in which the background ontology and semantic annotations in the documents are exploited to trace parts and requirements through the design process and across different applications.