ABSTRACT. We present an overview of our recent project on automated program verification based on higher-order fixpoint logic HFL(Z), a higher-order logic equipped with fixpoint operators and integer arithmetic. Various problems for higher-order program verification can naturally be reduced to the validity checking problem for HFL(Z) formulas. Thus, an HFL(Z) validity checker can serve as a common backend for automated verification tools for higher-order programs. We explain why the HFL(Z) approach is preferable to other representative approaches to automated higher-order program verification, such as the one based on the model checking of higher-order recursion schemes. We also outline how an automated HFL(Z) validity checker can be constructed, and discuss the remaining challenges and future directions.

ABSTRACT. The Autonomous Data Language (AuDaLa) is a recently introduced programming language and is supported by an operational semantics. This work presents a new operational semantics for AuDaLa with relaxed memory consistency and incoherent memory, with the goal of allowing more compiler optimisations. We show that both semantics are equivalent under the absence of read/write conflicts. Furthermore, we translate our operational semantics into an axiomatic memory consistency model and show how the memory operations of our semantics can be mapped onto the NVIDIA PTX virtual ISA.

ABSTRACT. We develop automata-theoretic concepts for hedges, a mathematical model for XML documents. First, we define context-free grammars on hedges, and connect our formulation with existing definitions of regular hedge languages and hedge automata. We also extend regular automata, push-down automata, and push-down transducers to hedges, and verify that the well-known correspondences with language classes in the string case carry over to the hedge setting. Based on the theory, we introduce a tool TXtruct, which serves as a grammar validator and transformer for XML and text files.

ABSTRACT. We present a novel language-agnostic approach to test case generation from a logic program representation generated by an existing framework. This is nontrivial for two reasons: since in such representation basic statements are usually composed into complex formulas, the trace enumerator cannot distill statements that are yet to be covered, and since the formulas obtained this way are more complex, then satisfiability checks are costlier and their number has to be kept low. Our approach performs an accelerated trace enumeration exploiting the program structure on the go. Our new implementation on top of the Horntinuum test case generator calls an SMT solver incrementally to achieve a significant performance increase. Furthermore, it has found many new test cases in public benchmarks that state-of-the-art did not find.

ABSTRACT. A {\em history deterministic\/} (HD) automaton can successfully resolve its nondeterministic choices in a way that only depends on the past. Formally, an HD automaton has a strategy that maps each finite word to the transition to be taken after the word is read, and following this strategy results in accepting all the words in the language of the automaton. HD automata can replace deterministic automata in several applications, most notably reactive synthesis, and they attract a lot of interest in the research community.

In 2015, Kuperberg and Skrzypczak proved that an HD B\"uchi automaton $\A$ can be determinized with a quadratic blow-up in the state space. The suggested construction also implicitly induces an HD co-B\"uchi automaton of linear size that complements $\A$. The construction is based on a series of transformations on an HD strategy for $\A$, which involves two drawbacks. First, the construction is conceptually hard to understand. Second, since the state space of the HD strategy is exponential, so is the runtime of a procedure implementing the construction.

In this paper, we describe a direct complementation procedure for HD B\"uchi automata. We believe that our procedure is easier to understand, as it is based on removal of transitions from $\A$ itself, which can be done in polynomial time. It results in an HD B\"uchi automaton equivalent to $\A$ on top of which we define a complementing HD co-B\"uchi automaton of linear size. A deterministic equivalent automaton of size quadratic in $\A$ can then be defined in polynomial time too. We also prove a quadratic lower bound on the size of an HD strategy for HD-NBWs.

We believe that our results contribute not only to efficient complementation and determinization constructions for HD B\"uchi automata, but also to better understanding of history determinism.

