Amir Pnueli

I&C Journal 2012 Journal Article

Low dimensional hybrid systems – decidable, undecidable, donʼt know

• Eugene Asarin
• Venkatesh P. Mysore
• Amir Pnueli
• Gerardo Schneider

Even though many attempts have been made to define the boundary between decidable and undecidable hybrid systems, the affair is far from being resolved. More and more low dimensional systems are being shown to be undecidable with respect to reachability, and many open problems in between are being discovered. In this paper, we present various two-dimensional hybrid systems for which the reachability problem is undecidable. We show their undecidability by simulating Minsky machines. Their proximity to the decidability frontier is understood by inspecting the most parsimonious constraints necessary to make reachability over these automata decidable. We also show that for other two-dimensional systems, the reachability question remains unanswered, by proving that it is as hard as the reachability problem for piecewise affine maps on the real line, which is a well known open problem.

TCS Journal 2005 Journal Article

A compositional approach to CTL * verification

• Yonit Kesten
• Amir Pnueli

The paper presents a compositional approach to the verification of CTL * properties over reactive systems. Both symbolic model-checking (SMC) and deductive verification are considered. Both methods are based on two decomposition principles. A general state formula is decomposed into basic state formulas which are CTL * formulas with no embedded path quantifiers. To deal with arbitrary basic state formulas, we introduce another reduction principle which replaces each basic path formula, i. e. , path formulas whose principal operator is temporal and which contain no embedded temporal operators or path quantifiers, by a newly introduced boolean variable which is added to the system. Thus, both the algorithmic and the deductive methods are based on two statification transformations which successively replace temporal formulas by assertions which contain no path quantifiers or temporal operators. Performing these decompositions repeatedly, we remain with basic assertional formulas, i. e. , formulas of the form E f p and A f p for some assertion p. In the model-checking method we present a single symbolic algorithm to verify both universal and existential basic assertional properties. In the deductive method we present a small set of proof rules and show that this set is sound and relatively complete for verifying universal and existential basic assertional properties over reactive systems. Together with two proof rules for the decompositions, we obtain a sound and relatively complete proof system for arbitrary CTL * properties. Interestingly, the deductive approach for CTL * presented here, offers a viable new approach to the deductive verification of arbitrary LTL formulas.

I&C Journal 2005 Journal Article

Bridging the gap between fair simulation and trace inclusion

• Yonit Kesten
• Nir Piterman
• Amir Pnueli

The paper considers the problem of checking abstraction between two finite-state fair discrete systems. In automata-theoretic terms this is trace inclusion between two nondeterministic Streett automata. We propose to reduce this problem to an algorithm for checking fair simulation between two generalized Büchi automata. For solving this question we present a new triply nested μ-calculus formula which can be implemented by symbolic methods. We then show that every trace inclusion of this type can be solved by fair simulation, provided we augment the concrete system (the contained automaton) by an appropriate ‘non-constraining’ automaton. This establishes that fair simulation offers a complete method for checking trace inclusion for finite-state systems. We illustrate the feasibility of the approach by algorithmically checking abstraction between finite state systems whose abstraction could only be verified by deductive methods up to now.

I&C Journal 2003 Journal Article

Erratum to “The small model property: how small can it be?” [Inform. Comput. 178 (2002) 279–293]

• Amir Pnueli
• Yoav Rodeh
• Ofer Strichman
• Michael Siegel

I&C Journal 2002 Journal Article

The Small Model Property: How Small Can It Be?

• Amir Pnueli
• Yoav Rodeh
• Ofer Strichman
• Michael Siegel

Efficient decision procedures for equality logic (quantifier-free predicate calculus+the equality sign) are of major importance when proving logical equivalence between systems. We introduce an efficient decision procedure for the theory of equality based on finite instantiations. The main idea is to analyze the structure of the formula and compute accordingly a small domain to each variable such that the formula is satisfiable iff it can be satisfied over these domains. We show how the problem of finding these small domains can be reduced to an interesting graph theoretic problem. This method enabled us to verify formulas containing hundreds of integer and floating point variables that could not be efficiently handled with previously known techniques.

I&C Journal 2000 Journal Article

Verification by Augmented Finitary Abstraction

• Yonit Kesten
• Amir Pnueli

