This paper describes how backward deterministic Büchi automata are defined, what their main features are, and how they can be applied to solve problems in temporal logic.

I was supposed to deliver one of the speeches at Wolfgang Thomas's retirement ceremony. Wolfgang had called me on the phone earlier and posed some questions about temporal logic, but I hadn't had good answers at the time. What I decided to do at the ceremony was to take up the conversation again and show how it could have evolved if only I had put more effort into answering his questions. Here is the imaginary conversation with Wolfgang. The contributions are (1) the first direct translation from counter-free omega-automata into future temporal formulas, (2) a definition of bimachines for omega-words, (3) a translation from arbitrary temporal formulas (including both, future and past operators) into counter-free omega-bimachines, and (4) an automata-based proof of separation: every arbitrary temporal formula is equivalent to a boolean combination of pure future, present, and pure past formulas when interpreted in omega-words.

Frontmatter, Table of Contents, Preface, Workshop Organization

We present a framework for obtaining effective characterizations of simple fragments of future temporal logic (LTL) with the natural numbers as time domain. The framework is based on prophetic automata (also known as complete unambiguous Büchi automata), which enjoy strong structural properties, in particular, they separate the “finitary fraction” of a regular language of infinite words from its “infinitary fraction” in a natural fashion. Within our framework, we provide characterizations of all natural fragments of temporal logic, where, in some cases, no effective characterization had been known previously, and give lower and upper bounds for their computational complexity. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Frontmatter, Foreword, Conference Organization, External Reviewers, Table of Contents

The paper considers several definitions of information flow security for intransitive policies from the point of view of the complexity of verifying whether a finite-state system is secure. The results are as follows. Checking (i) P-security (Goguen and Meseguer), (ii) IP-security (Haigh and Young), and (iii) TA-security (van der Meyden) are all in PTIME, while checking TO-security (van der Meyden) is undecidable. The most important ingredients in the proofs of the PTIME upper bounds are new characterizations of the respective security notions, which also enable the algorithms to return simple counterexamples demonstrating insecurity. Our results for IP-security improve a previous doubly exponential bound of Hadj-Alouane et al.

We prove secure a concrete and practical two-round authenticated message exchange protocol which reflects the authentication mechanisms for web services discussed in various standardization documents. The protocol consists of a single client request and a subsequent server response and works under the realistic assumptions that the responding server is long-lived, has bounded memory, and may be reset occasionally. The protocol is generic in the sense that it can be used to implement securely any service based on authenticated message exchange, because request and response can carry arbitrary payloads. Our security analysis is a computational analysis in the Bellare-Rogaway style and thus provides strong guarantees; it is novel from a technical point of view since we extend the Bellare-Rogaway framework by timestamps and payloads with signed parts.

Cody, Hazel, and Theo, two experienced Haskell programmers and an expert in automata theory, develop an elegant Haskell program for matching regular expressions: (i) the program is purely functional; (ii) it is overloaded over arbitrary semirings, which not only allows to solve the ordinary matching problem but also supports other applications like computing leftmost longest matchings or the number of matchings, all with a single algorithm; (iii) it is more powerful than other matchers, as it can be used for parsing every context-free language by taking advantage of laziness.

Research on the automatic analysis of cryptographic protocols has so far concentrated on reachability properties, such as secrecy and authentication. In this article, we prove that certain game-theoretic security properties, including balance for contract-signing protocols, can be decided in a Dolev-Yao style model with a bounded number of sessions. The decision algorithm that we develop is based on standard constraint-solving procedures, which, in the past, have successfully been employed in tools for reachability properties. Our result thus paves the way for extending these tools to deal with game-theoretic security properties.

We introduce (i) a general class of security protocols with private channel as cryptographic primitive and (ii) a probabilistic epistemic logic to express properties of security protocols. Our main theorem says that when a property expressed in our logic holds for an ideal protocol (where "ideal" means that the private channel hides everything), then it also holds when the private channel is implemented using an encryption scheme that guarantees perfect secrecy (in the sense of Shannon). Our class of protocols contains, for instance, an oblivious transfer protocol by Rivest and Chaum's solution to the dining cryptographers problem. In our logic we can express fundamental security properties of these protocols. The proof of the main theorem is based on a notion of refinement for probabilistic Kripke structures.

Planar spatial datasets can be modeled by closed semi-algebraic sets in the plane. We establish a characterization of the topological properties of such datasets expressible in the relational calculus with real polynomial constraints. The characterization is in the form of a query language that can only point that can only talk about points in the set and the “cones” around these points.

