A Formal Treatment of Expressiveness and Relevance of Digital Evidence - Gruber, Jan; Humml, Merlin (Digital Threats: Research and Practice, 2023)

Argumentation Schemes for Blockchain Deanonymisation - Deuber, Dominic; Gruber, Jan; Humml, Merlin; Ronge, Viktoria; Scheler, Nicole (FinTech, 2024)
Cryptocurrency forensics have become standard tools for law enforcement. Their basic idea is to deanonymise cryptocurrency transactions to identify the people behind them. Cryptocurrency deanonymisation techniques are often based on premises that largely remain implicit, especially in legal practice. On the one hand, this implicitness complicates investigations. On the other hand, it can have far-reaching consequences for the rights of those affected. Argumentation schemes could remedy this untenable situation by rendering the underlying premises more transparent. Additionally, they can aid in critically evaluating the probative value of any results obtained by cryptocurrency deanonymisation techniques. In the argumentation theory and AI community, argumentation schemes are influential as they state the implicit premises for different types of arguments. Through their critical questions, they aid the argumentation participants in critically evaluating arguments. We specialise the notion of argumentation schemes to legal reasoning about cryptocurrency deanonymisation. Furthermore, we demonstrate the applicability of the resulting schemes through an exemplary real-world case. Ultimately, we envision that using our schemes in legal practice can solidify the evidential value of blockchain investigations, as well as uncover and help to address uncertainty in the underlying premises—thus contributing to protecting the rights of those affected by cryptocurrency forensics.<br
Keywords: argumentation; legal reasoning; blockchain analysis

Argumentation Schemes for Blockchain Deanonymization - Deuber, Dominic; Gruber, Jan; Humml, Merlin; Ronge, Viktoria; Scheler, Nicole (Sixteenth International Workshop on Juris-informatics (JURISIN 2022), 2022)

Argument parsing via corpus queries - Dykes, Nathan; Evert, Stephanie; Göttlinger, Merlin; Heinrich, Philipp; Schröder, Lutz (it - Information Technology, 2021)
We present an approach to extracting arguments from social media, exemplified by a case study on a large corpus of Twitter messages collected under the #Brexit hashtag during the run-up to the referendum in 2016. Our method is based on constructing dedicated corpus queries that capture predefined argumentation patterns following standard Walton-style argumentation schemes. Query matches are transformed directly into logical patterns, i. e. formulae with placeholders in a general form of modal logic. We prioritize precision over recall, exploiting the fact that the sheer size of the corpus still delivers substantial numbers of matches for all patterns, and with the goal of eventually gaining an overview of widely-used arguments and argumentation schemes. We evaluate our approach in terms of recall on a manually annotated gold standard of 1000 randomly selected tweets for three selected high-frequency patterns. We also estimate precision by manual inspection of query matches in the entire corpus. Both evaluations are accompanied by an analysis of inter-annotator agreement between three independent judges.<br
Keywords: argument minig; reasoning; corpus linguistics; social media

Automatic verification of application-tailored OSEK kernels - Deifel, Hans-Peter; Göttlinger, Merlin; Milius, Stefan; Schröder, Lutz; Dietrich, Christian; Lohmann, Daniel (2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017, 2017)

Common Knowledge of Abstract Groups - Humml, Merlin; Schröder, Lutz (Thirty-Seventh AAAI Conference on Artificial Intelligence Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence Thirteenth Symposium on Educational Advances in Artificial Intelligence, 2023)
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.<br
Keywords: KRR: Knowledge Representation Languages; KRR: Description Logics; KRR: Ontologies and Semantic Web; KRR: Reasoning with Beliefs

COOL 2 – A Generic Reasoner for Modal Fixpoint Logics (System Description) - Görlitz, Oliver; Hausmann, Daniel; Humml, Merlin; Pattinson, Dirk; Prucker, Simon; Schröder, Lutz (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2023)
There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The COOL 2 reasoner provides an implementation of such generic algorithms for coalgebraic modal fixpoint logics. As concrete instances, we obtain in particular reasoners for the aconjunctive and alternation-free fragments of the graded μ -calculus and the alternating-time μ -calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic and alternating-time temporal logic (ATL), as well as on a dedicated set of benchmarks for the graded μ -calculus.
CRIS-Team Scopus Importer:2023-10-06

DIREGA – Building Decision Support for German Register Law - Adrian, Axel; Basaran, Osman Anil; Dykes, Nathan; Evert, Stephanie; Gritz, Michael; Humml, Merlin; Kohlhase, Michael; Lindner, Johannes; Maier, Andreas; Prettner, Stephan; Rapp, Max; Schröder, Lutz; et al. (Frontiers in Artificial Intelligence and Applications, 2024)
The interdisciplinary project DIREGA aims to analyse the joint application of linguistic, symbolic, and sub-symbolic AI techniques to German register law. This analysis is based on a dataset consisting of all past applications, related documents, and decisions of German register courts in the Free State of Bavaria. Corpus queries and sub-symbolic AI methods will be used for information extraction which then instantiate facts for the symbolic reasoning pipeline based on a manual formalization of the relevant laws. The goal is to build a prototypical implementation checking register applications and providing a detailed explanation for acceptance (or rejection) to aid legal professionals such as notaries in drafting and reviewing such document