The paper deals with the proof method of verification by finitary abstraction (VFA), which presents a feasible approach to the verification of the temporal properties of (potentially infinite-state) reactive systems. The method consists of a two-step process by which, in a first step, the system and its temporal specification are jointly abstracted into a finite-state system and a finite-state specification. The second step uses model checking to establish the validity of the abstracted property over the abstracted system. The VFA method can be considered a viable alternative to verification by temporal deduction which, up to now, has been the main method generally applicable for verification of infinite-state systems. The paper presents a general recipe for the joint abstraction, which is shown to be sound, where soundness means that validity over the abstract system implies validity over the concrete (original) system. To make the method applicable for the verification of liveness properties, pure abstraction is sometimes no longer adequate. We show that by augmenting the system by an appropriate (and standardly constructible) progress monitor, we obtain an augmented system, whose computations are essentially the same as the original system, and which may now be abstracted while preserving the desired liveness properties. We refer to the extended method as verification by augmented abstraction (VAA). We then proceed to show that the VAA method is sound and complete for proving all properties expressible by temporal logic (including both safety and liveness). Completeness establishes that whenever the property is valid, there exists a finitary abstraction which abstracts the system, augmented by an appropriate progress monitor, into a finite-state system which validated the abstracted property.

CSL Conference 1999 Conference Paper

Verifying Liveness by Augmented Abstraction

• Yonit Kesten
• Amir Pnueli

Abstract The paper deals with the proof method of verification by augmented finitary abstraction ( VAA ), which presents an effective approach to the verification of the temporal properties of (potentially infinitestate) reactive systems. The method consists of a two-step process by which, in a first step, the system and its temporal specification are combined an then abstracted into a finite-state Büchi automaton. The second step uses model checking to establish emptiness of the abstracted automaton. The ( VAA ) method can be considered as a viable alternative to verification by temporal deduction which, up to now, has been the main method shown to be complete for the verification of infinite-state systems. The paper presents a general recipe for the abstraction of Büchi automata which is shown to be sound, where soundness means that emptiness of the abstract automaton implies emptiness of the concrete (infinitestate) automaton. To make the method applicable for the verification of liveness properties, pure abstraction is sometimes no longer adequate. We show that by augmenting the system by an appropriate (and standardly constructible) progress monitor, we obtain an augmented system, whose computations are essentially the same as the original system, and which may now be abstracted while preserving the desired liveness properties. We then proceed to show that the ( VAA ) method is sound and complete for proving all properties expressible by temporal logic (including both safety and liveness). Completeness establishes that whenever an infinite-state Büchi automaton has no computations, there exists a finitary abstraction which abstracts the automaton, augmented by an appropriate progress monitor, into a finite-state Büchi automaton with no computations

MFCS Conference 1998 Invited Paper

Modularization and Abstraction: The Keys to Practical Formal Verification

• Yonit Kesten
• Amir Pnueli

Abstract In spite of the impressive progress in the development of the two main methods for formal verification of reactive systems — Model Checking (in particular symbolic) and Deductive Verification, they are still limited in their ability to handle large systems. It is generally recognized that the only way these methods can ever scale up is by the extensive use of abstraction and modularization, which breaks the task of verifying a large system into several smaller tasks of verifying simpler systems. In this methodological paper, we review the two main tools of compositionality and abstraction in the framework of linear temporal logic. We illustrate the application of these two methods for the reduction of an infinite-state system into a finite-state system that can then be verified using model checking. The modest technical contributions contained in this paper are a full formulation of abstraction when applied to a system with both weak and strong fairness requirements and to a general temporal formula, and a presentation of a compositional framework for shared variables and its application for forming network invariants.

FOCS Conference 1997 Invited Paper

Two Decades of Temporal Logic: Achievements and Challenges (Abstract)

• Amir Pnueli

TCS Journal 1995 Journal Article

Preface

• Amir Pnueli
• Joseph Sifakis

TCS Journal 1995 Journal Article

Reachability analysis of dynamical systems having piecewise-constant derivatives

• Eugene Asarin
• Oded Maler
• Amir Pnueli

In this paper we consider a class of hybrid systems, namely dynamical systems with piecewise-constant derivatives (PCD systems). Such systems consist of a partition of the Euclidean space into a finite set of polyhedral sets (regions). Within each region the dynamics is defined by a constant vector field, hence discrete transitions occur only on the boundaries between regions where the trajectories change their direction. With respect to such systems we investigate the reachability question: Given an effective description of the systems and of two polyhedral subsets P and Q of the state-space, is there a trajectory starting at some xϵP and reaching some point in Q? Our main results are a decision procedure for two-dimensional systems, and an undecidability result for three or more dimensions.

