Search

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.

A language L over the Cartesian product of component alphabets is called projective if it is closed under projections, i.e., together with each word α ∈ L, it contains all the words that have the same projections up to stuttering as α. We prove that the projective languages are precisely the languages obtained using parallel composition and intersection from stuttering-closed component languages in each of the following classes of languages: regular, star-free regular, ω-regular and star-free ω-regular. Languages of these classes can also be seen as properties of various temporal logics which are used to specify properties of concurrent systems. In particular, the star-free ω-regular languages coincide with properties expressed using Propositional Linear Temporal Logic. Some uses of projective properties for specification and verification of programs are studied.

The incorporation of a recovery algorithm into a program can be viewed as a program transformation, converting the basic program into a fault-tolerant version. We present a framework in which such program transformations are accompanied by a corresponding formula transformation which obtains properties of the fault-tolerant versions of the programs from properties of the basic programs. Compositionality is achieved when every property of the fault-tolerant version can be obtained from a transformed property of the basic program. A verification method for proving the correctness of formula transformations is presented. This makes it possible to prove just once that a formula transformation corresponds to a program transformation, removing the need to prove separately the correctness of each transformed program. Keywords: Parallel Algorithms, Distributed Algorithms, Fault-Tolerance, Specification, Verification.

Peled, D. and A. Pnueh, Proving partial order properties, Theoretical Computer Science 126 (1994) 143-182. 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.

Trace semantics is extended to allow conditional commutativity among operations. Conditional commutativity is obtained by identifying the context (the set of global states) in which operations are commutative using special predicates. These predicates allow collapsing execution histories into equivalence classes of conditional traces. Using this approach, it is possible that the execution of two operations will be dependent in one context and independent in another. The predicates allow defining a family of possible semantic definitions for each language, where each is an extension of previous standard definitions. Examples are shown when such a semantics is desired. As an example of an application, a proof method for total correctness is introduced.

This paper presents an automatic method for calculating the path condition for programs with real time constraints. We model concurrent systems using timed transition systems and translate them into extended timed automata. Then an acyclic extended timed automaton is constructed and the path condition is calculated backwards over it. This method can be used for semiautomatic verification of a unit of code in isolation, i.e., without providing the exact values of parameters with which it is called. It can also be used for test case generation for real-time systems. Such a symbolic model checking algorithm was implemented previous in the PET system [E. Gunter, D. Peled, Unit checking: Symbolic model checking for a unit of code, Verification: Theory and Practice 2003, Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday, Lecture Notes in Computer Science, vol. 2772, Springer, 548–567] for untimed systems. Our method can also be used for the automatic generation of test cases for unit testing. The current generalization of the calculation of path condition for the timed case turns out to be quite tricky, since not only the selected path contributes to the path condition, but also timing constraints of alternative choices in the code.

Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Two examples of such properties are serializability of a database and global snapshots of concurrent systems. Recently, a modest extension for LTL by an operator that expresses snapshots, has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot appeared in the past, perhaps not in the observed execution sequence, but possibly in an equivalent one.Originally, a model checking algorithm for this logic that is exponential space in the size of the system was suggested. In this paper, we provide a model checking algorithm that is in polynomial space in the size of the system. Our construction can also serve as an efficient (polynomial) algorithm for detecting conjunctive properties (i.e., conjunction of local process properties) in a concurrent history of execution.