Anthony W. Lin

TACAS Conference 2026 Conference Paper

Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)

• Kilian Lichtner
• Pascal Bergsträßer
• Moses Ganardi
• Anthony W. Lin
• Georg Zetzsche

CSL Conference 2024 Conference Paper

Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games

• Julian Gutierrez 0001
• Anthony W. Lin
• Muhammad Najib
• Thomas Steeples
• Michael J. Wooldridge

Concurrent multi-player mean-payoff games are important models for systems of agents with individual, non-dichotomous preferences. Whilst these games have been extensively studied in terms of their equilibria in non-cooperative settings, this paper explores an alternative solution concept: the core from cooperative game theory. This concept is particularly relevant for cooperative AI systems, as it enables the modelling of cooperation among agents, even when their goals are not fully aligned. Our contribution is twofold. First, we provide a characterisation of the core using discrete geometry techniques and establish a necessary and sufficient condition for its non-emptiness. We then use the characterisation to prove the existence of polynomial witnesses in the core. Second, we use the existence of such witnesses to solve key decision problems in rational verification and provide tight complexity bounds for the problem of checking whether some/every equilibrium in a game satisfies a given LTL or GR(1) specification. Our approach is general and can be adapted to handle other specifications expressed in various fragments of LTL without incurring additional computational costs.

CSL Conference 2024 Conference Paper

Concurrent Stochastic Lossy Channel Games

• Daniel Stan
• Muhammad Najib
• Anthony W. Lin
• Parosh Aziz Abdulla

Concurrent stochastic games are an important formalism for the rational verification of probabilistic multi-agent systems, which involves verifying whether a temporal logic property is satisfied in some or all game-theoretic equilibria of such systems. In this work, we study the rational verification of probabilistic multi-agent systems where agents can cooperate by communicating over unbounded lossy channels. To model such systems, we present concurrent stochastic lossy channel games (CSLCG) and employ an equilibrium concept from cooperative game theory known as the core, which is the most fundamental and widely studied cooperative equilibrium concept. Our main contribution is twofold. First, we show that the rational verification problem is undecidable for systems whose agents have almost-sure LTL objectives. Second, we provide a decidable fragment of such a class of objectives that subsumes almost-sure reachability and safety. Our techniques involve reductions to solving infinite-state zero-sum games with conjunctions of qualitative objectives. To the best of our knowledge, our result represents the first decidability result on the rational verification of stochastic multi-agent systems on infinite arenas.

ICLR Conference 2024 Conference Paper

Logical Languages Accepted by Transformer Encoders with Hard Attention

• Pablo Barceló
• Alexander Kozachinskiy
• Anthony W. Lin
• Vladimir V. Podolskii

We contribute to the study of formal languages that can be recognized by transformer encoders. We focus on two self-attention mechanisms: (1) UHAT (Unique Hard Attention Transformers) and (2) AHAT (Average Hard Attention Transformers). UHAT encoders are known to recognize only languages inside the circuit complexity class ${\sf AC}^0$, i.e., accepted by a family of poly-sized and depth-bounded boolean circuits with unbounded fan-ins. On the other hand, AHAT encoders can recognize languages outside ${\sf AC}^0$), but their expressive power still lies within the bigger circuit complexity class ${\sf TC}^0$, i.e., ${\sf AC}^0$-circuits extended by majority gates. We first show a negative result that there is an ${\sf AC}^0$-language that cannot be recognized by an UHAT encoder. On the positive side, we show that UHAT encoders can recognize a rich fragment of ${\sf AC}^0$-languages, namely, all languages definable in first-order logic with arbitrary unary numerical predicates. This logic, includes, for example, all regular languages from ${\sf AC}^0$. We then show that AHAT encoders can recognize all languages of our logic even when we enrich it with counting terms. Using these results, we obtain a characterization of which counting properties are expressible by UHAT and AHAT, in relation to regular languages.

NeurIPS Conference 2024 Conference Paper

The Power of Hard Attention Transformers on Data Sequences: A formal language theoretic perspective

