A True Concurrency Semantics for ET-LOTOS

One of the central objectives of the LOTOS restandardisation activity is to de ne an enhanced LOTOS language which supports real-time speci cation. The timed extension is based upon a timed LOTOS proposal ET-LOTOS. This report de nes a (branching-time) non-interleaving semantics for ET-LOTOS without data. As a denotational model a suitable timed extension of Langerak's bundle event structures is used. For guarded recursive processes we show the consistency between our non-interleaving semantics and the ET-LOTOS interleaving semantics. Several examples illustrate the non-interleaving approach. Since our semantical model does not have an explicit notion of the passage of time (as opposed to the interleaving semantics) we are able to handle unguarded recursion and Zeno-behaviours in a perspicuous way.

• Type: Conference
• Year: 1998
• Where: ACSD
• Authors: Howard Bowman, Joost-Pieter Katoen
• Keywords: ACSD 1998, Hardware, Non-interleaving Semantics, Timed Extension, Timed Lotos Proposal