We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.

The paper investigates a development process for reactive programs, in which the program is automatically generated (synthesized) from a high-level temporal specification. The method is based on previous results that proposed a similar synthesis method for the automatic construction of hardware designs from their temporal specifications. Thus, the work reported here can be viewed as a generalization of existing methods for the synthesis of synchronous reactive systems into the synthesis of asynchronous systems. In the synchronous case it was possible to identify a restricted subclass of formulas and present an algorithm that solves the synthesis problem for these restricted specifications in polynomial time. Here the results are less definitive in the sense that we can offer some heuristics that may provide polynomial-time solutions only in some of the cases.

Summary form only given. It is a known fact that finitary state abstraction methods (i.e. methods in which the abstract domain is finite), such as predicate abstraction, are inadequate for verifying general liveness properties or even termination of sequential programs. In this talk we will present an abstraction approach called ranking abstraction which is sound and complete for verifying all temporally specified properties, including all liveness properties. We will start by presenting a general simple framework for state abstraction emphasizing that, in order to get soundness, it is necessary to apply an over-approximating abstraction to the system and an under-approximating abstraction to the (temporal) property. We show that finitary version of this abstraction are complete for verifying all safety properties. We also show examples of simple programs whose termination provably cannot be established by finitary abstraction. We then consider abstraction approaches to the verification of deadlock freedom, presenting some sufficient conditions guaranteeing that deadlock freedom is inherited from the concrete to the abstract. Finally, we introduce the method of ranking abstraction and illustrate its application to the verification of termination and more general liveness properties. In this presentation we emphasize the similarity between predicate abstraction and its extension into ranking abstraction. In particular, the fact that the user does not have to provide a full ranking function but only to specify the ingredients from which such a function can be constructed. We also sketch how abstraction refinement can be applied to ranking abstraction, thus opening the way to a CEGAR-like methodology. Time permitting, we will present a brief comparison between ranking abstraction and the methods of transition abstraction developed by Podelski, Rybalchenko, and Cook which underly the Terminator system. The talk is based on results obtained through joint research with I. Balaban, Y. Kesten, and L.D. Zuck.

Translation Validation is an approach of ensuring compilation correctness in which each compiler run is followed by a validation pass that proves that the target code produced by the compiler is a correct translation (implementation) of the source code. It has been previously shown that the problem of translation validation can be reduced to checking if a single system - the corss-product of the source and target, satisfies a specific property. In this paper, we show how to adapt the existing program analysis techniques in the setting of translation validation. In addition, we present a novel invariant generation algorithm which strengthens our analysis when the input programs contain dynamically allocated data structures. Finally, we report on the prototype tool that applies the developed methodology to verification of the LLVM compiler. The tool handles many of the classical intraprocedural compiler optimizations such as constant folding, reassociation, common subexpression elimination, code motion, dead code elimination, and others.

We show how to verify the correctness of transactional memory implementations with a model checker. We show how to specify transactional memory in terms of the admissible interchange of transaction operations, and give proof rules for showing that an implementation satisfies this specification. This notion of an admissible interchange is a key to our ability to use a model checker, and lets us capture the various notions of transaction conflict as characterized by Scott. We demonstrate our work using the TLC model checker to verify several well-known implementations described abstractly in the TLA+ specification language.

In this paper we improve the complexity of solving Rabin and Streett games to approximately the square root of previous bounds. We introduce direct Rabin and Streett ranking that are a sound and complete way to characterize the winning sets in the respective games. By computing directly and explicitly the ranking we can solve such games in time O(mnk+1kk!) and space O(nk) for Rabin and O(nkk!) for Streett where n is the number of states, m the number of transitions, and k the number of pairs in the winning condition. In order to prove completeness of the ranking method we give a recursive fixpoint characterization of the winning regions in these games. We then show that by keeping intermediate values during the fixpoint evaluation, we can solve such games symbolically in time O(nk+1k!) and space O(nk+1k!). These results improve on the current bounds of O(mn2kk!) time in the case of direct (symbolic) solution or O(m(nk2k!)k) in the case of reduction to parity games

