Modelling opacity using petri nets

Jeremy W. Bryans, Maciej Koutny, Peter Y.A. Ryan

    Research output: Contribution to journalArticlepeer-review

    142 Citations (Scopus)
    56 Downloads (Pure)


    We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. We propose a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. We then discuss expressiveness of the resulting framework and the decidability of the associated verification problems.

    Publisher Statement: This is an Open Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (, which permits non-commercial re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
    Original languageEnglish
    Pages (from-to)101-115
    Number of pages15
    JournalElectronic Notes in Theoretical Computer Science
    Publication statusPublished - 10 Feb 2005


    • opacity
    • non-deducibility
    • Petri nets
    • observable behaviour


    Dive into the research topics of 'Modelling opacity using petri nets'. Together they form a unique fingerprint.

    Cite this