TY - JOUR
T1 - Past-Future Separation and Normal Forms in Temporal Predicate Logic Specifications
AU - Treur, J.
PY - 2009
Y1 - 2009
N2 - Temporal specifications are often used when phenomena are modelled where dynamics play a main role. If simulation is one of the aims of modelling, usually a restricted, executable modelling language format is used, based on some form of past to future implications. In this paper a detailed transformation procedure is described that takes any temporal predicate logic specification and generates a specification in a past-implies-future normal format. The procedure works for temporal specifications in which the atoms either express time ordering relations or are state-related, i.e., include only one time variable. © 2009 Elsevier Inc. All rights reserved.
AB - Temporal specifications are often used when phenomena are modelled where dynamics play a main role. If simulation is one of the aims of modelling, usually a restricted, executable modelling language format is used, based on some form of past to future implications. In this paper a detailed transformation procedure is described that takes any temporal predicate logic specification and generates a specification in a past-implies-future normal format. The procedure works for temporal specifications in which the atoms either express time ordering relations or are state-related, i.e., include only one time variable. © 2009 Elsevier Inc. All rights reserved.
UR - https://www.scopus.com/pages/publications/67349236419
UR - https://www.scopus.com/inward/citedby.url?scp=67349236419&partnerID=8YFLogxK
U2 - 10.1016/j.jalgor.2009.02.008
DO - 10.1016/j.jalgor.2009.02.008
M3 - Article
SN - 0196-6774
VL - 64
SP - 106
EP - 124
JO - Journal of Algorithms
JF - Journal of Algorithms
ER -
