Selected Papers of the 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021)

Editors: Davide Bresolin, Pierre Ganty

This special issue features extended versions of papers presented at GandALF 2021, the Twelfth International Symposium on Games, Automata, Logics, and Formal Verification, held in Padua, Italy, from September 20 to 22, 2021.

The aim of the GandALF Symposium is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The symposium covers a broad spectrum of topics, from theoretical foundations to practical
applications, and encourages interdisciplinary exchange.

The papers included in this special issue underwent a rigorous two-stage review process. In the first stage, the GandALF program committee selected 19 papers out of 39 submissions. Following the conference, the authors of the seven best papers were invited to submit revised and extended versions of their work. We received three submissions from this group. Additionally, we invited our keynote speakers to contribute, resulting in one submission.

In the second stage, all submitted extended and invited papers were reviewed according to the high standards of LMCS. Each paper received two additional reviews to ensure quality.

We extend our gratitude to all the authors for their professional contributions and to the expert reviewers for their insightful feedback, which significantly enhanced the original submissions.

Davide Bresolin, Pierre Ganty
Guest Editors of the GandALF 2021 Special Issue

1. Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials

Grädel, Erich ; Lücking, Niels ; Naaf, Matthias.

This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in Büchi games. Semiring semantics generalizes the classical Boolean semantics by permitting multiple truth values from certain semirings. Evaluating the fixed-point formula that defines the winning region in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. This is well-understood for reachability games, where the winning region is definable as a least fixed point. The case of Büchi games is of special interest, not only due to their practical importance, but also because it is the simplest case where the fixed-point definition involves a genuine alternation of a greatest and a least fixed point. We show that, in a precise sense, semiring semantics provide information about all absorption-dominant strategies -- strategies that win with minimal effort, and we discuss how these relate to positional and the more general persistent strategies. This information enables applications such as game synthesis or determining minimal modifications to the game needed to change its outcome. Lastly, we discuss limitations of our approach and present questions that cannot be immediately answered by semiring semantics.

2. The addition of temporal neighborhood makes the logic of prefixes and sub-intervals EXPSPACE-complete

Bozzelli, L. ; Montanari, A. ; Peron, A. ; Sala, P..

A classic result by Stockmeyer gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably for formulas that make use of the so-called chop operator. Such an operator can indeed be interpreted as the inverse of the concatenation operation on regular languages, and this correspondence enables reductions between non-emptiness of star-free generalized regular expressions and satisfiability of formulas of the interval temporal logic of chop under the homogeneity assumption. In this paper, we study the complexity of the satisfiability problem for suitable weakenings of the chop interval temporal logic, that can be equivalently viewed as fragments of Halpern and Shoham interval logic. We first consider the logic $\mathsf{BD}_{hom}$ featuring modalities $B$, for \emph{begins}, corresponding to the prefix relation on pairs of intervals, and $D$, for \emph{during}, corresponding to the infix relation. The homogeneous models of $\mathsf{BD}_{hom}$ naturally correspond to languages defined by restricted forms of regular expressions, that use union, complementation, and the inverses of the prefix and infix relations. Such a fragment has been recently shown to be PSPACE-complete . In this paper, we study the extension $\mathsf{BD}_{hom}$ with the temporal neighborhood modality $A$ (corresponding to the Allen relation \emph{Meets}), and prove […]

3. A Nivat Theorem for Weighted Alternating Automata over Commutative Semirings

Grabolle, Gustav.

This paper connects the classes of weighted alternating finite automata (WAFA), weighted finite tree automata (WFTA), and polynomial automata (PA). First, we investigate the use of trees in the run semantics for weighted alternating automata and prove that the behavior of a weighted alternating automaton can be characterized as the composition of the behavior of a weighted finite tree automaton and a specific tree homomorphism, if weights are taken from a commutative semiring. Based on this, we give a Nivat-like characterization for weighted alternating automata. Moreover, we show that the class of series recognized by weighted alternating automata is closed under inverses of homomorphisms, but not under homomorphisms. Additionally, we give a logical characterization of weighted alternating automata, which uses weighted MSO logic for trees. Finally, we investigate the strong connection between weighted alternating automata and polynomial automata. We prove: A weighted language is recognized by a weighted alternating automaton iff its reversal in recognized by a polynomial automaton. Using the corresponding result for polynomial automata, we are able to prove that the ZERONESS problem for weighted alternating automata with weights taken from the rational numbers decidable.

4. FlexFringe: Modeling Software Behavior by Learning Probabilistic Automata

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.