Finding Argument Fragments on Social Media with Corpus Queries and LLMs - Dykes, Nathan; Evert, Stephanie; Heinrich, Philipp; Humml, Merlin; Schröder, Lutz (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2024)
We are concerned with extracting argumentative fragments from social media, exemplified with a case study on a large corpus of English tweets about the UK Brexit referendum in 2016. Our overall approach is to parse the corpus using dedicated corpus queries that fill designated slots in predefined logical patterns. We present an inventory of logical patterns and corresponding queries, which have been carefully designed and refined. While a gold standard of substantial size is difficult to obtain by manual annotation, our queries can retrieve hundreds of thousands of examples with high precision. We show how queries can be combined to extract complex nested statements relevant to argumentation. We also show how to proceed for applications needing higher recall: high-precision query matches can be used as training data for an LLM classifier, and the trade-off between precision and recall can be freely adjusted with its cutoff threshold.
CRIS-Team Scopus Importer:2024-08-16
Keywords: Argument extraction; Corpus queries; LLMs; Semantic parsing; Social media

Formal Verification of Necessary and Sufficient Evidence in Forensic Event Reconstruction - Gruber, Jan; Humml, Merlin; Schröder, Lutz; Freiling, Felix (Proceedings of the Digital Forensics Research Conference Europe (DFRWS EU), 2023)
We study the problem of digital forensic event reconstruction, i.e., the question of whether a certain event has happened in the past of an execution by a given digital system. Instead of devising new search algorithms to solve the problem directly, we defne two novel concepts in standard linear- time temporal logic and use these concepts to solve event reconstruction using established tools for model checking. The fiirst concept is that of sufficient evidence, i.e., a characterization of states whose observation is sufficient to prove that a certain event happened in the past. The second concept is that of necessary evidence, i.e., a characterization of states whose negation can be used to refute the claim that a certain event happened in the past. Using the model checker NuSMV, we built a prototype that can calculate these two sets for a given digital system in order to solve the forensic event reconstruction problem. We relate these concepts to previous work in formal event reconstruction and apply it to Gladyshev's "ACME Manufacturing" benchmark example to illustrate the usefulness of our approach and the improved notion of digital evidence.
Keywords: digital evidence; digital investigations; forensic event reconstruction; formal methods; forensic computing

Generic Model Checking for Modal Fixpoint Logics in COOL-MC - Hausmann, Daniel; Humml, Merlin; Prucker, Simon; Schröder, Lutz; Strahlberger, Aaron (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2024)
We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (non-deterministic, game-based, probabilistic etc.) and in the next-step modalities used in formulae. The tool implements generic model checking algorithms developed in coalgebraic logic that are easily adapted to concrete instance logics. Apart from the standard modal μ -calculus, COOL-MC currently supports alternating-time, graded, probabilistic and monotone variants of the μ -calculus, but is also effortlessly extensible with new instance logics. The model checking process is realized by polynomial reductions to parity game solving, or, alternatively, by a local model checking algorithm that directly computes the extensions of formulae in a lazy fashion, thereby potentially avoiding the construction of the full parity game. We evaluate COOL-MC on informative benchmark sets.
CRIS-Team Scopus Importer:2024-01-19
Keywords: lazy evaluation; Model checking; parity games; μ -calculus

Informal Conversations in Formal Logic - Göttlinger, Merlin (Joint Workshop of the German Research Training Groups in Computer Science, 2021)

Leveraging High-Precision Corpus Queries for Text Classification via Large Language Models - Dykes, Nathan; Evert, Stephanie; Heinrich, Philipp; Humml, Merlin; Schröder, Lutz (Proceedings of the First Workshop on Language-driven Deliberation Technology (DELITE) @ LREC-COLING 2024, 2024)
We use query results from manually designed corpus queries for fine-tuning an LLM to identify argumentative fragments as a text mining task. The resulting model outperforms both an LLM fine-tuned on a relatively large manually annotated gold standard of tweets as well as a rule-based approach. This proof-of-concept study demonstrates the usefulness of corpus queries to generate training data for complex text categorisation tasks, especially if the targeted category has low prevalence (so that a manually annotated gold standard contains only a small number of positive examples).

Reconstructing Arguments from Noisy Text - Dykes, Nathan; Evert, Stephanie; Göttlinger, Merlin; Heinrich, Philipp; Schröder, Lutz (Datenbank-Spektrum, 2020)
Social media are of paramount importance to public discourse. RANT aims to contribute methods and formalisms for extracting, representing, and processing arguments from noisy text found in social media discussions, using a large corpus of pre-referendum Brexit tweets as a running case study. We identify recurring linguistic argumentation patterns in a corpus-linguistic analysis and formulate corresponding corpus queries to extract arguments automatically. Given the huge amount of social media data available, our approach aims at high precision at the possible price of low recall. Argumentation patterns are directly associated with logical patterns in a dedicated formalism and accordingly, individual arguments are directly parsed as logical formulae. The logical formalism for argument representation features a broad range of modalities capturing real-life modes of expression. We cast this formalism as a family of instance logics in the generic framework of coalgebraic logic and complement it by a flexible framework to represent relationships between arguments; including standard relations like attack and support but also relations extracted from metadata. Some relations are inferred from the logical content of individual arguments. We are in the process of developing suitable generalizations of various extension semantics for argumentation frameworks combined with corresponding algorithmic methods to allow for the automated retrieval of large-scale argumentative positions.<br

The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies - Göttlinger, Merlin; Schröder, Lutz; Pattinson, Dirk (Leibniz International Proceedings in Informatics (LIPIcs), 2021)
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 non-determinism 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∩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.<br
Keywords: Alternating-time logic; multi-agent systems; coalitional strength