ABSTRACT. This paper provides the first decremental algorithm for fair Büchi games. It efficiently recalculates the winning region under the deletion of \emph{live} edges in the underlying game graph. Our algorithm addresses the unique challenges posed by fair Büchi games such as exponential-memory strategies and the non-monotonicity of the winning region under edge deletion. This prevents a straight forward extension of dynamic algorithms from (normal) Büchi games, in particular Jurdziński's small progress measures, on which these algorithms rely. The main contribution of this paper is the definition of a specialized (one-digit) progress measure for fair Büchi games and its correctness proof. We further derive a decremental algorithm for fair Büchi games using a fixed-point calculation entailed by this progress measure. We show that the (non-optimized) prototype implementation of our decremental algorithm outperforms an (optimized) fair Büchi game solver on a large class of benchmarks. By this, our work not only expands the scope of dynamic algorithms but also underscores the benefit of tailored solutions for specific game structures such as fair Büchi games.

ABSTRACT. Games with multiple objectives arise naturally in synthesis of reactive systems. We study {\em games with weighted multiple objectives}. The winning objective in such games consists of a set $\alpha$ of underlying objectives, and a weight function $w: 2^\alpha \rightarrow \Nat$ that maps each subset $S$ of $\alpha$ to a reward earned when exactly all the objectives in $S$ are satisfied. The goal of a player may be to maximize or minimize the reward. As a special case, we obtain games where the goal is to maximize or minimize the number of satisfied objectives, and in particular satisfy them all (a.k.a. generalized conditions). A weight function allows for a much richer reference to the underlying objectives: prioritizing them, referring to desired and less desired combinations, and addressing settings where we cannot expect all sub-specifications to be satisfied together.

We focus on settings where the underlying objectives are all {\em \buchi}, {\em co-\buchi}, {\em reachability}, or {\em avoid} objectives, and the weight function is non-decreasing (a.k.a. {\em free disposal}). For each of the induced classes (that is, type of underlying condition, type of optimization, and type of weight function), we solve the problem of deciding the game and analyze its tight complexity. We also study the tight memory requirements for each of the players. Finally, we consider general weight functions, which make the setting similar to the one of Boolean \muller objectives.

ABSTRACT. We present WhyMon, a runtime monitoring tool that produces explanations as verdicts. Receiving as input a metric first-order temporal logic (MFOTL) formula and a stream prefix of time-stamped data-carrying events, WhyMon incrementally outputs explanations that describe why each variable assignment satisfies or violates the formula. The tool includes a graphical user interface that facilitates the exploration and understanding of these explanations. Additionally, it incorporates a formally verified checker that can certify the explanations. In this tool paper, we describe WhyMon’s architecture and its command line and interactive user interfaces, and demonstrate its usefulness in a case study.

ABSTRACT. Learning automata by queries is a long-studied area initiated by Angluin in 1987 with the introduction of the $L^*$ algorithm to learn regular languages, with a large body of work afterwards on many different variations and generalizations of DFAs. Recently, Chase and Freitag introduced a novel approach to proving query learning bounds by computing combinatorial complexity measures for the classes in question, which they applied to the setting of DFAs to obtain qualitatively different results compared to the $L^*$ algorithm. Using this approach, we prove new query learning bounds for two generalizations of DFAs. The first setting is that of advice DFAs, which are DFAs augmented with an advice string that informs the DFA's transition behavior at each step. For advice DFAs, we give the first known upper bounds for query complexity. The second setting is that of nominal DFAs, which generalize DFAs to infinite alphabets which admit some structure via symmetries. For nominal DFAs, we make qualitative improvements over prior results.

ABSTRACT. This paper proposes a Graph Neural Network-guided algorithm for solving word equations, based on Nielsen transformation for splitting string equations. The algorithm iteratively rewrites the first terms of each side of an equation to form a tree-like search space. The choice of path at each split point of the tree significantly impacts solving time, motivating the use of Graph Neural Networks (GNNs) for efficient split decision-making. Therefore, the split decision is encoded as a multi-classification task and five graph representations of word equations are introduced to encode their structural information for GNNs. The algorithm is implemented as a solver named DragonLi. Experiments are conducted on artificial and real-world benchmarks. The algorithm performs particularly well on satisfiable problems. For single-word equations, DragonLi can solve significantly more problems than well-established string solvers. For the conjunction of multiple-word equations, DragonLi is competitive with state-of-the-art string solvers.