Separation Logic consists of a Boolean combination of predicates of the form v i ≥ v j + c where c is a constant and v i ,v j are variables of some ordered infinite type like real or integer. Any equality or inequality can be expressed in this logic. We propose a decision procedure for Separation Logic based on allocating small domains (ranges) to the formula’s variables that are sufficient for preserving satisfiability. Given a Separation Logic formula φ, our procedure constructs the inequalities graph of φ, based on φ’s predicates. This graph represents an abstraction of the formula, as there are many formulas with the same set of predicates. Our procedure then analyzes this graph and allocates a range to each variable that is adequate for all of these formulas. This approach of finding small finite ranges and enumerating them symbolically is both theoretically and empirically more efficient than methods based on case-splitting or reduction to Propositional Logic. Experimental results show that the state-space (that is, the number of assignments that need to be enumerated) allocated by our procedure is frequently exponentially smaller than previous methods.

The paper presents a method for translation validation of a specific optimization, software pipelining optimization, used to increase the instruction level parallelism in EPIC type of architectures. Using a methodology as in [15] to establish simulation relation between source and target based on computational induction, we describe an algorithm that automatically produces a set of decidable proof obligations. The paper also describes SPV, a prototype translation validator that automatically produces verification conditions for software pipelining optimizations of the SGI Pro-64 compiler. These verification conditions are further checked automatically by the CVC [12] checker.

The paper presents an axiomatic system for quantified propositional temporal logic (QPTL), which is propositional temporal logic equipped with quantification over propositions (Boolean variables). The advantages of this extended temporal logic is that its expressive power is strictly higher than that of the unquantified version (PTL) and is equal to that of S1S, as well as that of ω‐automata. Another important application of QPTL is its use for formulating and verifying refinement relations between reactive systems. In fact, the completeness proof is based on the reduction of a QPTL formula into a Büchi automaton, and performing equivalence transformations on this automaton, formally justifying these transformations as a bi‐directional refinement.

We consider the problem of Uniform Algorithmic Verification of Parameterized Systems, which requires establishing in a single verification effort the correctness of a parameterized family of systems for any value of the parameter. As has been observed by several researchers, using regular expressions or equivalent formalisms (e.g. WS1S) as assertional language, we can perform symbolic model checking of systems of unbounded number of states.

In this work we investigate the problem of scheduling instructions on idealized microprocessors with multiple pipelines, in the presence of precedence constraints, release-times, deadlines, and latency constraints. A latency of l ij specifies that there must be at least l ij time-steps between the completion time of instruction i and the start time of instruction j . A latency of l ij =−1 can be used to specify that j may be scheduled concurrently with i but not earlier. We present a generic algorithm that runs in O ( n 2 log n α( n )+ ne ) time, given n instructions and e edges in the precedence DAG, where α( n ) is the functional inverse of the Ackermann function. Our algorithm can be used to construct feasible schedules for various classes of instances, including instances with the following configurations: (1) one pipeline, with individual release-times and deadlines and where the latencies between instructions are restricted to 0 and 1; (2) m pipelines, with individual release-times and deadlines, and monotone-interval order precedences; (3) two pipelines with latencies of −1 or 0, and release-times and deadlines; (4) one pipeline, latencies of 0 or 1 and individual processing times that are at least one; (5) m pipelines, intree precedences, constant latencies, and deadlines; (6) m pipelines, outtree precedences, constant latencies, and release-times. For instances with deadlines, optimal schedules that minimize the maximal tardiness can be constructed using binary search, in O (log n ) iterations of our algorithm. We obtain our results using backward scheduling, a very general relaxation method, which extends, unifies, and clarifies many previous results on instruction scheduling for pipelined and parallel machines.

No abstract available.

In this paper, we suggest a novel methodology for synthesizing switching controllers for continuous and hybrid systems whose dynamics are defined by linear differential equations. We formulate the synthesis problem as finding the conditions upon which a controller should switch the behavior of the system from one "mode" to another in order to avoid a set of bad states and propose an abstract algorithm that solves the problem by an iterative computation of reachable states. We have implemented a concrete version of the algorithm, which uses a new approximation scheme for reachability analysis of linear systems.

We present a framework integrating specification and scheduler generation for real time systems. In a first step, the system, which can include arbitrarily designed tasks (cyclic or sporadic, with or without precedence constraints, any number of resources and CPUs) is specified as a timed Petri net. In a second step, our tool generates the most general non preemptive online scheduler for the specification, using a controller synthesis technique.

