The project will focus on developing symbolic computation algorithms for the analysis of program loops with numeric and unbounded data structures, as well as probabilistic features. For doing so, computer algebra techniques in combination with statistical method will be designed to analyze safety and liveness properties of emerging applications of programming languages, such as synthesizing probabilistic loops from the value distributions of program variables and inferring tight bounds on the expected runtimes of probabilistic programs.

The project will focus on obtaining an in-depth understanding of the parameterized complexity of prominent problems that arise in artificial intelligence research and in related areas. The pursued topics and general approaches may, for instance, follow a similar direction as the following recent publications:

[1] Robert Ganian, Sebastian Ordyniak: The complexity landscape of decompositional parameters for ILP. Artif. Intell. 257: 61-71 (2018).
[2] Robert Ganian, Thekla Hamm, Guillaume Mescoff: The Complexity Landscape of Resource-Constrained Scheduling. IJCAI 2020: 1741-1747.

The project will target new fixed-parameter algorithms and algorithmic lower bounds for fundamental problems in theoretical computer science. The focus will lie on techniques that utilize structural parameters of an input graph.

Example papers:
[1] Robert Ganian, Fabian Klute, Sebastian Ordyniak: On Structural Parameterizations of the Bounded-Degree Vertex Deletion Problem. Algorithmica 83(1): 297-336 (2021)
[2] Eduard Eiben, Robert Ganian, Thekla Hamm, Fabian Klute, Martin Nöllenburg: Extending Partial 1-Planar Drawings. ICALP 2020: 43:1-43:19

Probabilistic programs (PPs) are now gaining momentum due to the several emerging applications in the areas of machine learning and artificial intelligence. High-tech giants, such as Google, Microsoft and Uber, have started to develop their own probabilistic programming languages that include native constructs for sampling distributions, enabling the programmer to freely mix deterministic and stochastic elements. This programming paradigm offers a unifying framework for encoding probabilistic machine learning models, such as Bayesian networks, with decision making routines used, for example, in autonomous parking. One of the main problems that arise from introducing randomness into the program is that we can no longer view variables as single values, but as distributions of values. Dealing with distributions is far more complex and some simplifications and approximations are necessary. The resulting flexible framework comes at the price of programs with behaviors hard to analyze, leading to unpredictable consequences in safety-critical applications, such as in autonomous driving. This research project consists in developing new automated techniques to analyse probabilistic programs (e.g. proving termination, learning invariants, verifying safety condition) or to automatically synthesize probabilistic programs satisfying certain properties.

Preliminary work of the supervisors:
[1] M. Moosbrugger, E. Bartocci, J.-P. Katoen, L. Kovacs: Automated Termination Analysis of Polynomial Probabilistic Programs. In Proc. of ESOP 2021: the 30th European Symposium on Programming, vol. 12648, pp. 491–518, 2021, doi: 10.1007/978-3-030-72019-3_18
[2] E. Bartocci, L. Kovacs, M. Stankovic: Analysis of Bayesian Networks via Prob-Solvable Loops. In Proc. of ICTAC 2020: International Colloquium on Theoretical Aspects of Computing, vol. 12545, pp. 221–241, 2020, doi: 10.1007/978-3-030-64276-1_12
[3] E. Bartocci, L. Kovacs, M. Stankovic: MORA – Automatic Generation of Moment-Based Invariant, In Proc. of TACAS 2020: the 26th Intern. Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 12078, pp. 492–498, 2020, doi: 10.1007/978-3-030-45190-5_28
[4] E. Bartocci, L. Kovacs, M. Stankovic: Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops, In Proc. of ATVA 2019: the 17th Intern. Conference on Automated Technology for Verification and Analysis, vol. 11724, pp. 69–86, 2019, doi: 10.1007/978-3-030-59152-6

Debugging Cyber-Physical Systems (CPS) is a cumbersome and costly activity. CPS models combine continuous and discrete dynamics. A fault in a physical component manifests itself in a very different way than a fault in a state machine. Furthermore, faults can propagate both in time and space before they can be detected at the observable interface of the model. In recent work we have investigated fault localization [1] and failure explanation techniques [2] for Simulink/Stateflow diagrams of cyber-physical systems. The main idea of our approach is to combine testing [3], specification mining [4,5], and failure analysis to automatically explain failures supporting the debugging activities. This research project aims at further developing these techniques and going beyond them by automatically proposing possible repair solutions to the engineer.

