Modal algebra and Petri nets

  • We use the by now well established setting of modal semirings to derive a modal algebra for Petri nets. It is based on a relation-algebraic calculus for separation logic that enables calculations of properties in a pointfree fashion and at an abstract level. Basically, we start from an earlier logical approach to Petri nets that in particular uses modal box and diamond operators for stating properties about the state space of such a net. We provide relational translations of the logical formulas which further allow the characterisation of general behaviour of transitions in an algebraic fashion. From the relational structure an algebra for frequently used properties of Petri nets is derived. In particular, we give connections to typical used assertion classes of separation logic. Moreover, we demonstrate applicability of the algebraic approach by calculations concerning a standard example of a mutex net.

Download full text files

Export metadata

Statistics

Number of document requests

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Han-Hing Dang, Bernhard MöllerGND
URN:urn:nbn:de:bvb:384-opus4-587365
Frontdoor URLhttps://opus.bibliothek.uni-augsburg.de/opus4/58736
ISSN:0001-5903OPAC
ISSN:1432-0525OPAC
Parent Title (English):Acta Informatica
Publisher:Springer Science and Business Media LLC
Type:Article
Language:English
Year of first Publication:2015
Publishing Institution:Universität Augsburg
Release Date:2019/07/23
Tag:Computer Networks and Communications; Software; Information Systems
Volume:52
Issue:2-3
First Page:109
Last Page:132
DOI:https://doi.org/10.1007/s00236-015-0216-3
Institutes:Fakultät für Angewandte Informatik
Fakultät für Angewandte Informatik / Institut für Informatik
Fakultät für Angewandte Informatik / Institut für Informatik / Professur für Programmiermethodik und Multimediale Informationssysteme
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):Deutsches Urheberrecht