LICS

Game logic with sabotage (GL_s) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. GL_s can be used to model infinite sabotage games, in which ...

We propose a local, past-oriented fragment of propositional dynamic logic to reason about concurrent scenarios modelled as Mazurkiewicz traces, and prove it to be expressively complete with respect to regular trace languages. Because of locality, ...

I introduce the falsifier calculus, a new deep-inference proof system for first-order predicate logic in the language of Hilbert's epsilon-calculus. It uses a new inference rule, the falsifier rule, to introduce epsilon-terms into a proof, distinct from ...

Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic ...

A fundamental issue in the λ-calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name λ-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in ...

Turn-based discounted-sum games are two-player zero-sum games played on finite directed graphs. The vertices of the graph are partitioned between player 1 and player 2. Plays are infinite walks on the graph where the next vertex is decided by a player ...

Vector addition system with states (VASS) is a popular model for the verification of concurrent systems. VASS consists of finitely many control states and a set of counters which can be incremented and decremented, but not tested for zero. VASS is a ...

We present a template for the Promise Constraint Satisfaction Problem (PCSP) which is NP-hard but does not satisfy the current state-of-the-art hardness condition [ACMTCT'21]. We introduce a new "injective" condition based on the smooth version of the ...

This paper presents the Relational Machine Calculus (RMC): a simple, foundational model of first-order relational programming. The RMC originates from the Functional Machine Calculus (FMC), which generalizes the lambda-calculus and its standard call-by-...

Following the success of the so-called algebraic approach to the study of decision constraint satisfaction problems (CSPs), exact optimization of valued CSPs, and most recently promise CSPs, we propose an algebraic framework for valued promise CSPs.

To ...

We investigate the decidability of the monadic second-order (MSO) theory of the structure (N; <, P₁,…,P_k), for various unary predicates P₁,…,P_k ⊆ N. We focus in particular on 'arithmetic' predicates arising in the study of linear recurrence sequences, ...

An "element-free" probability distribution is what remains of a probability distribution after we forget the elements to which the probabilities were assigned. These objects naturally arise in Bayesian statistics, in situations where elements are used as ...

Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability was shown ...

Valued constraint satisfaction problems (VCSPs) constitute a large class of computational optimisation problems. It was shown recently that, over finite domains, every VCSP is in P or NP-complete, depending on the admitted cost functions. In this article,...

A nondeterministic discounted-sum automaton (NDA) values a run by the discounted sum of the visited transition weights. That is, the weight in the i-th position of a run of a λ-NDA is divided by λⁱ, for a fixed discount factor λ > 1. This allows to model ...

We introduce the calculus of neo-Peircean relations, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. The axioms are obtained by combining ...

We study the computational complexity of solving stochastic games with mean-payoff objectives. Instead of identifying special classes in which simple strategies are sufficient to play ∈-optimally, or form ∈-Nash equilibria, we consider general partial-...

We show that restricting the elimination principle of the natural numbers type in Martin-Löf Type Theory (MLTT) to a universe of types not containing ####II-types ensures that all definable functions are primitive recursive. This extends the concept of ...

We consider contextual equivalence in an ML-like language, where contexts have access to both general references and continuations. We show that in a finitary setting, i.e. when the base types are finite and there is no recursion, the problem is ...

Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form ####Sⁿ = ####Sⁿ. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres,...

In the context of two-player games over graphs, a language L is called positional if, in all games using L as winning objective, the protagonist can play optimally using positional strategies, that is, strategies that do not depend on the history of the ...

We show that the problem of whether a given PCTL formula has a finite model is undecidable. The undecidability result holds even for formulae of the form [EQUATION] where the validity of ϕ₁, ϕ₂ depends only on the states reachable in at most two ...

Information-processing tasks modelled by homomorphisms between relational structures can witness quantum advantage when entanglement is used as a computational resource. We prove that the occurrence of quantum advantage is determined by the same type of ...

The 1-in-3 and Not-All-Eqal satisfiability problems for Boolean CNF formulas are two well-known NP-hard problems. In contrast, the promise 1-in-3 vs. Not-All-Eqal problem can be solved in polynomial time. In the present work, we investigate this ...

Indexed languages are a classical notion in formal language theory. As the language equivalent of second-order pushdown automata, they have received considerable attention in higher-order model checking. Unfortunately, counting properties are notoriously ...

Drawing inspiration from linear logic, quantitative semantics aim at representing quantitative information about programs and their executions: they include the relational model and its numerous extensions, game semantics, and syntactic approaches such ...

We introduce the first minimal and complete equational theory for quantum circuits. Hence, we show that any true equation on quantum circuits can be derived from simple rules, all of them being standard except a novel but intuitive one which states that ...

Markov's principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ⁰₁ propositions (i.e. existential quantification over a decidable predicate on N) are stable under double negation. However, there are various non-equivalent ...

We study the use of local consistency methods as reductions between constraint satisfaction problems (CSPs), and promise version thereof, with the aim to classify these reductions in a similar way as the algebraic approach classifies gadget reductions ...

Right-linear (or left-linear) grammars are a well-known class of context-free grammars computing just the regular languages. They may naturally be written as expressions with least fixed points but with products restricted to letters as left arguments, ...