We give efficient algorithms, improving optimal known bounds, for computing a variety of simulation relations on the state space of a Büchi automaton. Our algorithms are derived via a unified and simple parity-game framework. This framework incorporates previously studied notions like fair and direct simulation, but also a new natural notion of simulation called delayed simulation, which we introduce for the purpose of state space reduction. We show that delayed simulation---unlike fair simulation---preserves the automaton language upon quotienting and allows substantially better state space reduction than direct simulation. Using our parity-game approach, which relies on an algorithm by Jurdziński, we give efficient algorithms for computing all of the above simulations. In particular, we obtain an O(mn 3 )-time and O(mn)-space algorithm for computing both the delayed and the fair simulation relations. The best prior algorithm for fair simulation requires time and space O(n 6 ). Our framework also allows one to compute bisimulations: we compute the fair bisimulation relation in O(mn 3 ) time and O(mn) space, whereas the best prior algorithm for fair bisimulation requires time and space O(n 10 ).

Closed semi-algebraic sets in the plane form a powerful model of planar spatial datasets. We establish a characterization of the topological properties of such datasets expressible in the relational calculus with real polynomial constraints. The characterization is in the form of a query language that can only talk about points in the set and the "cones" around these points.

We reveal an intimate connection between semidirect products of finite semigroups and substitution of formulas in linear temporal logic. We use this connection to obtain an algebraic characterization of the until hierarchy of linear temporal logic. (The kth level of that hierarchy is comprised of all temporal properties that are expressible by a formula of nesting depth k in the until operator.) Applying deep results from finite semigroup theory we are able to prove that each level of the until hierarchy is decidable. By means of Ehrenfeucht--Fraissé games, we extend the results from linear temporal logic over finite sequences to linear temporal logic over infinite sequences.

We show a property of strings is expressible in the two-variable fragment of fist-order logic if and only if it is expressible by both a Cs and a II2 sentence.We thereby establish:where UTL stands for the string properties expressible in the temporal logic with 'eventually in the future' and 'eventually in the past' as the only temporal operators and UL stands for the class of unambiguous languages.This enables us to show that the problem of determining whether or not a given temporal string property belongs to UTL is decidable (in exponential space), which settles a hitherto open problem.Our proof of Cs n II2 = F02 involves a new combina- torial characterization of these two classes and introduces a new method of playing Ehrenfeucht-Fraikse games to verify identities in semigroups.

We investigate the power of first-order logic with only two variables over /spl omega/-words and finite words, a logic denoted by FO/sup 2/. We prove that FO/sup 2/ can express precisely the same properties as linear temporal logic with only the unary temporal operators: "next", "previously", "sometime in the future", and "sometime in the past", a logic we denote by unary-TL. Moreover, our translation from FO/sup 2/ to unary-TL converts every FO/sup 2/ formula to an equivalent unary-TL formula that is at most exponentially larger, and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is optimal. While satisfiability for full linear temporal logic, as well as for unary-TL, is known to be PSPACE-complete, we prove that satisfiability for FO/sup 2/ is NEXP-complete, in sharp contrast to the fact that satisfiability for FO/sup 3/ has non-elementary computational complexity. Our NEXP time upper bound for FO/sup 2/ satisfiability has the advantage of being in terms of the quantifier depth of the input formula. It is obtained using a small model property for FO/sup 2/ of independent interest, namely: a satisfiable FO/sup 2/ formula has a model whose "size" is at most exponential in the quantifier depth of the formula. Using our translation from FO/sup 2/ to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.

We reveal an intimate connection between semidirect products of finite semigroups and substitution of formulas in linear temporal logic. We use this connection to obtain an algebraic characterization of the 'until' hierarchy of linear temporal logic; the k-th level of that hierarchy is comprised of all temporal properties that are expressible by a formula of nesting depth at most k in the 'until' operator. Applying deep results from finite semigroup theory we are able to prove that each level of the until hierarchy is decidable.

We prove there is a strict hierarchy of expressive power according to the Until depth of linear temporal logic (TL) formulas: for each k, there is a very natural property that is not expressible with k nestings of Until operators, regardless of the number of applications of other operators, but is expressible by a formula with Until depth k+1. Our proof uses a new Ehrenfeucht-Fraisse (EF) game designed specifically for TL. These properties can all be expressed in first-order logic with quantifier depth and size O(log k), and we use them to observe some interesting relationships between TL and first-order expressibility. We then use the EF game in a novel way to effectively characterize (1) the TL properties expressible without Until, as well as (2) those expressible without both Until and Next. By playing the game "on finite automata", we prove that the automata recognizing languages expressible in each of the two fragments have distinctive structural properties. The characterization for the first fragment was originally proved by Cohen, Perrin, and Pin (1993) using sophisticated semigroup-theoretic techniques. They asked whether such a characterization exists for the second fragment. The technique we develop is general and can potentially be applied in other contexts.