Sufficient conditions for the marked graph realisability of labelled transition systems
| Autor: | Harro Wimmel, Eike Best, Thomas Hujsa |
|---|---|
| Přispěvatelé: | Department of Computing Science, Carl von Ossietzky Universität Oldenburg, D-26111 Oldenburg, Germany |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Discrete mathematics
Marked graph Class (set theory) General Computer Science Realisability Realisation Context (language use) 0102 computer and information sciences 02 engineering and technology Petri net 01 natural sciences Theoretical Computer Science Combinatorics Set (abstract data type) Synthesis 010201 computation theory & mathematics Petri Net 0202 electrical engineering electronic engineering information engineering Stochastic Petri net 020201 artificial intelligence & image processing [INFO.INFO-ES]Computer Science [cs]/Embedded Systems Representation (mathematics) Labelled Transition System Mathematics |
| Zdroj: | Theoretical Computer Science Theoretical Computer Science, Elsevier, 2018, 750, pp.101-116. ⟨10.1016/j.tcs.2017.10.006⟩ |
| ISSN: | 1879-2294 0304-3975 |
| Popis: | This paper describes two results within the context of Petri net synthesis from labelled transition systems. We consider a set of structural properties of transition systems, and we show that, given such properties, it is possible to re-engineer a Petri net realisation into one which lies inside the set of marked graphs, a well-understood and useful class of Petri nets. The first result originates from Petri net based workflow specifications, where it is desirable that k customers can share a system without mutual interferences. In a Petri net representation of a workflow, the presence of k customers can be modelled by an initial k-marking, in which the number of tokens on each place is a multiple of k. For any initial k-marking with k ≥ 2 , we show that other desirable assumptions such as reversibility and persistence suffice to guarantee marked graph realisability. For the case that k = 1 , we show that the existence of certain cycles, along with other properties such as reversibility and persistence, again suffices to guarantee marked graph realisability. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect