TY - GEN
T1 - Sometimes “tomorrow” is “sometime”
T2 - 1st International Conference on Temporal Logic, ICTL 1994
AU - Fiadeiro, José Luiz
AU - Maibaum, Tom
PY - 1994/1/1
Y1 - 1994/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84958959404&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84958959404
SN - 9783540582410
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 48
EP - 66
BT - Temporal Logic - 1st International Conference, ICTL 1994, Proceedings
A2 - Gabbay, Dov M.
A2 - Ohlbach, Hans Jurgen
PB - Springer Verlag
Y2 - 11 July 1994 through 14 July 1994
ER -