MetateM: A framework for programming in temporal logic
Lecture notes in computer sciencePublished 1 January 1990
Howard Barringer, Michael Fisher, Dov M. Gabbay, Graham Gough, Richard Owens
Citations132
SJR quartileQ2
SJR score0.35
SNIP0.55
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
This paper further develops the methodology of temporal logic as an executable imperative language, presented by Moszkowski and Gabbay and presents a concrete framework, called MetateM for executing (modal and) temporal logics.
Abstract
In this paper we further develop the methodology of temporal logic as an executable imperative language, presented by Moszkowski [Mos86] and Gabbay [Gab87, Gab89] and present a concrete framework, called MetateM for executing (modal and) temporal logics. Our approach is illustrated by the development of an execution mechanism for a propositional temporal logic and for a restricted first order temporal logic.
Keywords
Computer Science
ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications
3,555 Citations1986E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems.
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.
A Useful Four-Valued Logic
1,419 Citations1977Nuel Belnap
It is argued that a sophisticated question-answering machine that has the capability of making inferences from its data base should employ a certain four-valued logic, the motivating consideration being that minor inconsistencies in its data should not be allowed to lead to irrelevant conclusions.
Checking that finite state concurrent programs satisfy their linear specification
618 Citations1985Orna Lichtenstein, Amir Pnueli
An algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program and a formal proof in case the formula is valid over the program is presented.
Journal of Computer and System SciencesAutomata-theoretic techniques for modal logics of programs
523 Citations1986Moshe Y. Vardi, Pierre Wolper
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.
Lecture notes in computer scienceExecuting temporal logic programs
393 Citations1985Ben Moszkowski
This paper presents temporal logic as a tool for reasoning about computer programs, digital circuits and message-passing systems and investigates its role as an adjunct to existing languages.
Lecture notes in computer scienceOn the synthesis of an asynchronous reactive module
316 Citations1989Amir Pnueli, Roni Rosner
Lecture notes in computer scienceThe declarative past and imperative future
276 Citations1989Dov M. Gabbay
A new paradigm in executable logic, that of the declarative past and imperative future, is proposed, which is regarded as a natural meeting between the imperative anddeclarative paradigms.
Open Repository and Bibliography (University of Liège)The tableau method for temporal logic: An overview
235 Citations1985Pierre Wolper
An overview of the tableau decision method for propositional temporal logic and how it can be applied to other variants of temporal logic like branching time temporal Logic and extensions o f linear time temporal logic are presented.
Lecture notes in computer scienceReasoning in interval temporal logic
92 Citations1984Ben Moszkowski, Zohar Manna
This paper discusses interval temporal logic (ITL), a formalism that augments standard predicate logic with operators for time-dependent concepts and compares ITL with the logic-based programming languages Lucid and Prolog.
Temporal logic programming is complete and expressive
50 Citations1989Marianne Baudinet
It is shown how propositional TEMPLOG programs can be translated into a temporal fixpoint calculus and it is proved that they can express essentially all regular properties of sequences.
Lecture notes in computer scienceNonclausal temporal deduction
40 Citations1985Martı́n Abadi, Zohar Manna
This system is based on nonclausal resolution; proofs are natural and generally short and its extension to first-order temporal logic is considered.
IFIP CongressToward a Unified Logic Basis for Programming Languages.
29 Citations1983C. S. Tang
XYZ/E is a temporal-logic language that can express all conventional data structures and control structures, nondeterminate or concurrent programs, even programs with branching-time order, and adopts another approach that can ameliorate many problems of formalization.
Logic in Computer ScienceA timely resolution
28 Citations1986Martı́n Abadi, Zohar Manna
The system R is based on nonclausal resolution; proofs are natural and generally short, and special quantifier rules, unification techniques, and a resolution rule are introduced.
Theoretical Computer ScienceThe power of temporal proofs
11 Citations1989Martı́n Abadi
A typical temporal system turns out to be incomplete in a strong sense; the addition of new rules to define auxiliary predicates is suggested and one of the simple temporal systems described is as powerful as Peano Arithmetic.
Advances in software science and technologyRACCO: A Modal-Logic Programming Language for Writing Models of Real-Time Process-Control Systems
5 Citations1992Takashi Hattori, Takashi Sakuragawa +3 more
The grammar and semantics of RACCO are shown and its formal semantics and implementation will be explained and the design concept of RacCO will be discussed.