-
The Complexity of Boolean State Separation (Technical Report)
Authors:
Ronny Tredup,
Evgeny Erofeev
Abstract:
For a Boolean type of nets $τ$, a transition system $A$ is synthesizeable into a $τ$-net $N$ if and only if distinct states of $A$ correspond to distinct markings of $N$, and $N$ prevents a transition firing if there is no related transition in $A$. The former property is called $τ$-state separation property ($τ$-SSP) while the latter -- $τ$-event/state separation property ($τ$-ESSP). $A$ is embed…
▽ More
For a Boolean type of nets $τ$, a transition system $A$ is synthesizeable into a $τ$-net $N$ if and only if distinct states of $A$ correspond to distinct markings of $N$, and $N$ prevents a transition firing if there is no related transition in $A$. The former property is called $τ$-state separation property ($τ$-SSP) while the latter -- $τ$-event/state separation property ($τ$-ESSP). $A$ is embeddable into the reachability graph of a $τ$-net $N$ if and only if $A$ has the $τ$-SSP. This paper presents a complete characterization of the computational complexity of \textsc{$τ$-SSP} for all Boolean Petri net types.
△ Less
Submitted 2 October, 2020;
originally announced October 2020.
-
On the Parameterized Complexity of Synthesizing Boolean Petri Nets With Restricted Dependency
Authors:
Ronny Tredup,
Evgeny Erofeev
Abstract:
Modeling of real-world systems with Petri nets allows to benefit from their generic concepts of parallelism, synchronisation and conflict, and obtain a concise yet expressive system representation. Algorithms for synthesis of a net from a sequential specification enable the well-developed theory of Petri nets to be applied for the system analysis through a net model. The problem of $τ$-synthes…
▽ More
Modeling of real-world systems with Petri nets allows to benefit from their generic concepts of parallelism, synchronisation and conflict, and obtain a concise yet expressive system representation. Algorithms for synthesis of a net from a sequential specification enable the well-developed theory of Petri nets to be applied for the system analysis through a net model. The problem of $τ$-synthesis consists in deciding whether a given directed labeled graph $A$ is isomorphic to the reachability graph of a Boolean Petri net $N$ of type $τ$. In case of a positive decision, $N$ should be constructed. For many Boolean types of nets, the problem is NP-complete. This paper deals with a special variant of $τ$-synthesis that imposes restrictions for the target net $N$: we investigate dependency $d$-restricted tau-synthesis (DR$τ$S) where each place of $N$ can influence and be influenced by at most d transitions. For a type $τ$, if tau-synthesis is NP-complete then DR$τ$S is also NP-complete. In this paper, we show that DR$τ$S parameterized by $d$ is in XP. Furthermore, we prove that it is W[2]-hard, for many Boolean types that allow unconditional interactions set and reset.
△ Less
Submitted 16 September, 2020;
originally announced September 2020.
-
On the Parameterized Complexity of Synthesizing Boolean Petri Nets With Restricted Dependency (Technical Report)
Authors:
Ronny Tredup,
Evgeny Erofeev
Abstract:
The problem of $τ$-synthesis consists in deciding whether a given directed labeled graph $A$ is isomorphic to the reachability graph of a Boolean Petri net $N$ of type $τ$. In case of a positive decision, $N$ should be constructed. For many Boolean types of nets, the problem is NP-complete. This paper deals with a special variant of $τ$-synthesis that imposes restrictions for the target net $N$: w…
▽ More
The problem of $τ$-synthesis consists in deciding whether a given directed labeled graph $A$ is isomorphic to the reachability graph of a Boolean Petri net $N$ of type $τ$. In case of a positive decision, $N$ should be constructed. For many Boolean types of nets, the problem is NP-complete. This paper deals with a special variant of $τ$-synthesis that imposes restrictions for the target net $N$: we investigate \emph{dependency $d$-restricted $τ$-synthesis (DR$τ$S)} where each place of $N$ can influence and be influenced by at most $d$ transitions. For a type $τ$, if $τ$-synthesis is NP-complete then DR$τ$S is also NP-complete. In this paper, we show that DR$τ$S parameterized by $d$ is in XP. Furthermore, we prove that it is $W[2]$-hard, for many Boolean types that allow unconditional interactions $set$ and $reset$.
△ Less
Submitted 24 July, 2020;
originally announced July 2020.
-
Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems: A Geometric Approach
Authors:
Raymond Devillers,
Evgeny Erofeev,
Thomas Hujsa
Abstract:
Recent studies investigated the problems of analysing Petri nets and synthesising them from labelled transition systems (LTS) with two labels (transitions) only. In this paper, we extend these works by providing new conditions for the synthesis of Weighted Marked Graphs (WMGs), a well-known and useful class of weighted Petri nets in which each place has at most one input and one output. Some of th…
▽ More
Recent studies investigated the problems of analysing Petri nets and synthesising them from labelled transition systems (LTS) with two labels (transitions) only. In this paper, we extend these works by providing new conditions for the synthesis of Weighted Marked Graphs (WMGs), a well-known and useful class of weighted Petri nets in which each place has at most one input and one output. Some of these new conditions do not restrict the number of labels; the other ones consider up to 3 labels. Additional constraints are investigated: when the LTS is either finite or infinite, and either cyclic or acyclic. We show that one of these conditions, developed for 3 labels, does not extend to 4 nor to 5 labels. Also, we tackle geometrically the WMG-solvability of finite, acyclic LTS with any number of labels.
△ Less
Submitted 31 October, 2019;
originally announced November 2019.
-
Efficient Synthesis of Weighted Marked Graphs with Circular Reachability Graph, and Beyond
Authors:
Raymond Devillers,
Evgeny Erofeev,
Thomas Hujsa
Abstract:
In previous studies, several methods have been developed to synthesise Petri nets from labelled transition systems (LTS), often with structural constraints on the net and on the LTS. In this paper, we focus on Weighted Marked Graphs (WMGs) and Choice-Free (CF) Petri nets, two weighted subclasses of nets in which each place has at most one output; WMGs have the additional constraint that each place…
▽ More
In previous studies, several methods have been developed to synthesise Petri nets from labelled transition systems (LTS), often with structural constraints on the net and on the LTS. In this paper, we focus on Weighted Marked Graphs (WMGs) and Choice-Free (CF) Petri nets, two weighted subclasses of nets in which each place has at most one output; WMGs have the additional constraint that each place has at most one input. We provide new conditions for checking the existence of a WMG whose reachability graph is isomorphic to a given circular LTS, i.e. forming a single cycle; we develop two new polynomial-time synthesis algorithms dedicated to these constraints: the first one is LTS-based (classical synthesis) while the second one is vector-based (weak synthesis) and more efficient in general. We show that our conditions also apply to CF synthesis in the case of three-letter alphabets, and we discuss the difficulties in extending them to CF synthesis over arbitrary alphabets.
△ Less
Submitted 31 October, 2019;
originally announced October 2019.
