Pierre Wolper

I&C Journal 2001 Journal Article

Module Checking

• Orna Kupferman
• Moshe Y Vardi
• Pierre Wolper

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct model checking of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is much harder than model checking for the branching-time paradigm. We prove that the problem of module checking is EXPTIME-complete for specifications in CTL and 2EXPTIME-complete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems.

TIME Conference 2001 Conference Paper

Representing Periodic Temporal Information with Automata

• Pierre Wolper

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.

LOPSTR Conference 1990 Conference Paper

Algorithms for Synthesizing Reactive Systems: A Perspective (Abstract)

• Pierre Wolper

Abstract Starting in the early 1980s, a number of algorithmic techniques have been proposed for synthesizing the synchronization kernel of reactive systems from high-level temporal logic specifications. These techniques are based on nontrivial results in logic and automata theory and appear to be quite powerful. Nevertheless, essentially none of this work has found its way to practical use. This paper reviews the main results from this area and tries to identify the main reasons that explain their nonexploitation.

TCS Journal 1987 Journal Article

The complementation problem for Büchi automata with applications to temporal logic

• A. Prasad Sistla
• Moshe Y. Vardi
• Pierre Wolper

The problem of complementing Büchi automata arises when developing decision procedures for temporal logics of programs. Unfortunately, previously known constructions for complementing Büchi automata involve a doubly exponential blow-up in the size of the automaton. We present a construction that involves only an exponential blow-up. We use this construction to prove a polynomial space upper bound for the propositional temporal logic of regular events and to prove a complexity hierarchy result for quantified propositional temporal logic.

STOC Conference 1986 Conference Paper

Reasoning about Fair Concurrent Programs

• Costas Courcoubetis
• Moshe Y. Vardi
• Pierre Wolper

STOC Conference 1984 Conference Paper

Automata Theoretic Techniques for Modal Logics of Programs (Extended Abstract)

• Moshe Y. Vardi
• Pierre Wolper

We present a new technique for obtaining decision procedures for modal logics of programs. The technique centers around a new class of finite automata on infinite trees for which the emptiness problem can be solved in polynomial time. The decision procedures then consist of constructing an automaton A f for a given formula f , such that A f accepts some tree if and only if f is satisfiable. We illustrate our technique by giving an exponential decision procedure for deterministic propositional dynamic logic and a variant of the μ-calculus of Kozen.

FOCS Conference 1983 Conference Paper

Reasoning about Infinite Computation Paths (Extended Abstract)

• Pierre Wolper
• Moshe Y. Vardi
• A. Prasad Sistla

We investigate extensions of temporal logic by finite automata on infinite words. There are three different types of acceptance conditions (finite, looping and repeating) that one can give for these finite automata. This gives rise to three different logics. It turns out, however. that these logics have the same expressive power but differ in the complexity of their decision problem. We also investigate the addition of alternation and show that it does not increase the complexity of the decision problem.

FOCS Conference 1981 Conference Paper

Temporal Logic Can Be More Expressive

• Pierre Wolper

We start by proving that some properties of sequences are not expressible in Temporal Logic though they are expressible using for instance regular expressions. Then, we show how Temporal Logic can be extended to express any such property definable by a right-linear grammar and hence a regular expression, Finally, we give a decision procedure and complete axiomatization for the extended Temporal Logic.