Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
An Application of Temporal Projection to Interleaving Concurrency
verfasst von : Ben Moszkowski, Dimitar P. Guelev
Erschienen in: Dependable Software Engineering: Theories, Tools, and Applications
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We revisit the earliest temporal projection operator
$$\mathrm \Pi $$
in discrete-time Propositional Interval Temporal Logic (PITL) and use it to formalise interleaving concurrency. The logical properties of
$$\mathrm{\Pi }$$
as a normal modality and a way to eliminate it in both PITL and conventional point-based Linear-Time Temporal Logic (LTL), which can be viewed as a PITL subset, are examined. We also formalise concurrency without
$$\mathrm{\Pi }$$
, and relate the two approaches. Furthermore,
$$\mathrm{\Pi }$$
and another standard PITL projection operator are interdefinable and both suitable for reasoning about different time granularities. We mention other (mostly interval-based) temporal logics with similar forms of projection, as well as some related applications and international standards.