Abstract This year (1997) marks the 20th anniversary of the introduction of Temporal Logic (TL) into Computer Science as a language proposed for the specification and verification of reactive systems. The talk will present a personal view of the main contributions and achievements of TL over the last two decades emphasizing the recent, increase of acceptance and adoption of the temporal methodology by industry. We will then proceed to identify future challenges and directions that may extend the applicability of TL to wider classes of applications and the treatment of ever larger systems. We start by identifying the class of reactive systems for whose specification and verification TL has proved to be a most natural and effective language. These are systems whose role is to maintain an ongoing interaction with their environment, rather than produce a final result on termination. Most, embedded systems which control an external physical environment be-long to this important class. Such systems must be specified and analyzed in terms of their behavior.

No abstract available.

The paper presents an axiomatic system for quantified propositional temporal logic (QPTL), which is propositional temporal logic equipped with quantification over propositions (boolean variables). The advantages of this extended temporal logic is that its expressive power is strictly higher than that of the unquantified version (PTL) and is equal to that of SIS, as well as that of /spl omega/-automata. Another important application of QPTL is its use for formulating and verifying refinement relations between reactive systems. In fact, the completeness proof is based on the reduction of a QPTL formula into a Buchi automaton, and performing equivalence transformations on this automata, formally justifying these transformations.

It has long been known that past-time operators add no expressive power to linear temporal logics. In this paper, we consider the extension of branching temporal logics with past-time operators. Two possible views regarding the nature of past in a branching-time model induce two different such extensions. In the first view, past is branching and each moment in time may have several possible futures and several possible pasts. In the second view, past is linear and each moment in time may have several possible futures and a unique past. Both views assume that past is finite. We discuss the practice of these extensions as specification languages, characterize their expressive power, and examine the complexity of their model-checking and satisfiability problems.

Presents a compositional proof system for the verification of real-time systems. Real-time systems are modeled as timed transition modules, which explicitly model interaction with the environment and may be combined using composition operators. Composition rules are devised such that the correctness of a system may be determined from the correctness of its components. These proof rules are demonstrated on Fischer's mutual exclusion algorithm, for which mutual exclusion and bounded response are proven.>

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.

Two-way translations between various versions of temporal logic and between temporal logic over finite sequences and star-free regular expressions are presented. The main result is a translation from normal-form temporal logic formulas to formulas that use only future operators. The translation offers a new proof to a theorem claimed by D. Gabbay et al. (1980), stating that restricting temporal logic to the future operators does not impair its expressive power. The theorem is the basis of many temporal proof systems.>

Serializability of database transactions is first defined within the framework of linear temporal logic. For commutativity-based serializability, an alternative specification is given in a temporal logic whose semantic interpretation is especially tailored for reasoning about equivalence sequences of histories. The alternative specification method is given in ISTL* and is limited to the specification of concurrency control algorithms based on commutativity. A formal verification system for serializability that uses classical logic reasoning is provided. Within it, proving serializability of transactions executing a concurrency control algorithm is done along the same lines as proving properties of concurrent programs. Serializability for the multiversion-timestamp algorithm is verified.>

. We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of concurrent and reactive systems. A global, discrete, and asynchronous clock is incorporated into the model by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upperbound real-time requirements for transitions. We show how to model real-time systems that communicate either through shared variables or by message passing, and how to represent the important real-time constructs of priorities (interrupts), scheduling, and timeouts in this framework. Two styles for the specification of real-time properties are presented. The first style uses bounded versions of the temporal operators; the real-time requirements expressed in this style are classified ...

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.>

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.>

The authors present a single exponent decision procedure for the validity of XCTL formulas, and a double exponent decision procedure for the validity of XCTL formulas over finite state programs (model checking). The expressive power of XCTL is compared with that of some other logics proposed for the expression of real time properties. It is shown that it is incomparable with the expressive power of the recently proposed logic TPTL (timed propositional temporal logic).>