• Pascal Bergsträßer
• Chris Köcher
• Anthony W. Lin
• Georg Zetzsche

Formal language theory has recently been successfully employed to unravel the power of transformer encoders. This setting is primarily applicable in Natural Language Processing (NLP), as a token embedding function (where a bounded number of tokens is admitted) is first applied before feeding the input to the transformer. On certain kinds of data (e. g. time series), we want our transformers to be able to handle arbitrary input sequences of numbers (or tuples thereof) without a priori limiting the values of these numbers. In this paper, we initiate the study of the expressive power of transformer encoders on sequences of data (i. e. tuples of numbers). Our results indicate an increase in expressive power of hard attention transformers over data sequences, in stark contrast to the case of strings. In particular, we prove that Unique Hard Attention Transformers (UHAT) over inputs as data sequences no longer lie within the circuit complexity class AC0 (even without positional encodings), unlike the case of string inputs, but are still within the complexity class TC0 (even with positional encodings). Over strings, UHAT without positional encodings capture only regular languages. In contrast, we show that over data sequences UHAT can capture non-regular properties. Finally, we show that UHAT capture languages definable in an extension of linear temporal logic with unary numeric predicates and arithmetics.

KR Conference 2021 Conference Paper

Rational Verification for Probabilistic Systems

• Julian Gutierrez
• Lewis Hammond
• Anthony W. Lin
• Muhammad Najib
• Michael Wooldridge

Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational verification problem for both non-cooperative games and cooperative games in the qualitative probabilistic setting. In the former case, we consider LTL properties satisfied by the Nash equilibria of the game and in the latter case LTL properties satisfied by the core. In both cases, we show that the problem is 2EXPTIME-complete, thus not harder than the much simpler verification problem of model checking LTL properties of systems modelled as Markov decision processes (MDPs).

AAMAS Conference 2021 Conference Paper

Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems

• Daniel Stan
• Anthony W. Lin

We present a general framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In our framework, the number of agents or the amount of certain resources are parameterized (i. e. not known a priori), and the corresponding verification problem asks whether a given epistemic property is true regardless of the instantiation of the parameters. For example, in a muddy children puzzle, one could ask whether each child will eventually find out whether (s)he is muddy, regardless of the number of children. Our framework is regular model checking (RMC) -based, wherein synchronous finite-state automata (equivalently, monadic secondorder logic over words) are used to specify the systems. We propose an extension of public announcement logic as specification language. Of special interests is the addition of the so-called iterated public announcement operators, which are crucial for reasoning about knowledge in parameterized systems. Although the operators make the model checking problem undecidable, we show that this becomes decidable when an appropriate “disappearance relation” is given. Further, we show how Angluin’s L*-algorithm for learning finite automata can be applied to find a disappearance relation, which is guaranteed to terminate if it is regular. We have implemented the algorithm and apply this to such examples as the Muddy Children Puzzle, the Russian Card Problem, and Large Number Challenge.

TCS Journal 2018 Journal Article

Decidable models of integer-manipulating programs with recursive parallelism

• Matthew Hague
• Anthony W. Lin

We study safety verification for multithreaded programs with recursive parallelism (i. e. unbounded thread creation and recursion) as well as unbounded integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is state-extended ground-tree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since the model is Turing-complete, we propose a decidable underapproximation. First, using a restriction similar to context-bounding, we underapproximate the global control by a weak global control (i. e. DAGs possibly with self-loops), thereby limiting the number of synchronisations between different threads. Second, we bound the number of reversals between non-decrementing and non-incrementing modes of the counters. Under this restriction, we show that reachability becomes NP-complete. In fact, it is poly-time reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our decidable approximation strictly generalises known decidable models including (i) weakly-synchronised ground-tree rewrite systems, and (ii) synchronisation/reversal-bounded concurrent pushdown systems with counters. Finally, we show that, when equipped with reversal-bounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability.

LPAR Conference 2013 Conference Paper

Expressive Path Queries on Graphs with Data

• Pablo Barceló
• Gaëlle Fontaine
• Anthony W. Lin

