Th 38th Annual ACM/ IEEE Symposium on Logic in Computer Science (LICS), took place at Boston University, Boston, USA, from June 26 to June 29, 2023, with co-located events taking place on June 24 and June 25. Five workshops were co-located with LICS 2023: combinatorial games in finite model theory, the decision problem in first order logic, international workshop on quantitative logical method, structure meets power, and the logic mentoring workshop.

In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verification problem is to determine if a given system has a limit configuration satisfying a given regular property. This formulation of the problem encompasses verification of reachability as well as of many liveness properties. We show that this verification problem, while undecidable in general, is decidable for nested lock usage. We show Exptime-completeness of the verification problem. The main source of complexity is the number of parameters in the spawn operation. If the number of parameters is bounded, our algorithm works in Ptime for properties expressed by parity automata with a fixed number of ranks.

We study the Büchi non-emptiness problem for networks of timed automata. Standard solutions consider the network as a monolithic timed automaton obtained as a synchronized product and build its zone graph on-the-fly under the classical global-time semantics. In the global-time semantics, all processes are assumed to have a common global timeline. Bengtsson et al. in 1998 have proposed a local-time semantics where each process in the network moves independently according to a local timeline, and processes synchronize their timelines when they do a common action. It has been shown that the local-time semantics is equivalent to the global-time semantics for finite runs, and hence can be used for checking reachability. The local-time semantics allows computation of a local zone graph which has good independence properties and is amenable to partial-order methods. Hence local zone graphs are able to better tackle the state-space explosion due to concurrency. In this work, we extend the results to the Büchi setting. We propose a local zone graph computation that can be coupled with a partial-order method, to solve the Büchi non-emptiness problem in timed networks. In the process, we develop a theory of regions for the local-time semantics.

A timed network is a parallel composition of timed automata synchronizing on common actions. We develop a methodology that allows to use partial-order methods when solving the reachability problem for timed networks. It is based on a local-time semantics proposed by [Bengtsson et al. 1998]. A new simulation based abstraction of local-time zones is proposed. The main technical contribution is an efficient algorithm for testing subsumption between local-time zones with respect to this abstraction operator. The abstraction is not finite for all networks. It turns out that, under relatively mild conditions, there is no finite abstraction for local-time zones that works for arbitrary timed networks. To circumvent this problem, we introduce a notion of a bounded-spread network. The spread of a network is a parameter that says how far the local times of individual processes need to diverge. For bounded-spread networks, we show that it is possible to use subsumption and partial-order methods at the same time.

We present two active learning algorithms for sound deterministic negotiations. Sound deterministic negotiations are models of distributed systems, a kind of Petri nets or Zielonka automata with additional structure. We show that this additional structure allows to minimize such negotiations. The two active learning algorithms differ in the type of membership queries they use. Both have similar complexity to Angluin's L* algorithm, in particular, the number of queries is polynomial in the size of the negotiation, and not in the number of configurations.

The reachability problem for timed automata asks if a given automaton has a run leading to an accepting state, and the liveness problem asks if the automaton has an infinite run that visits accepting states infinitely often. Both of these problems are known to be P space -complete. We show that if P ≠P space , the liveness problem is more difficult than the reachability problem; in other words, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is P space -hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it to existing solutions.

The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm. One of the recent methods of verification of distributed algorithms is to abstract an algorithm to the Heard-Of model and then to verify the abstract algorithm using semi-automatic procedures. Our results allow, in some cases, to avoid the second step in this methodology.

The lambda Y-calculus with priorities is a variant of the simply-typed lambda calculus designed for higher-order model-checking. The higher-order model-checking problem asks if a given parity tree automaton accepts the Böhm tree of a given term of the simply-typed lambda calculus with recursion. We show that this problem can be reduced to the same question but for terms of lambda Y-calculus with priorities and visibly parity automata; a subclass of parity automata. The latter question can be answered by evaluating terms in a simple powerset model with least and greatest fixpoints. We prove that the recognizing power of powerset models and visibly parity automata are the same. So, up to conversion to the lambda Y-calculus with priorities, powerset models with least and greatest fixpoints are indeed the right semantic framework for the model-checking problem. The reduction to lambda Y-calculus with priorities is also efficient algorithmically: it gives an algorithm of the same complexity as direct approaches to the higher-order model-checking problem. This indicates that the task of calculating the value of a term in a powerset model is a central algorithmic problem for higher-order model-checking.

Automatic verification of concurrent systems is an active area of research since at least a quater of a century. We focus here on analyses of systems designed to operate with an arbitrary number of processes. German and Sistla, already in 1992, initiated in depth investigation of this problem for finite state systems. For infinite state systems, like pushdown systems, extra care is needed to avoid undecidability, as reachability is undecidable even for two identical pushdown processes communicating via single variable. Kahlon and Gupta in 2006 have proposed to use parametrization as means of bypassing this undecidability barrier. Indeed when instead of two pushdown processes we consider some unspecified number of them, the reachability problem becomes decidable. This idea of parametrization as an abstraction has been pursued further by Hague, who in 2011 has shown that the problem is still decidable when one of the pushdown processes is made different from the others: there is one leader process and many contributor processes. We discuss how the idea of parametrization as an abstraction leads to decidability, and in some cases even efficient algorithms, for verification of systems which combine recursion with dynamic thread creation.