We propose a classification of temporal properties into a hierarchy.The classes of the hierarchy are characterized through four views: a language-theoretic view, a topologica1 view, the temporal logic view, and an automata view.In the topological view, the considered hierarchy coincides with the two lower levels of the Bore1 hierarchy, starting with the closed and open sets.For properties that are expressible by temporal logic and predicate automata, we provide a syntactic characterization of the formulae and automata that specify properties in the different classes.We relate this classification to the well known safety-[iweness classification, and show that in some sense the two are orthogonal to one another.

STATEMATE is a set of tools, with a heavy graphical orientation, intended for the specification, analysis, design, and documentation of large and complex reactive systems. It enables a user to prepare, analyze, and debug diagrammatic, yet precise, descriptions of the system under development from three interrelated points of view, capturing structure, functionality, and behavior. These views are represented by three graphical languages, the most intricate of which is the language of statecharts, used to depict reactive behavior over time. In addition to the use of statecharts, the main novelty of STATEMATE is in the fact that it understands the entire descriptions perfectly, to the point of being able to analyze them for crucial dynamic properties, to carry out rigorous executions and simulations of the described system, and to create running code automatically. These features are invaluable when it comes to the quality and reliability of the final outcome.>

A hardware verification approach based on linear time temporal logic is described. The authors show that by introducing appropriate abbreviations into linear temporal logic, which facilitate the expression of precise timing constraints, they obtain a very convenient language for the description of the behavior of hardware systems, and for the development of a formal verification system used in proving that designs meet their specifications. The authors automatically verified several sequential circuits. As an example they describe the specification and verification of an edge-triggered D-type flip-flop and the discovery of an error in a published specification. It is demonstrated that the approach is practical and offers a viable alternative to simulation. Comparison is made with other formal methods.>

We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(x, y) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm for constructing the program whenever it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees in time exponential in the number of pairs, but only polynomial in the number of states. This leads to a synthesis algorithm whose complexity is double exponential in the length of the given specification.

We propose a classification of temporal properties into a hierarchy which refines the known safety-liveness classification of properties. The new classification recognizes the classes of safety, guarantee, persistence, fairness, and hyper-fairness. The classification suggested here is based on the different ways a property of finite computations can be extended into a property of infinite computations. For properties that are expressible by temporal logic and predicate automata, we provide a syntactic characterization of the formulae and automata that specify properties in the different classes. We consider the verification of properties over a given program, and provide a unique proof principle for each class.

∀-automata are non-deterministic finite-state automata over infinite sequences. They differ from conventional automata in that a sequence is accepted if all runs of the automaton over the sequence are accepting. These automata are suggested as a formalism for the specification and verification of temporal properties of concurrent programs. It is shown that they are as expressive as extended-temporal-logic (ETL), and in some cases provide a more compact representation of properties than temporal logic. A structured diagram notation is suggested for the graphical representation of these automata. A single sound and complete proof rule is presented for proving that all computations of a program have the property specified by a ∀-automaton.

Concurrent systems are typically large and complex, requiring long, development time and much labor. They are, therefore, prime candidates for simplification and automation of the design and programming process. Their major application areas include real time systems, operating systems and cooperative computation. New applications are emerging with the trends towards wide usage of personal computers connected in a network and towards use of parallel processing in supercomputer architectures.

In this paper we advance the radical notion that a computational model based on the reals provides a more abstract description of concurrent and reactive systems, than the conventional integers based behavioral model of execution sequences. The real model is studied in the setting of temporal logic, and we illustrate its advantages by providing a fully abstract temporal semantics for a simple concurrent language, and an example of verification of a concurrent program within the real temporal logic defined here. It is shown that, by imposing the crucial condition of finite variability, we achieve a balanced formalism that is insensitive to finite stuttering, but can recognize infinite stuttering, a distinction which is essential for obtaining a fully abstract semantics of non-terminating processes. Among other advantages, going into real-based semantics obviates the need for the controversial representation of concurrency by interleaving, and most of the associated fairness constraints.

We present an algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program. The running time of the algorithm is exponential in the size of the formula but linear in the size of the checked program. The algorithm yields also a formal proof in case the formula is valid over the program. The algorithm has four versions that check satisfiability by unrestricted, impartial, just and fair computations of the given program.

A new probabilistic symmetric solution to the n processes mutual exclusion problem is presented. The algorithm is verified formally using the extreme fairness approach to probabilistic verification.

We examine local area network protocols and verify the correctness of two representative algorithms using temporal logic. We introduce an interval temporal logic that allows us to make assertions of the form “in the next k units, X holds.” This logic encodes intuitive arguments about contention protocols quite directly. We present two proofs of an Ethernet-like contention protocol, one using the interval temporal logic and one using classical temporal logic. We also verify a contention-free protocol using an invariant that seems to have wide applicability for such protocols.

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.

A general method for proving properties of probabilistic programs is presented. This method generalizes the intermediate assertion method in that it extends a given assertion on the output distribution into an invariant assertion on all intermediate distributions, too. The proof method is shown to be sound and complete for programs which terminate with probability 1. A dual approach, based on the expected number of visits in each intermediate state, is also presented. All the methods are presented under the uniform framework which considers a probabilistic program as a discrete Markov process.

With the (necessary) condition that atomic programs in process logic (PL) be binary, we present an algorithm for the translation of a PL formula p into a program $\zeta (p)$ of propositional dynamic logic (PDL) such that a finite path satisfies p if it belongs to $\zeta (p)$. This reduction has two immediate corollaries: 1) validity in this PL can be tested by testing validity of formulas in PDL; 2) all state properties expressible in this PL are expressible in PDL. The translation, however, is of nonelementary time complexity.The significance of the result to the search for natural and powerful logics of programs is discussed.

