相关论文: B\"uchi Types for Infinite Traces and Liveness

We introduce a weight assignment logic for reasoning about quantitative languages of infinite words. This logic is an extension of the classical MSO logic and permits to describe quantitative properties of systems with multiple weight…

We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set of program traces using failure automata, finite-state…

We prove that $\omega$-regular languages accepted by B\"uchi or Muller automata satisfy an effective automata-theoretic version of the Baire property. Then we use this result to obtain a new effective property of rational functions over…

Altenbernd, Thomas and W\"ohrle have considered in [ATW02] acceptance of languages of infinite two-dimensional words (infinite pictures) by finite tiling systems, with the usual acceptance conditions, such as the B\"uchi and Muller ones,…

Alternating automata have been widely used to model and verify systems that handle data from finite domains, such as communication protocols or hardware. The main advantage of the alternating model of computation is that complementation is…

We introduce a novel technique to analyse unambiguous B\"uchi automata quantitatively, and apply this to the model checking problem. It is based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant…

In this note, we defend that the notion of algorithm as a set of execution traces is somewhat independent of the notion of abstract state machine. It can be reformulated in the more general framework of small step operational semantics.

Abu Radi and Kupferman (2019) demonstrated the efficient minimization of history-deterministic (transition-based) co-B\"uchi automata, building on the results of Kuperberg and Skrzypczak (2015). We give a congruence-based description of…

Probabilistic B\"uchi Automata (PBA) are randomized, finite state automata that process input strings of infinite length. Based on the threshold chosen for the acceptance probability, different classes of languages can be defined. In this…

Type-and-effect systems help the programmer to organize data and computational effects in a program. While for traditional type systems expressive variants with sophisticated inference algorithms have been developed and widely used in…

We present efficient algorithms to reduce the size of nondeterministic B\"uchi word automata (NBA) and nondeterministic finite word automata (NFA), while retaining their languages. Additionally, we describe methods to solve PSPACE-complete…

This paper constructs a finite state abstraction of a possibly continuous-time and infinite state model in two steps. First, a finite external signal space is added, generating a so called $\Phi$-dynamical system. Secondly, the strongest…

We study the strength of axioms needed to prove various results related to automata on infinite words and B\"uchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak…

We consider abstraction-based design of output-feedback controllers for dynamical systems with a finite set of inputs and outputs against specifications in linear-time temporal logic. The usual procedure for abstraction-based controller…

Traces and their extension called combined traces (comtraces) are two formal models used in the analysis and verification of concurrent systems. Both models are based on concepts originating in the theory of formal languages, and they are…

This paper proposes a new algorithm for the generation of unambiguous B\"uchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an…

This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We…

We prove the existence and computability of optimal strategies in weighted limit games, zero-sum infinite-duration games with a B\"uchi-style winning condition requiring to produce infinitely many play prefixes that satisfy a given regular…

We prove the existence and computability of optimal strategies in weighted limit games, zero-sum infinite-duration games with a B\"uchi-style winning condition requiring to produce infinitely many play prefixes that satisfy a given regular…

Programming benefits from a clear separation between pure, mathematical computation and impure, effectful interaction with the world. Existing approaches to enforce this separation include monads, type-and-effect systems, and capability…