TCS Journal 1994 Journal Article

Proving partial order properties

• Doron Peled
• Amir Pnueli

A temporal verification method which is based upon partial order semantics of traces (Mazurkiewicz, 1987) is presented. The semantic model used here can express the distributed aspects of a program, e. g. properties such as serializability of database transactions, layering of a program, snapshots or the parallel execution of program segments. The proof rules are shown to be sound and relatively complete.

TCS Journal 1991 Journal Article

Completing the temporal picture

• Zohar Manna
• Amir Pnueli

The paper presents a relatively complete proof system for proving the validity of temporal properties of reactive programs. The presented proof system improves on previous temporal systems, in that it reduces the validity of program properties into pure assertional reasoning, not involving additional temporal reasoning. The proof system is based on the classification of temporal properties according to the Borel hierarchy, providing appropriate proof rules for the classes of safety, response, and reactivity properties.

MFCS Conference 1991 Invited Paper

On the Faithfulness of Formal Models

• Zohar Manna
• Amir Pnueli

Abstract The paper presents a critical examination of the way certain central aspects of concurrent programs are formally modeled. The main formal model examined is the operational model of fair transition system which represents concurrency by interleaving of actions considered atomic. Several questions concerning the faithfulness of this representation naturally arise. The paper considers some of these questions and, while presenting and analyzing some of the alternatives, attempts to justify the design decisions actually taken in the construction of the model.

FOCS Conference 1990 Conference Paper

Distributed Reactive Systems Are Hard to Synthesize

• Amir Pnueli
• Roni Rosner

The problem of synthesizing a finite-state distributed reactive system is considered. Given a distributed architecture A, which comprises several processors P/sub 1/, .. ., P/sub k/ and their interconnection scheme, and a propositional temporal specification phi, a solution to the synthesis problem consists of finite-state programs Pi /sub 1/, .. ., Pi /sub k/ (one for each processor), whose joint (synchronous) behavior maintains phi against all possible inputs from the environment. Such a solution is referred to as the realization of the specification phi over the architecture A. Specifically, it is shown that the problem of realizing a given propositional specification over a given architecture is undecidable, and it is nonelementarily decidable for the very restricted class of hierarchical architectures. An extensive characterization of architecture classes for which the realizability problem is elementarily decidable and of classes for which it is undecidable is given. >

FOCS Conference 1990 Conference Paper

Tight Bounds on the Complexity of Cascaded Decomposition of Automata

• Oded Maler
• Amir Pnueli

Exponential upper and lower bounds on the size of the cascaded (Krohn-Rhodes) decomposition of automata are given. These results are used to obtain elementary algorithms for various translations between automata and temporal logic, where the previously known translations were nonelementary. The relevance of the result is discussed. >

STOC Conference 1984 Conference Paper

Now You May Compose Temporal Logic Specifications

• Howard Barringer
• Ruurd Kuiper 0001
• Amir Pnueli

A compositional temporal logic proof system for the specification and verification of concurrent programs is presented. Versions of the system are developed for shared variables and communication based programming languages that include procedures.

TCS Journal 1984 Journal Article

Symmetric and economical solutions to the mutual exclusion problem in a distributed system

• Shimon Cohen
• Daniel Lehmann
• Amir Pnueli

