Sometimes “tomorrow” is “sometime”: Action refinenent in a temporal logic of objects

José Luiz Fiadeiro, Tom Maibaum

Research output: Chapter in Book/Report/Conference proceedingConference contribution

37 Citations (Scopus)


We address the hierarchical (vertical) decomposition, or abstract implementation, of object specification in temporal logic. Whereas previous approaches to refinement in the context of temporal logic such as those developed by Lamport and by Barringer, Kuiper and Pnueli are based on a single logic that accommodates different levels of action granularity, our approach is based on relating different logics corresponding to different levels of granularity. More precisely, we map abstract actions (propositions) to concrete objects (theories) and, through inference rules that relate the different logics, derive properties of the abstracted actions from the behaviour of the corresponding objects. In this way, we keep a tighter control of action granularity and interference, enabling us to maintain the use of the “next” operator and make the development of reactive systems more tractable.

Original languageEnglish
Title of host publicationTemporal Logic - 1st International Conference, ICTL 1994, Proceedings
EditorsDov M. Gabbay, Hans Jurgen Ohlbach
PublisherSpringer Verlag
Number of pages19
ISBN (Electronic)9783540485858
ISBN (Print)9783540582410
Publication statusPublished - 1 Jan 1994
Event1st International Conference on Temporal Logic, ICTL 1994 - Bonn, Germany
Duration: 11 Jul 199414 Jul 1994

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume827 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference1st International Conference on Temporal Logic, ICTL 1994

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Sometimes “tomorrow” is “sometime”: Action refinenent in a temporal logic of objects'. Together they form a unique fingerprint.

Cite this