UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Petri Automata

Brunet, P; Pous, D; (2017) Petri Automata. Logical Methods in Computer Science , 13 (3) , Article 33. 10.23638/LMCS-13(3:33)2017. Green open access

1702.01804.pdf - Published version

Download (811kB) | Preview


Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations. We consider Kleene allegories, i.e., Kleene algebras with two additional operations and a constant which are natural in binary relation models: intersection, converse, and the full relation. While regular languages are closed under those operations, the above characterisation breaks. Putting together a few results from the literature, we give a characterisation in terms of languages of directed and labelled graphs. By taking inspiration from Petri nets, we design a finite automata model, Petri automata, allowing to recognise such graphs. We prove a Kleene theorem for this automata model: the sets of graphs recognisable by Petri automata are precisely the sets of graphs definable through the extended regular expressions we consider. Petri automata allow us to obtain decidability of identity-free relational Kleene lattices, i.e., the equational theory generated by binary relations on the signature of regular expressions with intersection, but where one forbids unit. This restriction is used to ensure that the corresponding graphs are acyclic. We actually show that this decision problem is EXPSPACE-complete.

Type: Article
Title: Petri Automata
Open access status: An open access version is available from UCL Discovery
DOI: 10.23638/LMCS-13(3:33)2017
Publisher version: http://dx.doi.org/10.23638/LMCS-13(3:33)2017
Language: English
Additional information: This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copy of this license, visit https://creativecommons.org/licenses/by-nd/4.0/
Keywords: Science & Technology, Technology, Computer Science, Theory & Methods, Logic, Computer Science, Science & Technology - Other Topics, Kleene allegories, Kleene lattices, Petri automata, Petri nets, decidability, graphs, Kleene theorem, EQUATIONAL THEORY, ALGEBRAS, NETS
UCL classification: UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10042457
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item