From Petri Nets with Shared Variables to ITL

• Main Authors: Klaudel, Hanna, Koutny, Maciej, Moszkowski, Ben
• Format: Conference Proceeding
• Language: English
• Subjects: Algebra; Analytical models; behavioural consistency; compositional translation; Computational modeling; concurrency; Concurrent computing; ITL; Petri nets; Reactive power; relations between models
• ISSN: 1550-4808; 2374-8567
• DOI: 10.1109/ACSD.2016.12

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 particular support 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.