A Petri Net-Based Notation for Normative Modeling: Evaluation on Deontic Paradoxes

Abstract

Developing systems operating in alignment with norms is not a straightforward endeavour. Part of the problems derive from the suggestion that law concerns a system of norms, which, in abstract, in a fixed point in time, could be approached and expressed atemporally, but, when it is contextualized and applied, it deals with a continuous flow of events modifying the normative directives as well. The paper presents an alternative approach to some of these problems, exemplified by well-known deontic puzzles, by extending the Petri net notation, most common in process modeling, to Logic Programming Petri Nets. The resulting visual formalism represents in a integrated, yet distinct fashion, procedural and declarative aspects of the system under study, including normative ones.

A Formalization

Here we present a simplified version of the LPPN notation considering only a propositional labeling. We start from the definition of propositional literals derived from ASP [15], accounting for strong and default negation.

Definition 2

(Literal and Extended literals). Given a set of propositional atoms A, the set of literals $L = L^{+} \cup L^{-}$ consists of positive literals (atoms) $L^{+} = A$, negative literals (negated atoms) $L^{-} = \{ -a \; |\; a \in A\}$, where ‘−’ stands for strong negation.⁷ The set of extended literals $L^{*} = L \cup L^{not}$ consists of literals and default negation literals $L^{not} = \{ notl |\; l \in L \}$, where ‘$not$’ stands for default negation.⁸

We denote the basic topology of a Petri net as a procedural net.

Definition 3

(Procedural net). A procedural net is a bipartite directed graph connecting two finite sets of nodes, called places and transitions. It can be written as $N = \left\langle P, T, E \right\rangle$, where $P = \{p_{1}, \ldots , p_{n}\}$ is the set of place nodes; $T = \{t_{1}, \ldots , t_{m}\}$ is the set of transition nodes; $E = E^+ \cup E^-$ is the set of arcs connecting them: $E^+$ from transitions to places, $E^{-}$ from places to transitions.

LPPNs consists of three components: a procedural net specifying causal or temporal relationships, and two declarative nets specifying respectively logical dependencies at the level of objects or ongoing events (on places), and on impulse events (on transitions). Furthermore, propositional LPPNs build upon a boolean marking on places (like condition/event nets).

Definition 4

(Propositional Logic Programming Petri Net). A propositional Logic Programming Petri Net $LPPN _\mathrm {prop}$ is a Petri Net whose places and transitions are labeled with literals, enriched with declarative nets of places and of transitions. It is defined by the following components:

• $\left\langle P, T, PE \right\rangle$ is a procedural net; $PE$ stands for procedural edges;

• $C_{P} : P \rightarrow L^{*}$ and $C_{T} : T \rightarrow L$ are labeling functions, associating literals respectively to places and to transitions;

• $OP = \{\lnot , -, \wedge , \vee , \rightarrow , \leftrightarrow , \ldots \}$ is a set of logic operators.

• $LP$ and $LT$ are sets of logic operator nodes (in the following called l-nodes) respectively for places and for transitions.

• $C_{ LP } : LP \rightarrow OP$ maps each l-node for places to a logic operator; similarly, $C_{ LT } : LT \rightarrow OP$ does the same for l-nodes for transitions.

• $DE _{ LP } = DE ^+_{ LP } \cup DE ^-_{ LP }$ is the set of arcs connecting l-nodes for places to places; similarly, $DE _{ LT } = DE ^+_{ LT } \cup DE ^-_{ LT }$ for l-nodes for transitions and transitions.⁹

• $M: P \rightarrow \{0, 1\}$ returns the marking of a place, i.e. whether the place contains (1) or does not contain (0) a token.

Note that if $LP \cup LT = \varnothing$, we have a strictly procedural $LPPN _\mathrm {prop}$, i.e. a standard binary Petri net. If $T = \varnothing$, we have a strictly declarative $LPPN _\mathrm {prop}$, that can be directly mapped to an ASP program.

With respect to the operational semantics, the execution cycle of a LPPN consists of four steps: (1) given a “source” marking M, the bindings of the declarative net of places entail a “ground” marking $M^*$; (2) an enabled transition is selected to pre-fire, so determining a “source” transition-event e; (3) the bindings of the declarative net of transitions entail all propagations of this event, obtaining a set of transition-events, also denoted as the “ground” event-marking $E^*$; (4) all transition-events are fired, producing and consuming the relative tokens. The steps (1) and (3) are processed by an ASP solver: the declarative net of places (respectively transitions) is translated as rules, tokens (transition-events) are reified as facts; the ASP solver takes as input the resulting program and, if satisfiable, it provides as output one or more ground marking (one or more sets transition-events to be fired). For the steps (2) and (4), the operational semantics distinguishes the external firings (started by the execution) from the internal firing, immediately propagated (triggered by the declarative net of transitions).

Definition 5

(Enabled transition). A transition t is enabled in a ground marking $M^*$ if a token is available for each input places:

$$ Enabled (t) \equiv \forall p_i \in \bullet t, M^*(p) = 1 $$

Similarly to what marking is for places, we consider an event-marking for transitions $E: T\rightarrow \{0, 1\}$. $E(t) = 1$ if the transition t produces a transition-event e. Each step s has a “source” event-marking E.

Definition 6

(Pre-firing). An enabled transition t pre-fires at a step s if it selected to produce a transition-event:

$$ \forall t \in Enabled (T) : t \; \text {pre-fires} \equiv E(t) = 1$$

As we apply an interleaving semantics for the pre-firing, the interpreter selects only one transition to pre-fire per step; for any other $t'$, $E(t') = 0$.

Definition 7

(Firing). An enabled transition t fires by propagation, consuming a token from each input place, and forging a token in each output place:

$$\begin{aligned} \begin{gathered} \forall t \in Enabled (T) : t \; \text {fires} \equiv \\ E^*(t) = 1 \leftrightarrow \forall p_i \in \bullet t : M'(p_i) = 0 \; \wedge \; \forall p_o \in t \bullet : M'(p_o) = 1 \end{gathered} \end{aligned}$$