Professor in Computer Science
Technische Universität Dresden, Germany
Standpoint logics have been introduced in recent work by Alvarez et al. as a multi-modal logic to reason about the integrated knowledge of multiple agents that might have different, possibly contradicting views (``standpoints''). The essential new feature are modalities for expressing that a property is conceivable according to the view of an agent. The talk considers the model checking problem for a standpoint extension of classical linear temporal logic (LTL) with five semantics for the standpoint modalities. The semantics differ in the information an agent can extract from the history. Starting with a generic non-elementary model checking algorithm that is applicable to all five semantics, a more detailed complexity analysis leads to improved upper bounds for four of the semantics. In three cases, the model checking problem turns out to be PSPACE-complete, i.e., not harder than the model checking problem for classical LTL, which stands in contrat to the known EXPSPACE-completeness result for the satisfiability problem for standpoint LTL.
Christel Baier is a full professor and head of the chair for Algebraic and Logic Foundations of Computer Science at the Faculty of Computer Science of the Technische Universität Dresden since 2006. Since 2022 she holds an honorary doctorate (Dr. rer. nat. h.c.) from RWTH Aachen. From the University of Mannheim she received her Diploma in Mathematics in 1990, her Ph.D. in Computer Science in 1994 and her Habilitation in 1999. She was an associate professor for Theoretical Computer Science at the University of Bonn from 1999 to 2006. She was member of the DFG (German Research Foundation) review board for computer science from 2012 to 2019, and is a member of the DFG senate commission on Research Training Groups since 2020. She is a member of Academia Europaea and of the Saxony Academy of Science. Her research focuses on modeling, specification and verification of reactive systems, quantitative analysis of stochastic systems, probabilistic model checking, temporal and modal logics and automata theory.
Professor of Quantum Programming
University of Edinburgh, UK
Quantum computing inherently has concurrent aspects. Even with only local operations, qubits can influence each other. This ability leads to genuinely new quantum communication protocols, but also raises even thornier questions of causality than in classical concurrent computing. Monoidal categories and their string diagrams form a convenient and popular language for quantum computing. After an introduction to quantum concurrency, I will discuss the framework of tensor topology, which aims to analyse the interaction of several agents in monoidal categories, using notions from sheaf theory and ordered locales.
Chris Heunen is the Professor of Quantum Programming at the University of Edinburgh, co-founder of the Quantum Software Lab, and Director of the Centre for Doctoral Training in Quantum Informatics. He has been working in theoretical computer science and quantum computing for over 20 years, obtaining his PhD at the Radboud University Nijmegen in the Netherlands and working at the University of Oxford and the California Institute of Technology before moving to Edinburgh. His expertise lies in categorical semantics of quantum programming, on which he has authored a textbook, and has published articles across top venues in computer science (LiCS, ICALP), mathematics (PNAS, Advances in Mathematics), and physics (PRL). His work has been awarded the 2012 Birkhoff-von Neumann prize by the International Quantum Structures Association.
Professor in Computer Science
Aalborg University, Denmark
Dependency graphs, introduced over two decades ago by Liu and Smolka, are directed graphs with hyperedges linking nodes to sets of target nodes to model causal dependencies. Many verification problems can be addressed by computing minimum or maximum fixed-point assignments on these graphs. I shall introduce the notion of dependency graph including efficient and distributed on-the-fly verification algorithms and demonstrate their applicability on a number of verification problems like CTL model checking of concurrent systems. In classical dependency graphs, assignments map nodes to Boolean values, but recent work has expanded to more general, even infinite, domains. In the second part of the talk, I will review recent advancements in extending dependency graphs towards verification of quantitative, probabilistic, parameterized, and timed systems and provide a link to existing verification tools supporting the dependency graph approach.
Jiri Srba is professor in computer science at Aalborg University, Denmark. He obtained his first PhD degree in 2003 at BRICS international PhD school in Aarhus and a second one in
2005 from Faculty of Informatics, Masaryk University in Brno, Czech Republic. Jiri Srba co- authored more than 140 peer-reviewed scientific papers and a book about verification of reactive systems. He is a steering committee member of CONCUR and a founder and prime investigator of the award-winning model checker TAPAAL. His research focuses on modeling, verifying, and analyzing real-time and embedded systems, with applications in web services, workflow analysis, and industrial cases, relying on formalisms like Petri nets, timed automata, modal transition systems, and process algebras. He also explores component-based software, energy game optimization, strategy synthesis, and the decidability and complexity questions for infinite-state processes.