[1] E. Bartocci, T. Ferrère, N. Manjunath, D. Nickovic: Localizing Faults in Simulink/Stateflow Models with STL. Proc. of HSCC 2018: 197-206, doi: 10.1145/3178126.3178131
[2] E. Bartocci, N. Manjunath, L. Mariani, et al. CPS Debug: Automatic failure explanation in CPS models. Int J Softw Tools Technol Transfer (2021), doi: 10.1007/s10009-020-00599-4
[3] E. Bartocci, R. Bloem, B. Maderbacher, N. Manjunath, D. Nickovic: Adaptive Testing for Specification Coverage in CPS Models, In Proc. of ADHS: the 7th IFAC Conference on Analysis and Design of Hybrid Systems, 2021 (preprint: https://arxiv.org/abs/2010.06674)
[4] E. Bartocci, J. Deshmukh, F. Gliger, C. Mateis, D. Nickovic, X. Qin: Mining Shape Expressions from Positive Examples, In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39(11), pp. 3809 -20, 2020, doi: 10.1109/TCAD.2020.3012240 [5] L. Nenzi, S. Silvetti, E. Bartocci, L. Bortolussi: A Robust Genetic Algorithm for Learning Temporal Specifications from Data, In Proc. of QEST 2018: the 15th International Conference on Quantitative Evaluation of SysTems, vol. 11024, pp. 323–338, 2018, doi: 10.1007/978-3-319-99154-2_20

Hyperproperties extend the conventional notion of trace properties from a set of traces to a set of sets of traces. Many interesting requirements in computing systems are hyperproperties and cannot be expressed by trace properties. Examples include (1) a wide range of information-flow security policies such as noninterference and observational determinism (2) sensitivity and robustness requirements in cyber-physical systems and consistency conditions such as linearizability in concurrent data structures. Hyperproperties can describe the requirements of probabilistic systems as well. They generally express probabilistic relations between multiple executions of a system. For example, in information-flow security, adding probabilities is motivated by establishing a connection between information theory and information flow across multiple traces. A prominent example is probabilistic schedulers that open up an opportunity for an attacker to set up a probabilistic covert channel. Or, probabilistic causation compares the probability of occurrence of an effect between scenarios where the cause is or is not present. This research project aims at developing new automated and possibly scalable exact or approximate techniques to verify probabilistic hyperproperties over different classes of probabilistic models ranging from Markov Decision Processes to Stochastic games.

Previous work of the supervisor:
[1] E. Ábrahám, E. Bartocci, B. Bonakdarpour, O. Dobe: Probabilistic Hyperproperties with Nondeterminism. ATVA 2020: 518-534, doi: 10.1007/978-3-030-59152-6
[2] E. Ábrahám, E. Bartocci, B. Bonakdarpour, O. Dobe: Parameter Synthesis for Probabilistic Hyperproperties. LPAR 2020: 12-31, doi: 10.1007/978-3-030-64276-1_12

Autonomous agents must  possess the ability to adapt to (potentially unpredictable) changes in their environment. Machine learning techniques such as reinforcement learning (RL) haven proven successful methods for teaching agents this behaviour. However, when supporting humans, AI agents should restrict their own action to the ethical standards recognized in fundamental right and ethical theories, introducing a requirement for ethical reasoning.  RL has been employed to enforce such standards as well; agents can be trained to act in line with further rewards/penalties assigned according to the performance of ethical/unethical behaviour through a reward function. However, this does not provide a guarantee of the desired behaviour. Moreover, such techniques are not well equipped to handle the complexities of ethical reasoning. In general, like other black-box machine learning methods, RL cannot transparently explain why a certain policy is compliant or not. Additionally, when the ethical values are embedded in the learning process, a small change in their definition would require us to retrain the policy from scratch. This project aims at investigating how to embed normative reasoning techniques with the machine learning components responsible for the decision making, thus combing symbolic and sub-symbolic AI.

[1] Emery Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori: A Normative Supervisor for Reinforcement Learning Agents. CADE 2021: 565-576, doi: 10.1007/978-3-030-79876-5_32

Proofs of security and privacy are extremely complex and error prone and the most popular protocols, applications, and services are regularly affected by bugs and vulnerabilities. This state of affairs calls for the design of formal methods for the enforcement of rigorous security and privacy properties in complex, large scale systems. A central challenge in this field is to strive for the sweet spot between automation and expressiveness. Target application domains include web applications, smart contracts, blockchain protocols, and learning-based systems.

[1] EThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. Schneidewind, Grischchenko, Scherer, Maffei. ACM CCS’20: 621-640

Software and hardware is widely acknowledged to be full of bugs. Despite decades-long efforts, formal verification hasn’t fufilled the promise of providing us with correct-by-construction or provenly correct systems. Hence, this project focuses on formal falsification: automated testing and the automated detection of bugs in software and hardware. We target a broad range of bugs, including bugs in concurrent and distributed systems, security bugs, but also bugs in machine learning-based systems. The goal is to provide automated techniques that provide formal guarantees.

Many computational problems that arise in Artificial Intelligence and Combinatorial Optimization are intractable. Nevertheless, efficient, practical algorithms have been developed that exploit the hidden structure of problem instances that arise from real-world applications. This project aims at utilizing recent progress in Machine Learning to speed up such solving algorithms.Relevant literature:
[1] Yoshua Bengio, Andrea Lodi, Antoine Prouvost: Machine learning for combinatorial optimization: A methodological tour d’horizon. Eur. J. Oper. Res. 290(2): 405-421 (2021)
[2] Jia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki: Learning Rate Based Branching Heuristic for SAT Solvers. SAT 2016: 123-140
[3] Holger H. Hoos, Tomás Peitl, Friedrich Slivovsky, Stefan Szeider: Portfolio-Based Algorithm Selection for Circuit QBFs. CP 2018: 195-209

Present day computing witnesses a swift change of view between a single program running on a computer to a complex system, such as a cloud, an autonomous car or a cryptocurrency. This project aims at providing logical tools for the design and verification of such systems, using the principle of local reasoning: a state change, either internal or a reconfiguration, involves a limited resource, the rest of the system remaining unchanged. We plan to design logics for reasoning about such reconfigurable systems and automate these logics by new (semi-)decision procedures integrated with compositional push-button verification methods, that guarantee behavioral correctness.

Stream reasoning is a topic of growing importance. It is in partciular challenging if multiple entities (agents) have to process and to exchange information resulting in streams, and if real-time settings play a role. While some proposals for semantics of systems of entities agents exist, there is room for improvement to take various features (numeric uncertainy, realibility, learning) etc. into account, in particular, if declarative methodes are used for describing the behaviour of the entities.

Answer Set Programming is a successful declarative problem solving paradigm that has been deployed to many application fields. In order to enlarge its applicability, Answer Set Programming has been extended and combined with other problem solving methods, among them SAT and SMT solving, imperative programming, constraint programming etc. Recently, there has been a strong interest in combining Answer Set Programming with Machine Learning, leading to neuro-symbolic computation models that integrate neural networks with rules, or apply reinfocement learning to rules and program evalution, or use Answer Set Programming to guide learning. In this project, the Hybrid ASP approach will be further extended, and novel integration, algorithms, and applications will be considered.

Symbolic formalisms, among them mixed integer programming, constraint solving, SAT solving and answer set programming, have been successfully used for describing and solving scheduling problems in different applications domains, such as assigning jobs to machines, assembling a roster for nurses in a hospital, etc.

However, the (non)existence of solutions is not always clear, why certain assignments are made (or not), why certain candidate schedules are not acceptable, or in case of optimization why they are not optimal etc. This project aims to research on methods and tools for answering these questions in terms of meaningful explanations that refer to data or statements in the problem description, providing valuable support to the user for obtaining more insight into a scheduling problem.

Drawing inferences and conclusions in general depends on the context in which a reasoner is situated; e.g., cheering to a goal of your team is natural in general, but may be inappropriate if you are in the stadium among hooligans favouring the opponents. Dealing with context often requires to deal with ambiguity and possibly overriding of information due to inheritance from more general to specific settings. Furthermore, contexts might come in different aspects, like time, space etc. (above, when we are watching a match, and where).
This project will explore challenges that come from such a setting, which leads to multi-objective optimisation problems. A possible starting point are context-knowledge repositories, which are a versatile formalisms based on description logics. In particular, providing semantics, studying complexity of inference (which besides classical query answering might also include what-if questions), developing efficient algorithms and addressing applications would be on the agenda.

Preferences are a crucial element in formalisations of argumentation scenarios. In this project, we aim to incorporate a recently proposed general framework for preference handling [1] to argumentation formalisms. Such preferences can be applied at different points in the evaluation process: one approach would be to rank outcomes of argumentation frameworks; another app roach is to rank possible completions of incomplete argumentation frameworks [2].

[1] Michael Bernreiter, Jan Maly, Stefan Woltran: Choice Logics and Their Computational Properties. Accepted for IJCAI’21.
[2] Dorothea Baumeister, Matti Järvisalo, Daniel Neugebauer, Andreas Niskanen, Jörg Rothe: Acceptance in incomplete argumentation frameworks. Artif. Intell. 295: 103470 (2021).

Notions of equivalence between logic programs constitute central a theoretical tool to understand concepts like program simplification. While several such notions have been studied in the literature (e.g., [1]), recent developments like forgetting [2] or abstraction call for refined notions of equivalence. The overall goal in this project to define such notions and explore suitable logical characterisations.

[1] Stefan Woltran: A common view on strong, uniform, and other notions of equivalence in answer-set programming. Theory Pract. Log. Program. 8(2): 217-234 (2008)
[2] Ricardo Gonçalves, Matthias Knorr, João Leite, Stefan Woltran: On the limits of forgetting in Answer Set Programming. Artif. Intell. 286: 103307 (2020)

There are many open problems in Discrete Mathematics, including Extremal Graph Theory, Ramsey Theory, and Design Theory, where one is interested in finding smallest examples or counterexamples to conjectures. Since the search space grows quickly with the size of the objects, advanced symmetry-breaking methods are essential. This project combines symmetry-breaking with SAT-based methods.

Relevant literature:
[1] Michael Codish, Alice Miller, Patrick Prosser, Peter J. Stuckey: Constraints for symmetry breaking in graph representation. Constraints, an Int. J. 24(1): 1-24 (2019).
[2] Tomás Peitl, Stefan Szeider: Finding the Hardest Formulas for Resolution. Journal Artificial Intelligence Research, volume 72, pages 69–97, 2021.

This project aims to utilize recent SAT-solving progress to tackle problems that arise in Computational Social Choice, such as the aggregation of preferences of multiple agents or the prevention of rigged elections. The work includes theoretical investigations combined with experimental evaluation on real-world data.

Relevant literature:
[1] Ulle Endriss: Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms. AAAI 2020: 1918-1925.
[2] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.

This project analyzes subsymbolic machine learning models, such as neural networks, with symbolic tools like SAT solvers. The aim is to replace opaque models with explainable and verifiable models, easily checked for bias.Relevant literature:
[1] Alexey Ignatiev, Nina Narodytska, João Marques-Silva: Abduction-Based Explanations for Machine Learning Models. AAAI 2019: 1511-1519.
[2] Christoph Molnar: Interpretable machine learning. A Guide for Making Black Box Models Explainable, 2019.
[3] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.

Norms are enormously important in a variety of fields, including law, emergency management and AI. The application of norms inevitably leads to deontic conflicts and deciding which norms override which other norms is often controversial. This project investigates conflict resolution methods for normative reasoning and aims to develop effective tools usable in application domains. As our main source of inspiration, we look at ways of dealing with normative reasoning that diverge from the contemporary European and Anglo-American approaches, thereby questioning implicit cultural biases in dealing with deontic conflicts. The various legal and philosophica ltraditions we will examine will be applied to real-world reasoning scenarios coming from contemporary ethical debates and normative AI cases. 

https://mimamsa.logic.at 

Logics different from classical logics (Non classical logics) provide adequate formalisms for reasoning, e.g., about time, norms, knowledge, dynamic data structures, vague information and resources. As such, these logics have been increasingly applied in various disciplines including artificial intelligence, philosophy, and in computer science, where most of these logics originate.

Non classical logics are usually introduced or described in a declarative way in the proof framework due to Hilbert and Frege. However, the resulting systems are extremely cumbersome when it comes to finding or analyzing proofs and for proving properties of the formalized logics. These tasks call for algorithmic presentations of the logics especially in the form of analytic calculi. Analyticity is crucial here since proofs in such calculi proceed by a stepwise decomposition of the objects to be proved.

The aim of this project is to advance the methods for the automated introduction of analytic calculi for non-classical logics, and their exploitation. 

Algorithmic decision making may be inherently prone to unfairness, even when there is no intention for it. This is the case, for instance, when the data sets used with Machine Learning algorithms contain biases. In this project we explore the use of logical methods to tackle this issue.

Description Logics (DLs) are a toolkit of decidable formalisms for representing knowledge, differing in their expressivity and in the computational cost of solving inference tasks. They are widely used in a range of application fields for writing “ontologies” that describe sharable domain knowledge.  Efficient reasoners exist even for very expressive DLs in which reasoning has high computational complexity. However, there are many important reasoning services for which no practicable algorithms have been developed. This applies, specifically, to DL reasoning with numeric constraints on predicates, with different forms of data incompleteness, or with constraints on the size of models. These problems all have high worst-case computational complexity, and the few known techniques are not scalable beyond toy examples  with a handful of predicates.  The goal of this project is to develop scalable algorithms for this kind of reasoning services, particularly by exploiting efficient reasoners for combinatorial problems like SAT solvers, SMT solvers, QBF solvers, and (M)ILP solvers.A. Schidler, S. Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.
C. Lutz, U. Sattler, L. Tendera: The complexity of finite model reasoning in description logics. Inf. Comput. 199(1-2): 132-171 (2005)

The Ontology-based data access (OBDA) paradigm facilitates access to data from possibly unstructured, incomplete, and disparate sources,  by using an ontology as an intermediate layer that provides a unified view of the data described in a familiar high-level vocabulary. But despite its many successful applications, current OBDA technologies still have severe limitations that hinder their application in many more fields. In particular, the standard formalisms for accessing data are very poorly suited for analysing temporal and streaming data. In this project, we want to build on recently developed rule-based languages for temporal and streaming data (like LARS and DatalogMTL) to query and analyse data in OBDA systems. We want to tailor variants of these languages that can be paired with the ontology languages typically used in OBDA,  to obtain rich declarative formalisms for temporal data analysis. The project is envisioned to cover both the theoretical study of the tailored formalisms, and practical challenges arising from real-life applications.S. Brandt, E. Güzel Kalayci, V. Ryzhikov, G. Xiao, and M. Zakharyaschev. Querying log data with metric temporal logic. J. Artif. Int. Res. 62, 1. 2018 https://doi.org/10.1613/jair.1.11229
H. Beck, M. Dao-Tran, T. Eiter: LARS: A Logic-based framework for Analytic Reasoning over Streams. Artif. Intell. 261: 16-70 (2018).

In this project, we want to continue with the study of expressive Knowledge Representation languages that allow to combine open- and closed-world reasoning with rules and ontologies. We want to  develop scalable algorithms for reasoning with knowledge bases in different fragments, and tailor variants that are better suited for real world use cases. We are also very interested in abductive automated reasoning techniques for explaining the inferences derived from such knowledge bases.L. Bajraktari, M. Ortiz, M. Simkus. Combining Rules and Ontologies into Clopen Knowledge Bases.   AAAI 2018.
S. Lukumbuzya,  M. Ortiz, M. Simkus. Resilient logic programs: answer set programs challenged by ontologies. AAAI 2020.

With associative web search, a user inputs a list of entities such as, for example, “BMW, Ford, Tesla” and obtains an expanded list with similar entities, in our example a list of all major car makes. The main technique for achieving associative web search is called entity set expansion (ESE). On a given input list, such as the one above, ESE makes web queries such as “+BMW +Ford +Tesla” using a standard search engine, and analyzes the first N (say N=100) results so as to discover lists in which the search entities co-occur with further entities. The original list is then  expanded with these new entities. This expansion process is iteratively continued until hopefully all similar items (in our case, car makes) are found. ESE is, unfortunately, a rather error prone technique which has been improved using various statistical methods, as well as machine learning and clustering methods. The topic of this PhD project is to investigate knowledge-based and rule-based reasoning methods for improving ESE (possibly in combination with the formerly mentioned methods). This will involve the use of large general factual knowledge graphs such as Wikidata , Wordnet, and BabelNet, as well as specialized knowledge graphs and rule-bases for particular application domains. 

Model Checking is a technique to automatically check whether a given system (model) satisfies a property. Model checking has been successfully applied to hardware as well as software. Many successful model checking algorithms are based on satisfiability solvers, taking advantage of the huge strides made in this field in the last two decades. This project focuses on the tight integration and similarities of contemporary model checking algorithms and satisfiability solvers, exploiting and lifting the latest and most promising advances in automated solving to model checking.