Thomas Wilke

I&C Journal 2015 Journal Article

Profile trees for Büchi word automata, with application to determinization

• Seth Fogarty
• Orna Kupferman
• Moshe Y. Vardi
• Thomas Wilke

The determinization of Büchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Schewe, and others. Despite the proliferation of solutions, they are all essentially ad-hoc constructions, with little theory behind them other than proofs of correctness. Since Safra, all optimal constructions employ trees as states of the deterministic automaton, and transitions between states are defined operationally over these trees. The operational nature of these constructions complicates understanding, implementing, and reasoning about them, and should be contrasted with complementation, where a solid theory in terms of automata run dags underlies modern constructions. In 2010, we described a profile-based approach to Büchi complementation, where a profile is simply the history of visits to accepting states. We developed a structural theory of profiles and used it to describe a complementation construction that is deterministic in the limit. Here we extend the theory of profiles to prove that every run dag contains a profile tree with at most a finite number of infinite branches. We then show that this property provides a theoretical grounding for a new determinization construction where macrostates are doubly preordered sets of states. In contrast to extant determinization constructions, transitions in the new construction are described declaratively rather than operationally.

MFCS Conference 2013 Conference Paper

Noninterference with Local Policies

• Sebastian Eggert
• Henning Schnoor
• Thomas Wilke

Abstract We develop a theory for state-based noninterference in a setting where different security policies—we call them local policies—apply in different parts of a given system. Our theory comprises appropriate security definitions, characterizations of these definitions, for instance in terms of unwindings, algorithms for analyzing the security of systems with local policies, and corresponding complexity results.

GandALF Workshop 2013 Workshop Paper

Profile Trees for Büchi Word Automata, with Application to Determinization

• Seth Fogarty
• Orna Kupferman
• Moshe Y. Vardi
• Thomas Wilke

The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Schewe, and others. Despite the proliferation of solutions, they are all essentially ad-hoc constructions, with little theory behind them other than proofs of correctness. Since Safra, all optimal constructions employ trees as states of the deterministic automaton, and transitions between states are defined operationally over these trees. The operational nature of these constructions complicates understanding, implementing, and reasoning about them, and should be contrasted with complementation, where a solid theory in terms of automata run DAGs underlies modern constructions. In 2010, we described a profile-based approach to Buchi complementation, where a profile is simply the history of visits to accepting states. We developed a structural theory of profiles and used it to describe a complementation construction that is deterministic in the limit. Here we extend the theory of profiles to prove that every run DAG contains a profile tree with at most a finite number of infinite branches. We then show that this property provides a theoretical grounding for a new determinization construction where macrostates are doubly preordered sets of states. In contrast to extant determinization constructions, transitions in the new construction are described declaratively rather than operationally.

CSL Conference 2011 Conference Paper

Unifying Büchi Complementation Constructions

• Seth Fogarty
• Orna Kupferman
• Moshe Y. Vardi
• Thomas Wilke

Complementation of Buechi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs are rejecting. The second is the slice-based approach of Kahler and Wilke. This approach tracks levels of "split trees" - run trees in which only essential information about the history of each run is maintained. While the slice-based construction is conceptually simple, the complementing automata it generates are exponentially larger than those of the recent rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding levels of split trees. In this work we reformulate the slice-based approach in terms of run DAGs and preorders over states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches. Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it generates. We are then able to employ the slice-based approach to provide a new odd ranking, called a retrospective ranking, that is different from the one provided by Kupferman and Vardi. This new ranking allows us to construct a deterministic-in-the-limit rank-based automaton with a highly restricted transition function. Further, by phrasing the slice-based approach in terms of ranks, our approach affords a simple symbolic encoding and achieves Schewe's tight bound.

TARK Conference 2007 Conference Paper

Preservation of epistemic properties in security protocol implementations

• Ron van der Meyden
• Thomas Wilke

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.

I&C Journal 2007 Journal Article

Transducer-based analysis of cryptographic protocols

• Ralf Küsters
• Thomas Wilke

Cryptographic protocols can be divided into (1) protocols where the protocol steps are simple from a computational point of view and can thus be modeled by simple means, for instance, by single rewrite rules—we call these protocols non-looping—and (2) protocols, such as group protocols, where the protocol steps are complex and typically involve an iterative or recursive computation—we call them recursive. While much is known on the decidability of security for non-looping protocols, only little is known for recursive protocols. In this paper, we prove decidability of security (with respect to the standard Dolev–Yao intruder) for a core class of recursive protocols and undecidability for several extensions. The key ingredient of our protocol model is specifically designed tree transducers which work over infinite signatures and have the ability to generate new constants (which allow us to mimic key generation). The decidability result is based on an automata-theoretic construction which involves a new notion of regularity, designed to work well with the infinite signatures we use.

TCS Journal 2005 Journal Article

Simulation relations for alternating Büchi automata

• Carsten Fritz
• Thomas Wilke

Quotienting by simulation equivalences is a well-established technique for reducing the size of nondeterministic Büchi automata. We adapt this technique to alternating Büchi automata. To this end we suggest two new quotients, namely minimax and semi-elective quotients, prove that they preserve the recognized languages, and show that computing them is not more difficult than computing quotients for nondeterministic Büchi automata. Our approach is game-theoretic; the proofs rely on a specifically tailored join operation for strategies in simulation games which is interesting in its own right. We explain the merits of our quotienting procedures with respect to converting alternating Büchi automata into nondeterministic ones.

LPAR Conference 2003 Conference Paper

Minimizing Automata on Infinite Words