In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.

In verification, an automata theoretic approach is by now a standard. In order to extend this approach to higher-order programs we need a good understanding of higher-order control flow, and for this semantics has the right tools. We present some results and methods of this subject between automata theory and semantics.

We study the topological complexity of languages of Buchi automata on infinite binary trees. We show that such a language is either Borel and WMSO-definable, or Sigma_1^1-complete and not WMSO-definable; moreover it can be algorithmically decided which of the two cases holds. The proof relies on a direct reduction to deciding the winner in a finite game with a regular winning condition.

We consider the model of parametrized asynchronous shared-memory pushdown systems, as introduced in [Hague'11]. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Esparza, Ganty, Majumdar'13] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdar'15]. We show here that the liveness problem is PSPACE-complete. We also introduce the universal reachability problem. We show that it is decidable, and coNEXPTIME-complete. Finally, using these results, we prove that the verifying regular properties of traces of executions, satisfying some stuttering condition, is also decidable in NEXPTIME for this model.

Simply typed λ-calculus with fixpoint combinators, λY-calculus, offers an interesting method for approximating program semantics. The Böhm tree of a λY-term represents the meaning of the program up to the meaning of built-in constants. It is much easier to reason about properties of such trees than properties of interpreted programs. Moreover, some interesting properties of programs are already expressible on the level of these trees.Collapsible pushdown automata (CPDA) give another way of generating the same class of trees as λY-terms. We clarify the relationship between the two models. In particular, we present two relatively simple translations from λY-terms to CPDA using Krivine machines as an intermediate step. The latter are general machines for describing computation of the weak head normal form in the λ-calculus. They provide the notions of closure and environment that facilitate reasoning about computation.

When a property needs to be checked against an unknown or very complex system, classical exploration techniques like model-checking are not applicable anymore. Sometimes a~monitor can be used, that checks a given property on the underlying system at runtime. A monitor for a property $L$ is a deterministic finite automaton $M_L$ that after each finite execution tells whether (1) every possible extension of the execution is in $L$, or (2) every possible extension is in the complement of $L$, or neither (1) nor (2) holds. Moreover, $L$ being monitorable means that it is always possible that in some future the monitor reaches (1) or (2). Classical examples for monitorable properties are safety and cosafety properties. On the other hand, deterministic liveness properties like "infinitely many $a$'s" are not monitorable. We discuss various monitor constructions with a focus on deterministic omega-regular languages. We locate a proper subclass of of deterministic omega-regular languages but also strictly large than the subclass of languages which are deterministic and codeterministic, and for this subclass there exists a canonical monitor which also accepts the language itself. We also address the problem to decide monitorability in comparison with deciding liveness. The state of the art is as follows. Given a B\"uchi automaton, it is PSPACE-complete to decide liveness or monitorability. Given an LTL formula, deciding liveness becomes EXPSPACE-complete, but the complexity to decide monitorability remains open.

We consider simply typed lambda-calculus with fixpoints as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as a potentially infinite tree of calls to built-in operations. Properties of such trees are properties of executions of programs and monadic second-order logic (MSOL) is well suited to express them. For a given MSOL property we show how to construct a finitary model recognizing it. In other words, the value of a lambda-term in the model determines if the tree that is the result of the execution of the term satisfies the property. The finiteness of the construction has as consequences many known results about the verification of higher-order programs in this framework.

The propositional μ-calculus (now more commonly known as the modal μ-calculus) was first published in 1983 by D. Kozen, although the system had been studied much earlier by J. de Bakker and D. Scott (unpublished notes, 1969). The system subsumes many popular propositional logics of programs, including linear temporal logic, computation tree logic CTL*, and propositional dynamic logic. Kozen proposed a deductive system whose chief rule of inference was a variant of the fixpoint induction rule of D. Park and conjectured it to be complete. During the decade after its introduction, this calculus attracted a great deal of attention within computer science circles. Despite the attention given to this calculus, it was not until this paper by Walukiewicz a dozen years later that the proof system was finally shown to be complete. In order to prove the completeness theorem, several technical innovations were developed. A full version of this paper appeared in Information and Computation in 2000.

In the past few years, more and more attention has been paid to the annoying difference between abstract algorithmic problems and their messy origins in the real world. While algorithms theory is highly developed for a large variety of clean, combinatorial optimization problems, their practical counterparts cannot always be solved by well understood theoretical methods, for a variety of reasons: Practical inputs suffer from uncertainties and inaccuracies, like noisy data, or algorithmic outputs cannot be realized exactly, due to physical inaccuracies. We aim at a better theoretical understanding of how to cope with uncertain input data for real problems. We propose a general approach that tends to lead to substantial algorithmic challenges and inefficiencies on the one hand, but promises on the other hand to deliver good results for practical problems as varied as robust trip planning in public transportation and robust de novo peptide sequencing in computational biology. This talk is about joint work with Katerina Böhmova, Joachim Buhmann, Matus Mihalak, Tobias Pröger, and Rasto Sramek. * A quote going back to Carveth Read, but incorrectly attributed to John Maynard Keynes after his death as “It is better to be roughly right than precisely wrong”. Towards Better Inapproximability Bounds for TSP: A Challenge of Global Dependencies