Abstract
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 language | English |
---|---|
Pages (from-to) | 106-124 |
Number of pages | 19 |
Journal | Journal of Algorithms |
Volume | 64 |
DOIs | |
Publication status | Published - 2009 |