School of Computing

A true concurrency semantics for ET-LOTOS

Howard Bowman and Joost-Pieter Katoen

In CSD'98 International Conference on Application of Concurrency to System Design, IEEE Computer Society, pages 182-196. IEEE Computer Society Press, March 1998.

Abstract

One of the central objectives of the LOTOS restandardisation activity is to define an enhanced LOTOS language which supports real-time specification. The timed extension is based upon a timed LOTOS proposal ET-LOTOS. This paper defines 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. 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.



Bibtex Record

@inproceedings{479,
author = {Howard Bowman and Joost-Pieter Katoen},
title = {A True Concurrency Semantics for {ET}-{LOTOS}},
month = {March},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/479},
    booktitle = {CSD'98 International Conference on Application of Concurrency to System Design},
    publisher = {IEEE Computer Society Press},
    refereed = {yes},
    series = {IEEE Computer Society},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014