Describes the use of a very high-level equational language and distributed processing in a methodology for the development of large-scale systems in natural and social sciences, or engineering. The methodology denoted as cooperative computation, consists of dividing the labour among a number of organizationally and geographically dispersed groups, with each responsible for a respective local area, and the integration of the local areas into a global system. With an equational language, the user is able to express computations in terms of equations that are commonly used in science and engineering, without the detail required in programming computers. Object programs are then produced automatically through the use of a program generator and a configurator. The methodology is discussed primarily through an example, using the model language applied in environment of Project Link.

An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied. Given a new language, it is sufficient to deline the interface notions of atomic transitions, justice, and fairness in order to obtain a full temporal proof system for this language. This construction is particularly useful for the analysis of concurrent systems. We illustrate the construction on the shared-variable model and on CSP. The generic proof system is shown to be relatively complete with respect to pure first-order temporal logic.

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]).

The asynchronous execution behavior of several concurrent processes, which may use randomization, is studied.Viewing each process as a discrete Markov chain over the set of common execution states, necessary and sufficient conditions are given for the processes to converge almost surely to a given set of goal states under any fair, but otherwise arbitrary, schedule, provided that the state space is finite.(These conditions can be checked mechanically.)An interesting feature of the proof method is that it depends only on the topology of the transitions and not on the actual values of the probabilities.It is also shown that in this model synchronization protocols that use randomization are in certain cases no more powerful than deterministic protocols.This is demonstrated by (1) establishing lower bounds, similar to those known for deterministic protocols, on the size of a shared variable necessary to ensure mutual exclusion and lockout-free behavior of a "randomized" protocol and ( 2) showing that no fully symmetric "randomized" protocol can ensure mutual exclusion and freedom from lockout.

The paper describes the compilation of a program specification, written in the very high level nonprocedural MODEL language, into an object, PL/1 or Cobol, procedural language program. Nonprocedural programming languages are descriptive and devoid of procedural controls. They are therefore easier to use and require less programming skills than procedural languages. The MODEL language is briefly presented and illustrated followed by a description of the compilation process. An important early phase in the compilation is the representation of the specification by a dependency graph, denoted as array graph, which expresses the data flow interdependencies between statements. Two classes of algorithms which utilize this graph are next described. The first class checks various completeness, nonambiguity, and consistency aspects of the specification. Upon detecting any problems, the system attempts some automatic correcting measures which are reported to the user, or alternately, when no corrections appear as reasonable, it reports the error and solicits a modification from the user. The second class of algorithms produces an intermediate design of an object program in a language independent form. Finally, PL/1 or Cobol code is generated.

The asynchronous execution behavior of several concurrent processes, which may use randomization, is studied. Viewing each process as a discrete Markov chain over the set of common execution states, we give necessary and sufficient conditions for the processes to converge almost surely to a given set of goal states, under any fair, but otherwise arbitrary schedule, provided that the state space is finite. (These conditions can be checked mechanically.) An interesting feature of the proof method is that it depends only on the topology of the transitions and not on the actual values of the probabilities. We also show that in our model synchronization protocols that use randomization are in certain cases no more powerful than deterministic protocols. This is demonstrated by (a) Proving lower bounds on the size of a shared variable necessary to ensure mutual exlusion and lockout-free behavior of the protocol; and (b) Showing that no fully symmetric 'randomized' protocol can ensure mutual exclusion and freedom from lockout.

With the (necessary) condition that atomic programs in PL be binary, we present an algorithm for the translation of a PL formula X into a PDL program τ (X) such that a finite path satisfies X iff it belongs to τ (X). This reduction has two immediate corollaries: 1) validity in this PL can be tested by testing validity of formulas in PDL; 2) all finite-path program properties expressible in this PL are expressible in PDL.The translation, however, seems to be of non-elementary time complexity. The significance of the result to the search for natural and powerful logics of programs is discussed.

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.

