L.0: a truly concurrent executable temporal logic language for protocols
IEEE Transactions on Software EngineeringPublished 1 April 1993
Linda Ness
Citations4
SJR quartileQ1
SJR score1.45
SNIP2.43
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 small portion of the logical layer specification of Futurebus+ is taken as the main example in this study, and the state predicates permitted include existence and nonexistence predicates, as well as the more traditional assignment and equality predicates.
Abstract
The semantics L.0, a programming language designed for the specification and simulation of protocols that assumes a true concurrency model, is given in terms of predicate linear temporal logic, and the restricted universe of models assumed in L.0 programs is defined. The execution algorithm for L.0 constructs a model in this universe. The restricted subset of temporal logic exploited permits a nonbacktracking execution algorithm. Fundamental to the semantics of L.0 is a frame assumption, which generalizes the frame assumption of standard imperative programming, and which eases specification of protocols. The data domain assumed in L.0 programs is sets of trees with labeled edges, and the state predicates permitted include existence and nonexistence predicates, as well as the more traditional assignment and equality predicates. These choices for data domain and predicates permit convenient specification of the hierarchical message structure often assumed in telecommunications protocols, for in such message structures, the existence or nonexistence of parts of the message hierarchy is determined by logical properties of the rest of the message hierarchy. A small portion of the logical layer specification of Futurebus+ is taken as the main example in this study.>
Keywords
Computer Science
The temporal logic of programs
5,586 Citations1977Amir Pnueli
A unified approach to program verification is suggested, which applies to both sequential and parallel programs, and the main proof method is that of temporal reasoning in which the time dependence of events is the basic concept.
Medical Entomology and ZoologyHandbook of theoretical computer science
4,202 Citations1990Jan Van Leeuwen
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.
Elsevier eBooksSome Philosophical Problems from the Standpoint of Artificial Intelligence
3,289 Citations1981John McCarthy, Patrick J. Hayes
The formalism of this paper represents an advance over McCarthy (1963) and Green (1969) in that it permits proof of the correctness of strategies that contain loops and strategies that involve the acquisition of knowledge; and it is also somewhat more concise.
Information and ComputationSymbolic model checking: 1020 States and beyond
2,674 Citations1992Jerry R. Burch, E. M. Clarke +3 more
It is shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata.
Elsevier eBooksTemporal and Modal Logic
1,890 Citations1990E. Allen Emerson
The chapter describes the framework of linear temporal logic, which has been widely employed in the specification and verification of programs and explains how temporal logic structures can be used to model concurrent programs using non-determinism and fairness.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)Symbolic model checking: an approach to the state explosion problem
980 Citations1992Kenneth L. McMillan
Lecture notes in computer scienceAutomata for modeling real-time systems
895 Citations2005Rajeev Alur, David L. Dill
To model the behavior of finite-state asynchronous real-time systems, the notion of timed Buchi automata (TBA) is proposed, coupled with a mechanism to express constant bounds on the timing delays between system events.
Model-checking for real-time systems
890 Citations2002Rajeev Alur, Costas Courcoubetis +1 more
An algorithm is developed for model checking, that is, for determining the truth of a TCTL formula with respect to a timed graph, and it is argued that choosing a dense domain, instead of a discrete domain, to model time does not blow up the complexity of the model-checking problem.
Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics
607 Citations1994Jan Van Leeuwen
This handbook will provide professionals and students with a comprehensive overview of the main results and developments in this rapidly evolving field of theoretical computer science with a focus on core areas of theoretical computer science as it is practiced today.
Lecture notes in computer scienceThe glory of the past
461 Citations1985Orna Lichtenstein, Amir Pnueli +1 more
The notion of α-fairness is presented which is proved to fully capture the behavior of probabilistic finite state programs.
Automatic verification of finite state concurrent system using temporal logic specifications
412 Citations1983E. 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.
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.
Model checking and abstraction
348 Citations1992Edmund M. Clarke, Orna Grümberg +1 more
A method for using abstraction to reduce the complexity of temporal logic model checking by constructing an abstract model of a program without ever examining the corresponding unabstracted model is described.
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.
Representing circuits more efficiently in symbolic model checking
176 Citations1991Jerry R. Burch, E. M. Clarke +1 more
This work significantly reduces the complexity of BDD-based symbolic verification by using partitioned transition relations to represent state transition graphs and was able to handle example pipelines with over l O l Z o reachable states.
Lecture notes in computer scienceAnalysis of discrete event coordination
141 Citations1990Robert P. Kurshan
A reduction is a validity-preserving transformation by which a complex assertion about a complex model may be replaced by a simpler assertion aboutA simpler model in such a way that the validity of the latter implies thevalidity of the former.
Explicit clock temporal logic
136 Citations2002Eyal Harel, Orna Lichtenstein +1 more
It is shown that XCTL's expressive power is incomparable with the expressive power of the recently proposed logic TPTL (timed propositional temporal logic).
Lecture notes in computer scienceMetateM: A framework for programming in temporal logic
132 Citations1990Howard Barringer, Michael Fisher +3 more
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.
Lecture notes in computer scienceModels and equality for logical programming
109 Citations2005Joseph A. Goguen, José Meseguer
It is argued that some standard tools from model theory provide a better semantic foundation than the more syntactic and operational approaches usually used in logic programming.
AT&T Technical JournalSoftware for Analytical Development of Communications Protocols
101 Citations1990Zvi Har'el, Robert P. Kurshan
A way to develop and implement communications protocols so they are logically sound and meet stated requirements and recount the experience of an application of this methodology to develop a new session protocol at an interface of an AT&T product called the Trunk Operations Provisioning Administration System (TOPAS).
Lecture notes in computer sciencePartial orderings descriptions and observations of nondeterministic concurrent processes
82 Citations1989Pierpaolo Degano, Rocco De Nicola +1 more
In order to obtain more abstract semantic definitions, new notions of observational equivalence on Labelled Event Structures are introduced that preserve both concurrency and nondeterminism.
Lecture notes in control and information sciencesReducibility in analysis of coordination
69 Citations2006Robert P. Kurshan
The use of automata to model non-terminating processes such as communication protocols and complex integrated hardware systems is conceptually attractive because it affords a well-understood mathematical model with an established literature.
ACM SIGSOFT Software Engineering NotesProgramming and verifying critical systems by means of the synchronous data-flow language LUSTRE
57 Citations1991Christophe Ratel, Nicolas Halbwachs +1 more
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 scienceTokio: Logic programming language based on temporal logic and its compilation to Prolog
42 Citations1986Masahiro Fujita, S. Kono +2 more
Tokio is a temporal logic programming language intended for specification of concurrent programs and has an extension that can execute Interval Temporal Logic.
Lecture notes in computer scienceSpecifying, programming and verifying real-time systems using a synchronous declarative language
42 Citations1990Nicolas Halbwachs, D. Pilaud +2 more
It is shown that the finite automaton produced by the Lustre compiler may be used for verifying many logical properties, by model checking, in the real-time system Lustre.
FigshareSML-a high level language for the design and verification of finite state machines
26 Citations2018M. C. Browne, E. M. Clarke
Theoretical Computer ScienceGraph rewriting for a partial ordering semantics of concurrent constraint programming
15 Citations1993Ugo Montanari, Francesca Rossi
This work can be regarded as the first attempt to give a true-concurrency semantics to concurrent constraint programming and, more generally, to graph grammars.
Executing multidatabase transactions
12 Citations1992M. A. Ansari, Marek Rusinkiewicz +2 more
One of such extensions, the flexible transaction model, is described, the scheduling of transactions involving multiple autonomous database systems managed by heterogeneous DBMS is discussed and the scheduling algorithm for flexible transactions is implemented using L.0.
IEEE Transactions on ComputersThe L.0 language and environment for protocol simulation and prototyping
11 Citations1991E.J. Cameron, David Cohen +5 more
L.0 has been used in several development projects to design, simulate, and prototype protocols and seems to provide a paradigm that is precise and yet can be used by designers and engineers who are not specialists in specification languages.
An executor for multidatabase transactions which achieves maximal parallelism
4 Citations2002E.J. Cameron, Linda Ness +1 more
The authors concisely specify a executor in the logically parallel language, L.0, for a particular extended transaction model called multidatabase transactions, which takes as input the data defining any particular multid atabase transaction, dynamically schedules the sub-transactions, and determines whether the multidAtabase transaction succeeded or failed.