2026-03-16
Frenkel, Hadar, Regaud, Gaëtan, Zimmermann, Martin, Frenkel, Hadar, Regaud, Gaëtan, Zimmermann, Martin
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is $Σ_1^2$-complete, and finite-state satisfiability and model-checking are equivalent to truth in second-order arithmetic. Finally, we also introduce closed-world semantics for second-order HyperLTL, where set quantification ranges only over subsets of the model, while set quantification in standard semantics ranges over arbitrary sets of traces. Here, satisfiability for the least fixed point fragment becomes $Σ_1^1$-complete, but all other results are unaffected.
DOI: 10.46298/lmcs-22(1:26)20262026-03-14
Capelli, Florent, Carmeli, Nofar, Irwin, Oliver, Salvati, Sylvain, Capelli, Florent, Carmeli, Nofar, Irwin, Oliver, Salvati, Sylvain
Given a conjunctive query $Q$ and a database $D$, a direct access to the answers of $Q$ over $D$ is the operation of returning, given an index $k$, the $k$-th answer for some order on its answers. While this problem is $\#\mathcal{P}$-hard in general with respect to combined complexity, many conjunctive queries have an underlying structure that allows for a direct access to their answers for some lexicographical ordering that takes polylogarithmic time in the size of the database after a polynomial time precomputation. Previous work has precisely characterised the tractable classes and given fine-grained lower bounds on the precomputation time needed depending on the structure of the query. In this paper, we generalise these tractability results to the case of signed conjunctive queries, that is, conjunctive queries that may contain negative atoms. Our technique is based on a class of circuits that can represent relational data. We first show that this class supports tractable direct access after a polynomial time preprocessing. We then give bounds on the size of the circuit needed to represent the answer set of signed conjunctive queries depending on their structure. Both results combined together allow us to prove the tractability of direct access for a large class of conjunctive queries. On the one hand, we recover the known tractable classes from the literature in the case of positive conjunctive queries. On the other hand, we generalise and unify known tractability results about negative conjunctive queries -- that is, queries having only negated atoms. In particular, we show that the class of $β$-acyclic negative conjunctive queries and the class of bounded nest set width negative conjunctive queries admit tractable direct access.
DOI: 10.46298/lmcs-22(1:24)20262026-03-10
Iosif, Radu, Zuleger, Florian, Iosif, Radu, Zuleger, Florian
We give a characterization of the sets of graphs that are both definable in Counting Monadic Second Order Logic (CMSO) and context-free, i.e., least solutions of Hyperedge-Replacement (HR) grammars introduced by Courcelle and Engelfriet. We prove the equivalence of these sets with: (a) recognizable sets (in the algebra of graphs with HR-operations) of bounded tree-width; we refine this condition further and show equivalence with recognizability in a finitely generated subalgebra of the HR-algebra of graphs; (b) parsable sets, for which there is a definable transduction from graphs to a set of derivation trees labelled by HR operations, such that the set of graphs is the image of the set of derivation trees under the canonical evaluation of the HR operations; (c) images of recognizable unranked sets of trees under a definable transduction, whose inverse is also definable. We rely on a novel connection between two seminal results, a logical characterization of context-free graph languages in terms of tree-to-graph definable transductions, by Courcelle and Engelfriet and a proof that an optimal-width tree decomposition of a graph can be built by an definable transduction, by Bojanczyk and Pilipczuk.
DOI: 10.46298/lmcs-22(1:22)20262026-03-10
Lemay, Jean-Simon Pacaud, Lemay, Jean-Simon Pacaud
Differential linear categories provide the categorical semantics of the multiplicative and exponential fragments of Differential Linear Logic. Briefly, a differential linear category is a symmetric monoidal category that is enriched over commutative monoids (called additive enrichment) and has a monoidal coalgebra modality that is equipped with a codereliction. The codereliction is what captures the ability of differentiating non-linear proofs via linearization in Differential Linear Logic. The additive enrichment plays an important role since it allows one to express the famous Leibniz rule. However, the axioms of a codereliction can be expressed without any sums or zeros. Therefore, it is natural to ask if one can consider a possible non-additive enriched version of differential linear categories. In this paper, we show that even if a codereliction can technically be defined in a non-additive setting, it nevertheless induces an additive enrichment via bialgebra convolution. Thus, we obtain a novel characterization of a differential linear category as a symmetric monoidal category with a monoidal bialgebra modality equipped with a codereliction. Moreover, we also show that coderelictions are, in fact, unique. We also introduce monoidal Hopf coalgebra modalities and discuss how antipodes relate to enrichment over Abelian groups.
DOI: 10.46298/lmcs-22(1:23)20262026-03-10
Haase, Christoph, Mansutti, Alessio, Pouly, Amaury, Haase, Christoph, Mansutti, Alessio, Pouly, Amaury
This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability requirements. It enables deciding sentences of such theories with arbitrary existential quantification, conjunction and a fixed number of negation symbols in polynomial time. It was recently shown by Nguyen and Pak [SIAM J. Comput. 51(2): 1--31 (2022)] that an even more restricted such fragment of Presburger arithmetic (the first-order theory of the integers with addition and order) is NP-hard. In contrast, by application of our framework, we show that the fixed negation fragment of weak Presburger arithmetic, which drops the order relation from Presburger arithmetic in favour of equality, is decidable in polynomial time. We give two further examples of instantiations of our framework, showing polynomial-time decidability of the fixed negation fragments of weak linear real arithmetic and of the restriction of Presburger arithmetic in which each inequality contains at most one variable.
DOI: 10.46298/lmcs-22(1:21)20262026-03-06
Domini, Davide, Aguzzi, Gianluca, Esterle, Lukas, Viroli, Mirko, Domini, Davide, Aguzzi, Gianluca, Esterle, Lukas, Viroli, Mirko
In the last years, Federated learning (FL) has become a popular solution to train machine learning models in domains with high privacy concerns. However, FL scalability and performance face significant challenges in real-world deployments where data across devices are non-independently and identically distributed (non-IID). The heterogeneity in data distribution frequently arises from spatial distribution of devices, leading to degraded model performance in the absence of proper handling. Additionally, FL typical reliance on centralized architectures introduces bottlenecks and single-point-of-failure risks, particularly problematic at scale or in dynamic environments. To close this gap, we propose Field-Based Federated Learning (FBFL), a novel approach leveraging macroprogramming and field coordination to address these limitations through: (i) distributed spatial-based leader election for personalization to mitigate non-IID data challenges; and (ii) construction of a self-organizing, hierarchical architecture using advanced macroprogramming patterns. Moreover, FBFL not only overcomes the aforementioned limitations, but also enables the development of more specialized models tailored to the specific data distribution in each subregion. This paper formalizes FBFL and evaluates it extensively using MNIST, FashionMNIST, and Extended MNIST datasets. We demonstrate that, when operating under IID data conditions, FBFL performs comparably to the widely-used FedAvg algorithm. Furthermore, in challenging non-IID scenarios, FBFL not only outperforms FedAvg but also surpasses other state-of-the-art methods, namely FedProx and Scaffold, which have been specifically designed to address non-IID data distributions. Additionally, we showcase the resilience of FBFL's self-organizing hierarchical architecture against server failures.
DOI: 10.46298/lmcs-22(1:19)20262026-03-05
Dell'Erba, Daniele, Dumas, Arthur, Schewe, Sven, Dell'Erba, Daniele, Dumas, Arthur, Schewe, Sven
While discounted payoff games and classic games that reduce to them, like parity and mean-payoff games, are symmetric, their solutions are not. We have taken a fresh view on the properties that optimal solutions need to have, and devised a novel way to converge to them, which is entirely symmetric. We achieve this by building a constraint system that uses every edge to define an inequation, and update the objective function by taking a single outgoing edge for each vertex into account. These edges loosely represent strategies of both players, where the objective function intuitively asks to make the inequation to these edges sharp. In fact, where they are not sharp, there is an `error' represented by the difference between the two sides of the inequation, which is 0 where the inequation is sharp. Hence, the objective is to minimise the sum of these errors. For co-optimal strategies, and only for them, it can be achieved that all selected inequations are sharp or, equivalently, that the sum of these errors is zero. While no co-optimal strategies have been found, we step-wise improve the error by improving the solution for a given objective function or by improving the objective function for a given solution. This also challenges the gospel that methods for solving payoff games are either based on strategy improvement or on value iteration.
DOI: 10.46298/lmcs-22(1:17)20262026-02-27
Fritsche, Lars, Lauer, Alexander, Kratz, Maximilian, Schürr, Andy, Taentzer, Gabriele, Fritsche, Lars, Lauer, Alexander, Kratz, Maximilian, Schürr, Andy, Taentzer, Gabriele
When using graphs and graph transformations to model systems, consistency is an important concern. While consistency has primarily been viewed as a binary property, i.e., a graph is consistent or inconsistent with respect to a set of constraints, recent work has presented an approach to consistency as a graduated property. This allows living with inconsistencies for a while and repairing them when necessary. For repairing inconsistencies in a graph, we use graph transformation rules with so-called {\em impairment-indicating and repair-indicating application conditions} to understand how much repair gain certain rule applications would bring. Both types of conditions can be derived from given graph constraints. Our main theorem shows that the difference between the number of actual constraint violations before and after a graph transformation step can be characterised by the difference between the numbers of violated impairment-indicating and repair-indicating application conditions. This theory forms the basis for algorithms with look-ahead that rank graph transformations according to their potential for graph repair. An evaluation shows that graph repair can be well-supported by rules with these new types of application conditions in terms of effectiveness and scalability.
DOI: 10.46298/lmcs-22(1:10)20262026-02-27
Endrullis, Jörg, Overbeek, Roy, Endrullis, Jörg, Overbeek, Roy
We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we generalize the technique to other categories, and we allow for variations of DPO that occur in the literature.
DOI: 10.46298/lmcs-22(1:15)20262026-02-16
Ulus, Dogan, Ulus, Dogan
Metric Temporal Logic (MTL) is a popular formalism to specify temporal patterns with timing constraints over the behavior of cyber-physical systems with application areas ranging in property-based testing, robotics, optimization, and learning. This paper focuses on the unified construction of sequential networks from MTL specifications over discrete and dense time behaviors to provide an efficient and scalable online monitoring framework. Our core technique, future temporal marking, utilizes interval-based symbolic representations of future discrete and dense timelines. Building upon this, we develop efficient update and output functions for sequential network nodes for timed temporal operations. Finally, we extensively test and compare our proposed technique with existing approaches and runtime verification tools. Results highlight the performance and scalability advantages of our monitoring approach and sequential networks.
DOI: 10.46298/lmcs-22(1:12)20262026-01-09
Bezhanishvili, Nick, Bussi, Laura, Ciancia, Vincenzo, Gabelaia, David, Jibladze, Mamuka, Latella, Diego, Massink, Mieke, de Vink, Erik P., Bezhanishvili, Nick, Bussi, Laura, Ciancia, Vincenzo, Gabelaia, David, Jibladze, Mamuka, Latella, Diego, Massink, Mieke, de Vink, Erik P.
The work described in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking on polyhedral models using the logical language SLCS$η$, a weaker version of SLCS. In this work we show that the mapping from polyhedral models to cell poset models preserves and reflects SLCS$η$. We also propose weak simplicial bisimilarity on polyhedral models and weak $\pm$-bisimilarity on cell poset models, where by ``weak'' we mean that the relevant equivalence is coarser than the corresponding one for SLCS, leading to a greater reduction of the size of models and thus to more efficient model checking. We show that the proposed bisimilarities enjoy the Hennessy-Milner property, i.e. two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS$η$. Similarly, two cells are weakly $\pm$-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS$η$. Furthermore we present a model minimisation procedure and prove that it correctly computes the minimal model with respect to weak $\pm$-bisimilarity, i.e. with respect to logical equivalence of SLCS$η$. The procedure works via an encoding into LTSs and then exploits branching bisimilarity on those LTSs, exploiting the minimisation capabilities as included in the mCRL2 toolset. Various examples show the effectiveness of the approach.
DOI: 10.46298/lmcs-22(1:6)20262026-01-05
Gamard, Guilhem, Goubault-Larrecq, Aliénor, Guillon, Pierre, Ohlmann, Pierre, Perrot, Kévin, Theyssier, Guillaume, Gamard, Guilhem, Goubault-Larrecq, Aliénor, Guillon, Pierre, Ohlmann, Pierre, Perrot, Kévin, Theyssier, Guillaume
Our main result is a succinct counterpoint to Courcelle's meta-theorem as follows: every cw-nontrivial monadic second-order (MSO) property is either NP-hard or coNP-hard over graphs given by succinct representations. Succint representations are Boolean circuits computing the adjacency relation. Cw-nontrivial properties are those which have infinitely many models and infinitely many countermodels with bounded cliquewidth. Moreover, we explore what happens when the cw-nontriviality condition is dropped and show that, under a reasonable complexity assumption, the previous dichotomy fails, even for questions expressible in first-order logic.
DOI: 10.46298/lmcs-22(1:3)20262026-01-05
Ghica, Dan R., Kaye, George, Ghica, Dan R., Kaye, George
In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to its input. Such a structure is particularly interesting because any traced Cartesian (dataflow) category has an underlying traced comonoid structure. We show that certain subclasses of hypergraphs are fully complete for traced comonoid categories: that is to say, every term in such a category has a unique corresponding hypergraph up to isomorphism, and from every hypergraph with the desired properties, a unique term in the category can be retrieved up to the axioms of traced comonoid categories. We also show how the framework of double pushout rewriting (DPO) can be adapted for traced comonoid categories by characterising the valid pushout complements for rewriting in our setting. We conclude by presenting a case study in the form of recent work on an equational theory for sequential circuits: circuits built from primitive logic gates with delay and feedback. The graph rewriting framework allows for the definition of an operational semantics for sequential circuits.
DOI: 10.46298/lmcs-22(1:2)20262025-12-30
Almagor, Shaull, Dafni, Neta, Salgado, Ishai, Almagor, Shaull, Dafni, Neta, Salgado, Ishai
Jumping automata are finite automata that read their input in a non-sequential manner, by allowing a reading head to ``jump'' between positions on the input, consuming a permutation of the input word. We argue that allowing the head to jump should incur some cost. To this end, we propose four quantitative semantics for jumping automata, whereby the jumps of the head in an accepting run define the cost of the run. The four semantics correspond to different interpretations of jumps: the \emph{absolute distance} semantics counts the distance the head jumps, the \emph{reversal} semantics counts the number of times the head changes direction, the \emph{Hamming distance} measures the number of letter-swaps the run makes, and the \emph{maximum jump} semantics counts the maximal distance the head jumps in a single step, We study these measures, with the main focus being the \emph{boundedness problem}: given a jumping automaton, decide whether its (quantitative) language is bounded by some given number $k$. We establish the decidability and complexity for this problem under several variants.
DOI: 10.46298/lmcs-21(4:31)20252025-12-12
Quist, Arend-Jan, Laarman, Alfons, Quist, Arend-Jan, Laarman, Alfons
Pebble games are used to study space/time trade-offs. Recently, spooky pebble games were introduced to study classical space / quantum space / time trade-offs for simulation of classical circuits on quantum computers. In this paper, the spooky pebble game framework is applied for the first time to general circuits. Using this framework we prove an upper bound for quantum space in the spooky pebble game. We also prove that solving the spooky pebble game is PSPACE-complete. Moreover, we present a solver for the spooky pebble game based on satisfiability solvers combined with heuristic optimizers. This spooky pebble game solver was empirically evaluated by calculating optimal classical space / quantum space / time trade-offs. Within limited runtime, the solver could find a strategy reducing quantum space when classical space is taken into account, showing that the spooky pebble model is useful to reduce quantum space.
DOI: 10.46298/lmcs-21(4:29)20252025-12-01
Koprivec, Filip, Pretnar, Matija, Koprivec, Filip, Pretnar, Matija
Algebraic effect handlers are becoming an increasingly popular way of structuring effectful computations, and their performance is often a concern. One of the proposed approaches towards efficient compilation is tracking effect information through explicit subtyping coercions. However, in the presence of polymorphism, these coercions are compiled into additional arguments of compiled functions, incurring significant overhead. In this paper, we present a polymorphic effectful calculus, identify simplification phases needed to reduce the number of unnecessary constraints, and prove that they preserve semantics. In addition, we implement the simplification algorithm in the Eff language and evaluate its performance on a number of benchmarks. Though we do not prove the optimality of the presented simplifications, the results show that the algorithm eliminates all coercions, resulting in code as efficient as manually monomorphised one.
DOI: 10.46298/lmcs-21(4:25)20252025-11-07
Grochow, Joshua A., Levet, Michael, Grochow, Joshua A., Levet, Michael
In this paper, we explore the descriptive complexity theory of finite groups by examining the power of the second Ehrenfeucht--Fraïssé bijective pebble game in Hella's (Ann. Pure Appl. Log., 1989) hierarchy. This is a Spoiler--Duplicator game in which Spoiler can place up to two pebbles each round. While it trivially solves graph isomorphism, it may be nontrivial for finite groups, and other ternary relational structures. We first provide a novel generalization of Weisfeiler--Leman (WL) coloring, which we call 2-ary WL. We then show that 2-ary WL is equivalent to the second Ehrenfeucht--Fraïssé bijective pebble game in Hella's hierarchy. Our main result is that, in the pebble game characterization, only $O(1)$ pebbles and $O(1)$ rounds are sufficient to identify all groups without Abelian normal subgroups (a class of groups for which isomorphism testing is known to be in $\mathsf{P}$; Babai, Codenotti, & Qiao, ICALP 2012). We actually show that $7$ pebbles and $7$ rounds suffice. In particular, we show that within the first few rounds, Spoiler can force Duplicator to select an isomorphism between two such groups at each subsequent round. By Hella's results (ibid.), this is equivalent to saying that these groups are identified by formulas in first-order logic with generalized 2-ary quantifiers, using only $7$ variables and $7$ quantifier depth.
DOI: 10.46298/lmcs-21(4:20)20252025-11-04
Curzi, Gianluca, Das, Anupam, Curzi, Gianluca, Das, Anupam
We study the computational expressivity of proof systems with fixed point operators, within the 'proofs-as-programs' paradigm. We start with a calculus muLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, muLJ admits a standard extension to a 'circular' calculus CmuLJ. Our main result is that, perhaps surprisingly, both muLJ and CmuLJ represent the same first-order functions: those provably total in $Π^1_2$-$\mathsf{CA}_0$, a subsystem of second-order arithmetic beyond the 'big five' of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points. For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to $Π^1_2$-$\mathsf{CA}_0$ (due to Möllerfeld). For the upper bound we construct a novel computability model in order to give a totality argument for circular proofs with fixed points. In fact we formalise this argument itself within $Π^1_2$-$\mathsf{CA}_0$ in order to obtain the tight bounds we are after. Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.
DOI: 10.46298/lmcs-21(4:18)20252025-10-30
Takahashi, Yuta, Takahashi, Yuta
Rathjen proved that Aczel's constructive set theory $\mathbf{CZF}$ extended with inaccessible sets of all transfinite orders can be interpreted in Martin-Löf type theory $\mathbf{MLTT}$ extended with Setzer's Mahlo universe and another universe above it. In this paper we show that this interpretation can be carried out bottom-up without the universe above the Mahlo universe, provided we add an accessibility predicate instead. If we work in Martin-Löf type theory with extensional identity types the accessibility predicate can be defined in terms of $\mathrm{W}$-types. The main part of our interpretation has been formalised in the proof assistant Agda.
DOI: 10.46298/lmcs-21(4:16)20252025-10-27
Radi, Bader Abu, Kupferman, Orna, Leshkowitz, Ofer, Radi, Bader Abu, Kupferman, Orna, Leshkowitz, Ofer
We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton $\mathcal{A}$ is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to $\mathcal{A}$ by removing some of its transitions. Then, $\mathcal{A}$ is history deterministic (HD) if its nondeterministic choices can be resolved in a way that only depends on the past. Finally, $\mathcal{A}$ is semantically deterministic (SD) if different nondeterministic choices in $\mathcal{A}$ lead to equivalent states. Some applications of automata in formal methods require deterministic automata, yet in fact can use automata with some level of nondeterminism. For example, DBP automata are useful in the analysis of online algorithms, and HD automata are useful in synthesis and control. For automata on finite words, the three levels in the hierarchy coincide. We study the hierarchy for Büchi, co-Büchi, and weak automata on infinite words. We show that the hierarchy is strict, study the expressive power of the different levels in it, as well as the complexity of deciding the membership of a language in a given level. Finally, we describe a probability-based analysis of the hierarchy, which relates the level of nondeterminism with the probability that a random run on a word in the language is accepting. We relate the latter to nondeterministic automata that can be used when reasoning about probabilistic systems.
DOI: 10.46298/lmcs-21(4:13)20252025-10-27
Geuvers, Herman, Golov, Komi, Geuvers, Herman, Golov, Komi
Labelled transitions systems can be studied in terms of modal logic and in terms of bisimulation. These two notions are connected by Hennessy-Milner theorems, that show that two states are bisimilar precisely when they satisfy the same modal logic formulas. Recently, apartness has been studied as a dual to bisimulation, which also gives rise to a dual version of the Hennessy-Milner theorem: two states are apart precisely when there is a modal formula that distinguishes them. In this paper, we introduce "directed" versions of Hennessy-Milner theorems that characterize when the theory of one state is included in the other. For this we introduce "positive modal logics" that only allow a limited use of negation. Furthermore, we introduce directed notions of bisimulation and apartness, and then show that, for this positive modal logic, the theory of $s$ is included in the theory of $t$ precisely when $s$ is directed bisimilar to $t$. Or, in terms of apartness, we show that $s$ is directed apart from $t$ precisely when the theory of $s$ is not included in the theory of $t$. From the directed version of the Hennessy-Milner theorem, the original result follows. In particular, we study the case of branching bisimulation and Hennessy-Milner Logic with Until (HMLU) as a modal logic. We introduce "directed branching bisimulation" (and directed branching apartness) and "Positive Hennessy-Milner Logic with Until" (PHMLU) and we show the directed version of the Hennessy-Milner theorems. In the process, we show that every HMLU formula is equivalent to a Boolean combination of Positive HMLU formulas, which is a very non-trivial result. This gives rise to a sublogic of HMLU that is equally expressive but easier to reason about.
DOI: 10.46298/lmcs-21(4:14)20252025-10-17
Rauh, Andreas, Lahme, Marit, Rohou, Simon, Jaulin, Luc, Dinh, Thach Ngoc, Raissi, Tarek, Fnadi, Mohamed, Rauh, Andreas, Lahme, Marit, Rohou, Simon, Jaulin, Luc, Dinh, Thach Ngoc, Raissi, Tarek, Fnadi, Mohamed
Control and state estimation procedures need to be robust against imprecisely known parameters, uncertainty in initial conditions, and external disturbances. Interval methods and other set-based techniques form the basis for the implementation of powerful approaches that can be used to identify parameters of dynamic system models in the presence of the aforementioned types of uncertainty. Moreover, they are applicable to a verified feasibility and stability analysis of controllers and state estimators. In addition to these approaches which are typically used offline for analysis of system models designed with classical floating point procedures, interval and set-based methods have also been developed in recent years, which allow to directly solve the associated design tasks and to implement reliable techniques that are applicable online, i.e., during system operation. The latter approaches include set-based model predictive control, online parameter adaptation techniques for nonlinear variable-structure and backstepping controllers, interval observers, and fault diagnosis techniques. This paper provides an overview of the methodological background and reviews numerous practical applications for which interval and other set-valued approaches have been employed successfully.
DOI: 10.46298/lmcs-21(4:11)20252025-10-15
Baader, Franz, Giesl, Jürgen, Baader, Franz, Giesl, Jürgen
Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system $R$, a term $s$, and a natural number $n$, decide whether there is a term $t$ of size $\leq n$ reachable from $s$ using the rules of $R$. We investigate the complexity of this problem depending on how termination of $R$ can be established. We show that the problem is in general NP-complete for length-reducing term rewriting systems. Its complexity increases to N2ExpTime-complete (NExpTime-complete) if termination is proved using a (linear) polynomial order and to PSpace-complete for systems whose termination can be shown using a restricted class of Knuth-Bendix orders. Confluence reduces the complexity to P for the length-reducing case, but has no effect on the worst-case complexity in the other two cases. Finally, we consider the large term reachability problem, a variant of the problem where we are interested in reachability of a term of size $\geq n$. It turns out that this seemingly innocuous modification in some cases changes the complexity of the problem, which may also become dependent on whether the number $n$ is is represented in unary or binary encoding, whereas this makes no difference for the complexity of the small term reachability problem.
DOI: 10.46298/lmcs-21(4:8)20252025-10-08
Kurucz, Agi, Wolter, Frank, Zakharyaschev, Michael, Kurucz, Agi, Wolter, Frank, Zakharyaschev, Michael
None of the first-order modal logics between $\mathsf{K}$ and $\mathsf{S5}$ under the constant domain semantics enjoys Craig interpolation or projective Beth definability, even in the language restricted to a single individual variable. It follows that the existence of a Craig interpolant for a given implication or of an explicit definition for a given predicate cannot be directly reduced to validity as in classical first-order and many other logics. Our concern here is the decidability and computational complexity of the interpolant and definition existence problems. We first consider two decidable fragments of first-order modal logic $\mathsf{S5}$: the one-variable fragment $\mathsf{Q^1S5}$ and its extension $\mathsf{S5}_{\mathcal{ALC}^u}$ that combines $\mathsf{S5}$ and the description logic$\mathcal{ALC}$ with the universal role. We prove that interpolant and definition existence in $\mathsf{Q^1S5}$ and $\mathsf{S5}_{\mathcal{ALC}^u}$ is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. These results transfer to the two-variable fragment $\mathsf{FO^2}$ of classical first-order logic without equality. We also show that interpolant and definition existence in the one-variable fragment $\mathsf{Q^1K}$ of first-order modal logic $\mathsf{K}$ is non-elementary decidable, while uniform interpolant existence is again undecidable.
DOI: 10.46298/lmcs-21(4:6)20252025-10-08
Møgelberg, Rasmus Ejlers, Zwart, Maaike, Møgelberg, Rasmus Ejlers, Zwart, Maaike
The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to combine the delay monad with the monads of these effects. Here we present a first systematic study of such combinations. We study both the coinductive delay monad and its guarded recursive cousin, giving concrete examples of combining these with well-known computational effects. We also provide general theorems stating which algebraic effects distribute over the delay monad, and which do not. Lastly, we salvage some of the impossible cases by considering distributive laws up to weak bisimilarity.
DOI: 10.46298/lmcs-21(4:5)20252025-10-02
Audrito, Giorgio, Casadei, Roberto, Damiani, Ferruccio, Torta, Gianluca, Viroli, Mirko, Audrito, Giorgio, Casadei, Roberto, Damiani, Ferruccio, Torta, Gianluca, Viroli, Mirko
Recent trends like the Internet of Things (IoT) suggest a vision of dense and multi-scale deployments of computing devices in nearly all kinds of environments. A prominent engineering challenge revolves around programming the collective adaptive behaviour of such computational ecosystems. This requires abstractions able to capture concepts like ensembles (dynamic groups of cooperating devices) and collective tasks (joint activities carried out by ensembles). In this work, we consider collections of devices interacting with neighbours and that execute in nearly-synchronised sense-compute-interact rounds, where the computation is given by a single program mapping sensing values and incoming messages to output and outcoming messages. To support programming whole computational collectives, we propose the abstraction of a distributed collective process, which can be used to define at once the ensemble formation logic and its collective task. We formalise the abstraction in the eXchange Calculus (XC), a core functional language based on neighbouring values (maps from neighbours to values) where state and interaction is handled through a single primitive, exchange, and provide a corresponding implementation in the FCPP language. Then, we exercise distributed collective processes using two case studies: multi-hop message propagation and distributed monitoring of spatial properties. Finally, we discuss the features of the abstraction and its suitability for different kinds of distributed computing applications.
DOI: 10.46298/lmcs-21(4:3)20252025-10-02
Kleest-Meißner, Sarah, Marasus, Jonas, Niewerth, Matthias, Kleest-Meißner, Sarah, Marasus, Jonas, Niewerth, Matthias
We describe a framework for maintaining forest algebra representations that are of logarithmic height for unranked trees. Such representations can be computed in O(n) time and updated in O(log(n)) time. The framework is of potential interest for data structures and algorithms for trees whose complexity depend on the depth of the tree (representation). We provide an exemplary application of the framework to the problem of efficiently enumerating answers to MSO-definable queries over trees which are subject to local updates. We exhibit an algorithm that uses an O(n) preprocessing phase and enumerates answers with O(log(n)) delay between them. When the tree is updated, the algorithm can avoid repeating expensive preprocessing and restart the enumeration phase within O(log(n)) time. Our algorithms and complexity results in the paper are presented in terms of node-selecting tree automata representing the MSO queries.
DOI: 10.46298/lmcs-21(4:2)20252025-09-24
Spengler, Stephan, Sil, Sanchari, Spengler, Stephan, Sil, Sanchari
We consider an extension of the classical Total Store Order (TSO) semantics by expanding it to turn-based 2-player safety games. During her turn, a player can select any of the communicating processes and perform its next transition. We consider different formulations of the safety game problem depending on whether one player or both of them transfer messages from the process buffers to the shared memory. We give the complete decidability picture for all the possible alternatives.
DOI: 10.46298/lmcs-21(3:30)20252025-09-24
Verwer, Sicco, Hammerschmidt, Christian, Verwer, Sicco, Hammerschmidt, Christian
We present the efficient implementations of probabilistic deterministic finite automaton learning methods available in FlexFringe. These implement well-known strategies for state-merging including several modifications to improve their performance in practice. We show experimentally that these algorithms obtain competitive results and significant improvements over a default implementation. We also demonstrate how to use FlexFringe to learn interpretable models from software logs and use these for anomaly detection. Although less interpretable, we show that learning smaller more convoluted models improves the performance of FlexFringe on anomaly detection, outperforming an existing solution based on neural nets.
DOI: 10.46298/lmcs-21(3:31)20252025-09-24
Rauzy, Emmanuel, Rauzy, Emmanuel
We revisit Dieter Spreen's notion of a representation associated to a numbered basis equipped with a strong inclusion relation. We show that by relaxing his requirements, we obtain different classically considered representations as subcases, including representations considered by Grubba, Weihrauch and Schröder. We show that the use of an appropriate strong inclusion relation guarantees that the representation associated to a computable metric space seen as a topological space always coincides with the Cauchy representation. We also show how the use of a formal inclusion relation guarantees that when defining multi-representations on a set and on one of its subsets, the obtained multi-representations will be compatible, i.e. inclusion will be a computable map. The proposed definitions are also more robust under change of equivalent bases.
DOI: 10.46298/lmcs-21(3:29)2025