A temporal language and system are presented which are based on branching time structure. By the introduction of symmetrically dual sets of temporal operators, it is possible to discuss properties which hold either along one path or along all paths. Consequently it is possible to express in this system all the properties that were previously expressible in linear time or branching time systems. We present an exponential decision procedure for satisfiability in the language based on tableaux methods, and a complete deduction system. As associated temporal semantics is illustrated for both structured and graph representation of programs.

Finite State Linear Programs (FSLP) are introduced to model simple data processing applications. Essentially these are finite automata with the added capability of performing linear operations on a set of registers and the input. Algorithmic constructions are given to test equivalence of FSLP programs, and to minimize the number of states and registers. Linear algebraic methods are used for the register minimization procedure (and its correctness proof).

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.

The use of the temporal logic formalism for program reasoning is reviewed. Several aspects of responsiveness and fairness are analyzed, leading to the need for an additional temporal operator: the 'until' operator -U. Some general questions involving the 'until' operator are then discussed. It is shown that with the addition of this operator the temporal language becomes expressively complete. Then, two deductive systems DX and DUX are proved to be complete for the languages without and with the new operator respectively.

A class of schemes called synchronous schemes is defined. A synchronous scheme can have several variables, but all the active ones are required to keep a synchronized rate of computation as measured by the height of their respective Herbrand values. A "reset" statement, which causes all the variables to restart a new computation, is admitted. It is shown that equivalence, convergence, and other properties are decidable for schemes in this class. The class of synchronous schemes contains, as special cases, the known decidable classes of Ianov schemes, one-variable schemes with resets, and progressive schemes.

The Model II language and the associated program generator are used to explain and illustrate the use of very high level nonprocedural languages for computer programming. The effect of a very high level language is obtained in Model II through the elimination of procedural and control facilities that exist in high level programming languages such as PL/I or Cobol. In particular, the statements may be given in any order and there are no control constructs such as input/output, iterations, and memory allocation. The task of ordering the statements for execution and providing control statements is performed by the automatic program generator. The specification of a program is therefore much shorter (approximately one-fifth) than the equivalent high level procedural language program. Most important, a user need not regard the task of specifying a program as defining a process but rather as describing data and relations. This point of view greatly reduces the computer programming proficiency required of a user. The paper focuses on an example of the use of the language in business data processing, its advantages, and its novelty. It only briefly reviews the methodology incorporated in the existing program generator, a detailed description of which may be found in the references.

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.

Denoting a version of Hoare's system for proving partial correctness of recursive programs by H, we present an extension D which may be thought of as H υ {@@@@,@@@@,@@@@,@@@@} υ H-1, including the rules of H, four special purpose rules and inverse rules to those of Hoare. D is shown to be a complete system (in Cook's sense) for proving deductions of the form σ1,....σn @@@@ σ over a language, the wff's of which are assertions in some assertion language L and partial correctness specifications of the form p(α)q. All valid formulae of L are taken as axioms of D. It is shown that D is sufficient for proving partial correctness, total correctness and program equivalence as well as other important properties of programs, the proofs of which are impossible in H. The entire presentation is worked out in the framework of nondeterministic programs employing iteration and mutually recursive procedures.

A class of (monadic) functional schemas which properly includes “Ianov” flowchart schemas is defined. It is shown that the termination, divergence, and freedom problems for functional schemas are decidable. Although it is possible to translate a large class of non-free functional schemas into equivalent free functional schemas, it is shown that in general this cannot be done. It is also shown that the equivalence problem for free functional schemas is decidable. Most of the results are obtained from well-known results in formal languages and automata theory.

A graph G with vertex set N = {1, 2, .-. , n} is called a permutation graph there exists a permutation P on N such that for i,j E N, (i -j)[P-'(i) -P-'(j)] < 0 if ar only if i and j are joined by an edge in G.A structural relationship is established between permutation graphs and transitive graph An algorithm for determining whether a given graph is a permutation graph is given.Efficie, algorithms for finding a maximum size clique and a minimum coloration of transitive grapl are presented.These algorithms are then shown to be applicable in solving problems in memo] allocation and circuit layout.

The problems of convergence, correctness, and equivalence of computer programs can be formulated by means of the satisfiability or validity of certain first-order formulas. An algorithm is presented for constructing such formulas for functional programs, i.e. programs defined by LISP-like conditional recursive expressions.

This paper is concerned with the relationship between the convergence, correctness and equivalence of recursively defined functions and the satisfiability (or unsatisfiability) of certain first-order formulas.