Past-Future Separation and Normal Forms in Temporal Predicate Logic Specifications

Research output: Contribution to JournalArticleAcademicpeer-review


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.
Original languageEnglish
Pages (from-to)106-124
Number of pages19
JournalJournal of Algorithms
Publication statusPublished - 2009


Dive into the research topics of 'Past-Future Separation and Normal Forms in Temporal Predicate Logic Specifications'. Together they form a unique fingerprint.

Cite this