Modeling of safe timed Petri nets by two-level (max,+) automata

Abstract

In this paper we will show that safe timed Petri nets (TPNs) with preselection semantics can be represented by deterministic two-level (max,+) automata (2l-MPA). In 2lMPA, the outer dynamics, corresponding to the evolution of component clocks, is represented by deterministic Mealy automata with vector-valued outputs from (max,+) semiring. The outer dynamics is then adjusted by inner dynamics corresponding to synchronizations, which are implemented through scalar-like multiplication of the coefficients by symmetric Boolean matrices. These Boolean matrices encode synchronization among the state machines components. The previous approaches encoded either safe TPNs under preselection policy as nondeterministic (max,+) automata, or TPNs under (more restrictive) race policy as deterministic (max,+) automata.

Projects

IGA PrF 2022 018

Martin Trnečka
Jiří Balun, Jiří Valůšek

Verification and Control of Networked Discrete Event Systems

Tomáš Masopust, Jan Komenda
Jiří Balun, Stéphane Lafortune, Spyros Reveliotis, Feng Lin

Authors

Jan Komenda
Jiří Balun
Davide Zorzenon

WODES, 2022
Discrete-Event Systems and Theoretical Computer Science Research Group

Downloads

BibTex