Author name cluster

A. Pnueli

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

1 author row

TCS Journal 2001 Journal Article

Symbolic model checking with rich assertional languages

Y. Kesten
O. Maler
M. Marcus
A. Pnueli
E. Shahar

The paper shows that, by an appropriate choice of a rich assertional language, it is possible to extend the utility of symbolic model checking beyond the realm of BDD-represented finite-state systems into the domain of infinite-state systems, leading to a powerful technique for uniform verification of unbounded (parameterized) process networks. The main contributions of the paper are a formulation of a general framework for symbolic model checking of infinite-state systems, a demonstration that many individual examples of uniformly verified parameterized designs that appear in the literature are special cases of our general approach, verifying the correctness of the Futurebus+ design for all single-bus configurations, and extending the technique to tree architectures.

Details DOI

I&C Journal 1995 Journal Article

On the Learnability of Infinitary Regular Sets

O. Maler
A. Pnueli

In this paper we extend the automaton synthesis paradigm to infinitary languages, that is, to subsets of the set Σ ω of all infinite sequences over some alphabet Σ. Our main result is a polynomial algorithm for learning a sub-class of the ω-regular sets from membership queries and counter-examples based on the framework suggested by Angluin (Angluin, D. (1987), Inform. and Comput. 75, 87-106) for learning regular subsets of Σ*.

Details DOI

I&C Journal 1994 Journal Article

Temporal Proof Methodologies for Timed Transition-Systems

T.A. Henzinger
Z. Manna
A. Pnueli

We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-; time properties of reactive systems. The abstract notion of timed transition systems generalizes traditional transition systems conservatively: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound timing constraints on transitions. This framework can model real-time systems that communicate either through shared variables or by message passing and real-time issues such as timeouts, process priorities (interrupts), and process scheduling. We exhibit two styles for the specification of real-time systems. While the first approach uses time-bounded versions of the temporal operators, the second approach allows explicit references to time through a special clock variable. Corresponding to the two styles of specification, we present and compare two different proof methodologies for the verification of timing requirements that are expressed in these styles. For the bounded-operator style, we provide a set of proof rules for establishing bounded-invariance and bounded-responce properties of timed transition systems. This approach generalizes the standard temporal proof rules for verifying invariance and response properties conservatively. For the explicit-clock style, we exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety properties.

Details DOI

I&C Journal 1993 Journal Article

Probabilistic Verification

A. Pnueli
L.D. Zuck

Probabilistic elements are often introduced in concurrent programs in order to solve problems that either cannot be solved efficiently or cannot be solved at all by deterministic programs. Temporal logic is often used to specify the correctness conditions of concurrent programs. The paper presents a procedure that, given a probabilistic finite state program and a (restricted) temporal logic specification, decides whether the program satisfies its specification with probability 1. The paper also presents the notion of α-fairness and shows that a program satisfies its temporal specification with probability 1 if and only if all its α-fair computations satisfy the property.

Details DOI

TCS Journal 1984 Journal Article

A linear-history semantics for languages for distributed programming

N. Francez
D. Lehmann
A. Pnueli

A denotational semantics is given for a language for distributed programming based on communication (CSP). The semantics uses both linear sequences of communications to record computations and special states, called ‘expectation sets’, characterizing potential deadlocks. 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.

Details DOI

TCS Journal 1984 Journal Article

Fair termination revisited—with delay

K.R. Apt
A. Pnueli
J. Stavi

A proof method for establishing the fair termination and total correctness of both nondeterministic and concurrent programs is presented. The method calls for the extension of state by auxiliary delay variables which count down to the instant in which certain action will be scheduled. It then uses well-founded ranking to prove fair termination allowing nested fair selection and loops.

Details DOI