• Thomas Wilke

Abstract Büchi automata (non-deterministic automata on infinite words with a simple acceptance condition) play a central rôle in model checking when properties are specified in temporal logic and state spaces are represented explicitly. Model checking then amounts to a graph search in a product of a transition system with a Büchi automaton that represents the specification. From a practical perspective it is therefore important to have procedures at hand which minimize the automata involved if possible. As computing–even approximating–minimum-state automata is PSPACE-hard, heuristics are applied. In the talk, a technique that is frequently used in current heuristics is presented: state-space reductions via simulation relations.

CSL Conference 2003 Conference Paper

Program Complexity of Dynamic LTL Model Checking

• Detlef Kähler
• Thomas Wilke

Abstract Using a recent result by Hesse we show that for any fixed linear-time temporal formula the dynamic model checking problem is in Dyn-TC 0, a complexity class introduced by Hesse, Immerman, Patnaik, containing all dynamic problems where the update after an operation has been performed can be computed by a DLOGTIME-uniform constant-depth threshold circuit. The operations permitted to modify the transition system to be verified include insertion and deletion of transitions and relabeling of states.

I&C Journal 2002 Journal Article

First-Order Logic with Two Variables and Unary Temporal Logic

• Kousha Etessami
• Moshe Y. Vardi
• Thomas Wilke

We investigate the power of first-order logic with only two variables over ω-words and finite words, a logic denoted by FO2. We prove that FO2 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 FO2 to unary-TL converts every FO2 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 essentially 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 FO2 is NEXP-complete, in sharp contrast to the fact that satisfiability for FO3 has nonelementary computational complexity. Our NEXP upper bound for FO2 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 FO2 of independent interest, namely, a satisfiable FO2 formula has a model whose size is at most exponential in the quantifier depth of the formula. Using our translation from FO2 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.

MFCS Conference 2001 Invited Paper

Linear Temporal Logic and Finite Semigroups

• Thomas Wilke

Abstract This paper gives a gentle introduction to the semigroup-theoretic approach to classifying discrete temporal properties and surveys the most important results.

I&C Journal 2000 Journal Article

An Until Hierarchy and Other Applications of an Ehrenfeucht–Fraı̈ssé Game for Temporal Logic

• Kousha Etessami
• Thomas Wilke

We prove there is a strict hierarchy of expressive power according to the Until depth of linear temporal logic (LTL) formulas: for each k, there is a natural property, based on quantitative fairness, 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–Fraı̈ssé (EF) game designed specifically for LTL. 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 LTL and first-order expressibility. We note that our Until hierarchy proof for LTL carries over to the branching time logics, CTL and CTL*. We then use the EF game in a novel way to effectively characterize (1) the LTL 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 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.

TCS Journal 1998 Journal Article

An algorithmic approach for checking closure properties of temporal logic specifications and ω-regular languages

• Doron Peled
• Thomas Wilke
• Pierre Wolper

In concurrency theory, there are several examples where the interleaved model of concurrency can distinguish between execution sequences which are not significantly different. One such example is sequences that differ from each other by stuttering, i. e. , the number of times a state can adjacently repeat. Another example is executions that differ only by the ordering of independently executed events. Considering these sequences as different is semantically rather meaningless. Nevertheless, specification languages that are based on interleaving semantics, such as linear temporal logic (LTL), can distinguish between them. This situation has led to several attempts to define languages that cannot distinguish between such equivalent sequences. In this paper, we take a different approach to this problem: we develop algorithms for deciding if a property cannot distinguish between equivalent sequences, i. e. , is closed under the equivalence relation. We focus on properties represented by regular languages, ω-regular languages, or prepositional LTL formulas and show that for such properties there is a wide class of equivalence relations for which determining closure is decidable, in fact is in PSPACE. Hence, checking the closure of a specification is no more difficult than checking satisfiability of a temporal formula. Among the closure properties we are able to handle, one finds trace closedness, stutter closedness and projective closedness, for all of which we are also able to prove a PSPACE lower bound. Being able to check that a property is closed under an equivalence relation has an immediate application in state-space exploration based verification. Indeed, the knowledge that the specification does not distinguish between equivalent execution sequences allows constructing a reduced state space where it is sufficient that at least one sequence per equivalence class is represented.

STOC Conference 1998 Conference Paper

Over Words, Two Variables Are as Powerful as One Quantifier Alternation

• Denis Thérien
• Thomas Wilke

TCS Journal 1996 Journal Article

An algebraic characterization of frontier testable tree languages

• Thomas Wilke

The class of frontier testable (i. e. , reverse definite) tree languages is characterized by a finite set of pseudoidentities for tree algebras, which are introduced here for this characterization. An efficient algorithm is presented that decides whether a given tree automaton recognizes a frontier testable tree language. The algorithm runs in time O(mn 3 + m 2 n 2), where m is the cardinality of the alphabet and n is the number of states of the automaton.

I&C Journal 1996 Journal Article

Computing the Rabin Index of a Regular Language of Infinite Words

• Thomas Wilke
• Haiseung Yoo

The Rabin index of a regular language of infinite words is the minimum number of accepting pairs used in any deterministic Rabin automaton recognizing this language. We show that the Rabin index of a language given by a Muller automaton withnstates andmaccepting sets is computable in timeO(m 2 nc) wherecis the cardinality of the alphabet.

FOCS Conference 1996 Conference Paper

Temporal Logic and Semidirect Products: An Effective Characterization of the Until Hierarchy

• Denis Thérien
• Thomas Wilke

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.