Realizable and unrealizable specifications of reactive systems
Lecture notes in computer sciencePublished 1 January 1989Open access
Martı́n Abadi, Leslie Lamport, Pierre Wolper
Citations243
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A class of realizable specifications is defined, which includes all specifications that can be implemented by physically possible systems, but also some that have no real implementations for reasons that do not concern us.
Abstract
peer reviewed
Keywords
Computer Science
Journal of the Franklin InstituteContributions to the theory of games.
1,842 Citations1960Kuhn, H W, Tucker, A W +1 more
On the synthesis of a reactive module
1,448 Citations1989Amir Pnueli, Roni Rosner
An algorithm is presented 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 theNumber of states, which leads to a synthesis algorithm whose complexity is doubleonential in the length of the given specification.
On a Decision Method in Restricted Second Order Arithmetic
1,277 Citations1990J Büchi
Open Repository and Bibliography (University of Liège)An Automata-Theoretic Approach to Automatic Program Verification
1,254 Citations1986Moshe Y. Vardi, Pierre Wolper
Journal of the ACMA Theory of Communicating Sequential Processes
1,191 Citations1984Stephen Brookes, C. A. R. Hoare +1 more
A mathematical model for communicating sequential processes is given, and a number of its interesting and useful properties are stated and proved.
Transactions of the American Mathematical SocietyDecidability of second-order theories and automata on infinite trees.
1,159 Citations1969Michael O. Rabin
Information Processing LettersDefining liveness
1,025 Citations1985Bowen Alpern, Fred B. Schneider
A formal definition for liveness properties is proposed, and every property is shown to be the intersection of a safety property and a liveness property.
On the Development of Reactive Systems
836 Citations1985David Harel, Amir Pnueli
The recently proposed statechart method is recommended for finding satisfactory methods for behavioral description in reactive systems, observing that most reactive systems cannot be developed in a linear stepwise fashion, but, rather, give rise to a two-dimensional development process, featuring behavioral aspects in the one dimension and implementational ones in the other.
Notes on Communicating Sequential Systems
769 Citations1986C. A. R. Hoare
These notes present a coherent and comprehensive introduction to the theory and applications of Communicating Sequential Processes, which can be used for proofs of equivalence and can justify correctness-preserving transformations.
Theoretical Computer ScienceThe temporal semantics of concurrent programs
701 Citations1981Amir Pnueli
It is 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.
Science of Computer ProgrammingUsing branching time temporal logic to synthesize synchronization skeletons
662 Citations1982E. Allen Emerson, Edmund M. Clarke
A method of constructing concurrent programs in which the synchronization skeleton of the program is automatically synthesized from a (branching time) temporal logic specification by using a decision procedure based on the finite model property of the logic.
Distributed ComputingRecognizing safety and liveness
552 Citations1987Bowen Alpern, Fred B. Schneider
A formal characterization for safety properties and liveness properties is given in terms of the structure of the Buchi automaton that specifies the property.
Journal of Computer and System SciencesAutomata-theoretic techniques for modal logics of programs
523 Citations1986Moshe Y. Vardi, Pierre Wolper
On the complexity of omega -automata
508 Citations1988Muli Safra
The author presents a determinisation construction that is simpler and yields a single exponent upper bound for the general case, and can be used to obtain an improved complementation construction for Buchi automata that is essentially optimal.
ACM Transactions on Programming Languages and SystemsSynthesis of Communicating Processes from Temporal Logic Specifications
497 Citations1984Zohar Manna, Pierre Wolper
Propositional Temporal Logic is applied to the specification and synthesis of the synchronization part of communicating processes by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL.
Solving Sequential Conditions by Finite-State Strategies
466 Citations1990J Büchi, Lawrence H. Landweber
IFIP CongressWhat Good is Temporal Logic
444 Citations1983Leslie Lamport
This was an invited paper and describes the state of my views on specification and verification at the time, notable for introducing the idea of invariance under stuttering and explaining why it’s a vital attribute of a specification logic.
Theoretical Computer ScienceThe complementation problem for Büchi automata with applications to temporal logic
382 Citations1987A. Prasad Sistla, Moshe Y. Vardi +1 more
A construction that involves only an exponential blow-up in the size of the automaton is presented 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.
Trees, automata, and games
326 Citations1982Yuri Gurevich, Leo Harrington
This work gives here an alternative and transparent proof of Rabin's result on tree automata, which is based on ideas of his predecessors and especially those of B- and-uuml;chi-&-mdash;.
Journal of Computer and System SciencesA complete inference system for a class of regular behaviours
319 Citations1984Robin Milner
Les arbres consideres sont des arcs etiquetes par des symboles faits d'un ensemble ACT={a, b, ...}, que nous appellerons «actions».
Lecture notes in computer scienceOn the synthesis of an asynchronous reactive module
316 Citations1989Amir Pnueli, Roni Rosner
Reasoning about infinite computation paths
309 Citations1983Pierre Wolper, Moshe Y. Vardi +1 more
This work investigates extensions of temporal logic by finite automata on infinite words by investigating the addition of alternation and shows that it does not increase the complexity of the decision problem.
The complexity of tree automata and logics of programs
296 Citations1988E. Allen Emerson, Charanjit S. Jutla
It is shown that for tree automata with m states and n pairs nonemptiness can be tested in time O((mn)/sup 3n/), even though the problem is in general NP-complete, and it follows that satisfiability for propositional dynamic logic with a repetition construct and for the propositional mu-calculus can be tests in deterministic single exponential time.
Transactions of the American Mathematical SocietySolving sequential conditions by finite-state strategies
269 Citations1969J Büchi, Lawrence H. Landweber
An algorithm which decides whether or not a condition 𝕮(X, Y) stated in sequential calculus admits a finite automata solution, and produces one if it exists, and solves a problem stated in [4] and contains the answer to Case 4 left open in [6].
The existence of refinement mappings
187 Citations2003M. Abadi, Leslie Lamport
Studies in logic and the foundations of mathematicsDescriptive Set Theory: Projective Sets
44 Citations1977
The emptiness problem for automata on infinite trees
42 Citations1972R. Hossley, Charles Rackoff
The proof reduces the emptiness problem for automata on infinite trees to that for Automata on finite trees, by showing that any automata definable set of infinite trees must contain a finitely-generable tree.
Lecture notes in computer scienceProcess theory: Semantics, specification and verification
31 Citations1986Ernst-Rüdiger Olderog
Process theory seeks to overcome difficulty by providing sound formal descriptions of processes (semantics) which facilitate their specification, verification and construction.
Specifying and Verifying Concurrent Programs.
1 Citations1985Leslie Lamport
The goal of this project was the development of formal methods for the specification and verification of concurrent programs to help avoid software errors in concurrent systems.