Toggle Main Menu Toggle Search

ePrints

From Petri Nets with Shared Variables to ITL

Lookup NU author(s): Professor Maciej Koutny, Dr Ben Moszkowski

Downloads


Licence

This is the authors' accepted manuscript of a conference proceedings (inc. abstract) that has been published in its final definitive form by IEEE, 2016.

For re-use rights please refer to the publisher's terms and conditions.


Abstract

Petri nets and Interval Temporal Logic (ITL) are two formalisms for the specification and analysis of concurrent computing systems. Petri nets allow for a direct expression of causality aspects in system behaviour and in particularsupport system verification based on partial order reductions or invariant-based techniques. ITL, on the other hand, supports system verification by proving that the formula describing a system implies the formula describing a correctness requirement.It would therefore be desirable to establish a strong semantical link between these two models, thus allowing one to apply diverse analytical methods and techniques to a given system design. We have recently proposed such a semantical link between the propositional version of ITL (PITL) and Box Algebra (BA), which is a compositional model of basic (low-level) Petri nets supporting handshake action synchronisation between concurrent processes. In this paper, we extend this result by considering a compositional model of (high-level) Petri nets where concurrent processes communicate through shared variables. The main result is a method for translating a design expressed using a high-level Petri net into a semantically equivalent ITL formula.


Publication metadata

Author(s): Klaudel H, Koutny M, Moszkowski B

Editor(s): Desel, J; Yakovlev, A

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: 16th International Conference on Application of Concurrency to System Design (ACSD)

Year of Conference: 2016

Online publication date: 06/02/2017

Acceptance date: 30/03/2016

ISSN: 1550-4808

Publisher: IEEE

URL: http://dx.doi.org/10.1109/ACSD.2016.12

DOI: 10.1109/ACSD.2016.12

Library holdings: Search Newcastle University Library for this item

ISBN: 9781509025893


Actions

Link to this publication


Share