Abstract Graph data models have recently become popular owing to their applications, e. g. , in social networks, semantic web. Typical navigational query languages over graph databases — such as Conjunctive Regular Path Queries (CRPQs) — cannot express relevant properties of the interaction between the underlying data and the topology. Two languages have been recently proposed to overcome this problem: walk logic (WL) and regular expressions with memory (REM). In this paper, we begin by investigating fundamental properties of WL and REM, i. e. , complexity of evaluation problems and expressive power. We first show that the data complexity of WL is nonelementary, which rules out its practicality. On the other hand, while REM has low data complexity, we point out that many natural data/topology properties of graphs expressible in WL cannot be expressed in REM. To this end, we propose register logic, an extension of REM, which we show to be able to express many natural graph properties expressible in WL, while at the same time preserving the elementariness of data complexity of REMs. It is also incomparable in expressive power against WL.

MFCS Conference 2012 Conference Paper

Weakly-Synchronized Ground Tree Rewriting - (with Applications to Verifying Multithreaded Programs)

• Anthony W. Lin

Abstract Ground tree rewrite systems (GTRS) are a well-known treeextension of prefix-rewrite systems on words (a. k. a. pushdown systems), where subtrees (instead of word prefixes) are rewritten. GTRS can model programs with unbounded recursion depth and thread-spawning, wherein the threads have a tree-shaped dependency graph. We consider the extension of GTRS with a finite (global) control unit for synchronizing among the active threads, a. k. a. state-extended GTRS (sGTRS). Since sGTRS is Turing-complete, we restrict the finite control unit to dags possibly with self-loops, a. k. a. weakly-synchronized GTRS (wGTRS). wGTRS can be regarded as a generalization of context-bounded analysis of multipushdown systems with dynamic thread spawning. We show that reachability, repeated reachability, and the complement of model checking deterministic LTL over weakly-synchronized GTRS (wGTRS) are NP-complete by a polynomial reduction to checking existential Presburger formulas, for which highly optimized solvers are available.

CSL Conference 2009 Conference Paper

Model Checking FO(R) over One-Counter Processes and beyond

• Anthony W. Lin

Abstract One-counter processes are pushdown processes over a singleton stack alphabet (plus a stack-bottom symbol). We study the problems of model checking asynchronous products of one-counter processes against 1) first-order logic FO (R) with reachability predicate, 2) the finite variable fragments FO k (R) (k ≥ 2) of FO (R), 3) EF-logic which is a fragment of FO 2 (R), and 4) all these logics extended with simple component-wise synchronizing predicates. We give a rather complete picture of their combined, expression, and data complexity. To this end, we show that these problems are poly-time reducible to two syntactic restrictions of Presburger Arithmetic, which are equi-expressive with first-order modulo counting theory of (ℕ, <), for which we give optimal quantifier elimination procedures. In particular, these problems are all shown to be in PSPACE, which is in sharp contrast to the closely related problem of model checking FO (R) over pushdown processes (with one stack) which has nonelementary complexity. Finally, we apply our proof method to give a fixed automatic (and so rational) graph whose modal logic theory has nonelementary complexity, solving a recently posed open question.

LPAR Conference 2008 Conference Paper

Recurrent Reachability Analysis in Regular Model Checking

• Anthony W. Lin
• Leonid Libkin

Abstract We consider the problem of recurrent reachability over infinite systems given by regular relations on words and trees, i. e, whether a given regular set of states can be reached infinitely often from a given initial state in the given transition system. Under the condition that the transitive closure of the transition relation is regular, we show that the problem is decidable, and the set of all initial states satisfying the property is regular. Moreover, our algorithm constructs an automaton for this set in polynomial time, assuming that a transducer of the transitive closure can be computed in poly-time. We then demonstrate that transition systems generated by pushdown systems, regular ground tree rewrite systems, and the well-known process algebra PA satisfy our condition and transducers for their transitive closures can be computed in poly-time. Our result also implies that model checking EF-logic extended by recurrent reachability predicate (EGF) over such systems is decidable.