The mutual exclusion problem in a distributed system, in which each process has a memory of its own, into which it has exclusive write privileges but from which others may read, is reconsidered. Symmetric solutions are looked for. It is shown that, though no such solution may be deterministic, there are probabilistic solutions. Different solutions are provided for two processes, and then a solution is proposed for any number of processes. The solutions offered are amenable to a formal proof of their correctness with a small effort. The solutions are correct even against a very well informed scheduler, unlike Rabin's probabilistic solution to the mutual exclusion problem in a centralized system. Some of the solutions are correct even against an evil scheduler the knows in advance the results of the future random draws, in sharp contrast with the algorithms of Lehmann and Rabin (1981). The solutions are economical: mutual exclusion between two processes may be achieved with variables capable of holding four different values (to be compared with Peterson and Fischer's three), mutual exclusion between n processes may be achieved with variables capable of holding ten different values (to be compared with Peterson and Fischer's fourteen). All solutions have been attained by careful reasoning and not by an exhaustive computer search: they exhibit general principles of design that may be useful in solving other similar problems.

STOC Conference 1983 Conference Paper

On the Extremely Fair Treatment of Probabilistic Algorithms

• Amir Pnueli

A proof system based on linear temporal logic for the qualitative verification of concurrent probabilistic programs is proposed. The concept of extreme fairness is introduced as an approximation to the notion of probabilistic executions. The proof system proposed is shown to be relatively complete with respect to validity over all extremely fair computations. The proof methodology is demonstrated by proving correctness of a new probabilistic algorithm for solving the mutual exclusion problem ([CLP]).

FOCS Conference 1981 Conference Paper

Propositional Dynamic Logic of Context-Free Programs

• David Harel
• Amir Pnueli
• Jonathan Stavi

The borderline between decidable and undecidable Propositional Dynamic Logic (PDL) is sought when iterative programs represented by regular expressions are augmented with increasingly more complex recursive programs represented by context-free languages. The results in this paper and its companion [HPS] indicate that this line is extremely close to the original regular PDL. The main result of the present paper is: The validity problem for PDL with additional programs αΔ(β)γΔ for regular α, β and γ, defined as Uiαi; β; γi, is Π11-complete. One of the results of [HPS] shows that the single program AΔ(B) AΔ for atomic A and B is actually sufficient for obtaining Π11- completeness. However, the proofs of this paper use different techniques which seem to be worthwhile in their own right.

TCS Journal 1981 Journal Article

The temporal semantics of concurrent programs

• Amir Pnueli

The formalism of Temporal Logic is suggested as an appropriate tool for formalizing the semantics of concurrent programs. A simple model of concurrent program is presented in which n processors are executing concurrent n disjoint programs under a shared memory environment. The semantics of such a program specifies the class of state sequences which are admissible as proper execution sequences under the program. The two main criteria which are required are 1. (a) Each state is obtained from its predecessor in the sequence by exactly one processor performing an atomic instruction in its process. 2. (b) Fair Scheduling: no processor which is infinitely often enabled will be indefinitely delayed. The basic elements of Temporal Logic are introduced in a particular logic framework DX. The usefulness of Temporal Logic notation in describing properties of concurrent programs is demonstrated. A construction is then given for assigning to a program P a temporal formula W(P) which is true on all proper execution sequences of P. In order to prove that a program P possesses a property R 1, one has only to prove the implications W(P)⊃R. An example of such proof is given. It is then demonstrated that specification of the Temporal character of the program's behavior is absolutely essential for the unambiguous understanding of the meaning of programming constructs.

FOCS Conference 1980 Conference Paper

A Linear History Semantics for Distributed Languages (Extended Abstract)

• Nissim Francez
• Daniel Lehmann 0001
• Amir Pnueli

A denotational semantics is given for a distributed language based on communication (CSP). The semantics uses linear sequences of communications to record computations; for any well formed program segment the semantics is a relation between attainable states and the communication sequences needed to attain these states. In binding two or more processes we match and merge the communication sequences assumed by each process to obtain a sequence and State of the combined process. The approach taken here is distinguished by relatively simple semantic domains and ordering.

STOC Conference 1977 Conference Paper

A Complete Axiomatic System for Proving Deductions about Recursive Programs

• David Harel
• Amir Pnueli
• Jonathan Stavi

TCS Journal 1977 Journal Article

A direct algorithm for checking equivalence of LL(k) grammars

• Tmima Olshansky
• Amir Pnueli

We deal with the problem of testing equivalence of two LL(k) grammars. The problem had been shown to be decidable for general k by Rosenkrantz and Stearns [2], who solved it by reduction into an equivalence problem for special DPDA's. In a paper by Korenjak and Hopcroft [1] the equivalence problem for LL(1) grammars is solved by a branching algorithm operating directly on the grammars. Our work presents a direct branching algorithm for the general LL(k) grammars equivalence problem.

FOCS Conference 1977 Conference Paper

The Temporal Logic of Programs

• Amir Pnueli

A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.

STOC Conference 1969 Conference Paper

Formalization of Properties of Recursively Defined Functions

• Zohar Manna
• Amir Pnueli